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>
Bool in Init.Prelude
Nat in Init.Prelude
Int.xor in Mathlib.Data.Int.Bitwise
Nat.testBit in Init.Data.Nat.Bitwise.Basic
Fin in Init.Prelude
Fin.castLE in Init.Data.Fin.Basic
Fin.last in Init.Data.Fin.Basic
List in Init.Prelude

syntax "max" : MLIR.Pretty.uniform_op

syntax "slt" : 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) )

def Predicate.evalUlt (t₁ t₂ : BitStream) : BitStream := (~~~ (t₁.borrow t₂)).concat true

def BitStream : Type := Nat → Bool

def borrow (x y : BitStream) : BitStream :=
  fun n => (subAux x y n).2

def subAux (x y : BitStream) : Nat → Bool × Bool
  | 0 => (xor (x 0) (y 0), !(x 0) && y 0)
  | n+1 =>
    let borrow := (subAux x y n).2
    let a := x (n + 1)
    let b := y (n + 1)
    (xor a (xor b borrow), !a && b || ((!(xor a b)) && borrow))

inductive Predicate : Type where
 
| width (wp : WidthPredicate) (n : Nat) : Predicate
| binary (p : BinaryPredicate) (t₁ t₂ : Term)
| land  (p q : Predicate) : Predicate
| lor (p q : Predicate) : Predicate
deriving Repr, Inhabited, Lean.ToExpr

@[simp] def Predicate.evalFin (p : Predicate) (vars : Fin (arity p) → BitStream) : BitStream :=
match p with
| .width .eq n => BitStream.falseIffEq n
| .width .neq n => BitStream.falseIffNeq n
| .width .lt n => BitStream.falseIffLt n
| .width .le n => BitStream.falseIffLe n
| .width .gt n => BitStream.falseIffGt n
| .width .ge n => BitStream.falseIffGe n
| .binary .eq t₁ t₂ =>
    let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    Predicate.evalEq x₁ x₂
| .binary .neq t₁ t₂  =>
    let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    Predicate.evalNeq x₁ x₂
| .land p q =>
  
  
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLand x₁ x₂
| .lor p q =>
  
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLor x₁ x₂
| .binary .slt p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalSlt x₁ x₂
| .binary .sle p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLor (Predicate.evalSlt x₁ x₂) (Predicate.evalEq x₁ x₂)
| .binary .ult p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  (Predicate.evalUlt x₁ x₂)
| .binary .ule p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLor (Predicate.evalUlt x₁ x₂) (Predicate.evalEq x₁ x₂)

def Predicate.evalLor (t₁ t₂ : BitStream) : BitStream := (t₁ &&& t₂)

@[simp] def Term.evalFin (t : Term) (vars : Fin (arity t) → BitStream) : BitStream :=
  match t with
  | var n => vars (Fin.last n)
  | zero    => BitStream.zero
  | one     => BitStream.one
  | negOne  => BitStream.negOne
  | ofNat n => BitStream.ofNat n
  | and t₁ t₂ =>
      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ &&& x₂
  | or t₁ t₂ =>
      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ ||| x₂
  | xor t₁ t₂ =>
      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ ^^^ x₂
  | not t     => ~~~(t.evalFin vars)
  | add t₁ t₂ =>
      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ + x₂
  | sub t₁ t₂ =>
      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ - x₂
  | neg t       => -(Term.evalFin t vars)
 
 
  | shiftL t n  => BitStream.shiftLeft (Term.evalFin t vars) n

abbrev negOne : BitStream := fun _ => true

def shiftLeft (x : BitStream) (k : Nat) : BitStream :=
  fun i => if i < k then false else x (i - k)

def ofNat (x : Nat) : BitStream :=
  Nat.testBit x

abbrev one    : BitStream := (· == 0)

abbrev zero   : BitStream := fun _ => false

@[simp] def Term.arity : Term → Nat
| (var n) => n+1
| zero => 0
| one => 0
| negOne => 0
| ofNat _ => 0
| Term.and t₁ t₂ => max (arity t₁) (arity t₂)
| Term.or t₁ t₂ => max (arity t₁) (arity t₂)
| Term.xor t₁ t₂ => max (arity t₁) (arity t₂)
| Term.not t => arity t
| add t₁ t₂ => max (arity t₁) (arity t₂)
| sub t₁ t₂ => max (arity t₁) (arity t₂)
| neg t => arity t

| shiftL t .. => arity t

inductive Term : Type
| var : Nat → Term
 
| zero : Term
 
| negOne : Term
 
| one : Term
 
| ofNat (n : Nat) : Term
 
| and : Term → Term → Term
 
| or : Term → Term → Term
 
| xor : Term → Term → Term
 
| not : Term → Term
 
| add : Term → Term → Term
 
| sub : Term → Term → Term
 
| neg : Term → Term

| shiftL : Term → Nat → Term

deriving Repr, Inhabited, Lean.ToExpr

def Predicate.evalSlt (t₁ t₂ : BitStream) : BitStream :=
    (((Predicate.evalUlt t₁ t₂)) ^^^ (Predicate.evalMsbEq t₁ t₂))

def Predicate.evalMsbEq (t₁ t₂ : BitStream) : BitStream :=
  (t₁ ^^^ t₂).concat false

def Predicate.evalLand (t₁ t₂ : BitStream) : BitStream := (t₁ ||| t₂)

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

def nxor (a b : BitStream) : BitStream := fun i => a i == b i

def scanAnd (s : BitStream) : BitStream := scanl true Bool.and s

abbrev scanl (init : Bool) (f : Bool → Bool → Bool) (s : BitStream) : BitStream :=
  fun n => match n with
    | 0 => f init (s 0)
    | n+1 => f (scanl init f s n) (s (n + 1))

