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
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
AList.insert in Mathlib.Data.List.AList
Valuation.map in Mathlib.RingTheory.Valuation.Basic
PUnit in Init.Prelude
Finset in Mathlib.Data.Finset.Defs
Sigma in Init.Core
Sigma.mk in Init.Core
liftM in Init.Prelude
Iff in Init.Core
IsEmpty in Mathlib.Logic.IsEmpty
StateT.bind in Init.Control.State
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

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 -/
    )

@[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 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 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 HVector.vars {l : List d.Ty} (T : HVector (Var Γ) l) : VarSet Γ :=
  T.foldl (fun _ s a => insert ⟨_, a⟩ s) ∅

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

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

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

@[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 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) -> ()
}
]

def xor_to_xor3_after := [llvm|
{
^0(%arg81 : i32, %arg82 : i32):
  %0 = llvm.xor %arg81, %arg82 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

Lean.Meta.reduce in Lean.Meta.Reduce

def slt_swap_and_not_max_logical_before := [llvm|
{
^0(%arg116 : i8, %arg117 : i8):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "sgt" %arg117, %arg116 : i8
  %3 = llvm.icmp "ne" %arg116, %0 : i8
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def masked_icmps_mask_notallzeros_bmask_mixed_swapped_7b_before := [llvm|
{
^0(%arg32 : i32):
  %0 = llvm.mlir.constant(6 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(15 : i32) : i32
  %3 = llvm.mlir.constant(8 : i32) : i32
  %4 = llvm.and %arg32, %0 : i32
  %5 = llvm.icmp "ne" %4, %1 : i32
  %6 = llvm.and %arg32, %2 : i32
  %7 = llvm.icmp "eq" %6, %3 : i32
  %8 = llvm.and %7, %5 : i1
  "llvm.return"(%8) : (i1) -> ()
}
]

def test16_after := [llvm|
{
^0(%arg1 : i32):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

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 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 idempotent_prop_freeze : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %0 = llvm.freeze %x : i64
      %1 = llvm.freeze %0 : i64
      llvm.return %1 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %0 = llvm.freeze %x : i64
      llvm.return %0 : i64
  }]

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

def scalar_i8_shl_ult_const_3_before := [llvm|
{
^0(%arg17 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.mlir.constant(64 : i8) : i8
  %2 = llvm.shl %arg17, %0 : i8
  %3 = llvm.icmp "ult" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

def or_not_and_commute3_after := [llvm|
{
^0(%arg528 : i32, %arg529 : i32, %arg530 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg529, %arg530 : i32
  %2 = llvm.xor %arg528, %0 : i32
  %3 = llvm.and %1, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def select_bittest_to_sub_before := [llvm|
{
^0(%arg4 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(4 : i32) : i32
  %3 = llvm.mlir.constant(3 : i32) : i32
  %4 = llvm.and %arg4, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = "llvm.select"(%5, %2, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%6) : (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 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 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 ashrsgt_03_13_exact_after := [llvm|
{
^0(%arg56 : i4):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

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 test_logical_or_eq_a_b_before := [llvm|
{
^0(%arg9 : i1, %arg10 : i8, %arg11 : i8):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.icmp "eq" %arg10, %arg11 : i8
  %2 = "llvm.select"(%arg9, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = "llvm.select"(%2, %arg10, %arg11) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

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

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

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 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 t1_flags_nuw_nsw_first_after := [llvm|
{
^0(%arg33 : i8, %arg34 : i8, %arg35 : i8):
  %0 = llvm.add %arg34, %arg35 : i8
  %1 = llvm.sub %arg33, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def lshrugt_02_02_exact_before := [llvm|
{
^0(%arg203 : i4):
  %0 = llvm.mlir.constant(2 : i4) : i4
  %1 = llvm.lshr exact %arg203, %0 : i4
  %2 = llvm.icmp "ugt" %1, %0 : i4
  "llvm.return"(%2) : (i1) -> ()
}
]

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

abbrev Width φ := ConcreteOrMVar Nat φ

ZMod.val in Mathlib.Data.ZMod.Basic

def shl_nsw_add_after := [llvm|
{
^0(%arg22 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.shl %0, %arg22 overflow<nsw> : i32
  %2 = llvm.xor %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def div {Γ : Ctxt _} (e₁ e₂: Ctxt.Var Γ .bv) : Expr RV64 Γ .pure [.bv]  :=
  Expr.mk
    (op := Op.div)
    (eff_le := by admit /- proof elided -/
    )
    (ty_eq := by admit /- proof elided -/
    )
    (args := .cons e₁ <| .cons e₂ .nil)
    (regArgs := HVector.nil)

def or_test2_after := [llvm|
{
^0(%arg0 : i7, %arg1 : i7):
  %0 = llvm.mlir.constant(-64 : i7) : i7
  "llvm.return"(%0) : (i7) -> ()
}
]

def negate_add_with_single_negatible_operand_depth2_after := [llvm|
{
^0(%arg35 : i8, %arg36 : i8):
  %0 = llvm.mlir.constant(-21 : i8) : i8
  %1 = llvm.sub %0, %arg35 : i8
  %2 = llvm.mul %1, %arg36 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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 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 right_identity_zero_ror : RISCVPeepholeRewrite [Ty.riscv (.bv)] where
  lhs := [LV| {
    ^entry (%x: !riscv.reg):
      %c = li (0) : !riscv.reg
      %0 = ror %x, %c : !riscv.reg
      ret %0 : !riscv.reg
  }]
  rhs := [LV| {
    ^entry (%x: !riscv.reg):
      ret %x : !riscv.reg
  }]

def test_srem_canonicalize_op0_before := [llvm|
{
^0(%arg8 : i32, %arg9 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.sub %0, %arg8 overflow<nsw> : i32
  %2 = llvm.srem %1, %arg9 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

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

def icmp_ne_and_pow2_lshr_pow2_case2_after := [llvm|
{
^0(%arg40 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def ult_swap_or_not_max_logical_before := [llvm|
{
^0(%arg36 : i8, %arg37 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.icmp "ugt" %arg37, %arg36 : i8
  %3 = llvm.icmp "ne" %arg36, %0 : i8
  %4 = "llvm.select"(%2, %1, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def scalar_zext_slt_before := [llvm|
{
^0(%arg1 : i16):
  %0 = llvm.mlir.constant(500 : i32) : i32
  %1 = llvm.zext %arg1 : i16 to i32
  %2 = llvm.icmp "slt" %1, %0 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def t0_before := [llvm|
{
^0(%arg12 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.shl %arg12, %0 : i8
  %2 = llvm.ashr %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

instance : Coe (Γ.Var t) ((Γ ++ ts).Var t) where coe := appendInl

def negative4_logical_after := [llvm|
{
^0(%arg4 : i32, %arg5 : i32):
  %0 = llvm.mlir.constant(2147483647 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.and %arg5, %0 : i32
  %3 = llvm.icmp "ne" %arg4, %2 : i32
  %4 = llvm.icmp "sgt" %arg4, %1 : i32
  %5 = llvm.and %3, %4 : i1
  "llvm.return"(%5) : (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 not_or_or_and_no_and_after := [llvm|
{
^0(%arg121 : i32, %arg122 : i32, %arg123 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg121, %0 : i32
  %2 = llvm.xor %arg122, %0 : i32
  %3 = llvm.and %arg123, %2 : i32
  %4 = llvm.or %3, %1 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

def c_1_0_0_after := [llvm|
{
^0(%arg32 : i4, %arg33 : i4, %arg34 : i4):
  %0 = llvm.xor %arg33, %arg32 : i4
  %1 = llvm.and %0, %arg34 : i4
  %2 = llvm.xor %1, %arg32 : i4
  "llvm.return"(%2) : (i4) -> ()
}
]

def test43_before := [llvm|
{
^0(%arg145 : i8):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.zext %arg145 : i8 to i32
  %2 = llvm.add %1, %0 : i32
  %3 = llvm.sext %2 : i32 to i64
  "llvm.return"(%3) : (i64) -> ()
}
]

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) -> ()
}
]

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 uadd_sat_canon_nuw_after := [llvm|
{
^0(%arg31 : i32, %arg32 : i32):
  %0 = llvm.add %arg31, %arg32 overflow<nuw> : i32
  "llvm.return"(%0) : (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 irc_constants_AMinusC1PlusC2_1_1 : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%a: i64):
      %c1 = llvm.mlir.constant (1) : i64
      %c2 = llvm.mlir.constant (1) : i64
      %0 = llvm.sub %a, %c1 : i64
      %1 = llvm.add %0, %c2 : i64
      llvm.return %1 : i64
  }]
  rhs := [LV| {
    ^entry (%a: i64):
      %c1 = llvm.mlir.constant (1) : i64
      %c2 = llvm.mlir.constant (1) : i64
      %0 = llvm.sub %c2, %c1 : i64
      %1 = llvm.add %a, %0 : i64
      llvm.return %1 : i64
  }]

|

Neg in Init.Prelude

pure res
</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
AList.lookup_isSome in Mathlib.Data.List.AList
Finset.mem_singleton in Mathlib.Data.Finset.Insert
Option.mem_def in Init.Data.Option.Instances
Sigma.mk.inj_iff in Mathlib.Data.Sigma.Basic
and_imp 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
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

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

@[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

theorem sgt_positive_multip_rem_nz_thm (e : IntW 8) :
  icmp IntPred.sgt (mul e (const? 8 5) { «nsw» := true, «nuw» := false }) (const? 8 21) ⊑
    icmp IntPred.sgt e (const? 8 4)

theorem both_sides_fold_eq_proof : both_sides_fold_eq_before ⊑ both_sides_fold_eq_after

theorem xor_signbit_select_lshr_thm (e : IntW 32) (e_1 : IntW 1) :
  lshr (select e_1 (LLVM.xor e (const? 32 (-65536))) e) (const? 32 8) ⊑
    select e_1 (LLVM.xor (lshr e (const? 32 8)) (const? 32 16776960)) (lshr e (const? 32 8))

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

theorem icmp_slt_0_or_icmp_sgt_0_i32_proof : icmp_slt_0_or_icmp_sgt_0_i32_before ⊑ icmp_slt_0_or_icmp_sgt_0_i32_after

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 test23_proof : test23_before ⊑ test23_after

theorem demorgan_and_apint1_proof : demorgan_and_apint1_before ⊑ demorgan_and_apint1_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 lowmask_or_zext_commute_proof : lowmask_or_zext_commute_before ⊑ lowmask_or_zext_commute_after

theorem e_49 :
    11 * (x |||  ~~~y) + 2 * x - 12 *  ~~~(x ||| y) - 13 * (x &&&  ~~~y) - 14 * (x &&& y) =  - 1 *  ~~~(x ^^^ y)

theorem t1_flags_nuw_nsw_first_thm (e e_1 e_2 : IntW 8) :
  sub (sub e_2 e_1 { «nsw» := true, «nuw» := true }) e ⊑ sub e_2 (add e_1 e)

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

theorem and_to_xor1_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), (x_1 ||| x) &&& (x_1 &&& x ^^^ -1#32) = x_1 ^^^ x

theorem sgt_or_not_min_commute_logical_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 != BitVec.ofInt 8 (-128)) = 1#1 → 1#1 = ofBool (x_1 != BitVec.ofInt 8 (-128))

theorem test14_thm.extracted_1._1 : ∀ (x : BitVec 8), ofBool (x &&& BitVec.ofInt 8 (-128) != 0#8) = ofBool (x <ₛ 0#8)

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 ashr_and_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬(x ≥ ↑8 ∨ x + 1#8 ≥ ↑8) →
    ¬x ≥ ↑8 →
      (BitVec.ofInt 8 (-64)).sshiftRight' x &&& (BitVec.ofInt 8 (-128)).sshiftRight' (x + 1#8) =
        (BitVec.ofInt 8 (-64)).sshiftRight' x

theorem test_logical_proof : test_logical_before ⊑ test_logical_after

theorem src_srem_shl_demand_min_signbit_proof : src_srem_shl_demand_min_signbit_before ⊑ src_srem_shl_demand_min_signbit_after

theorem lshrult_01_12_exact_proof : lshrult_01_12_exact_before ⊑ lshrult_01_12_exact_after

theorem xor_or2_proof : xor_or2_before ⊑ xor_or2_after

theorem fold_icmp_shl_nuw_c2_non_pow2_proof : fold_icmp_shl_nuw_c2_non_pow2_before ⊑ fold_icmp_shl_nuw_c2_non_pow2_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 xor_and_logic_or1_thm.extracted_1._3 : ∀ (x x_1 x_2 : BitVec 1), ¬x_2 = 1#1 → x_2 &&& x_1 ^^^ x = x

theorem t0_commutative_thm.extracted_1._7 : ∀ (x x_1 x_2 : BitVec 8),
  ¬ofBool (x_2 == x_1) = 1#1 → ¬ofBool (x_2 != x_1) = 1#1 → ¬0#1 = 1#1 → False

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 logical_or_not_proof : logical_or_not_before ⊑ logical_or_not_after

theorem uge_to_sgt_proof : uge_to_sgt_before ⊑ uge_to_sgt_after

theorem test69_xor_proof : test69_xor_before ⊑ test69_xor_after

@[simp] theorem cons_getElem_toCons (x : A a) (v : Var Γ u)
    (h : as = Γ.toList := by rfl) (h' : a :: as = (Γ.cons a).toList := by rfl) :
    (HVector.cons x xs)[v.toCons (t' := a)]'h' = xs[v]'h

theorem test46_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬8#32 ≥ ↑32 → 8#32 ≥ ↑32 ∨ True ∧ (truncate 32 x <<< 8#32 &&& 10752#32).msb = true → False

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

theorem eq_commuted_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬(x == 0 || 8 != 1 && 43#8 == intMin 8 && x == -1) = true →
    ofBool (x_1 == 0#8) ||

theorem add_select_sext_thm (e : IntW 1) :
  add (select e (const? 64 64) (const? 64 1)) (sext 64 e) ⊑ select e (const? 64 63) (const? 64 1)

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

theorem different_size_zext_zext_eq_thm.extracted_1._1 : ∀ (x : BitVec 7) (x_1 : BitVec 4),
  ofBool (zeroExtend 25 x_1 == zeroExtend 25 x) = ofBool (x == zeroExtend 7 x_1)

theorem e_2224 :
     - 7 *  ~~~( ~~~d &&& ( ~~~e &&& f)) + 5 * ((d |||  ~~~e) &&& (d ^^^ (e ^^^ f))) + 5 *  ~~~(d ^^^ e) - 2 *  ~~~(d ^^^ ( ~~~e ||| f)) - 11 * (e ^^^  ~~~( ~~~d &&& (e ||| f))) - 6 * (e ^^^  ~~~(d ||| f)) - 5 * (d ^^^ ( ~~~e &&& f)) + 7 *  ~~~(d ^^^ ( ~~~e &&& f)) + 1 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) + 5 * (d ^^^ f) - 3 * ((d &&& e) |||  ~~~(e ||| f)) + 5 * (f ^^^  ~~~(d &&&  ~~~e)) + 2 *  ~~~(d ^^^ (e ||| f)) - 1 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) - 6 * (f ^^^ ( ~~~d &&& (e ||| f))) + 7 * (d &&& ( ~~~e ||| f)) + 1 * (d &&&  ~~~f) + 1 *  ~~~(d |||  ~~~f) + 4 * ((d &&& e) ||| (d ^^^ (e ^^^ f))) - 11 *  ~~~( ~~~d ||| ( ~~~e &&& f)) + 1 * (e &&&  ~~~(d ^^^ f)) - 1 * (f ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) + 1 * (d ^^^ (e &&& f)) + 11 * ( ~~~(d |||  ~~~e) ||| (e ^^^ f)) - 7 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) + 3 * (e ^^^  ~~~( ~~~d &&& (e ^^^ f))) - 2 * (e ^^^ (d &&& (e ||| f))) + 2 * ((d &&& f) ^^^ (e ||| f)) + 4 * ((d &&& e) |||  ~~~(e ^^^ f)) - 1 * f + 2 * ((d ^^^ e) &&&  ~~~(d ^^^ f)) + 2 *  ~~~(d ||| f) - 1 * d - 1 *  ~~~(d &&& e) + 5 * ( ~~~e |||  ~~~(d ^^^ f)) + 2 * (f ^^^  ~~~(d |||  ~~~e)) - 1 * e + 1 * (d ||| ( ~~~e &&& f)) - 1 * (e ^^^  ~~~(d &&& (e ^^^ f))) - 5 * ((d &&& f) ^^^ (d ^^^ (e &&& f))) - 6 * (e |||  ~~~(d ^^^ f)) + 7 * (e ^^^ (d &&& f)) - 1 * (d &&& e) - 2 * ( ~~~e &&&  ~~~(d ^^^ f)) + 1 * (d ||| (e ^^^ f)) + 3 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) + 10 *  ~~~(d ||| (e ||| f)) - 11 *  ~~~(d ||| ( ~~~e ||| f)) + 8 *  ~~~( ~~~d ||| (e ||| f)) + 12 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 27 * ( ~~~d &&& ( ~~~e &&& f)) + 6 * ( ~~~d &&& (e &&& f)) - 2 * (d &&& ( ~~~e &&& f)) + 30 * (d &&& (e &&& f)) = 1 * (e ^^^ (d &&& ( ~~~e ||| f))) + 5 * (f ||| (d &&& e))

theorem positive_biggerlshr_shlnsw_lshrexact_thm (e : IntW 8) :
  shl (lshr e (const? 8 6) { «exact» := true }) (const? 8 3) { «nsw» := true, «nuw» := false } ⊑
    lshr e (const? 8 3) { «exact» := true }

theorem src_x_or_mask_ne_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 1),
  ¬x_1 = 1#1 → ofBool (0#8 ||| x ^^^ -1#8 != -1#8) = ofBool (0#8 <ᵤ x)

theorem e_1943 :
    5 * (b |||  ~~~(a ^^^ c)) - 11 * ((a &&& b) ^^^ (b ||| c)) - 2 * (b ^^^  ~~~( ~~~a ||| (b ^^^ c))) + 4 * ( ~~~(a &&&  ~~~b) &&& (b ^^^ c)) + 1 *  ~~~(b &&&  ~~~c) + 1 *  ~~~(a ^^^ b) - 1 *  ~~~(a ||| (b &&& c)) + 1 * (c ^^^  ~~~(a &&& (b &&& c))) - 2 *  ~~~(a &&&  ~~~b) - 7 *  ~~~(a &&& c) + 7 * (c ^^^ (a ||| b)) + 3 * (b ^^^ (a &&& c)) - 1 * (a |||  ~~~b) - 7 * (b ||| (a &&&  ~~~c)) + 5 * (b ^^^ (a ||| (b ||| c))) - 2 * (c ^^^  ~~~(a ||| (b &&& c))) + 1 * (a ^^^ (b ^^^ c)) + 11 * ((a ^^^ b) &&&  ~~~(a ^^^ c)) + 4 * (c ^^^  ~~~( ~~~a &&& (b ||| c))) - 6 * (c ^^^ ( ~~~a ||| (b ||| c))) + 2 * ((a ^^^ b) |||  ~~~(a ^^^ c)) + 2 * ( ~~~(a |||  ~~~b) |||  ~~~(b ^^^ c)) + 7 * ((a ||| b) &&&  ~~~(a ^^^ (b ^^^ c))) + 11 * ( ~~~c &&&  ~~~(a ^^^ b)) - 2 * ((b &&&  ~~~c) |||  ~~~( ~~~a ||| ( ~~~b &&& c))) - 2 * ( ~~~b &&&  ~~~(a ^^^ c)) - 2 * (c ^^^  ~~~(a &&& b)) + 1 *  ~~~a + 3 * (b ^^^ ( ~~~a &&& (b ||| c))) + 4 * (b ^^^  ~~~( ~~~a &&& (b ^^^ c))) + 7 * (b ^^^ ( ~~~a &&& ( ~~~b ||| c))) + 7 *  ~~~(a &&& (b &&& c)) - 1 * (c &&& (a ^^^ b)) - 2 * (c ^^^  ~~~(a |||  ~~~b)) - 3 * (c ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) + 2 * ((a &&& b) |||  ~~~(b ||| c)) - 1 *  ~~~(b &&& c) - 1 * ((a &&& b) ||| (a ^^^ (b ^^^ c))) + 3 * (c ^^^ (a ||| (b &&& c))) + 1 * ( ~~~a ||| (b &&& c)) + 1 * ((a &&& b) |||  ~~~(b |||  ~~~c)) - 2 * (c ^^^ (a &&& b)) + 7 * ((a ^^^ b) ||| (a ^^^ c)) - 1 * ((a &&&  ~~~b) ||| (b ^^^ c)) - 1 * ((a &&& b) ^^^ (b |||  ~~~c)) + 5 * (b ^^^ (a ||| c)) - 25 *  ~~~(a ||| (b ||| c)) - 21 *  ~~~(a ||| ( ~~~b ||| c)) - 23 *  ~~~( ~~~a ||| (b ||| c)) - 38 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 26 * ( ~~~a &&& ( ~~~b &&& c)) - 35 * (a &&& ( ~~~b &&& c)) - 8 * (a &&& (b &&& c)) =  - 4 *  ~~~(a ||| ( ~~~b &&& c)) + 9 * ( ~~~a &&& (b &&& c))

theorem positive_biggershl_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬(3#8 ≥ ↑8 ∨ 6#8 ≥ ↑8) → ¬3#8 ≥ ↑8 → x >>> 3#8 <<< 6#8 = x <<< 3#8 &&& BitVec.ofInt 8 (-64)

theorem and_or2_commuted_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1),
  ¬x_1 &&& (x ^^^ 1#1) = 1#1 → x_1 = 1#1 → ¬x = 1#1 → False

theorem slt_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬(31#32 ≥ ↑32 ∨ 32#64 ≥ ↑64) →
    31#32 ≥ ↑32 ∨ 32#64 ≥ ↑64 ∨ True ∧ zeroExtend 64 (truncate 32 (x >>> 32#64)) ≠ x >>> 32#64 → False

theorem ashr_ne_exact_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ x >>> 3#8 <<< 3#8 ≠ x ∨ 3#8 ≥ ↑8) → ofBool (x.sshiftRight' 3#8 != 10#8) = ofBool (x != 80#8)

theorem lshrult_01_03_exact_thm (e : IntW 4) :
  icmp IntPred.ult (lshr e (const? 4 1) { «exact» := true }) (const? 4 3) ⊑
    icmp IntPred.ult e (const? 4 6)

theorem AvoidCollision_toNat_setWidth_of_le {w w' : Nat} {b : BitVec w} (h : w ≤ w') : (b.setWidth w').toNat = b.toNat

theorem mul_x_selectp2_thm (e : IntW 1) (e_1 : IntW 8) :
  mul (mul e_1 e_1) (select e (const? 8 8) (const? 8 1)) ⊑
    shl (mul e_1 e_1) (select e (const? 8 3) (const? 8 0))

theorem e_2140 :
    1 * (f ^^^  ~~~(d ||| (e &&& f))) + 1 * ((d &&&  ~~~e) ||| (e ^^^ f)) - 5 * (d ||| ( ~~~e &&& f)) + 1 * (e ||| (d &&&  ~~~f)) - 7 * (d &&& (e ||| f)) - 1 * ((d &&& e) ||| (e ^^^ f)) - 7 *  ~~~(d &&& (e ||| f)) + 7 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) - 2 * ( ~~~(d &&& e) &&&  ~~~(e ^^^ f)) - 5 *  ~~~(d ||| e) + 1 *  ~~~(d ^^^ (e ^^^ f)) + 2 * (f ^^^ (d ||| ( ~~~e &&& f))) + 1 * (e ||| f) + 1 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f)) - 6 *  ~~~(d &&&  ~~~f) - 5 * ( ~~~d &&& (e ||| f)) - 2 * ( ~~~f |||  ~~~(d ^^^ e)) + 2 * (e ^^^ ( ~~~d &&& (e ||| f))) + 2 * (f ^^^ (d ||| e)) - 1 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 2 * (e ^^^ (d ||| ( ~~~e &&& f))) - 11 * (f &&&  ~~~(d &&&  ~~~e)) - 6 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 11 * (d &&& (e ^^^ f)) + 11 * (e &&&  ~~~(d &&& f)) - 5 * (e &&& (d ||| f)) + 7 *  ~~~( ~~~d ||| (e &&& f)) + 3 *  ~~~f + 11 * (e ||| (d ^^^ f)) + 3 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) + 5 *  ~~~(d &&& e) + 3 *  ~~~(d ||| f) - 1 * (f &&& (d ||| e)) - 2 * ( ~~~(d &&& e) &&& (d ^^^ (e ^^^ f))) + 3 * ( ~~~(d ^^^ e) |||  ~~~(d ^^^ f)) - 2 * ( ~~~(d |||  ~~~e) ||| (e ^^^ f)) + 1 * (e ^^^ ( ~~~d ||| (e &&& f))) - 1 * ((d &&& f) ^^^ (e ||| f)) + 11 * (f &&&  ~~~(d &&& e)) + 18 *  ~~~(d ||| (e ||| f)) - 19 *  ~~~(d ||| ( ~~~e ||| f)) - 16 *  ~~~( ~~~d ||| (e ||| f)) - 29 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 2 * ( ~~~d &&& ( ~~~e &&& f)) - 9 * ( ~~~d &&& (e &&& f)) - 23 * (d &&& ( ~~~e &&& f)) + 18 * (d &&& (e &&& f)) = 7 * ((e &&& f) ^^^  ~~~( ~~~d &&& (e ^^^ f)))

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 width2 {v w : Nat} (x : BitVec v) :
    x.signExtend (max v (min v w)) = x.zeroExtend (max v (min v w))

theorem masked_icmps_mask_notallzeros_bmask_mixed_1_logical_proof : masked_icmps_mask_notallzeros_bmask_mixed_1_logical_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_1_logical_after

theorem positive_biggerlshr_shlnuwnsw_lshrexact_proof : positive_biggerlshr_shlnuwnsw_lshrexact_before ⊑ positive_biggerlshr_shlnuwnsw_lshrexact_after

theorem ashrslt_02_13_exact_thm (e : IntW 4) :
  icmp IntPred.slt (ashr e (const? 4 2) { «exact» := true }) (const? 4 (-3)) ⊑ const? 1 0

theorem icmp_select_implied_cond_thm (e e_1 : IntW 8) :
  icmp IntPred.eq (select (icmp IntPred.eq e_1 (const? 8 0)) (const? 8 0) e) e_1 ⊑
    select (icmp IntPred.eq e_1 (const? 8 0)) (const? 1 1) (icmp IntPred.eq e e_1)

theorem test1_trunc_proof : test1_trunc_before ⊑ test1_trunc_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 mul_of_bool_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 32),
  ofBool (255#32 <ᵤ (x_1 &&& 1#32) * zeroExtend 32 x) = 0#1

theorem negative_trunc_not_arg_logical_thm (e e_1 : IntW 32) :
  select (icmp IntPred.sgt (trunc 8 e_1) (const? 8 (-1)))
      (icmp IntPred.ult (add e (const? 32 128)) (const? 32 256)) (const? 1 0) ⊑
    select (icmp IntPred.eq (LLVM.and e_1 (const? 32 128)) (const? 32 0))
      (icmp IntPred.ult (add e (const? 32 128)) (const? 32 256)) (const? 1 0)

theorem n2_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(BitVec.ofInt 8 (-128) == 0 || 8 != 1 && x == intMin 8 && BitVec.ofInt 8 (-128) == -1) = true →
    x.sdiv (BitVec.ofInt 8 (-128)) = zeroExtend 8 (ofBool (x == BitVec.ofInt 8 (-128)))

theorem shl_nsw_add_nuw_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(True ∧ (1#32 <<< x).sshiftRight' x ≠ 1#32 ∨ x ≥ ↑32 ∨ True ∧ (1#32 <<< x).uaddOverflow (-1#32) = true) →
    1#32 <<< x + -1#32 = -1#32

theorem neg_mask1_lshr_proof : neg_mask1_lshr_before ⊑ neg_mask1_lshr_after

omit [Fintype S] [LawfulBEq A] in
lemma addOrCreate_preserves_map (st : worklist.St A S) (final? : Bool) (sa sa' : S) :
    let (_, st') := st.addOrCreateState _ _  final? sa'
    st.map[sa]? = some s →
    st'.map[sa]? = some s

theorem shl_nsw_add_negative_proof : shl_nsw_add_negative_before ⊑ shl_nsw_add_negative_after

theorem test40_proof : test40_before ⊑ test40_after

theorem ashr_x_by_const_cmp_sge_x_thm (e : IntW 32) :
  icmp IntPred.sge (ashr e (const? 32 5)) e ⊑ icmp IntPred.slt e (const? 32 1)

theorem substitute_constant_or_ne_swap_sle_proof : substitute_constant_or_ne_swap_sle_before ⊑ substitute_constant_or_ne_swap_sle_after
</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_matchVar {Δ_out}
    {varMap : Mapping Δ_in Γ_out} {ma : Mapping Δ_in Γ_out}
    {lets : Lets d Γ_in eff Γ_out} {v : Var Γ_out t} /- : -/
    {matchLets : Lets d Δ_in .pure Δ_out}  {w : Var Δ_out t}
    (hvarMap : ((), varMap) ∈ matchVar lets v matchLets w ma)
    {t': _ } {v' : _}
    (hMatchLets : ⟨t', v'⟩ ∈ matchLets.vars w) :
  ⟨t', v'⟩ ∈ varMap :=
</target_theorem>

