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
Sigma in Init.Core
Sigma.mk in Init.Core
liftM in Init.Prelude
Iff in Init.Core
IsEmpty in Mathlib.Logic.IsEmpty

syntax "neg" : MLIR.Pretty.uniform_op

macro_rules
  | `(mlir_op| $res:mlir_op_operand = const ($x)
      $[: $outer_type]? ) => do
      let outer_type ← outer_type.getDM `(mlir_type| _)
      `(mlir_op| $res:mlir_op_operand = "const"()
          {val = $x:num : $outer_type} : ($outer_type) -> ($outer_type) )

macro_rules
  | `(mlir_op| $res:mlir_op_operand = li ($x)
     $[: $outer_type]?  ) => do
      let outer_type ← outer_type.getDM `(mlir_type| _ )
      `(mlir_op| $res:mlir_op_operand = "li"()
          {imm = $x:num : $outer_type } : ($outer_type) -> ($outer_type))

macro_rules
| `(mlir_op| $res:mlir_op_operand = $op1:MLIR.Pretty.RV.opWithImmediate $reg1 , $x : $t)  => do
    let some opName := MLIR.EDSL.Pretty.extractOpName op1.raw
      | Macro.throwUnsupported
    `(mlir_op| $res:mlir_op_operand = $opName ($reg1) {imm = $x:num : $t} : ($t) -> ($t) )

macro_rules
| `(mlir_op| $res:mlir_op_operand = $op1:MLIR.Pretty.RV.opWithShamt $reg1 , $x  : $t )  => do
    let some opName := MLIR.EDSL.Pretty.extractOpName op1.raw
      | Macro.throwUnsupported
    `(mlir_op| $res:mlir_op_operand = $opName ($reg1) {shamt = $x:num : $t}  : ($t) -> ($t) )

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 appendInl (v : Γ.Var t) : (Γ ++ Δ).Var t :=
  ⟨v.val, by admit /- proof elided -/
  ⟩

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 effectKind   := Signature.effectKind ∘ s.signature

def returnTypes  := Signature.returnTypes ∘ s.signature

def Expr.ty : Expr d Γ eff [t] → d.Ty := fun _ => t

def Expr.op {Γ : Ctxt d.Ty} {eff : EffectKind} {ty} (e : Expr d Γ eff ty) : d.Op :=
  Expr.casesOn e (fun op _ _ _ _ => op)

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

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