def Predicate.evalEq (t₁ t₂ : BitStream) : BitStream := (t₁ ^^^ t₂).concat false |>.scanOr

def scanOr (s : BitStream) : BitStream := scanl false Bool.or s

abbrev falseIffNeq (n : Nat) : BitStream := fun i => decide (i == n)

abbrev falseIffLt (n : Nat) : BitStream := fun i => decide (i ≥ n)

abbrev falseIffLe (n : Nat) : BitStream := fun i => decide (i > n)

abbrev falseIffGe (n : Nat) : BitStream := fun i => decide (i < n)

abbrev falseIffEq (n : Nat) : BitStream := fun i => decide (i != n)

abbrev falseIffGt (n : Nat) : BitStream := fun i => decide (i ≤ n)

def Term.width (t : Term) : WidthExpr :=
  match t with

| .ofNat w _n => w
  | .var _v w => w
  | .add w _a _b => w
  | .zext _a wnew => wnew
  | .setWidth _a wnew => wnew
  | .sext _a wnew => wnew
  | .bor w _a _b => w
  | .band w _a _b => w
  | .bxor w _a _b => w
  | .bnot w _a => w
  | .boolVar _v => WidthExpr.const 1 
  | .boolConst _b => WidthExpr.const 1
  | .shiftl w _a _k => w
  | .bvOfBool _b => WidthExpr.const 1
  | binWidthRel _k wa wb => WidthExpr.const 0
  | binRel _k w _a _b => w
  | or _p1 _p2 => WidthExpr.const 0
  | and _p1 _p2 => WidthExpr.const 0
  | pvar _v => WidthExpr.const 0
  | boolBinRel _k _a _b => WidthExpr.const 0

@[simp] def Predicate.arity : Predicate → Nat
| .width _ _ => 0
| .binary .eq t1 t2 => max t1.arity t2.arity
| .binary .neq t₁ t₂ => max t₁.arity t₂.arity
| .binary .ult t₁ t₂ => max t₁.arity t₂.arity
| .binary .ule t₁ t₂ => t₁.arity ⊔ t₂.arity ⊔ (t₁.arity ⊔ t₂.arity)
| .binary .slt t₁ t₂ => (t₁.arity ⊔ t₂.arity ⊔ (t₁.arity ⊔ t₂.arity))
| .binary .sle t₁ t₂ => (t₁.arity ⊔ t₂.arity ⊔ (t₁.arity ⊔ t₂.arity) ⊔ (t₁.arity ⊔ t₂.arity))
| .lor p q => max p.arity q.arity
| .land p q => max p.arity q.arity

inductive BinaryPredicate
| eq
| neq
| ult
| ule
| slt
| sle
deriving Repr, Lean.ToExpr

inductive WidthPredicate
| eq
| neq
| lt
| le
| gt
| ge
deriving Repr, Inhabited, Lean.ToExpr

def Predicate.eval (p : Predicate) (vars : List BitStream) : BitStream :=
  match p with
  | .width .eq n => BitStream.falseIffEq n
  | .width .neq n => BitStream.falseIffNeq n
  | .width .lt n => BitStream.falseIffLt n
  | .width .le n => BitStream.falseIffLe n
  | .width .gt n => BitStream.falseIffGt n
  | .width .ge n => BitStream.falseIffGe n
  | lor p q => Predicate.evalLor (p.eval vars) (q.eval vars)
  | land p q => Predicate.evalLand (p.eval vars) (q.eval vars)
  | binary .eq t₁ t₂ => Predicate.evalEq (t₁.eval vars) (t₂.eval vars)
   
  | binary .neq t1 t2 => Predicate.evalNeq (t1.eval vars) (t2.eval vars)
  | binary .ult t₁ t₂ => Predicate.evalUlt (t₁.eval vars) (t₂.eval vars)
  | binary .ule t₁ t₂ =>
     Predicate.evalLor
       (Predicate.evalEq (t₁.eval vars) (t₂.eval vars))
       (Predicate.evalUlt (t₁.eval vars) (t₂.eval vars))
  | binary .slt t₁ t₂ => Predicate.evalSlt (t₁.eval vars) (t₂.eval vars)
  | binary .sle t₁ t₂ => Predicate.evalLor
       (Predicate.evalEq (t₁.eval vars) (t₂.eval vars))
       (Predicate.evalSlt (t₁.eval vars) (t₂.eval vars))

def Term.eval (t : Term) (vars : List BitStream) : BitStream :=
  match t with
  | var n       => vars.getD n default
  | zero        => BitStream.zero
  | one         => BitStream.one
  | negOne      => BitStream.negOne
  | ofNat n     => BitStream.ofNat n
  | and t₁ t₂   => (t₁.eval vars) &&& (t₂.eval vars)
  | or t₁ t₂    => (t₁.eval vars) ||| (t₂.eval vars)
  | xor t₁ t₂   => (t₁.eval vars) ^^^ (t₂.eval vars)
  | not t       => ~~~(t.eval vars)
  | add t₁ t₂   => (Term.eval t₁ vars) + (Term.eval t₂ vars)
  | sub t₁ t₂   => (Term.eval t₁ vars) - (Term.eval t₂ vars)
  | neg t       => -(Term.eval t vars)

| shiftL t n  => BitStream.shiftLeft (Term.eval t vars) n

def test_add_fold_LHS :=
[mod_arith q, hq| {
  ^bb0():
    %e1 = mod_arith.constant 12 : !R
    %e2 = mod_arith.constant 34 : !R
    %add = mod_arith.add %e1, %e2 : !R
    %e3 = mod_arith.constant 56 : !R
    %add2 = mod_arith.add %add, %e3 : !R
    return %add2 : !R
}]

