You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
DecidableEq in Init.Prelude
Lean.ToExpr in Lean.ToExpr
List in Init.Prelude
Repr in Init.Data.Repr
Nat in Init.Prelude
AList in Mathlib.Data.List.AList
Option in Init.Prelude
StateT in Init.Control.State
Unit in Init.Prelude
AList.insert in Mathlib.Data.List.AList
String in Init.Prelude
BEq in Init.Prelude
ite in Init.Prelude
Vector in Init.Data.Vector.Basic
Bool in Init.Prelude
Int in Init.Data.Int.Basic
bool in Init.Control.Basic
Computation in Mathlib.Data.Seq.Computation
Valuation.map in Mathlib.RingTheory.Valuation.Basic
PUnit in Init.Prelude
Finset in Mathlib.Data.Finset.Defs
Sigma in Init.Core
StateT.bind in Init.Control.State
Sigma.mk in Init.Core
liftM in Init.Prelude
Iff in Init.Core
IsEmpty in Mathlib.Logic.IsEmpty
Set in Mathlib.Data.Set.Defs
Set.Subset in Mathlib.Data.Set.Defs
List.Subset in Init.Data.List.Basic
reduceCtorEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

abbrev Mapping (Γ Δ : Ctxt Ty) : Type :=
  @AList (Σ t, Var Γ t) (fun x => Var Δ x.1)

structure Ctxt (Ty : Type) : Type where
  ofList :: toList : List Ty
  
  deriving Repr, Lean.ToExpr, DecidableEq