def slt_to_ugt_before := [llvm|
{
^0(%arg28 : i8, %arg29 : i8):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.xor %arg28, %0 : i8
  %2 = llvm.xor %arg29, %0 : i8
  %3 = llvm.icmp "slt" %1, %2 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

def no_shift_xor_multiuse_and_before := [llvm|
{
^0(%arg130 : i32, %arg131 : i32):
  %0 = llvm.mlir.constant(4096 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(-4097 : i32) : i32
  %3 = llvm.and %arg130, %0 : i32
  %4 = llvm.icmp "ne" %1, %3 : i32
  %5 = llvm.and %arg131, %2 : i32
  %6 = "llvm.select"(%4, %arg131, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %7 = llvm.mul %6, %5 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

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

let mut res : ExpressionSynthesisResult := Std.HashMap.emptyWithCapacity
  for combo in inputsAndSymVars do
    let inputsSubstitutions := bvExprToSubstitutionValue (Std.HashMap.ofList (List.zip inputVars combo.fst))
    let symVarsSubstitutions := bvExprToSubstitutionValue (Std.HashMap.ofList (List.zip lhsSymVars.keys combo.snd))

@[simp_denote]
def add_shl_sext_llvm := [LV| {
    ^entry (%a: i32):
    %0 = llvm.mlir.constant (3) : i32
    %1 = llvm.add %a, %0 : i32
    %2 = llvm.shl %1, %a : i32
    %3 = llvm.sext %2 : i32 to i64
    llvm.return %3 : i64
  }]

def sgt_smax2_before := [llvm|
{
^0(%arg37 : i32, %arg38 : i32):
  %0 = llvm.icmp "sgt" %arg38, %arg37 : i32
  %1 = "llvm.select"(%0, %arg38, %arg37) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "sgt" %1, %arg37 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def Predicate.evalNeq (t₁ t₂ : BitStream) : BitStream := (t₁.nxor t₂).concat true |>.scanAnd

def lhsSketchEnumeration  (lhsSketch: GenBVExpr w) (inputVars: List Nat) (lhsSymVars rhsSymVars : Std.HashMap Nat BVExpr.PackedBitVec) : ExpressionSynthesisResult := Id.run do
  let zero := wrap (GenBVExpr.const (BitVec.ofNat w 0))
  let one := wrap (GenBVExpr.const (BitVec.ofNat w 1 ))
  let minusOne := wrap (GenBVExpr.const (BitVec.ofInt w (-1)))

def lshrult_01_10_before := [llvm|
{
^0(%arg357 : i4):
  %0 = llvm.mlir.constant(1 : i4) : i4
  %1 = llvm.mlir.constant(-6 : i4) : i4
  %2 = llvm.lshr %arg357, %0 : i4
  %3 = llvm.icmp "ult" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def shl_or_lshr_comm_after := [llvm|
{
^0(%arg106 : i32, %arg107 : i32, %arg108 : i32):
  %0 = llvm.lshr %arg108, %arg107 : i32
  %1 = llvm.or %0, %arg106 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def RawCNFA.newState (m : RawCNFA A) : State × RawCNFA A :=
  let old := m.stateMax
  let m := { m with stateMax := old + 1 }
  (old, m)

def constLLVM31 : Com LLVMPlusRiscV ⟨[]⟩ .pure (.llvm (.bitvec 64)) := [LV| {
  ^entry ():
    %1 = llvm.mlir.constant (31) : i64
    llvm.return %1 : i64
  }]

def ugt_swap_and_not_min_before := [llvm|
{
^0(%arg70 : i8, %arg71 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.icmp "ult" %arg71, %arg70 : i8
  %2 = llvm.icmp "ne" %arg70, %0 : i8
  %3 = llvm.and %1, %2 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def and_zext_zext_after := [llvm|
{
^0(%arg58 : i8, %arg59 : i4):
  %0 = llvm.zext %arg59 : i4 to i8
  %1 = llvm.and %arg58, %0 : i8
  %2 = llvm.zext nneg %1 : i8 to i16
  "llvm.return"(%2) : (i16) -> ()
}
]

def always_false [DecidableEq α] (c : Circuit α) : Bool :=
   nonempty c = false

def mul_mask_pow2_eq0_after := [llvm|
{
^0(%arg25 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.and %arg25, %0 : i8
  %3 = llvm.icmp "eq" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

def test6_before := [llvm|
{
^0(%arg3 : i65):
  %0 = llvm.mlir.constant(1 : i65) : i65
  %1 = llvm.mlir.constant(64 : i65) : i65
  %2 = llvm.shl %0, %1 : i65
  %3 = llvm.xor %arg3, %2 : i65
  %4 = llvm.add %3, %2 : i65
  "llvm.return"(%4) : (i65) -> ()
}
]

def bool_zext_before := [llvm|
{
^0(%arg172 : i1):
  %0 = llvm.mlir.constant(15 : i16) : i16
  %1 = llvm.sext %arg172 : i1 to i16
  %2 = llvm.lshr %1, %0 : i16
  "llvm.return"(%2) : (i16) -> ()
}
]

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

def t7_after := [llvm|
{
^0(%arg209 : i32):
  %0 = llvm.mlir.constant(4 : i32) : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

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

def ashr_ult_exact_before := [llvm|
{
^0(%arg169 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.mlir.constant(10 : i8) : i8
  %2 = llvm.ashr exact %arg169, %0 : i8
  %3 = llvm.icmp "ult" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

LawfulHashable in Init.Data.LawfulHashable

def not_not_cmp_after := [llvm|
{
^0(%arg147 : i32, %arg148 : i32):
  %0 = llvm.icmp "sgt" %arg147, %arg148 : i32
  "llvm.return"(%0) : (i1) -> ()
}
]

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

def test67_after := [llvm|
{
^0(%arg113 : i1, %arg114 : i32):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def trunc_before := [llvm|
{
^0(%arg15 : i32, %arg16 : i32, %arg17 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.icmp "ult" %arg15, %arg16 : i32
  %2 = "llvm.select"(%1, %0, %arg17) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %3 = llvm.trunc %2 : i32 to i16
  "llvm.return"(%3) : (i16) -> ()
}
]

def ripple_nsw4_before := [llvm|
{
^0(%arg17 : i16, %arg18 : i16):
  %0 = llvm.mlir.constant(-21845 : i16) : i16
  %1 = llvm.mlir.constant(21843 : i16) : i16
  %2 = llvm.and %arg18, %0 : i16
  %3 = llvm.and %arg17, %1 : i16
  %4 = llvm.add %3, %2 : i16
  "llvm.return"(%4) : (i16) -> ()
}
]

def ValueStream := Stream

def TokenStream := Stream Unit

def foo_before := [llvm|
{
^0(%arg0 : i8, %arg1 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.mlir.constant(84 : i8) : i8
  %2 = llvm.mlir.constant(-118 : i8) : i8
  %3 = llvm.mlir.constant(33 : i8) : i8
  %4 = llvm.mlir.constant(-88 : i8) : i8
  %5 = llvm.mlir.constant(5 : i8) : i8
  %6 = llvm.shl %arg0, %0 : i8
  %7 = llvm.and %arg1, %1 : i8
  %8 = llvm.and %arg1, %2 : i8
  %9 = llvm.and %arg1, %3 : i8
  %10 = llvm.sub %4, %7 : i8
  %11 = llvm.and %10, %1 : i8
  %12 = llvm.or %9, %11 : i8
  %13 = llvm.xor %6, %8 : i8
  %14 = llvm.or %12, %13 : i8
  %15 = llvm.lshr %13, %0 : i8
  %16 = llvm.shl %15, %5 : i8
  %17 = llvm.xor %16, %14 : i8
  "llvm.return"(%17) : (i8) -> ()
}
]

def product (final? : Bool → Bool → Bool) (m₁ m₂ : CNFA n) : CNFA n :=
  worklistRun (m₁.m.states × m₂.m.states) final (product.inits m₁ m₂)
    (by admit /- proof elided -/
    ) f
where final (ss : m₁.m.states × m₂.m.states) := final? (ss.1 ∈ m₁.m.finals) (ss.2 ∈ m₂.m.finals)
      f (ss : m₁.m.states × m₂.m.states) :=
        let (s1, s2) := ss
        (FinEnum.toList (α := BitVec n)).foldl (init := Array.empty) fun as a =>
          product.prodArray' (λ s₁ s₂ ↦ (a, (s₁, s₂)))
            (fun s' => m₁.wf.trans_tgt_lt (s := s1) (a := a)) (fun s' => m₂.wf.trans_tgt_lt (s := s2) (a := a)) as

Fintype in Mathlib.Data.Fintype.Defs

def or_or_and_pat1_before := [llvm|
{
^0(%arg74 : i8, %arg75 : i8, %arg76 : i8, %arg77 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.udiv %0, %arg76 : i8
  %2 = llvm.and %arg74, %arg75 : i8
  %3 = llvm.and %arg74, %arg77 : i8
  %4 = llvm.or %1, %3 : i8
  %5 = llvm.or %4, %2 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def sub_ult_zext_after := [llvm|
{
^0(%arg161 : i1, %arg162 : i8, %arg163 : i8):
  %0 = llvm.icmp "eq" %arg162, %arg163 : i8
  %1 = llvm.and %0, %arg161 : i1
  "llvm.return"(%1) : (i1) -> ()
}
]

def neg_mask2_lshr_before := [llvm|
{
^0(%arg14 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.mlir.constant(2 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = llvm.lshr %arg14, %0 : i8
  %4 = llvm.and %3, %1 : i8
  %5 = llvm.sub %2, %4 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def ne_smax4_before := [llvm|
{
^0(%arg41 : i32, %arg42 : i32):
  %0 = llvm.mlir.constant(3 : i32) : i32
  %1 = llvm.add %arg41, %0 : i32
  %2 = llvm.icmp "sgt" %arg42, %1 : i32
  %3 = "llvm.select"(%2, %arg42, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %4 = llvm.icmp "ne" %1, %3 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

def no_shift_xor_multiuse_cmp_xor_after := [llvm|
{
^0(%arg44 : i32, %arg45 : i32, %arg46 : i32, %arg47 : i32):
  %0 = llvm.mlir.constant(4096 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.and %arg44, %0 : i32
  %3 = llvm.icmp "eq" %2, %1 : i32
  %4 = llvm.xor %arg45, %0 : i32
  %5 = "llvm.select"(%3, %4, %arg45) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %6 = "llvm.select"(%3, %arg47, %arg46) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %7 = llvm.mul %5, %6 : i32
  %8 = llvm.mul %7, %4 : i32
  "llvm.return"(%8) : (i32) -> ()
}
]

def bitwise_and_logical_and_masked_icmp_allzeros_poison1_before := [llvm|
{
^0(%arg144 : i1, %arg145 : i32, %arg146 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.mlir.constant(7 : i32) : i32
  %3 = llvm.and %arg145, %arg146 : i32
  %4 = llvm.icmp "eq" %3, %0 : i32
  %5 = "llvm.select"(%4, %arg144, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %6 = llvm.and %arg145, %2 : i32
  %7 = llvm.icmp "eq" %6, %0 : i32
  %8 = llvm.and %5, %7 : i1
  "llvm.return"(%8) : (i1) -> ()
}
]

Sum in Init.Core

def ashr_mul_times_3_div_2_exact_2_after := [llvm|
{
^0(%arg17 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.ashr exact %arg17, %0 : i32
  %2 = llvm.add %arg17, %1 overflow<nsw> : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def mul_add_to_mul_3_before := [llvm|
{
^0(%arg30 : i16):
  %0 = llvm.mlir.constant(2 : i16) : i16
  %1 = llvm.mlir.constant(3 : i16) : i16
  %2 = llvm.mul %arg30, %0 : i16
  %3 = llvm.mul %arg30, %1 : i16
  %4 = llvm.add %2, %3 overflow<nsw> : i16
  "llvm.return"(%4) : (i16) -> ()
}
]

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

def and_or_not_not_commute4_after := [llvm|
{
^0(%arg363 : i32, %arg364 : i32, %arg365 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.or %arg365, %arg364 : i32
  %2 = llvm.and %1, %arg363 : i32
  %3 = llvm.xor %2, %0 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def nonexact_lshr_ne_noexactlog_before := [llvm|
{
^0(%arg135 : i8):
  %0 = llvm.mlir.constant(90 : i8) : i8
  %1 = llvm.mlir.constant(30 : i8) : i8
  %2 = llvm.lshr %0, %arg135 : i8
  %3 = llvm.icmp "ne" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

def icmp_ne_riscv_eq_icmp_ne_llvm_64_pseudo : LLVMPeepholeRewriteRefine 1 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] :=
  {lhs:= icmp_neq_llvm_64, rhs:= icmp_ne_riscv_64_pseudo}

def dec_inj {n : Nat} : Function.Injective (dec (n := n)) :=

def or_not_and_before := [llvm|
{
^0(%arg537 : i32, %arg538 : i32, %arg539 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.or %arg537, %arg538 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.and %2, %arg539 : i32
  %4 = llvm.or %arg537, %arg539 : i32
  %5 = llvm.xor %4, %0 : i32
  %6 = llvm.and %5, %arg538 : i32
  %7 = llvm.or %3, %6 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

let mut allInputs : Std.HashMap (FpExpr w)  PreconditionSynthesisCacheValue := Std.HashMap.emptyWithCapacity
    for key in positiveExamplesByKey.keys do
      allInputs := allInputs.insert key {positiveExampleValues := positiveExamplesByKey[key]!, negativeExampleValues := negativeExamplesByKey[key]!}

def masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_3b_logical_before := [llvm|
{
^0(%arg19 : i32):
  %0 = llvm.mlir.constant(15 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(3 : i32) : i32
  %3 = llvm.mlir.constant(true) : i1
  %4 = llvm.and %arg19, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.and %arg19, %2 : i32
  %7 = llvm.icmp "ne" %6, %1 : i32
  %8 = "llvm.select"(%7, %3, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%8) : (i1) -> ()
}
]

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

def sub_ashr_and_i32_after := [llvm|
{
^0(%arg27 : i32, %arg28 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "slt" %arg28, %arg27 : i32
  %2 = "llvm.select"(%1, %arg27, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def test_zext4_after := [llvm|
{
^0(%arg35 : i1, %arg36 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.xor %arg36, %0 : i1
  %2 = "llvm.select"(%1, %0, %arg35) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = llvm.zext %2 : i1 to i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

match safety with
  | DefinitionSafety.unsafe  => m := m ++ "unsafe "
  | DefinitionSafety.partial => m := m ++ "partial "
  | DefinitionSafety.safe    => pure ()

def printParsedFpExprState (s: ParsedInputState) :=
    s!"ParsedFpExprState:\n" ++
    s!"  maxFreeVarId: {s.maxFreeVarId}\n" ++
    s!"  numSymVars: {s.numSymVars}\n" ++
    s!"  displayNameToVariable: {s.displayNameToVariable}\n" ++
    s!"  BVExprIdToFreeVar: {s.inputVarIdToVariable}\n" ++
    s!"  symVarToVal: {s.symVarToVal}" ++
    s!"  symVarToDisplayName: {s.symVarIdToVariable}"

def tryFactorization_xor_lshr_ashr_after := [llvm|
{
^0(%arg39 : i32):
  %0 = llvm.mlir.constant(-8 : i32) : i32
  %1 = llvm.ashr %0, %arg39 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def n4_after := [llvm|
{
^0(%arg36 : i32, %arg37 : i32):
  %0 = llvm.mlir.constant(32 : i32) : i32
  %1 = llvm.mlir.constant(-16 : i32) : i32
  %2 = llvm.mlir.constant(262143) : i64
  %3 = llvm.mlir.constant(0 : i32) : i32
  %4 = llvm.sub %0, %arg37 : i32
  %5 = llvm.shl %arg36, %4 : i32
  %6 = llvm.add %arg37, %1 : i32
  %7 = llvm.zext nneg %6 : i32 to i64
  %8 = llvm.lshr %2, %7 : i64
  %9 = llvm.trunc %8 overflow<nsw,nuw> : i64 to i32
  %10 = llvm.and %5, %9 : i32
  %11 = llvm.icmp "ne" %10, %3 : i32
  "llvm.return"(%11) : (i1) -> ()
}
]

Lean.Core.State in Lean.CoreM

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

def test1_after := [llvm|
{
^0(%arg19 : i32, %arg20 : i8):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.zext nneg %arg20 : i8 to i32
  %2 = llvm.lshr %arg19, %1 : i32
  %3 = llvm.and %2, %0 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def ashr_ule_exact_after := [llvm|
{
^0(%arg168 : i8):
  %0 = llvm.mlir.constant(88 : i8) : i8
  %1 = llvm.icmp "ult" %arg168, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def nonexact_ashr_eq_noexactdiv_after := [llvm|
{
^0(%arg138 : i8):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

@[simp_denote]
def andi_riscv_i64 :=
  [LV| {
    ^entry (%arg: i64):
    %a = "builtin.unrealized_conversion_cast" (%arg) : (i64) -> (!i64)
    %0 = andi %a, 6 : !i64
    %1 = "builtin.unrealized_conversion_cast" (%0) : (!i64) -> (i64)
    llvm.return %1 : i64
  }]

def select2_before := [llvm|
{
^0(%arg9 : i1, %arg10 : i8, %arg11 : i8, %arg12 : i8):
  %0 = llvm.zext %arg10 : i8 to i32
  %1 = llvm.zext %arg11 : i8 to i32
  %2 = llvm.zext %arg12 : i8 to i32
  %3 = llvm.add %0, %1 : i32
  %4 = "llvm.select"(%arg9, %2, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %5 = llvm.trunc %4 : i32 to i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def positive_biggershl_after := [llvm|
{
^0(%arg59 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.mlir.constant(-64 : i8) : i8
  %2 = llvm.shl %arg59, %0 : i8
  %3 = llvm.and %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def test_before := [llvm|
{
^0(%arg0 : i31):
  %0 = llvm.mlir.constant(16384 : i32) : i32
  %1 = llvm.mlir.constant(15 : i32) : i32
  %2 = llvm.sext %arg0 : i31 to i32
  %3 = llvm.add %2, %0 : i32
  %4 = llvm.lshr %3, %1 : i32
  %5 = llvm.trunc %4 : i32 to i16
  "llvm.return"(%5) : (i16) -> ()
}
]

def shl_add_nsw_nuw_before := [llvm|
{
^0(%arg23 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.shl %0, %arg23 : i32
  %3 = llvm.add %2, %1 overflow<nsw,nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def test_negative_nsw_and_unsigned_pred_after := [llvm|
{
^0(%arg52 : i64):
  %0 = llvm.mlir.constant(-8) : i64
  %1 = llvm.mlir.constant(3) : i64
  %2 = llvm.add %arg52, %0 : i64
  %3 = llvm.icmp "ult" %2, %1 : i64
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

def test15a_after := [llvm|
{
^0(%arg27 : i32):
  %0 = llvm.mlir.constant(16 : i32) : i32
  %1 = llvm.and %arg27, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def not_or_or_and_not_and_and_commute4_after := [llvm|
{
^0(%arg184 : i32, %arg185 : i32, %arg186 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sdiv %0, %arg186 : i32
  %3 = llvm.xor %arg184, %1 : i32
  %4 = llvm.xor %2, %arg185 : i32
  %5 = llvm.or %4, %3 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

return allInputs
</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.get_some in Init.Data.Option.Basic
Option.isSome_iff_exists in Init.Data.Option.Lemmas
forall_exists_index in Init.PropLemmas

theorem eq.ty_eq {v : Γ.Var t} {w : Γ.Var u} (h : v.eq w) : t = u

@[simp]
theorem Expr.op_mk {Γ : Ctxt d.Ty} {ty} {eff : EffectKind} (op : d.Op)
    (ty_eq : ty = DialectSignature.returnTypes op)
    (eff_le : DialectSignature.effectKind op ≤ eff)
    (args : HVector (Var Γ) (DialectSignature.sig op))
    (regArgs) :
    (Expr.mk op ty_eq eff_le args regArgs).op = op

@[simp]
theorem Expr.regArgs_mk {Γ : Ctxt d.Ty} {ty eff op}
    (ty_eq : ty = DialectSignature.returnTypes op)
    (eff_le : DialectSignature.effectKind op ≤ eff)
    (args : HVector (Var Γ) (DialectSignature.sig op)) (regArgs) :
    (Expr.mk op ty_eq eff_le args regArgs).regArgs = regArgs

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

@[simp]
theorem Expr.args_mk {Γ : Ctxt d.Ty} {ty eff op}
    (ty_eq : ty = DialectSignature.returnTypes op)
    (eff_le : DialectSignature.effectKind op ≤ eff)
    (args : HVector (Var Γ) (DialectSignature.sig op)) (regArgs) :
    (Expr.mk op ty_eq eff_le args regArgs).args = args

theorem neg_not_signbit1_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬7#8 ≥ ↑8 → 1#32 - zeroExtend 32 (x >>> 7#8) = zeroExtend 32 (ofBool (-1#8 <ₛ x))

theorem test1_proof : test1_before ⊑ test1_after

theorem ashr_16_to_64_add_zext_basic_proof : ashr_16_to_64_add_zext_basic_before ⊑ ashr_16_to_64_add_zext_basic_after

theorem add_select_not_sext_proof : add_select_not_sext_before ⊑ add_select_not_sext_after

theorem e_684 :
     - 2 *  ~~~x + 2 * (x ||| y) + 5 * y + 1 * (x |||  ~~~y) - 1 * (x ^^^ y) - 2 *  ~~~y - 7 * x + 3 *  ~~~(x &&& y) + 4 * (x &&&  ~~~y) - 1 * (x &&& y) = 7 *  ~~~(x |||  ~~~y)

theorem zext_ult_zext_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 8),
  ofBool (zeroExtend 16 (x_1 * x_1) <ᵤ zeroExtend 16 x) = ofBool (x_1 * x_1 == 0#8) &&& x

theorem imp1 (w : Nat) (a b : BitVec w) : (a < b) → (a ≠ b)

theorem lshrult_01_09_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬1#4 ≥ ↑4 → ofBool (x >>> 1#4 <ᵤ BitVec.ofInt 4 (-7)) = 1#1

theorem exact_lshr_eq_opposite_msb_proof : exact_lshr_eq_opposite_msb_before ⊑ exact_lshr_eq_opposite_msb_after

theorem test1_thm.extracted_1._1 : ∀ (x x_1 : BitVec 33),
  ofBool (x_1 &&& 65280#33 != x &&& 65280#33) = ofBool ((x_1 ^^^ x) &&& 65280#33 != 0#33)

@[simp]
lemma BitVec.cons_inj : cons b1 bv1 = cons b2 bv2 ↔ (b1 = b2) ∧ bv1 = bv2

theorem lshrugt_03_11_exact_thm (e : IntW 4) :
  icmp IntPred.ugt (lshr e (const? 4 3) { «exact» := true }) (const? 4 (-5)) ⊑ const? 1 0

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

theorem test_shl_nsw__nuw_is_safe_thm.extracted_1._1 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ofBool (x_1 &&& 1073741822#32 == 0#32) = 1#1 →
    2#32 ≥ ↑32 ∨
        True ∧ (x_1 <<< 2#32 &&& BitVec.ofInt 32 (-8)).msb = true ∨
          zeroExtend 64 (x_1 <<< 2#32 &&& BitVec.ofInt 32 (-8)) ≥ ↑64 →
      False

theorem t0_proof : t0_before ⊑ t0_after

lemma simul_equiv {m : CNFA n} {M : NFA' n} :
    m.Sim M → m.toNFA'.M.Bisim M.M

theorem select_icmp_ne_0_and_8_or_1073741824_thm.extracted_1._2 : ∀ (x : BitVec 32) (x_1 : BitVec 8),
  ¬ofBool (0#8 != x_1 &&& 8#8) = 1#1 → ¬ofBool (x_1 &&& 8#8 == 0#8) = 1#1 → x ||

theorem bv_AndOrXor_794 :
    ∀ (e e_1 : LLVM.IntW w),
      LLVM.and (LLVM.icmp LLVM.IntPred.sgt e e_1) (LLVM.icmp LLVM.IntPred.ne e e_1) ⊑ LLVM.icmp LLVM.IntPred.sgt e e_1

theorem t7_ugt_sgt_neg1_thm.extracted_1._15 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (65535#32 <ᵤ x_2) = 1#1 → ¬ofBool (65535#32 <ₛ x_2) = 1#1 → ofBool (x_2 <ₛ 0#32) = 1#1 → x_2 = x

theorem test2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 1), x_1 &&& x &&& x_1 = x_1 &&& x

theorem substitute_constant_and_eq_ugt_swap_logical_proof : substitute_constant_and_eq_ugt_swap_logical_before ⊑ substitute_constant_and_eq_ugt_swap_logical_after

theorem e_1528 :
     - 1 * ((a &&& c) ||| (b &&&  ~~~c)) - 11 *  ~~~(a &&&  ~~~c) - 5 * ( ~~~(a ||| b) ||| (a ^^^ (b ^^^ c))) + 5 *  ~~~(a ||| (b ||| c)) + 19 *  ~~~(a ||| ( ~~~b ||| c)) - 4 *  ~~~( ~~~a ||| (b ||| c)) - 10 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 5 * ( ~~~a &&& ( ~~~b &&& c)) + 2 * ( ~~~a &&& (b &&& c)) + 12 * (a &&& ( ~~~b &&& c)) + 6 * (a &&& (b &&& c)) =  - 11 * ( ~~~(a ^^^ b) ||| (a ^^^ c)) + 2 * (b ^^^  ~~~( ~~~a ||| ( ~~~b &&& c)))

theorem bools_logical_commute0_thm.extracted_1._2 : ∀ (x : BitVec 1), ¬x ^^^ 1#1 = 1#1 → ¬x = 1#1 → 0#1 = 1#1 → False

theorem main7a_logical_thm.extracted_1._9 : ∀ (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 → 0#1 = 1#1 → 0#32 = zeroExtend 32 1#1

theorem test_or_eq_a_b_commuted_proof : test_or_eq_a_b_commuted_before ⊑ test_or_eq_a_b_commuted_after

theorem positive_samevar_proof : positive_samevar_before ⊑ positive_samevar_after

theorem a_thm.extracted_1._3 : ∀ (x x_1 : BitVec 1),
  ¬x_1 = 1#1 → True ∧ (1#32).saddOverflow (signExtend 32 x) = true → False

theorem Holor.reindex_functorial
  (ix : HolorIndex ds₂ → HolorIndex ds₁) (iy : HolorIndex ds₃ → HolorIndex ds₂)
  (h : Holor α ds₁) : Holor.reindex iy (Holor.reindex ix h) = Holor.reindex (ix ∘ iy) h

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 e_1301 :
    4 * (z |||  ~~~t) - 1 *  ~~~z + 1 *  ~~~(z &&& t) + 11 *  ~~~t - 3 *  ~~~(z ^^^ t) - 10 *  ~~~(z ||| t) + 2 *  ~~~(z |||  ~~~t) - 14 * (z &&&  ~~~t) + 1 * (z &&& t) = 2 *  ~~~(z &&&  ~~~z)

theorem trunc_proof : trunc_before ⊑ trunc_after

theorem test31 (w : Nat) (x : BitVec w) : x &&& x = x

theorem xor_or_xor_common_op_commute3_proof : xor_or_xor_common_op_commute3_before ⊑ xor_or_xor_common_op_commute3_after

theorem urem_common_divisor_defined_cond_proof : urem_common_divisor_defined_cond_before ⊑ urem_common_divisor_defined_cond_after

theorem t0_basic_proof : t0_basic_before ⊑ t0_basic_after

theorem ugt_swap_and_min_commute_logical_proof : ugt_swap_and_min_commute_logical_before ⊑ ugt_swap_and_min_commute_logical_after

theorem sle_swap_or_min_commute_proof : sle_swap_or_min_commute_before ⊑ sle_swap_or_min_commute_after

theorem mul64_low_proof : mul64_low_before ⊑ mul64_low_after

theorem lshrugt_02_07_exact_proof : lshrugt_02_07_exact_before ⊑ lshrugt_02_07_exact_after

theorem test_zext2_thm.extracted_1._1 : ∀ (x : BitVec 1), x = 1#1 → 1#32 = zeroExtend 32 1#1

theorem test_sub_nsw__nuw_is_safe_thm (e : IntW 32) :
  select (icmp IntPred.eq (LLVM.and e (const? 32 2147483647)) (const? 32 1073741824)) (const? 32 1073741824)
      (sub (const? 32 (-2147483648)) (LLVM.and e (const? 32 2147483647)) { «nsw» := true, «nuw» := false }) ⊑
    sub (const? 32 (-2147483648)) (LLVM.and e (const? 32 2147483647)) { «nsw» := false, «nuw» := true }

theorem bools_logical_thm.extracted_1._17 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 ^^^ 1#1 = 1#1 → ¬x_2 = 1#1 → 0#1 = 1#1 → 1#1 = x_1

theorem ashrslt_01_06_exact_proof : ashrslt_01_06_exact_before ⊑ ashrslt_01_06_exact_after

theorem or_xor_commute4_thm (e e_1 : IntW 32) :
  LLVM.xor (LLVM.udiv (const? 32 42) e_1) (LLVM.or (LLVM.udiv (const? 32 42) e) (LLVM.udiv (const? 32 42) e_1)) ⊑
    LLVM.and (LLVM.udiv (const? 32 42) e) (LLVM.xor (LLVM.udiv (const? 32 42) e_1) (const? 32 (-1)))

theorem test_thm.extracted_1._1 : ∀ (x : BitVec 64), zeroExtend 64 (truncate 32 x) = x &&& 4294967295#64

theorem gt_unsigned_to_small_unsigned_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (17#32 <ᵤ zeroExtend 32 x) = ofBool (17#8 <ᵤ x)

theorem logic_or_logic_and_2_proof : logic_or_logic_and_2_before ⊑ logic_or_logic_and_2_after

theorem sext_multiuse_proof : sext_multiuse_before ⊑ sext_multiuse_after

theorem basic_proof : basic_before ⊑ basic_after

theorem trunc_ashr_trunc_exact_proof : trunc_ashr_trunc_exact_before ⊑ trunc_ashr_trunc_exact_after

theorem a_true_implies_b_false2_comm_thm.extracted_1._8 : ∀ (x x_1 : BitVec 1) (x_2 : BitVec 8),
  ¬ofBool (x_2 == 10#8) = 1#1 → ¬ofBool (20#8 <ᵤ x_2) = 1#1 → x &&& ofBool (20#8 <ᵤ x_2) = 0#1

theorem e_1547 :
    1 * ( ~~~a ||| (b &&& c)) - 11 * ( ~~~b &&& (a ^^^ c)) + 1 * (b ^^^  ~~~(a &&& c)) + 4 * (c ^^^  ~~~( ~~~a ||| (b &&& c))) + 1 *  ~~~(b |||  ~~~c) + 11 * (c ^^^ (a ||| (b &&& c))) - 7 * (a ^^^ (b &&& c)) - 2 *  ~~~(a ||| (b ||| c)) + 2 *  ~~~( ~~~a ||| (b ||| c)) - 8 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 7 * ( ~~~a &&& ( ~~~b &&& c)) + 2 * ( ~~~a &&& (b &&& c)) - 6 * (a &&& (b &&& c)) =  - 6 * (a &&& ( ~~~b &&& c)) + 1 *  ~~~(a ||| ( ~~~b ||| c))

theorem negative3_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 <ₛ x_1 &&& 2147483647#32) &&& ofBool (0#32 ≤ₛ x) =
    ofBool (x_2 <ₛ x_1 &&& 2147483647#32) &&& ofBool (-1#32 <ₛ x)

theorem ne_umax3_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x <ᵤ x_1 + 3#32) = 1#1 → ofBool (x_1 + 3#32 != x_1 + 3#32) = ofBool (x_1 + 3#32 <ᵤ x)

theorem land_lor_right1_thm.extracted_1._3 : ∀ (x x_1 : BitVec 1), x_1 = 1#1 → 1#1 = x_1

theorem not_signbit_trunc_proof : not_signbit_trunc_before ⊑ not_signbit_trunc_after

theorem not_or_or_and_not_and_and_commute1_proof : not_or_or_and_not_and_and_commute1_before ⊑ not_or_or_and_not_and_and_commute1_after

theorem ashr_exact_thm.extracted_1._1 : ∀ (x : BitVec 1),
  ¬x = 1#1 → ¬(True ∧ 16#8 >>> 3#8 <<< 3#8 ≠ 16#8 ∨ 3#8 ≥ ↑8) → (16#8).sshiftRight' 3#8 = 2#8

theorem e_963 :
     - 2 *  ~~~(z &&&  ~~~t) + 1 *  ~~~(z ^^^ t) - 11 * t - 1 *  ~~~(z ||| t) + 13 *  ~~~(z |||  ~~~t) - 2 * (z &&&  ~~~t) =  - 12 * (z &&& t) - 2 *  ~~~t

theorem trunc_sel_equal_zext_thm.extracted_1._1 : ∀ (x : BitVec 1), ¬x = 1#1 → zeroExtend 32 42#16 = 42#32

theorem test_sub__nuw_is_safe_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x &&& 2147483647#32 == 1073741824#32) = 1#1 →
    ¬(True ∧ (BitVec.ofInt 32 (-2147483648)).usubOverflow (x &&& 2147483647#32) = true) →
      1073741824#32 = BitVec.ofInt 32 (-2147483648) - (x &&& 2147483647#32)

theorem p0_proof : p0_before ⊑ p0_after

theorem masked_icmps_mask_notallzeros_bmask_mixed_swapped_4_proof : masked_icmps_mask_notallzeros_bmask_mixed_swapped_4_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_swapped_4_after

theorem sdiv_ult_smin_proof : sdiv_ult_smin_before ⊑ sdiv_ult_smin_after

theorem invert_both_cmp_operands_add_thm (e e_1 : IntW 32) :
  icmp IntPred.sgt (add e_1 (LLVM.xor e (const? 32 (-1)))) (const? 32 0) ⊑
    icmp IntPred.slt (sub e e_1) (const? 32 (-1))

theorem AvoidCollision_signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w) :
  x.signExtend v = x.setWidth v

theorem main7e_logical_thm.extracted_1._12 : ∀ (x x_1 x_2 x_3 x_4 : BitVec 32),
  ofBool (x_4 &&& x_3 &&& x_2 == x_4 &&& x_3) = 1#1 →
    ¬ofBool (x_4 &&& x_3 &&& x_2 != x_4 &&& x_3) = 1#1 →
      ¬ofBool (x_1 &&& x &&& x_2 == x_1 &&& x) = 1#1 → 1#32 = zeroExtend 32 (ofBool (x_1 &&& x &&& x_2 != x_1 &&& x))

theorem ashr_ult_4_proof : ashr_ult_4_before ⊑ ashr_ult_4_after

theorem icmp_ne_zext_eq_non_boolean_proof : icmp_ne_zext_eq_non_boolean_before ⊑ icmp_ne_zext_eq_non_boolean_after

theorem bv_AndOrXor_1247_AB__AB__AB :
    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.xor (LLVM.and e e_1) (LLVM.const? w (-1))) (LLVM.or e e_1) ⊑ LLVM.xor e e_1

theorem lshr_and_add_fail_thm (e e_1 : IntW 8) :
  add (lshr e_1 (const? 8 1)) (LLVM.and (lshr e (const? 8 1)) (const? 8 123)) ⊑
    add (lshr e_1 (const? 8 1)) (LLVM.and (lshr e (const? 8 1)) (const? 8 123))
      { «nsw» := false, «nuw» := true }

theorem udiv_shl_pair1_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  ¬(True ∧ x_2 <<< x_1 >>> x_1 ≠ x_2 ∨ x_1 ≥ ↑32 ∨ True ∧ x_2 <<< x >>> x ≠ x_2 ∨ x ≥ ↑32 ∨ x_2 <<< x = 0) →
    True ∧ 1#32 <<< x_1 >>> x_1 ≠ 1#32 ∨ x_1 ≥ ↑32 ∨ x ≥ ↑32 → False

theorem or_xor_tree_1111_thm (e e_1 e_2 : IntW 32) :
  LLVM.or (LLVM.xor (mul e_2 (const? 32 42)) (LLVM.xor (mul e_1 (const? 32 42)) (mul e (const? 32 42))))
      (LLVM.xor (mul e (const? 32 42)) (mul e_2 (const? 32 42))) ⊑
    LLVM.or (LLVM.xor (mul e (const? 32 42)) (mul e_2 (const? 32 42))) (mul e_1 (const? 32 42))

theorem test6_proof : test6_before ⊑ test6_after

theorem positive_biggershl_shlnuw_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(3#8 ≥ ↑8 ∨ True ∧ x >>> 3#8 <<< 6#8 >>> 6#8 ≠ x >>> 3#8 ∨ 6#8 ≥ ↑8) →
    True ∧ x <<< 3#8 >>> 3#8 ≠ x ∨ 3#8 ≥ ↑8 → False

theorem n4_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬16#32 ≥ ↑32 → True ∧ zeroExtend 32 x <<< 16#32 >>> 16#32 ≠ zeroExtend 32 x ∨ 16#32 ≥ ↑32 → False

theorem e_929 :
     - 2 *  ~~~(z &&& t) + 3 *  ~~~t - 5 * (z ^^^ t) - 1 * (z |||  ~~~t) + 7 *  ~~~(z |||  ~~~t) + 1 * (z &&& t) =  - 5 * (z &&&  ~~~t)

theorem p_constmask2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  True ∧ (x_1 &&& 61440#32 &&& (x &&& BitVec.ofInt 32 (-65281)) != 0) = true → False

theorem ule_swap_or_not_min_commute_proof : ule_swap_or_not_min_commute_before ⊑ ule_swap_or_not_min_commute_after

theorem t4_c1_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), x_1 - 42#8 - x = x_1 + BitVec.ofInt 8 (-42) - x

theorem test1_proof : test1_before ⊑ test1_after

theorem neg_nsw_slt_n1_proof : neg_nsw_slt_n1_before ⊑ neg_nsw_slt_n1_after

theorem and_or1_thm.extracted_1._8 : ∀ (x x_1 x_2 : BitVec 1), ¬x_2 ^^^ 1#1 ||

theorem e_380 :
    3 *  ~~~(x &&& y) + 1 * (x |||  ~~~y) + 5 *  ~~~(x ^^^ y) - 2 * (x ^^^ y) - 11 *  ~~~y - 1 *  ~~~(x |||  ~~~y) + 11 * (x &&&  ~~~y) - 4 * (x &&& y) =  - 2 *  ~~~(x ||| y) + 2 * x

theorem e_2017 :
     - 1 * ( ~~~e &&&  ~~~(d ^^^ f)) - 7 * ((d &&& f) |||  ~~~(e ||| f)) + 7 * ((d ^^^ e) &&& (d ^^^ f)) + 4 * (f ||| (d &&&  ~~~e)) + 4 * (f &&&  ~~~(d &&&  ~~~e)) + 1 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) + 2 * (d ^^^ (e &&& f)) + 1 * (e ||| (d &&&  ~~~f)) + 2 * (e ||| f) - 2 * (e ^^^  ~~~(d ||| (e ^^^ f))) + 2 * (f &&&  ~~~(d &&& e)) - 2 *  ~~~(d ||| ( ~~~e &&& f)) - 6 * ((d &&& e) ^^^ (e ||| f)) - 7 * (e ^^^  ~~~(d &&&  ~~~f)) - 5 * (d ||| (e ^^^ f)) + 1 *  ~~~(d ||| e) + 1 * ( ~~~(d |||  ~~~e) |||  ~~~(e ^^^ f)) - 11 * (e ^^^ (d &&& (e ||| f))) + 1 * (f |||  ~~~(d ^^^ e)) - 5 * (e &&&  ~~~f) - 1 * (d &&&  ~~~e) - 3 * ((d &&& e) |||  ~~~(e ||| f)) + 7 * (e ^^^ ( ~~~d &&& ( ~~~e ||| f))) + 1 * (f ^^^ ( ~~~d &&& (e ||| f))) - 3 * ( ~~~(d ^^^ e) &&& (d ^^^ f)) + 11 * (f ^^^ (d |||  ~~~e)) + 2 *  ~~~(d &&& (e ^^^ f)) - 1 *  ~~~(d ||| (e ||| f)) - 15 *  ~~~( ~~~d ||| (e ||| f)) + 1 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 4 * ( ~~~d &&& ( ~~~e &&& f)) - 19 * ( ~~~d &&& (e &&& f)) + 24 * (d &&& ( ~~~e &&& f)) - 6 * (d &&& (e &&& f)) =  - 16 *  ~~~(d ||| ( ~~~e ||| f)) - 2 * (e ^^^ (d ||| (e ||| f)))

theorem test5_proof : test5_before ⊑ test5_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}
</local_ctx>

<target_theorem>
theorem matchVar_appendInl {w : Var ⟨te⟩ t} :
    matchVar lets v (.var matchLets matchExpr) w.appendInl ma = some ma' →
    ∃ args,
      lets.getPureExpr v
        = some ⟨_, w, matchExpr.op, matchExpr.ty_eq, matchExpr.eff_le, args, matchExpr.regArgs⟩
      ∧ matchArg lets matchLets args matchExpr.args ma = some ma' :=
</target_theorem>