def positive_samevar_shlnuwnsw_lshrexact_after := [llvm|
{
^0(%arg27 : i8, %arg28 : i8):
  "llvm.return"(%arg27) : (i8) -> ()
}
]

def ult_swap_and_not_max_commute_before := [llvm|
{
^0(%arg98 : i8, %arg99 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.icmp "ugt" %arg99, %arg98 : i8
  %2 = llvm.icmp "ne" %arg98, %0 : i8
  %3 = llvm.and %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

def mkStateUniqueCircuitN {arity : Type _}
  [DecidableEq arity] [Fintype arity] [Hashable arity]
  (p : FSM arity) (n : Nat) : Circuit (Vars p.α arity n) :=
  let sn : p.α → Circuit (Vars p.α arity n) := fun s =>
    Circuit.var true (Vars.stateN s n)
  let circs := (List.range n).attach |>.map fun ⟨i, hi⟩ =>
    let si : p.α → Circuit (Vars p.α arity n) := fun s =>
      Circuit.var true (Vars.stateN s i (by admit /- proof elided -/
      ))
    (mkStateNeqCircuit p si sn)
  Circuit.bigOr circs

HXor.hXor in Init.Prelude

def not_or_or_not_commute1_before := [llvm|
{
^0(%arg546 : i32, %arg547 : i32, %arg548 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg547, %0 : i32
  %2 = llvm.xor %arg548, %0 : i32
  %3 = llvm.or %1, %arg546 : i32
  %4 = llvm.or %3, %2 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

instance {n} : ShiftLeft (BitVec n) := ⟨fun x y => x <<< y.toNat⟩

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

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

def sub_add_reg_x_sub_y_add_x : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64, %y: i64):
      %1 = llvm.add %y, %x : i64
      %2 = llvm.sub %x, %1 : i64
      llvm.return %2 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64, %y: i64):
      %c = llvm.mlir.constant (0) : i64
      %0 = llvm.sub %c, %y : i64
      llvm.return %0 : i64
  }]

def masked_bit_clear_commute_after := [llvm|
{
^0(%arg77 : i32, %arg78 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.mlir.constant(1 : i32) : i32
  %3 = llvm.srem %0, %arg77 : i32
  %4 = llvm.xor %3, %1 : i32
  %5 = llvm.lshr %4, %arg78 : i32
  %6 = llvm.and %5, %2 : i32
  "llvm.return"(%6) : (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 lshrugt_03_03_after := [llvm|
{
^0(%arg380 : i4):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def sub_const_const_sub_after := [llvm|
{
^0(%arg35 : i32):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.sub %0, %arg35 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def sge_swap_or_not_max_after := [llvm|
{
^0(%arg312 : i8, %arg313 : i8):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def ashr_lshr_shift_amt_mismatch_after := [llvm|
{
^0(%arg72 : i32, %arg73 : i32, %arg74 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.lshr %arg72, %arg73 : i32
  %2 = llvm.ashr %arg72, %arg74 : i32
  %3 = llvm.icmp "slt" %arg72, %0 : i32
  %4 = "llvm.select"(%3, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

def commutativity_constant_6_vary_invmask_after := [llvm|
{
^0(%arg16 : i4, %arg17 : i4):
  %0 = llvm.mlir.constant(6 : i4) : i4
  %1 = llvm.xor %arg16, %0 : i4
  %2 = llvm.and %1, %arg17 : i4
  %3 = llvm.xor %2, %0 : i4
  "llvm.return"(%3) : (i4) -> ()
}
]

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

def icmp_slt_0_and_icmp_sge_neg1_i64_fail_after := [llvm|
{
^0(%arg59 : i64):
  %0 = llvm.mlir.constant(-2) : i64
  %1 = llvm.mlir.constant(62) : i64
  %2 = llvm.mlir.constant(1) : i64
  %3 = llvm.mlir.constant(0) : i64
  %4 = llvm.icmp "sgt" %arg59, %0 : i64
  %5 = llvm.lshr %arg59, %1 : i64
  %6 = llvm.and %5, %2 : i64
  %7 = "llvm.select"(%4, %6, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  "llvm.return"(%7) : (i64) -> ()
}
]

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

def sdiv_ult_smin_before := [llvm|
{
^0(%arg18 : i8, %arg19 : i8):
  %0 = llvm.mlir.constant(-128 : i8) : i8
  %1 = llvm.sdiv %arg18, %arg19 : i8
  %2 = llvm.icmp "ult" %1, %0 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def ult_umin3_before := [llvm|
{
^0(%arg32 : i32, %arg33 : i32):
  %0 = llvm.mlir.constant(3 : i32) : i32
  %1 = llvm.add %arg32, %0 : i32
  %2 = llvm.icmp "ult" %1, %arg33 : i32
  %3 = "llvm.select"(%2, %1, %arg33) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %4 = llvm.icmp "ugt" %1, %3 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

def negative_not_next_power_of_two_logical_before := [llvm|
{
^0(%arg4 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.mlir.constant(64 : i32) : i32
  %2 = llvm.mlir.constant(256 : i32) : i32
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.icmp "sgt" %arg4, %0 : i32
  %5 = llvm.add %arg4, %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 uge_swap_and_max_before := [llvm|
{
^0(%arg230 : i8, %arg231 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.icmp "ule" %arg231, %arg230 : i8
  %2 = llvm.icmp "eq" %arg230, %0 : i8
  %3 = llvm.and %1, %2 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

def llvm_const_lower_riscv_li_40 : LLVMPeepholeRewriteRefine 64 [] :=
  {lhs := constLLVM_40, rhs:= liRiscv_40,
   correct := by admit /- proof elided -/

Sigma.fst in Init.Core

def match_signed_before := [llvm|
{
^0(%arg15 : i64):
  %0 = llvm.mlir.constant(299) : i64
  %1 = llvm.mlir.constant(64) : i64
  %2 = llvm.mlir.constant(19136) : i64
  %3 = llvm.mlir.constant(9) : i64
  %4 = llvm.srem %arg15, %0 : i64
  %5 = llvm.sdiv %arg15, %0 : i64
  %6 = llvm.srem %5, %1 : i64
  %7 = llvm.sdiv %arg15, %2 : i64
  %8 = llvm.srem %7, %3 : i64
  %9 = llvm.mul %6, %0 : i64
  %10 = llvm.add %4, %9 : i64
  %11 = llvm.mul %8, %2 : i64
  %12 = llvm.add %10, %11 : i64
  "llvm.return"(%12) : (i64) -> ()
}
]

def shl_sub_i64_before := [llvm|
{
^0(%arg15 : i64):
  %0 = llvm.mlir.constant(63) : i64
  %1 = llvm.mlir.constant(1) : i64
  %2 = llvm.sub %0, %arg15 : i64
  %3 = llvm.shl %1, %2 : i64
  "llvm.return"(%3) : (i64) -> ()
}
]

instance : ToString (CIRCTStream.Stream (BitVec w))where
  toString s := toString (Stream.toList 10 s)

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

def slt_zero_ne_ne_0_before := [llvm|
{
^0(%arg5 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(31 : i32) : i32
  %2 = llvm.icmp "ne" %arg5, %0 : i32
  %3 = llvm.zext %2 : i1 to i32
  %4 = llvm.lshr %arg5, %1 : i32
  %5 = llvm.icmp "ne" %3, %4 : i32
  "llvm.return"(%5) : (i1) -> ()
}
]

def not_mul_of_bool_commute_after := [llvm|
{
^0(%arg87 : i32, %arg88 : i32):
  %0 = llvm.mlir.constant(30 : i32) : i32
  %1 = llvm.mlir.constant(255 : i32) : i32
  %2 = llvm.lshr %arg87, %0 : i32
  %3 = llvm.and %arg88, %1 : i32
  %4 = llvm.mul %3, %2 overflow<nsw,nuw> : i32
  %5 = llvm.icmp "ugt" %4, %1 : i32
  "llvm.return"(%5) : (i1) -> ()
}
]

@[simp_denote]
def llvm_urem_64 : Com  LLVMPlusRiscV ⟨[.llvm (.bitvec 64), .llvm (.bitvec 64)]⟩
  .pure (.llvm (.bitvec 64)) := [LV| {
  ^entry (%x: i64, %y: i64 ):
    %1 = llvm.urem    %x, %y : i64
    llvm.return %1 : i64
  }]

def test_add_nuw_nsw__nuw_is_safe_after := [llvm|
{
^0(%arg43 : i32):
  %0 = llvm.mlir.constant(2147483647 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.and %arg43, %0 : i32
  %3 = llvm.add %2, %1 overflow<nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def and_not_or_or_not_or_xor_commute2_before := [llvm|
{
^0(%arg319 : i32, %arg320 : i32, %arg321 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sdiv %0, %arg319 : i32
  %3 = llvm.or %arg320, %arg321 : i32
  %4 = llvm.xor %3, %1 : i32
  %5 = llvm.and %2, %4 : i32
  %6 = llvm.xor %arg320, %arg321 : i32
  %7 = llvm.or %6, %2 : i32
  %8 = llvm.xor %7, %1 : i32
  %9 = llvm.or %5, %8 : i32
  "llvm.return"(%9) : (i32) -> ()
}
]

def or_not_xor_common_op_commute6_before := [llvm|
{
^0(%arg89 : i8, %arg90 : i8, %arg91 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.sub %0, %arg91 : i8
  %3 = llvm.xor %arg89, %1 : i8
  %4 = llvm.xor %arg90, %arg89 : i8
  %5 = llvm.or %2, %3 : i8
  %6 = llvm.or %4, %5 : i8
  "llvm.return"(%6) : (i8) -> ()
}
]

def alive_AddSub_1043_tgt  (w : Nat)  :=
[llvm( w )| {
^bb0(%C1 : _, %Z : _, %RHS : _):
  %v1 = llvm.not %C1
  %v2 = llvm.or %Z, %v1
  %v3 = llvm.and %Z, %C1
  %v4 = llvm.xor %v3, %C1
  %v5 = llvm.mlir.constant 1
  %v6 = llvm.add %v4, %v5
  %v7 = llvm.sub %RHS, %v2
  llvm.return %v7
}]

def select_icmp_eq_and_1_0_or_2_before := [llvm|
{
^0(%arg255 : i32, %arg256 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(2 : i32) : i32
  %3 = llvm.and %arg255, %0 : i32
  %4 = llvm.icmp "eq" %3, %1 : i32
  %5 = llvm.or %arg256, %2 : i32
  %6 = "llvm.select"(%4, %arg256, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%6) : (i32) -> ()
}
]

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

Lean.Exception in Lean.Exception

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

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

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 packedBitVecToFpSubstitutionValue (map: Std.HashMap Nat BVExpr.PackedBitVec) :
    Std.HashMap Nat (SubstitutionValue FpExpr) :=
  Std.HashMap.ofList (List.map (fun item => (item.fst, SubstitutionValue.packedBV item.snd)) map.toList)

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

def addMax (a : BitVec v) (b : BitVec w) : BitVec (max v w + 1) :=
   a.signExtend _ + b.signExtend _

Erased in Mathlib.Data.Erased

def test21_before := [llvm|
{
^0(%arg0 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.ashr %arg0, %0 : i8
  %3 = llvm.and %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def eq_basic_equal_minus_1_before := [llvm|
{
^0(%arg30 : i8, %arg31 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.add %arg30, %0 : i8
  %3 = llvm.icmp "eq" %arg30, %1 : i8
  %4 = llvm.icmp "ugt" %2, %arg31 : i8
  %5 = llvm.or %3, %4 : i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def shl_nsw_nuw_uge_Csle0_before := [llvm|
{
^0(%arg10 : i8, %arg11 : i8):
  %0 = llvm.mlir.constant(-120 : i8) : i8
  %1 = llvm.shl %arg10, %arg11 overflow<nsw,nuw> : i8
  %2 = llvm.icmp "uge" %1, %0 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def udiv_shl_shl_nuw_nsw2_before := [llvm|
{
^0(%arg55 : i8, %arg56 : i8, %arg57 : i8):
  %0 = llvm.shl %arg55, %arg57 overflow<nsw,nuw> : i8
  %1 = llvm.shl %arg56, %arg57 overflow<nsw> : i8
  %2 = llvm.udiv %0, %1 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

Lean.Meta.Simp.Step in Lean.Meta.Tactic.Simp.Types

def reduce_xor_common_op_commute0_before := [llvm|
{
^0(%arg10 : i4, %arg11 : i4, %arg12 : i4):
  %0 = llvm.xor %arg10, %arg11 : i4
  %1 = llvm.xor %0, %arg12 : i4
  %2 = llvm.or %1, %arg10 : i4
  "llvm.return"(%2) : (i4) -> ()
}
]

def test5_after := [llvm|
{
^0(%arg118 : i32):
  %0 = llvm.mlir.constant(1234 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.mlir.constant(5 : i32) : i32
  %3 = llvm.xor %arg118, %0 : i32
  %4 = llvm.lshr %arg118, %1 : i32
  %5 = llvm.xor %4, %2 : i32
  %6 = llvm.add %5, %3 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def src_x_and_nmask_eq_after := [llvm|
{
^0(%arg30 : i8, %arg31 : i8, %arg32 : i1):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.shl %0, %arg31 overflow<nsw> : i8
  %3 = llvm.icmp "ule" %2, %arg30 : i8
  %4 = llvm.xor %arg32, %1 : i1
  %5 = "llvm.select"(%4, %1, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def test2_before := [llvm|
{
^0(%arg11 : i47):
  %0 = llvm.mlir.constant(-70368744177664 : i47) : i47
  %1 = llvm.xor %arg11, %0 : i47
  %2 = llvm.add %1, %0 : i47
  "llvm.return"(%2) : (i47) -> ()
}
]

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

def or_and_not_constant_commute3_before := [llvm|
{
^0(%arg106 : i32, %arg107 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(-2 : i32) : i32
  %2 = llvm.or %arg106, %arg107 : i32
  %3 = llvm.and %0, %2 : i32
  %4 = llvm.and %1, %arg107 : i32
  %5 = llvm.or %4, %3 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def or_basic_before := [llvm|
{
^0(%arg15 : i16):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.mlir.constant(-256 : i16) : i16
  %2 = llvm.mlir.constant(17664 : i16) : i16
  %3 = llvm.trunc %arg15 : i16 to i8
  %4 = llvm.icmp "ne" %3, %0 : i8
  %5 = llvm.and %arg15, %1 : i16
  %6 = llvm.icmp "ne" %5, %2 : i16
  %7 = llvm.or %4, %6 : i1
  "llvm.return"(%7) : (i1) -> ()
}
]

def alive_AndOrXor_1294_A__B__A__B___A__B_tgt :=
[sllvm| {
^bb0(%A : i64, %B : i64):
  %v1 = llvm.or %A, %B : i64
  %v2 = llvm.mlir.constant -1 : i64
  %v3 = llvm.xor %A, %v2 : i64
  %v4 = llvm.xor %v3, %B : i64
  %v5 = llvm.and %A, %B : i64
  llvm.return %v5 : i64
}]

def test1_after := [llvm|
{
^0(%arg2 : i33, %arg3 : i33):
  %0 = llvm.mlir.constant(65280 : i33) : i33
  %1 = llvm.mlir.constant(0 : i33) : i33
  %2 = llvm.xor %arg2, %arg3 : i33
  %3 = llvm.and %2, %0 : i33
  %4 = llvm.icmp "ne" %3, %1 : i33
  "llvm.return"(%4) : (i1) -> ()
}
]

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

List.Sublist in Init.Data.List.Basic

|
</all_available_defs>

<all_available_lemmas>
...

theorem and_comm (x y : BitStream) : x &&& y = y &&& x

theorem lshr_pow2_ult_proof : lshr_pow2_ult_before ⊑ lshr_pow2_ult_after

@[simp]
theorem BitVec.zero_concat (b : Bool) : (0#0).concat b = BitVec.ofBool b

theorem ult_rem_zero_thm (e : IntW 8) :
  icmp IntPred.ult (mul e (const? 8 7) { «nsw» := false, «nuw» := true }) (const? 8 21) ⊑
    icmp IntPred.ult e (const? 8 3)

theorem exact_lshr_ne_proof : exact_lshr_ne_before ⊑ exact_lshr_ne_after

theorem exactly_one_set_signbit_wrong_pred_thm (e e_1 : IntW 8) :
  icmp IntPred.sgt (lshr e_1 (const? 8 7)) (zext 8 (icmp IntPred.sgt e (const? 8 (-1)))) ⊑
    icmp IntPred.slt (LLVM.and e e_1) (const? 8 0)

theorem mul_of_udiv_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ x.umod 12#8 ≠ 0 ∨ 12#8 = 0) → True ∧ x >>> 1#8 <<< 1#8 ≠ x ∨ 1#8 ≥ ↑8 → False

theorem lshr_mul_times_5_div_4_exact_2_proof : lshr_mul_times_5_div_4_exact_2_before ⊑ lshr_mul_times_5_div_4_exact_2_after

theorem or_xor_tree_1111_proof : or_xor_tree_1111_before ⊑ or_xor_tree_1111_after

theorem scalar_i32_lshr_and_signbit_ne_proof : scalar_i32_lshr_and_signbit_ne_before ⊑ scalar_i32_lshr_and_signbit_ne_after

theorem e_459 :
     - 3 *  ~~~(x &&&  ~~~y) - 1 *  ~~~(x &&&  ~~~x) - 1 * (x ||| y) + 4 * (x ^^^ y) - 3 * x + 2 *  ~~~x - 2 *  ~~~(x ||| y) - 1 *  ~~~(x |||  ~~~y) - 3 * (x &&&  ~~~y) =  - 8 * (x &&& y) - 4 *  ~~~y

theorem bools_multi_uses2_logical_thm.extracted_1._7 : ∀ (x x_1 : BitVec 1),
  ¬x_1 ^^^ 1#1 = 1#1 → ¬x_1 = 1#1 → 0#1 = 1#1 → x = 1#1 → True → 0#1 + 0#1 = 0#1 ^^^ 0#1

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

theorem foo_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(-1#32 == 0 || 32 != 1 && x == intMin 32 && -1#32 == -1) = true → ofBool (x.srem (-1#32) == 0#32) = 1#1

theorem scalar_i64_signbit_lshr_and_eq_proof : scalar_i64_signbit_lshr_and_eq_before ⊑ scalar_i64_signbit_lshr_and_eq_after

theorem and_ne_with_one_bit_diff_constants3_logical_proof : and_ne_with_one_bit_diff_constants3_logical_before ⊑ and_ne_with_one_bit_diff_constants3_logical_after

theorem test_and_ne_a_b_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1),
  x_2 &&& ofBool (x_1 != x) = 1#1 → ¬x_2 = 1#1 → x_1 = x

theorem e_751 :
     - 7 * (z ||| t) + 2 *  ~~~z + 7 * z =  - 5 *  ~~~(z |||  ~~~t) + 2 *  ~~~(z ||| t)

theorem test3_thm.extracted_1._4 : ∀ (x : BitVec 1) (x_1 : BitVec 59),
  ¬x = 1#1 → ¬4096#59 = 0 → ¬12#59 ≥ ↑59 → x_1 / 4096#59 = x_1 >>> 12#59

theorem testi64i32_ne_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬(31#32 ≥ ↑32 ∨ 32#64 ≥ ↑64) →
    ofBool ((truncate 32 x).sshiftRight' 31#32 != truncate 32 (x >>> 32#64)) =
      ofBool (x + BitVec.ofInt 64 (-2147483648) <ᵤ BitVec.ofInt 64 (-4294967296))

theorem demorgan_and_apint2_proof : demorgan_and_apint2_before ⊑ demorgan_and_apint2_after

theorem sub_from_constant_of_sub_from_constant_thm.extracted_1._1 : ∀ (x : BitVec 8),
  11#8 - (42#8 - x) = x + BitVec.ofInt 8 (-31)

theorem bv_AndOrXor_1683_2 :
    ∀ (e e_1 : LLVM.IntW w), LLVM.or (LLVM.icmp LLVM.IntPred.uge e e_1) (LLVM.icmp LLVM.IntPred.ne e e_1) ⊑ LLVM.const? 1 1

theorem t11_no_shift_proof : t11_no_shift_before ⊑ t11_no_shift_after

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

theorem sgt_zero_eq_not_neg_sgt_zero (A : BitVec w) (h_ne_intMin : A ≠ intMin w)
    (h_ne_zero : A ≠ 0) : (A >ₛ 0#w) ↔ ¬ ((-A) >ₛ 0#w)

theorem shr_umax_proof : shr_umax_before ⊑ shr_umax_after

theorem ashr_1_thm (e e_1 e_2 : IntW 8) (e_3 : IntW 1) :
  LLVM.xor (ashr (select e_3 (LLVM.xor e_2 (const? 8 (-1))) (LLVM.xor e_1 (const? 8 123))) e) (const? 8 (-1)) ⊑
    ashr (select e_3 e_2 (LLVM.xor e_1 (const? 8 (-124)))) e

theorem test_add__nuw_is_safe_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 2147483647#32 == 2147483647#32) = 1#1 → True ∧ (x &&& 2147483647#32).uaddOverflow 1#32 = true → False

theorem foo_proof : foo_before ⊑ foo_after

theorem add_constant_equal_with_the_top_bit_of_demandedbits_insertpt_proof : add_constant_equal_with_the_top_bit_of_demandedbits_insertpt_before ⊑ add_constant_equal_with_the_top_bit_of_demandedbits_insertpt_after

theorem a_thm (e : IntW 32) :
  LLVM.and (LLVM.srem e (const? 32 8)) (const? 32 1) ⊑ LLVM.and e (const? 32 1)

theorem shift_xor_multiuse_cmp_xor_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (0#32 != x_2 &&& 4096#32) = 1#1 → ofBool (x_2 &&& 4096#32 == 0#32) = 1#1 → False

theorem bor_lor_right2_thm (e e_1 : IntW 1) : select e_1 (const? 1 1) (LLVM.or e e_1) ⊑ select e_1 (const? 1 1) e

theorem t3_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(32#32 - x ≥ ↑32 ∨ zeroExtend 64 (x + BitVec.ofInt 32 (-16)) ≥ ↑64) →
    ofBool (x_1 <<< (32#32 - x) &&& truncate 32 (131071#64 >>> zeroExtend 64 (x + BitVec.ofInt 32 (-16))) != 0#32) =
      ofBool (x_1 &&& 1#32 != 0#32)

@[simp]
lemma evalRelation_coe (rel : Relation) (bv1 bv2 : BitVec w1) (heq : w1 = w2) :
    evalRelation rel (heq ▸ bv1) (heq ▸ bv2) = evalRelation rel bv1 bv2

@[grind =, simp]
lemma RawCNFA.addInitial_finals {m : RawCNFA A} : (m.addInitial s).finals = m.finals

theorem icmp_sgt6_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ (x <<< 1#8).sshiftRight' 1#8 ≠ x ∨ 1#8 ≥ ↑8) → ofBool (16#8 <ₛ x <<< 1#8) = ofBool (8#8 <ₛ x)

theorem pb_thm (e : IntW 65) :
  icmp IntPred.eq e (ashr (shl e (const? 65 1)) (const? 65 1) { «exact» := true }) ⊑
    icmp IntPred.sgt (add e (const? 65 9223372036854775808)) (const? 65 (-1))

theorem e_1084 :
     - 6 * t + 1 *  ~~~(z &&& t) + 1 * z - 6 *  ~~~(z ^^^ t) - 1 * (z ||| t) + 5 *  ~~~(z ||| t) + 6 *  ~~~(z |||  ~~~t) - 1 * (z &&&  ~~~t) =  - 12 * (z &&& t)

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

theorem exact_ashr_ne_both_equal_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ BitVec.ofInt 8 (-128) >>> x <<< x ≠ BitVec.ofInt 8 (-128) ∨ x ≥ ↑8) →
    ofBool ((BitVec.ofInt 8 (-128)).sshiftRight' x != BitVec.ofInt 8 (-128)) = ofBool (x != 0#8)

theorem sge_to_ugt_proof : sge_to_ugt_before ⊑ sge_to_ugt_after

theorem bools_logical_commute0_and2_thm.extracted_1._11 : ∀ (x x_1 x_2 : BitVec 1),
  x_2 ^^^ 1#1 = 1#1 → x_2 = 1#1 → x_1 = 1#1 → 1#1 = x

theorem main4f_like_logical_thm.extracted_1._5 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 &&& x_1 != x_1) = 1#1 →
    ofBool (x_2 &&& x_1 == x_1) = 1#1 → True → 0#32 = zeroExtend 32 (ofBool (x_2 &&& x == x))

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

theorem select_or_icmp_bad_proof : select_or_icmp_bad_before ⊑ select_or_icmp_bad_after

theorem test6_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬32#128 ≥ ↑128 →
    ¬(32#64 ≥ ↑64 ∨ True ∧ zeroExtend 64 (truncate 32 (x >>> 32#64)) ≠ x >>> 32#64) →
      truncate 32 (zeroExtend 128 x >>> 32#128) = truncate 32 (x >>> 32#64)

theorem e_1485 :
     - 2 *  ~~~(z &&&  ~~~t) + 2 *  ~~~(z &&& t) + 5 * z + 1 * (z |||  ~~~t) - 2 *  ~~~z + 3 *  ~~~(z ^^^ t) + 1 * (z ^^^ t) - 3 *  ~~~(z &&&  ~~~z) + 1 *  ~~~(z ||| t) + 12 *  ~~~(z |||  ~~~t) + 4 * (z &&& t) = 2 * t + 6 * (z ||| t)

@[simp]
theorem Factor.numVars_term : (Factor.var n).numVars = n + 1

theorem sel_false_val_is_a_masked_ashr_of_true_val1_proof : sel_false_val_is_a_masked_ashr_of_true_val1_before ⊑ sel_false_val_is_a_masked_ashr_of_true_val1_after

theorem select_bittest_to_add_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 1#32 == 0#32) = 1#1 →
    True ∧ (x &&& 1#32).saddOverflow 3#32 = true ∨ True ∧ (x &&& 1#32).uaddOverflow 3#32 = true → False

theorem ashrsgt_01_09_proof : ashrsgt_01_09_before ⊑ ashrsgt_01_09_after

theorem nomask_rhs_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 1#32 == 0#32) ||

theorem e_1735 :
    4 * ( ~~~(a &&&  ~~~b) &&&  ~~~(b ^^^ c)) - 1 *  ~~~(b &&&  ~~~c) - 5 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) - 1 * (b ^^^ ( ~~~a &&& ( ~~~b ||| c))) - 11 * (b ^^^  ~~~( ~~~a &&& (b ^^^ c))) - 7 * (c ^^^  ~~~(a |||  ~~~b)) - 6 * (b ^^^ (a ||| c)) + 1 * ( ~~~b ||| (a ^^^ c)) - 2 * ((a &&& b) ||| (a ^^^ (b ^^^ c))) - 1 * ((a &&& b) ^^^  ~~~(a ^^^ (b &&& c))) - 2 * (b &&& c) - 6 * (b |||  ~~~(a |||  ~~~c)) + 1 * (a ||| b) - 1 *  ~~~(a &&& (b &&& c)) + 11 * ((b &&&  ~~~c) |||  ~~~(a ||| ( ~~~b &&& c))) + 4 * ( ~~~(a &&&  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) + 4 * (c ^^^ (a ||| (b ||| c))) + 2 * (b ^^^ (a ||| ( ~~~b ||| c))) - 7 * ( ~~~c &&&  ~~~(a ^^^ b)) + 4 *  ~~~( ~~~a ||| (b ^^^ c)) - 3 * (c ^^^ ( ~~~a ||| ( ~~~b ||| c))) + 1 * (c ^^^ (a ||| ( ~~~b ||| c))) + 3 * (c ^^^  ~~~(a ||| (b &&& c))) + 4 * (c ^^^  ~~~(a &&&  ~~~b)) - 5 *  ~~~(a ||| (b ||| c)) + 13 *  ~~~(a ||| ( ~~~b ||| c)) + 11 *  ~~~( ~~~a ||| (b ||| c)) - 13 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 27 * ( ~~~a &&& ( ~~~b &&& c)) - 19 * ( ~~~a &&& (b &&& c)) + 15 * (a &&& ( ~~~b &&& c)) + 7 * (a &&& (b &&& c)) =  - 5 * (b ^^^  ~~~(a ||| c))

theorem trunc_lshr_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬2#8 ≥ ↑8 → ¬2#6 ≥ ↑6 → truncate 6 (x >>> 2#8) &&& 14#6 = truncate 6 x >>> 2#6 &&& 14#6

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

theorem main12_logical_proof : main12_logical_before ⊑ main12_logical_after

theorem ashrsgt_03_01_exact_proof : ashrsgt_03_01_exact_before ⊑ ashrsgt_03_01_exact_after

theorem icmp_slt_0_or_icmp_sge_neg1_i32_proof : icmp_slt_0_or_icmp_sge_neg1_i32_before ⊑ icmp_slt_0_or_icmp_sge_neg1_i32_after

theorem foo_proof : foo_before ⊑ foo_after

theorem zext_sext_add_icmp_slt_1_rhs_not_const_thm (e : IntW 8) (e_1 e_2 : IntW 1) :
  icmp IntPred.slt (add (zext 8 e_2) (sext 8 e_1)) e ⊑
    icmp IntPred.slt (add (zext 8 e_2) (sext 8 e_1) { «nsw» := true, «nuw» := false }) e

theorem t1_ult_slt_0_proof : t1_ult_slt_0_before ⊑ t1_ult_slt_0_after

theorem src_fv_ne_proof : src_fv_ne_before ⊑ src_fv_ne_after

theorem eq_21_comm_eq_thm (e e_1 : IntW 32) :
  LLVM.and (icmp IntPred.eq (trunc 8 (lshr e_1 (const? 32 16))) (trunc 8 (lshr e (const? 32 16))))
      (icmp IntPred.eq (trunc 8 (lshr e (const? 32 8))) (trunc 8 (lshr e_1 (const? 32 8)))) ⊑
    icmp IntPred.eq (trunc 16 (lshr e_1 (const? 32 8))) (trunc 16 (lshr e (const? 32 8)))

theorem e_1045 :
     - 1 *  ~~~(z &&&  ~~~t) + 1 *  ~~~(z &&&  ~~~z) + 1 * (z ||| t) - 5 * (z |||  ~~~t) + 1 *  ~~~(z |||  ~~~t) + 5 * (z &&&  ~~~t) + 4 * (z &&& t) = 2 *  ~~~(z &&& t) - 7 *  ~~~(z ||| t)

theorem XorZextXor_thm.extracted_1._1 : ∀ (x : BitVec 3), zeroExtend 5 (x ^^^ 3#3) ^^^ 12#5 = zeroExtend 5 x ^^^ 15#5

theorem _root_.AList.mem_of_mem_entries {α : Type _} {β : α → Type _} {s : AList β}
    {k : α} {v : β k} :
    ⟨k, v⟩ ∈ s.entries → k ∈ s

theorem shift_xor_multiuse_or_thm (e e_1 : IntW 32) :
  mul (select (icmp IntPred.ne (const? 32 0) (LLVM.and e_1 (const? 32 4096))) e (LLVM.or e (const? 32 2048)))
      (LLVM.or e (const? 32 2048)) ⊑
    mul (select (icmp IntPred.eq (LLVM.and e_1 (const? 32 4096)) (const? 32 0)) (LLVM.or e (const? 32 2048)) e)
      (LLVM.or e (const? 32 2048))

theorem sub_to_xor_and_commuted_proof : sub_to_xor_and_commuted_before ⊑ sub_to_xor_and_commuted_after

theorem and_ne_with_diff_one_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (x != 40#32) = 1#1 → 0#1 = ofBool (x + BitVec.ofInt 32 (-41) <ᵤ BitVec.ofInt 32 (-2))

theorem t0_shl_proof : t0_shl_before ⊑ t0_shl_after

theorem slt_smin3_thm (e e_1 : IntW 32) :
  icmp IntPred.sgt (add e_1 (const? 32 3))
      (select (icmp IntPred.slt (add e_1 (const? 32 3)) e) (add e_1 (const? 32 3)) e) ⊑
    icmp IntPred.slt e (add e_1 (const? 32 3))

theorem nomask_rhs_proof : nomask_rhs_before ⊑ nomask_rhs_after
</all_available_lemmas>

<local_ctx>
import Mathlib.Data.Fintype.Card

import Mathlib.Data.Fintype.Sum

import Mathlib.Data.Fintype.Sigma

import Mathlib.Data.Fintype.BigOperators

import Mathlib.Tactic.Zify

import Mathlib.Tactic.Ring

import Blase.Fast.Defs

import Blase.Fast.BitStream

open Term
</local_ctx>

<target_theorem>
lemma Predicate.evalFin_eq_eval (p : Predicate)
   (varsList : List BitStream) (varsFin : Fin p.arity → BitStream)
   (hvars : ∀ (i : Fin p.arity), varsList.getD i default = (varsFin i)) :
    Predicate.evalFin p varsFin  = Predicate.eval p varsList :=
</target_theorem>