def Var (Γ : Ctxt Ty) (t : Ty) : Type :=
  { i : Nat // Γ[i]? = some t }

inductive Lets (Γ_in : Ctxt d.Ty) (eff : EffectKind) :
    (Γ_out : Ctxt d.Ty) → Type where
  | nil : Lets Γ_in eff Γ_in
  | var (body : Lets Γ_in eff Γ_out) (e : Expr d Γ_out eff t) : Lets Γ_in eff e.outContext

protected instance Expr.decidableEq [DecidableEq d.Op] [DecidableEq d.Ty] :
    {Γ : Ctxt d.Ty} → {ty : List d.Ty} → DecidableEq (Expr d Γ eff ty)
  | Γ, _, .mk op₁ rfl eff_le₁ arg₁ regArgs₁, .mk op₂ eq eff_le₂ arg₂ regArgs₂ =>
    if ho : op₁ = op₂ then by
      subst ho
      letI := HVector.decidableEq arg₁ arg₂
      letI := HVector.decidableEqReg regArgs₁ regArgs₂
      exact decidable_of_iff (arg₁ = arg₂ ∧ regArgs₁ = regArgs₂) (by admit /- proof elided -/
      )
    else isFalse (by admit /- proof elided -/
    )

def Var (Γ : Context Ty) (ty : Ty) : Type := { v : VarName // Γ.hasType v ty }

def Valuation.nil : Ctxt.Valuation (∅ : Ctxt Ty) := fun _ v => v.emptyElim

inductive EffectKind
| pure 
| impure 
deriving Repr, DecidableEq, Lean.ToExpr

@[elab_as_elim]
def appendCases
    {motive : (Γ ++ Δ).Var t → Sort u}
    (left : (v : Var Γ t) → motive (appendInl v))
    (right : (v : Var Δ t) → motive (appendInr v)) :
    (v : (Γ ++ Δ).Var t) → motive v
  | ⟨idx, h⟩ =>
    if hv : idx < Γ.length then
      left ⟨idx, by admit /- proof elided -/
      ⟩
    else
      let v' : Var _ _ := ⟨idx - Γ.length, by admit /- proof elided -/
      ⟩
      have eq : v'.appendInr = ⟨idx, h⟩ := by admit /- proof elided -/

@[match_pattern]
def last (Γ : Ctxt Ty) (t : Ty) : Ctxt.Var (Ctxt.cons t Γ) t :=
  ⟨0, by admit /- proof elided -/
  ⟩

def Valuation.cons {Γ : Ctxt Ty} {t : Ty} (x : toType t) (V : Γ.Valuation) :
    (Γ.cons t).Valuation :=

protected instance HVector.decidableEqReg [DecidableEq d.Op] [DecidableEq d.Ty] :
    ∀ {l : RegionSignature d.Ty}, DecidableEq (HVector (fun t => Com d t.1 .impure t.2) l)
  | _, .nil, .nil => isTrue rfl
  | _, .cons x₁ v₁, .cons x₂ v₂ =>
    letI := HVector.decidableEqReg v₁ v₂
    letI := Com.decidableEq x₁ x₂
    decidable_of_iff (x₁ = x₂ ∧ v₁ = v₂) (by admit /- proof elided -/
    )

def Lets.varsOfVec (lets : Lets d Γ_in eff Γ_out) (vs : HVector Γ_out.Var ts) :
    VarSet Γ_in :=
  (vs.vars).biUnion (fun v => lets.vars v.2)

def Lets.vars : Lets d Γ_in eff Γ_out → Var Γ_out t → VarSet Γ_in
  | .nil, v => VarSet.ofVar v
  | .var lets e, v => by admit /- proof elided -/
      | right v => exact lets.vars v
      | left _ => exact lets.varsOfVec e.args

def Com.vars (com : Com d Γ eff ts) : VarSet Γ :=
  com.toLets.varsOfVec com.returnVars

def Expr.returnVars (e : Expr d Γ eff tys) : HVector e.outContext.Var tys :=
  .ofFn _ _ <| fun i => (Var.ofFin i).appendInl

def Com.outContext {Γ} : Com d Γ eff ts → Ctxt d.Ty :=
  Com.rec' (motive := fun _ => Ctxt d.Ty)
    (@fun Γ _ => Γ) 
    (fun _ _ r => r)

def Com.rec' {Γ} (com : Com d Γ eff t) : motive com :=
   
  Com.rec
    (motive_1 := fun _ _ _ _ => PUnit)
    (motive_2 := fun _ eff' t' c =>
      (h₁ : eff = eff') → (h₂ : t = t') → motive (h₁ ▸ h₂ ▸ c))
    (motive_3 := fun _ _ => PUnit)
    (fun _ _ _ _ _ _ => ⟨⟩) 
    (fun v h₁ h₂ => 
      cast (by admit /- proof elided -/
      ) <| rets (h₂ ▸ v))
    (fun e' body' _ r' h₁ h₂ => 
      let e := h₁ ▸ e'
      let body : Com _ _ eff t := cast (by admit /- proof elided -/
      ) body'
      let r : motive body := cast (by admit /- proof elided -/
      ) (r' h₁ h₂)
      cast (by admit /- proof elided -/
      ) <| var e body r)
    ⟨⟩
    (fun _ _ _ _ => ⟨⟩)
    com
    rfl
    rfl

inductive Com : Ctxt d.Ty → EffectKind → List d.Ty → Type where
  | rets {Γ} {tys} {eff : EffectKind} (vs : HVector Γ.Var tys) : Com Γ eff tys
  | var (e : Expr Γ eff ty) (body : Com (ty ++ Γ) eff β) : Com Γ eff β

def Valuation.cast {Γ Δ : Ctxt Ty} (h : Γ = Δ) (V : Valuation Γ) : Valuation Δ :=
  fun _ v => V <| v.castCtxt h.symm

abbrev Expr.outContext (_ : Expr d Γ eff ts) : Ctxt d.Ty :=
  ts ++ Γ

def ofFin (i : Fin Γ.length) : Γ.Var (Γ[i]) :=
  ⟨i.val, by admit /- proof elided -/
  ⟩

def Com.returnVars : (com : Com d Γ eff ts) → HVector (Var com.outContext) ts
  | .rets vs => vs
  | .var _ body => body.returnVars

def Com.toLets (com : Com d Γ eff t) : Lets d Γ eff com.outContext :=
  Lets.nil.addComToEnd com

abbrev VarSet (Γ : Ctxt Ty) : Type :=
  Finset (Σ t, Γ.Var t)

def Expr.args {Γ ts} (e : Expr d Γ eff ts) :
    HVector (Var Γ) (DialectSignature.sig e.op) :=
  Expr.casesOn e (fun _ _ _ args _ => args)

def sig          := Signature.sig ∘ s.signature

structure Signature (Ty : Type) where
  mkEffectful ::
  sig         : List Ty
  regSig      : RegionSignature Ty
  returnTypes : List Ty
  effectKind  : EffectKind := .pure

class DialectSignature (d : Dialect) where
  signature : d.Op → Signature d.Ty

def HVector.vars {l : List d.Ty} (T : HVector (Var Γ) l) : VarSet Γ :=
  T.foldl (fun _ s a => insert ⟨_, a⟩ s) ∅

@[simp]
def ofVar {Γ : Ctxt Ty} (v : Γ.Var t) : VarSet Γ :=
  {⟨_, v⟩}

def foldl {B : Type*} (f : ∀ (a : α), B → A a → B) :
    ∀ {l : List α}, B → HVector A l → B
  | [],   b, .nil       => b
  | t::_, b, .cons a as => foldl f (f t b a) as

infixr:50 "::ₕ" => HVector.cons

infixr:67 "::ᵥ" => Valuation.cons

def not? {w : Nat} (x : BitVec w) : IntW w := do
  .value (~~~x)

def lshrult_01_13_after := [llvm|
{
^0(%arg354 : i4):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def demorgan_nor_use2ac_after := [llvm|
{
^0(%arg22 : i8, %arg23 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(17 : i8) : i8
  %2 = llvm.mlir.constant(23 : i8) : i8
  %3 = llvm.xor %arg22, %0 : i8
  %4 = llvm.mul %3, %1 : i8
  %5 = llvm.or %arg23, %3 : i8
  %6 = llvm.mul %5, %2 : i8
  %7 = llvm.xor %5, %0 : i8
  %8 = llvm.sdiv %7, %6 : i8
  %9 = llvm.sdiv %8, %4 : i8
  "llvm.return"(%9) : (i8) -> ()
}
]

def tryFactorization_add_mul_nuw_mul_var_before := [llvm|
{
^0(%arg0 : i32, %arg1 : i32, %arg2 : i32):
  %0 = llvm.mul %arg0, %arg1 overflow<nuw> : i32
  %1 = llvm.mul %arg0, %arg2 overflow<nuw> : i32
  %2 = llvm.add %0, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def lshrugt_03_15_exact_after := [llvm|
{
^0(%arg174 : i4):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def llvm_const_lower_riscv_li_6 : LLVMPeepholeRewriteRefine 64 [] :=
  {lhs := constLLVM_6, rhs:= liRiscv_6,
   correct := by admit /- proof elided -/

def trunc_shl_1_i32_i64_before := [llvm|
{
^0(%arg35 : i64):
  %0 = llvm.mlir.constant(1) : i64
  %1 = llvm.shl %arg35, %0 : i64
  %2 = llvm.trunc %1 : i64 to i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def src2_after := [llvm|
{
^0(%arg10 : i32, %arg11 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg11, %arg10 : i32
  %2 = llvm.xor %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def and_xor_common_op_before := [llvm|
{
^0(%arg695 : i32, %arg696 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(43 : i32) : i32
  %2 = llvm.udiv %0, %arg695 : i32
  %3 = llvm.udiv %1, %arg696 : i32
  %4 = llvm.xor %2, %3 : i32
  %5 = llvm.and %2, %4 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def ashrsgt_01_01_after := [llvm|
{
^0(%arg316 : i4):
  %0 = llvm.mlir.constant(3 : i4) : i4
  %1 = llvm.icmp "sgt" %arg316, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

def positive_with_icmp_logical_before := [llvm|
{
^0(%arg57 : i32):
  %0 = llvm.mlir.constant(512 : i32) : i32
  %1 = llvm.mlir.constant(128 : i32) : i32
  %2 = llvm.mlir.constant(256 : i32) : i32
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.icmp "ult" %arg57, %0 : i32
  %5 = llvm.add %arg57, %1 : i32
  %6 = llvm.icmp "ult" %5, %2 : i32
  %7 = "llvm.select"(%4, %6, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%7) : (i1) -> ()
}
]

def negative_trunc_not_arg_logical_after := [llvm|
{
^0(%arg20 : i32, %arg21 : i32):
  %0 = llvm.mlir.constant(128 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(256 : i32) : i32
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.and %arg20, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.add %arg21, %0 : i32
  %7 = llvm.icmp "ult" %6, %2 : i32
  %8 = "llvm.select"(%5, %7, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%8) : (i1) -> ()
}
]

def zext_lshr_before := [llvm|
{
^0(%arg12 : i8):
  %0 = llvm.mlir.constant(4 : i16) : i16
  %1 = llvm.zext %arg12 : i8 to i16
  %2 = llvm.lshr %1, %0 : i16
  %3 = llvm.and %2, %1 : i16
  "llvm.return"(%3) : (i16) -> ()
}
]

def sdiv {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW w := do
  let x' ← x
  let y' ← y
  if flag.exact ∧ x'.smod y' ≠ 0 then
    .poison
  else
    sdiv? x' y'

def FpBinaryPredKind.toString : FpBinaryPredKind → String
  | FpBinaryPredKind.eq => "="

def pr40493_neg3_after := [llvm|
{
^0(%arg15 : i32):
  %0 = llvm.mlir.constant(2 : i32) : i32
  %1 = llvm.mlir.constant(4 : i32) : i32
  %2 = llvm.shl %arg15, %0 : i32
  %3 = llvm.and %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def ashrsgt_02_15_exact_after := [llvm|
{
^0(%arg70 : i4):
  %0 = llvm.mlir.constant(-1 : i4) : i4
  %1 = llvm.icmp "sgt" %arg70, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

ZMod.val in Mathlib.Data.ZMod.Basic

def t0_after := [llvm|
{
^0(%arg12 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.and %arg12, %0 : i8
  %3 = llvm.sub %1, %2 overflow<nsw> : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

RV64.mulhsu in RISCV.Instructions

def and_ranges_overlap_single_before := [llvm|
{
^0(%arg255 : i8):
  %0 = llvm.mlir.constant(5 : i8) : i8
  %1 = llvm.mlir.constant(10 : i8) : i8
  %2 = llvm.mlir.constant(20 : i8) : i8
  %3 = llvm.icmp "uge" %arg255, %0 : i8
  %4 = llvm.icmp "ule" %arg255, %1 : i8
  %5 = llvm.and %3, %4 : i1
  %6 = llvm.icmp "uge" %arg255, %1 : i8
  %7 = llvm.icmp "ule" %arg255, %2 : i8
  %8 = llvm.and %6, %7 : i1
  %9 = llvm.and %5, %8 : i1
  "llvm.return"(%9) : (i1) -> ()
}
]

def xor_common_op_commute2_after := [llvm|
{
^0(%arg204 : i8, %arg205 : i8):
  %0 = llvm.mlir.constant(5 : i8) : i8
  %1 = llvm.xor %arg204, %0 : i8
  %2 = llvm.or %1, %arg205 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def lshrugt_02_04_exact_after := [llvm|
{
^0(%arg201 : i4):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def uge_umin3_after := [llvm|
{
^0(%arg48 : i32, %arg49 : i32):
  %0 = llvm.mlir.constant(3 : i32) : i32
  %1 = llvm.add %arg48, %0 : i32
  %2 = llvm.icmp "uge" %arg49, %1 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

Lean.Meta.reduce in Lean.Meta.Reduce

abbrev Width φ := ConcreteOrMVar Nat φ

def n10_wrong_low_bit_mask_after := [llvm|
{
^0(%arg11 : i8):
  %0 = llvm.mlir.constant(31 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.mlir.constant(-16 : i8) : i8
  %3 = llvm.mlir.constant(16 : i8) : i8
  %4 = llvm.and %arg11, %0 : i8
  %5 = llvm.icmp "eq" %4, %1 : i8
  %6 = llvm.and %arg11, %2 : i8
  %7 = llvm.add %6, %3 : i8
  %8 = "llvm.select"(%5, %arg11, %7) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%8) : (i8) -> ()
}
]

Lean.Elab.Term.mkFreshBinderName in Lean.Elab.Term.TermElabM

def ashrsgt_03_13_exact_after := [llvm|
{
^0(%arg56 : i4):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def src_is_mask_or_before := [llvm|
{
^0(%arg117 : i8, %arg118 : i8):
  %0 = llvm.mlir.constant(123 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.mlir.constant(7 : i8) : i8
  %3 = llvm.xor %arg117, %0 : i8
  %4 = llvm.lshr %1, %arg118 : i8
  %5 = llvm.and %4, %2 : i8
  %6 = llvm.and %5, %3 : i8
  %7 = llvm.icmp "eq" %3, %6 : i8
  "llvm.return"(%7) : (i1) -> ()
}
]

def icmp_eq_and_pow2_shl1_before := [llvm|
{
^0(%arg69 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(16 : i32) : i32
  %2 = llvm.mlir.constant(0 : i32) : i32
  %3 = llvm.shl %0, %arg69 : i32
  %4 = llvm.and %3, %1 : i32
  %5 = llvm.icmp "eq" %4, %2 : i32
  %6 = llvm.zext %5 : i1 to i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def ule_or_not_min_logical_after := [llvm|
{
^0(%arg270 : i427, %arg271 : i427):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

@[simp_denote]
def zext_llvm_8_to_64 := [LV| {
  ^entry (%arg: i8):
    %0 = llvm.zext %arg: i8 to i64
    llvm.return %0: i64
  }]

def n10_after := [llvm|
{
^0(%arg0 : i64):
  %0 = llvm.mlir.constant(-1) : i64
  %1 = llvm.icmp "sgt" %arg0, %0 : i64
  %2 = llvm.zext %1 : i1 to i64
  "llvm.return"(%2) : (i64) -> ()
}
]

def llvm_mul_lower_riscv_nsw_flag_32 : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] where
  lhs := mul_llvm_nsw_32
  rhs := mul_riscv_32

def test_simplify_decrement_invalid_ne_after := [llvm|
{
^0(%arg209 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.icmp "eq" %arg209, %0 : i8
  %2 = llvm.sext %1 : i1 to i8
  "llvm.return"(%2) : (i8) -> ()
}
]

abbrev ofTerm (t : Term) : FSM (Fin t.arity) := termEvalEqFSM t |>.toFSM

def add_nsw_poison_constant_fold_after := [llvm|
{
^0(%arg2 : i1, %arg3 : i8):
  %0 = llvm.mlir.constant(64 : i8) : i8
  %1 = llvm.mlir.constant(-127 : i8) : i8
  %2 = llvm.add %arg3, %0 overflow<nsw> : i8
  %3 = "llvm.select"(%arg2, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def ule_swap_and_min_commute_logical_after := [llvm|
{
^0(%arg192 : i8, %arg193 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.icmp "eq" %arg192, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def uadd_sat_canon_nuw_after := [llvm|
{
^0(%arg31 : i32, %arg32 : i32):
  %0 = llvm.add %arg31, %arg32 overflow<nuw> : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def test1_after := [llvm|
{
^0(%arg3 : i333):
  %0 = llvm.mlir.constant(70368744177663 : i333) : i333
  %1 = llvm.and %arg3, %0 : i333
  "llvm.return"(%1) : (i333) -> ()
}
]

def test_with_3_after := [llvm|
{
^0(%arg316 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "eq" %arg316, %0 : i32
  %2 = llvm.zext %1 : i1 to i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def test16_after := [llvm|
{
^0(%arg42 : i8, %arg43 : i8):
  %0 = llvm.mlir.constant(33 : i8) : i8
  %1 = llvm.xor %arg43, %arg42 : i8
  %2 = llvm.xor %arg42, %arg43 : i8
  %3 = llvm.xor %2, %0 : i8
  %4 = llvm.and %3, %1 : i8
  %5 = llvm.mul %4, %3 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def irc_constants_C2MinusAPlusC1_neg1_0 : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%a: i64):
      %c1 = llvm.mlir.constant (-1) : i64
      %c2 = llvm.mlir.constant (0) : i64
      %0 = llvm.add %a, %c1 : i64
      %1 = llvm.sub %c2, %0 : i64
      llvm.return %1 : i64
  }]
  rhs := [LV| {
    ^entry (%a: i64):
      %c1 = llvm.mlir.constant (-1) : i64
      %c2 = llvm.mlir.constant (0) : i64
      %0 = llvm.sub %c2, %c1 : i64
      %1 = llvm.sub %0, %a : i64
      llvm.return %1 : i64
  }]

def test15_before := [llvm|
{
^0(%arg24 : i1):
  %0 = llvm.mlir.constant(3 : i45) : i45
  %1 = llvm.mlir.constant(1 : i45) : i45
  %2 = llvm.mlir.constant(2 : i45) : i45
  %3 = "llvm.select"(%arg24, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i45, i45) -> i45
  %4 = llvm.shl %3, %2 : i45
  "llvm.return"(%4) : (i45) -> ()
}
]

def trunc_shl_1_i32_i64_after := [llvm|
{
^0(%arg35 : i64):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.trunc %arg35 : i64 to i32
  %2 = llvm.shl %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

match res with
          | .ok _ => pure none
          | .error counterExample =>
            let nameToId : Std.HashMap Name Nat := Std.HashMap.ofList (allVars.toList.map (λ (id, var) => (var.name, id)))
            let mut assignment : Std.HashMap Nat BVExpr.PackedBitVec := Std.HashMap.emptyWithCapacity
            for (var, val) in counterExample.equations do
              let name := ((← getLCtx).get! var.fvarId!).userName
              assignment := assignment.insert nameToId[name]! val
            pure (some assignment)
    return res

def test_sub_nuw__all_are_safe_after := [llvm|
{
^0(%arg30 : i32):
  %0 = llvm.mlir.constant(255 : i32) : i32
  %1 = llvm.mlir.constant(-254 : i32) : i32
  %2 = llvm.and %arg30, %0 : i32
  %3 = llvm.sub %1, %2 overflow<nsw,nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def nomask_lhs_before := [llvm|
{
^0(%arg115 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.icmp "eq" %arg115, %0 : i32
  %3 = llvm.and %arg115, %1 : i32
  %4 = llvm.icmp "eq" %3, %0 : i32
  %5 = llvm.or %2, %4 : i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def pr89516_after := [llvm|
{
^0(%arg0 : i8, %arg1 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.icmp "slt" %arg1, %0 : i8
  %3 = llvm.shl %1, %arg0 overflow<nuw> : i8
  %4 = llvm.srem %1, %3 : i8
  %5 = "llvm.select"(%2, %3, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %6 = llvm.add %4, %5 overflow<nuw> : i8
  "llvm.return"(%6) : (i8) -> ()
}
]

def alive_Select_1100_src  (w : Nat)   :=
[llvm( w )| {
^bb0(%Y : _, %X : _):
  %v1 = llvm.mlir.constant 1 :  i1
  %v2 = llvm.select %v1, %X, %Y
  llvm.return %v2
}]

def and_zext_before := [llvm|
{
^0(%arg40 : i32, %arg41 : i1):
  %0 = llvm.zext %arg41 : i1 to i32
  %1 = llvm.and %arg40, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def Expr.KInductionCircuits.mkIsLawful_mkN (fsm : Expr) (n : Expr) : MetaM Expr :=
  mkAppM ``ReflectVerif.BvDecide.KInductionCircuits.IsLawful_mkN #[fsm, n]

def icmp_eq_zext_ne_zero_after := [llvm|
{
^0(%arg39 : i32):
  %0 = llvm.mlir.constant(2 : i32) : i32
  %1 = llvm.icmp "ult" %arg39, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def lor_bor_left1_after := [llvm|
{
^0(%arg66 : i1, %arg67 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = "llvm.select"(%arg66, %0, %arg67) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%1) : (i1) -> ()
}
]

def negtest_near_pow2_cmpval_ashr_wrong_cmp_pred_after := [llvm|
{
^0(%arg2 : i8):
  %0 = llvm.mlir.constant(10 : i8) : i8
  %1 = llvm.icmp "eq" %arg2, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def test_with_5_after := [llvm|
{
^0(%arg315 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "eq" %arg315, %0 : i32
  %2 = llvm.zext %1 : i1 to i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def sgt_mulzero_before := [llvm|
{
^0(%arg144 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(21 : i8) : i8
  %2 = llvm.mul %arg144, %0 overflow<nsw> : i8
  %3 = llvm.icmp "sgt" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

@[simp_denote]
def add_shl_moreOneUse_sh1add_riscv_no_ZBA := [LV| {
    ^entry (%a: i32):
    %a0 = "builtin.unrealized_conversion_cast" (%a) : (i32) -> (!i64)
    %0 = ori %a0, 1 : !i64
    %1 = slli %a0, 1 : !i64
    %2 = ori %1, 2 : !i64
    %3 = add %2, %0 : !i64
    %4 = "builtin.unrealized_conversion_cast" (%3) : (!i64) -> (i32)
    llvm.return %4 : i32
  }]

def dec_sub_after := [llvm|
{
^0(%arg16 : i8, %arg17 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.xor %arg17, %0 : i8
  %2 = llvm.add %arg16, %1 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def test_sle_xor_before := [llvm|
{
^0(%arg42 : i32, %arg43 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg43, %0 : i32
  %2 = llvm.xor %1, %arg42 : i32
  %3 = llvm.icmp "sle" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def positive_biggerashr_shlnuwnsw_ashrexact_after := [llvm|
{
^0(%arg25 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.ashr exact %arg25, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def test43_before := [llvm|
{
^0(%arg205 : i32, %arg206 : i32, %arg207 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.mul %arg206, %arg207 : i32
  %2 = llvm.or %arg205, %1 : i32
  %3 = llvm.xor %arg205, %0 : i32
  %4 = llvm.xor %3, %1 : i32
  %5 = llvm.and %2, %4 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def and_xor_commute1_after := [llvm|
{
^0(%arg155 : i32, %arg156 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.udiv %0, %arg155 : i32
  %3 = llvm.udiv %0, %arg156 : i32
  %4 = llvm.xor %2, %1 : i32
  %5 = llvm.and %3, %4 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def lshrult_03_10_exact_after := [llvm|
{
^0(%arg107 : i4):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def shl_mask_after := [llvm|
{
^0(%arg6 : i32):
  %0 = llvm.mlir.constant(255 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.and %arg6, %0 : i32
  %3 = llvm.shl %2, %1 overflow<nsw,nuw> : i32
  %4 = llvm.or disjoint %2, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

|

Neg in Init.Prelude
</all_available_defs>

<all_available_lemmas>
Bool.false_eq_true in Init.Data.Bool
IsEmpty.exists_iff in Mathlib.Logic.IsEmpty
Option.isSome_none in Init.Data.Option.Basic
iff_false in Init.SimpLemmas
Option.bind_eq_some_iff in Init.Data.Option.Lemmas
AList.entries_insert_of_notMem in Mathlib.Data.List.AList
AList.lookup_eq_none in Mathlib.Data.List.AList
List.subset_cons_of_subset in Init.Data.List.Sublist
Option.mem_def in Init.Data.Option.Instances
IsEmpty.forall_iff in Mathlib.Logic.IsEmpty
forall_eq' in Init.PropLemmas
iff_true in Init.SimpLemmas
implies_true in Init.SimpLemmas
AList.keys_subset_keys_of_entries_subset_entries in Mathlib.Data.List.AList
Finset.biUnion_insert in Mathlib.Data.Finset.Union
Finset.mem_biUnion in Mathlib.Data.Finset.Union
Finset.mem_union in Mathlib.Data.Finset.Lattice.Basic
AList.lookup_isSome in Mathlib.Data.List.AList
Finset.mem_singleton in Mathlib.Data.Finset.Insert
Sigma.mk.inj_iff in Mathlib.Data.Sigma.Basic
and_imp in Init.SimpLemmas

@[simp] theorem appendCases_appendInl (v : Γ.Var t) :
    appendCases (motive := motive) left right v.appendInl = (left v)

@[simp] theorem HVector.vars_cons {t  : d.Ty} {l : List d.Ty}
    (v : Var Γ t) (T : HVector (Var Γ) l) :
    (HVector.cons v T).vars = insert ⟨_, v⟩ T.vars

@[simp] theorem appendCases_appendInr (v : Γ.Var t) :
    appendCases (motive := motive) left right v.appendInr = (right v)

theorem e_2267 :
    3 * (f &&&  ~~~(d &&& e)) + 4 * ((d &&& f) ^^^ (e ||| f)) + 4 * (d ^^^ e) - 11 *  ~~~( ~~~d &&& (e &&& f)) + 1 *  ~~~(d ||| f) - 2 *  ~~~(d ^^^ e) - 3 * (f ^^^ (d &&& ( ~~~e ||| f))) + 1 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) - 1 * ( ~~~d &&& (e ||| f)) + 2 *  ~~~(d ||| e) + 1 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) - 3 *  ~~~( ~~~d &&& (e ^^^ f)) - 1 * (f ^^^  ~~~(d &&& e)) - 5 *  ~~~(d &&& e) + 5 * ( ~~~d &&& ( ~~~e ||| f)) - 1 * ( ~~~(d |||  ~~~e) |||  ~~~(e ^^^ f)) + 1 * (e ^^^  ~~~(d |||  ~~~f)) + 5 *  ~~~(d ||| ( ~~~e &&& f)) + 1 * (d &&&  ~~~f) + 1 * (f |||  ~~~(d ^^^ e)) + 1 * (f &&& (d |||  ~~~e)) + 1 * (e ^^^  ~~~(d ||| ( ~~~e &&& f))) + 1 * (e &&& (d |||  ~~~f)) - 11 * (f &&&  ~~~(d &&&  ~~~e)) - 11 *  ~~~(d &&& (e ^^^ f)) + 3 *  ~~~(e ||| f) - 5 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) - 2 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) - 1 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) - 2 * ( ~~~e |||  ~~~(d ^^^ f)) + 4 * (e ^^^  ~~~(d &&& (e ^^^ f))) + 11 * ( ~~~(d &&& e) &&& (e ^^^ f)) - 2 * (e ^^^ ( ~~~d ||| (e ^^^ f))) - 3 * (e &&&  ~~~(d &&& f)) + 3 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f)) - 1 * (e ^^^ (d ||| (e &&& f))) - 2 * (e ^^^ ( ~~~d ||| (e &&& f))) + 3 *  ~~~(d |||  ~~~f) - 1 * (d &&& (e ||| f)) + 2 * (e ^^^  ~~~(d ||| f)) - 7 * ( ~~~(d &&& e) &&&  ~~~(e ^^^ f)) - 6 * ((d &&& e) |||  ~~~(e |||  ~~~f)) + 1 * ( ~~~(d |||  ~~~e) ||| (e ^^^ f)) + 3 * (f ^^^ (d &&& e)) + 2 * ((d &&& e) ||| (d ^^^ (e ^^^ f))) + 7 * (d ||| e) - 11 *  ~~~(d &&& ( ~~~e &&& f)) - 5 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) + 1 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) + 1 *  ~~~(e &&&  ~~~f) - 6 * (e |||  ~~~f) + 30 *  ~~~(d ||| (e ||| f)) + 16 *  ~~~(d ||| ( ~~~e ||| f)) + 46 *  ~~~( ~~~d ||| (e ||| f)) + 15 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 27 * ( ~~~d &&& ( ~~~e &&& f)) + 21 * ( ~~~d &&& (e &&& f)) - 2 * (d &&& ( ~~~e &&& f)) + 54 * (d &&& (e &&& f)) =  - 7 *  ~~~(d &&& ( ~~~e ||| f))

theorem icmp_eq_sext_ne_allones_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (signExtend 32 (ofBool (x != -1#32)) == x) = 0#1

theorem eq_smax2_thm (e e_1 : IntW 32) :
  icmp IntPred.eq (select (icmp IntPred.sgt e_1 e) e_1 e) e ⊑ icmp IntPred.sge e e_1

theorem test21 (x y : BitVec w) : (~~~(x - y)) = (~~~x + y)

theorem main7b_logical_thm.extracted_1._6 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 == x_1 &&& x_2) = 1#1 →
    ofBool (x_2 != x_1 &&& x_2) = 1#1 → ¬ofBool (x == x_1 &&& x) = 1#1 → 1#32 = zeroExtend 32 1#1

theorem shl_nsw_add_nsw_nuw_proof : shl_nsw_add_nsw_nuw_before ⊑ shl_nsw_add_nsw_nuw_after

theorem main7c_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 == x_2 &&& x_1) &&& ofBool (x * 42#32 == x * 42#32 &&& x_1) = 1#1 →
    0#32 = zeroExtend 32 (ofBool (x_1 &&& (x_2 ||| x * 42#32) != x_2 ||| x * 42#32))

theorem bv_AndOrXor_2486 :
    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.add e e_1) (LLVM.const? w (-1)) ⊑ LLVM.sub (LLVM.sub (LLVM.const? w (-1)) e_1) e

theorem dec_mask_commute_neg_i32_proof : dec_mask_commute_neg_i32_before ⊑ dec_mask_commute_neg_i32_after

theorem ashr_ugt_5_proof : ashr_ugt_5_before ⊑ ashr_ugt_5_after

theorem and_logic_and_logic_or_8_thm.extracted_1._3 : ∀ (x x_1 : BitVec 1), ¬x_1 = 1#1 → 0#1 = 1#1 → False

theorem alive_820   : alive_820_src ⊑ alive_820_tgt

theorem test_or1_thm (e e_1 : IntW 32) :
  LLVM.or (icmp IntPred.slt e_1 (const? 32 0)) (icmp IntPred.sge e_1 (LLVM.and e (const? 32 2147483647))) ⊑
    icmp IntPred.uge e_1 (LLVM.and e (const? 32 2147483647))

theorem ashrsgt_01_05_thm.extracted_1._1 : ∀ (x : BitVec 4), ¬1#4 ≥ ↑4 → ofBool (5#4 <ₛ x.sshiftRight' 1#4) = 0#1

theorem positive_biggerlshr_shlnuwnsw_lshrexact_proof : positive_biggerlshr_shlnuwnsw_lshrexact_before ⊑ positive_biggerlshr_shlnuwnsw_lshrexact_after

theorem masked_icmps_mask_notallzeros_bmask_mixed_5_logical_proof : masked_icmps_mask_notallzeros_bmask_mixed_5_logical_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_5_logical_after

theorem test9_thm (e e_1 : IntW 32) : LLVM.xor (LLVM.and e_1 e) (LLVM.xor e_1 e) ⊑ LLVM.or e_1 e

theorem or_eq_with_diff_one_signed_logical_proof : or_eq_with_diff_one_signed_logical_before ⊑ or_eq_with_diff_one_signed_logical_after

theorem ashrslt_01_04_exact_thm (e : IntW 4) :
  icmp IntPred.slt (ashr e (const? 4 1) { «exact» := true }) (const? 4 4) ⊑ const? 1 1

theorem icmp_slt_0_or_icmp_sge_100_i32_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 → x >>> 31#32 ||

theorem t0_thm (e : IntW 8) :
  select (icmp IntPred.eq (LLVM.and e (const? 8 15)) (const? 8 0)) e
      (LLVM.and (add e (const? 8 16)) (const? 8 (-16))) ⊑
    LLVM.and (add e (const? 8 15)) (const? 8 (-16))

theorem test_logical_thm.extracted_1._1 : ∀ (x : BitVec 32), ofBool (255#32 <ᵤ x) = 1#1 → 1#1 = ofBool (255#32 <ᵤ x)

theorem mul_sel_op0_thm.extracted_1._2 : ∀ (x : BitVec 32) (x_1 : BitVec 1),
  ¬x_1 = 1#1 → ¬(True ∧ (42#32).umod x ≠ 0 ∨ x = 0) → 42#32 / x * x = 42#32

@[simp] theorem Com.denote_var [LawfulMonad d.m] {e : Expr d Γ eff α} :
    (Com.var e body).denote =
    fun Γv => (e.denote Γv) >>= body.denote

theorem slt_zero_ne_ne_0_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 → ofBool (zeroExtend 32 (ofBool (x != 0#32)) != x >>> 31#32) = ofBool (0#32 <ₛ x)

theorem main10_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x &&& 64#32 == 0#32) = 1#1 →
    ¬ofBool (x &&& 192#32 == 0#32) = 1#1 → ofBool (0#8 ≤ₛ truncate 8 x) = 1#1 → 2#32 = 1#32

theorem src_srem_shl_demand_min_signbit_proof : src_srem_shl_demand_min_signbit_before ⊑ src_srem_shl_demand_min_signbit_after

theorem icmp_ne_zext_eq_non_boolean_thm (e : IntW 32) :
  icmp IntPred.ne (zext 32 (icmp IntPred.eq e (const? 32 2))) e ⊑
    icmp IntPred.ne e (const? 32 0)

theorem PR42691_7_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (BitVec.ofInt 32 (-2147483647) ≤ᵤ x) = 1#1 → 1#1 = ofBool (x + -1#32 <ₛ 0#32)

theorem test8_thm (e : IntW 7) : shl (shl e (const? 7 4)) (const? 7 3) ⊑ const? 7 0

theorem main3_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (x &&& 7#32 == 0#32) &&& ofBool (x &&& 48#32 == 0#32) = 1#1 →
    1#32 = zeroExtend 32 (ofBool (x &&& 55#32 != 0#32))

theorem sle_or_not_min_commute_thm (e e_1 : IntW 8) :
  LLVM.or (icmp IntPred.ne e_1 (const? 8 (-128))) (icmp IntPred.sle e_1 e) ⊑ const? 1 1

theorem substitute_constant_or_ne_swap_sle_proof : substitute_constant_or_ne_swap_sle_before ⊑ substitute_constant_or_ne_swap_sle_after

theorem icmp_x_slt_0_xor_icmp_y_sgt_neg1_i32_proof : icmp_x_slt_0_xor_icmp_y_sgt_neg1_i32_before ⊑ icmp_x_slt_0_xor_icmp_y_sgt_neg1_i32_after

theorem icmp_shl_nsw_sge0_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(True ∧ (x <<< 21#32).sshiftRight' 21#32 ≠ x ∨ 21#32 ≥ ↑32) → ofBool (0#32 ≤ₛ x <<< 21#32) = ofBool (-1#32 <ₛ x)

theorem a_thm (e e_1 : IntW 1) :
  add (add (zext 32 e_1) (const? 32 1)) (sub (const? 32 0) (zext 32 e)) ⊑
    add (select e_1 (const? 32 2) (const? 32 1)) (sext 32 e) { «nsw» := true, «nuw» := false }

theorem icmp_ne_and_pow2_shl_pow2_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬x ≥ ↑32 → zeroExtend 32 (ofBool (2#32 <<< x &&& 16#32 != 0#32)) = zeroExtend 32 (ofBool (x == 3#32))

theorem scalar_i8_shl_ult_const_1_proof : scalar_i8_shl_ult_const_1_before ⊑ scalar_i8_shl_ult_const_1_after

theorem e_1726 :
     - 5 * ((a |||  ~~~b) &&& (a ^^^ (b ^^^ c))) - 6 * c - 1 *  ~~~(a |||  ~~~c) - 1 * ((a &&& b) ^^^ (b |||  ~~~c)) - 5 * (b ^^^  ~~~( ~~~a &&& (b &&& c))) + 4 * (c ^^^ (a ||| (b &&& c))) - 1 *  ~~~(a &&&  ~~~a) + 1 * (b ^^^ (a ||| c)) - 1 * ( ~~~(a ||| b) |||  ~~~(a ^^^ (b ^^^ c))) - 3 * ( ~~~(a ^^^ b) &&&  ~~~(a ^^^ c)) + 5 * (b ^^^ (a &&&  ~~~c)) - 1 * ((a ^^^ b) &&& (a ^^^ c)) + 11 * (c ^^^ ( ~~~a ||| ( ~~~b ||| c))) + 2 * (a ^^^ ( ~~~b &&& c)) - 11 * ((a ||| b) &&&  ~~~(b ^^^ c)) + 1 *  ~~~(a ^^^ ( ~~~b ||| c)) - 1 *  ~~~(a ^^^ (b ||| c)) + 1 * (b ^^^  ~~~( ~~~a &&& (b ||| c))) + 1 *  ~~~( ~~~a ||| (b ^^^ c)) - 11 * (b ^^^  ~~~(a &&& (b ||| c))) + 11 * (c ^^^  ~~~(a &&&  ~~~b)) + 3 * (c ^^^  ~~~( ~~~a &&& (b &&& c))) - 11 * (a &&&  ~~~b) + 8 *  ~~~(a ||| (b ||| c)) - 20 *  ~~~(a ||| ( ~~~b ||| c)) + 17 *  ~~~( ~~~a ||| (b ||| c)) - 6 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 34 * ( ~~~a &&& ( ~~~b &&& c)) + 18 * ( ~~~a &&& (b &&& c)) + 11 * (a &&& ( ~~~b &&& c)) + 29 * (a &&& (b &&& c)) = 11 *  ~~~(a ||| (b &&& c))

theorem test1_trunc_proof : test1_trunc_before ⊑ test1_trunc_after

theorem test23_thm (e : IntW 44) : trunc 11 (ashr (shl e (const? 44 33)) (const? 44 33)) ⊑ trunc 11 e

theorem ashrsgt_03_10_exact_thm (e : IntW 4) :
  icmp IntPred.sgt (ashr e (const? 4 3) { «exact» := true }) (const? 4 (-6)) ⊑ const? 1 1

theorem eq_rem_zero_nonuw_proof : eq_rem_zero_nonuw_before ⊑ eq_rem_zero_nonuw_after

theorem fast_div_201_proof : fast_div_201_before ⊑ fast_div_201_after

theorem test15h_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (x &&& 8#32 != 0#32) = 1#1 → -1#32 = x &&& 8#32 ^^^ -1#32

theorem negative2_proof : negative2_before ⊑ negative2_after

theorem n8_wrong_pred3_thm (e e_1 : IntW 8) :
  icmp IntPred.ne (sub e_1 e) e_1 ⊑ icmp IntPred.ne e (const? 8 0)

theorem icmp_eq_and_pow2_shl1_thm (e : IntW 32) :
  zext 32 (icmp IntPred.eq (LLVM.and (shl (const? 32 1) e) (const? 32 16)) (const? 32 0)) ⊑
    zext 32 (icmp IntPred.ne e (const? 32 4))

theorem neg_mask1_lshr_proof : neg_mask1_lshr_before ⊑ neg_mask1_lshr_after

theorem test69_and_proof : test69_and_before ⊑ test69_and_after

theorem sub_mask1_lshr_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬1#8 ≥ ↑8 → 6#8 ≥ ↑8 ∨ 7#8 ≥ ↑8 ∨ True ∧ ((x <<< 6#8).sshiftRight' 7#8).saddOverflow 10#8 = true → False

theorem main3d_proof : main3d_before ⊑ main3d_after

theorem ashrslt_03_04_proof : ashrslt_03_04_before ⊑ ashrslt_03_04_after

theorem alive_InstCombineShift__582 : alive_InstCombineShift__582_src ⊑ alive_InstCombineShift__582_tgt

theorem e_10 :
     - 3 * x - 2 *  ~~~y + 6 * (x &&&  ~~~y) + 4 * (x &&& y) =  - 3 *  ~~~(x ||| y) + 1 * (x |||  ~~~y)

theorem PR39793_bswap_u32_as_u16_trunc_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32) → 8#32 ≥ ↑32 → False

theorem icmp_power2_and_icmp_shifted_mask_swapped_1073741824_1073741823_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 1073741823#32 != 1073741823#32) &&& ofBool (x <ᵤ 1073741824#32) = ofBool (x <ᵤ 1073741823#32)

theorem and_xor_common_op_commute1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬(x_1 = 0 ∨ x = 0 ∨ x_1 = 0) →
    ¬(x_1 = 0 ∨ x = 0) → 42#32 / x_1 &&& (43#32 / x ^^^ 42#32 / x_1) = 42#32 / x_1 &&& (43#32 / x ^^^ -1#32)

theorem e_1339 :
    1 *  ~~~z + 1 *  ~~~(z &&&  ~~~z) - 7 * (z ^^^ t) - 2 *  ~~~(z &&&  ~~~t) + 2 *  ~~~t + 5 *  ~~~(z ^^^ t) + 1 * (z |||  ~~~t) + 3 *  ~~~(z |||  ~~~t) + 3 * (z &&&  ~~~t) - 9 * (z &&& t) =  - 4 * t + 8 *  ~~~(z ||| t)

theorem logical_and_not_proof : logical_and_not_before ⊑ logical_and_not_after

theorem or_not_and_commute6_thm (e e_1 e_2 : IntW 32) :
  LLVM.or (LLVM.and (LLVM.xor (LLVM.or e_2 e_1) (const? 32 (-1))) e)
      (LLVM.and (LLVM.xor (LLVM.or e e_2) (const? 32 (-1))) e_1) ⊑
    LLVM.and (LLVM.xor e_1 e) (LLVM.xor e_2 (const? 32 (-1)))

theorem and_zext_demanded_thm (e : IntW 16) (e_1 : IntW 32) :
  LLVM.and (LLVM.or e_1 (const? 32 255)) (zext 32 (lshr e (const? 16 8))) ⊑
    zext 32 (lshr e (const? 16 8)) { «nneg» := true }

theorem test20_proof : test20_before ⊑ test20_after

theorem foo1_or_signbit_lshr_without_shifting_signbit_both_sides_proof : foo1_or_signbit_lshr_without_shifting_signbit_both_sides_before ⊑ foo1_or_signbit_lshr_without_shifting_signbit_both_sides_after

theorem lshr_ne_msb_low_last_zero_thm (e : IntW 8) :
  icmp IntPred.ne (lshr (const? 8 127) e) (const? 8 0) ⊑ icmp IntPred.ult e (const? 8 7)

theorem test2_thm (e : IntW 15) : LLVM.xor e (const? 15 0) ⊑ e

theorem sge_or_not_max_logical_proof : sge_or_not_max_logical_before ⊑ sge_or_not_max_logical_after

theorem e_2067 :
     - 1 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) - 11 * (e &&& (d |||  ~~~f)) - 11 * (f ^^^ (d &&& (e ||| f))) + 2 * ((d &&& e) ^^^ (d ^^^ ( ~~~e ||| f))) - 1 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) - 1 * (d |||  ~~~e) - 1 * (f ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) + 2 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 1 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 6 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) - 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) - 3 * (e ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) + 1 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) + 1 * ( ~~~(d ^^^ e) ||| (d ^^^ f)) - 6 * (f ^^^ ( ~~~d ||| ( ~~~e ||| f))) - 7 * ( ~~~d ||| ( ~~~e ||| f)) + 2 * (e ^^^  ~~~(d ||| f)) - 5 * (d |||  ~~~f) - 2 * (e |||  ~~~(d ||| f)) - 2 * (f ^^^  ~~~(d &&& (e ||| f))) + 1 * (e |||  ~~~(d |||  ~~~f)) + 3 * ( ~~~d &&& (e ^^^ f)) + 1 * ( ~~~(d &&& e) &&& (e ^^^ f)) - 1 * (e ^^^ (d ||| ( ~~~e &&& f))) + 1 * (e ||| (d ^^^ f)) + 11 * ( ~~~e ||| (d ^^^ f)) + 11 * (e ^^^  ~~~( ~~~d &&& (e &&& f))) - 1 * (f ^^^  ~~~(d |||  ~~~e)) + 2 * (f &&& (d |||  ~~~e)) + 1 * (d ^^^ f) - 1 * ((d &&& e) |||  ~~~(e |||  ~~~f)) - 4 *  ~~~(d ||| (e ||| f)) + 33 *  ~~~(d ||| ( ~~~e ||| f)) - 2 *  ~~~( ~~~d ||| (e ||| f)) + 16 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 10 * ( ~~~d &&& ( ~~~e &&& f)) - 9 * ( ~~~d &&& (e &&& f)) - 11 * (d &&& ( ~~~e &&& f)) + 19 * (d &&& (e &&& f)) =  - 3 *  ~~~( ~~~d &&& (e &&& f))

theorem sub_select_sext_op_swapped_non_const_args_thm.extracted_1._1 : ∀ (x : BitVec 6) (x_1 : BitVec 1),
  x_1 = 1#1 → signExtend 6 x_1 - x = x ^^^ -1#6
</all_available_lemmas>

<local_ctx>
import LeanMLIR.Framework

import LeanMLIR.Transforms.Rewrite.Mapping

open Ctxt (Var VarSet Valuation Hom)

variable {d} [DialectSignature d] [DecidableEq d.Ty]

variable {Γ : Ctxt d.Ty} {ty : d.Ty}

abbrev MatchVarM (Δ Γ : Ctxt d.Ty) := (StateT (Mapping Δ Γ) Option)

abbrev MatchVar (Δ Γ : Ctxt d.Ty)  := MatchVarM Δ Γ Unit

def MatchVarM.unifyVars {Δ Γ : Ctxt d.Ty} (v : Δ.Var t) (w : Γ.Var t) : MatchVar Δ Γ :=
  fun ma =>
    match ma.lookup ⟨_, v⟩ with
    | some v =>
      if v = w then
        some ((), ma)
      else
        none
    | none =>
      some ((), AList.insert ⟨_, v⟩ w ma)

open MatchVarM

variable [DecidableEq d.Op]

def matchArg [DecidableEq d.Op]
    (lets : Lets d Γ_in eff Γ_out) (matchLets : Lets d Δ_in .pure Δ_out) :
    {l : List d.Ty} → HVector (Var Γ_out) l → HVector (Var Δ_out) l →
    MatchVar Δ_in Γ_out
  | _, .nil, .nil => return
  | t::l, .cons vₗ vsₗ, .cons vᵣ vsᵣ => do
      matchVar (t := t) lets vₗ matchLets vᵣ
      matchArg lets matchLets vsₗ vsᵣ
  termination_by l => (sizeOf matchLets, l.length + 1)

def matchVar {Γ_in Γ_out Δ_in Δ_out : Ctxt d.Ty} {t : d.Ty} [DecidableEq d.Op]
    (lets : Lets d Γ_in eff Γ_out) (v : Var Γ_out t) :
    (matchLets : Lets d Δ_in .pure Δ_out) →
    (w : Var Δ_out t) →
    MatchVar Δ_in Γ_out
   
  | @Lets.var _ _ _ _ Δ_out ts matchLets matchExpr, w => by admit /- proof elided -/
      | right w =>
        exact matchVar lets v matchLets w
      | left w => exact do
        let ⟨ts', w', ie⟩ ← lets.getPureExpr v
        if hs : ∃ h : ie.op = matchExpr.op, ie.regArgs = (h ▸ matchExpr.regArgs) then
          have hts : Ctxt.ofList ts' = ts := by admit /- proof elided -/

end

section MatchVar

variable [DecidableEq d.Op] {Γ_in Γ_out Δ_in Δ_out t te}
          {lets : Lets d Γ_in eff Γ_out} {v : Var Γ_out t}
          {matchLets : Lets d Δ_in .pure Δ_out}
          {matchExpr : Expr d Δ_out .pure te}

variable (lets v matchLets w) (mapIn : Mapping _ _) in

variable (lets matchLets) {tys} (vs ws : HVector _ tys) (mapIn : Mapping _ _) in

namespace MatchVarResult

variable [TyDenote d.Ty] [∀ (t : d.Ty), Inhabited ⟦t⟧] in

section Left

variable {w : Δ_out.Var t}

variable {mapIn} (mapOut : MatchVarResult lets v (.var matchLets matchExpr) w.appendInr mapIn)

end Left

variable {w : Var ⟨te⟩ _} {mapIn}

end MatchVarResult

end MatchVar

section SubsetEntries

def MatchVar.IsMonotone (f : MatchVar Δ Γ) : Prop :=
    ∀ mapIn, ∀ mapOut ∈ f mapIn,
      mapIn.entries ⊆ mapOut.2.entries

open MatchVar

section UnifyVars

variable {Δ Γ : Ctxt d.Ty} {t} (w : Δ.Var t) (v : Γ.Var t)

end UnifyVars

variable [DecidableEq d.Op]

end SubsetEntries

namespace MatchArgResult

variable [DecidableEq d.Op] {Γ_in Γ_out Δ_in Δ_out te}
          {lets : Lets d Γ_in eff Γ_out}
          {matchLets : Lets d Δ_in .pure Δ_out}
          {matchExpr : Expr d Δ_out .pure te}
          {u us}
          {v : Γ_out.Var u} {vs : HVector Γ_out.Var us}
          {w : Δ_out.Var u} {ws : HVector Δ_out.Var us}
          {mapIn : Mapping _ _}
          (mapOut : MatchArgResult lets matchLets (v ::ₕ vs) (w ::ₕ ws) mapIn)

end MatchArgResult

section DenoteLemmas

variable [TyDenote d.Ty] [DecidableEq d.Op]

variable [∀ (t : d.Ty), Inhabited ⟦t⟧]

variable [Monad d.m] [LawfulMonad d.m] [DialectDenote d]

section DenoteIntoSubtype

end DenoteIntoSubtype

variable {Γ_in Γ_out Δ_in Δ_out : Ctxt d.Ty}
    {lets : Lets d Γ_in eff Γ_out}
    {matchLets : Lets d Δ_in .pure Δ_out}
</local_ctx>

<target_theorem>
theorem mem_matchArg {Δ_out}
    {lets : Lets d Γ_in eff Γ_out}
    {matchLets : Lets d Δ_in .pure Δ_out}
    {l : List d.Ty} {argsₗ : HVector (Var Γ_out) l}
    {argsᵣ : HVector (Var Δ_out) l} {ma : Mapping Δ_in Γ_out}
    {varMap : Mapping Δ_in Γ_out}
    (hvarMap : ((), varMap) ∈ matchArg lets matchLets argsₗ argsᵣ ma)
    {t' v'} : ⟨t', v'⟩ ∈ matchLets.varsOfVec argsᵣ → ⟨t', v'⟩ ∈ varMap :=
</target_theorem>

