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>
BitVec in Init.Prelude
List in Init.Prelude
List.Vector in Mathlib.Data.Vector.Defs
Nat in Init.Prelude
Set in Mathlib.Data.Set.Defs
NFA in Mathlib.Computability.NFA
Language in Mathlib.Computability.Language
BitVec.cons in Init.Data.BitVec.Basic
List.Vector.ofFn in Mathlib.Data.Vector.Defs
List.Vector.replicate in Mathlib.Data.Vector.Defs
Bool in Init.Prelude
Fin in Init.Prelude
BitVec.iunfoldr in Init.Data.BitVec.Folds
List.finRange in Init.Data.List.FinRange
List.reverseRecOn in Mathlib.Data.List.Induction

structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def enc (bvs : BitVecs n) : BitVecs' n :=
  (List.finRange bvs.w).map (fun i =>
    BitVec.ofFn (fun (k : Fin n) => (bvs.bvs.get k)[i]))

abbrev BitVecs' (n : Nat) := List (BitVec n)

def BitVec.ofFn {w : Nat} (f : Fin w → Bool) : BitVec w :=
  BitVec.iunfoldr (fun i _ => ((), f i)) () |>.2

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

def accepts (M : NFA' n) : Set (BitVecs n) := dec '' M.accepts'

structure NFA' (n : Nat) where
  σ : Type
  M : NFA (BitVec n) σ

def accepts' (M : NFA' n) : Set (BitVecs' n) := M.M.accepts

def BitStream : Type := Nat → Bool

@[inline]
def CNFA.proj (m: CNFA n2) (f : Fin n1 → Fin n2) : CNFA n1 :=
  ⟨m.m.proj f, m.m.proj_wf m.wf⟩

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

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

private def tensor2dTest : MLIRTy := [mlir_type| tensor2d]

def sext_sub_nuw_before := [llvm|
{
^0(%arg14 : i8, %arg15 : i1):
  %0 = llvm.sext %arg15 : i1 to i8
  %1 = llvm.sub %arg14, %0 overflow<nuw> : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def test9_after := [llvm|
{
^0(%arg111 : i32, %arg112 : i32):
  %0 = llvm.or %arg111, %arg112 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

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

def and_and_logic_or_1_before := [llvm|
{
^0(%arg102 : i1, %arg103 : i1, %arg104 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.and %arg102, %arg103 : i1
  %2 = llvm.and %arg102, %arg104 : i1
  %3 = "llvm.select"(%1, %0, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

Prod in Init.Prelude

def trunc_sel_larger_sext_after := [llvm|
{
^0(%arg85 : i32, %arg86 : i1):
  %0 = llvm.mlir.constant(42) : i64
  %1 = llvm.trunc %arg85 : i32 to i16
  %2 = llvm.sext %1 : i16 to i64
  %3 = "llvm.select"(%arg86, %2, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  "llvm.return"(%3) : (i64) -> ()
}
]

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

def ugt_swap_or_not_min_logical_after := [llvm|
{
^0(%arg4 : i8, %arg5 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.icmp "ne" %arg4, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

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

instance : Lean.ToExpr (LLVM.Ty) :=

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

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

def ashrsgt_02_14_exact_after := [llvm|
{
^0(%arg71 : i4):
  %0 = llvm.mlir.constant(-8 : i4) : i4
  %1 = llvm.icmp "ne" %arg71, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def State.cseArgList
 [TyDenote d.Ty] [DialectSignature d] [DialectDenote d]
  {Γstart Γ : Ctxt d.Ty} {lets : Lets d Γstart .pure Γ} (s : State d lets)
  {ts : List d.Ty}
  (as : HVector (Ctxt.Var Γ) <| ts) :
  { as' : HVector (Ctxt.Var Γ) <| ts // ∀ (V : Γstart.Valuation),
    as.map (lets.denote V).eval = as'.map (lets.denote V).eval  } :=
  match as with
  | .nil => ⟨.nil, by admit /- proof elided -/
    ⟩
  | .cons a as =>
    let ⟨a', ha'⟩ :=  s.var2var a
    let ⟨as', has'⟩ := s.cseArgList as
    ⟨.cons a' as', by admit /- proof elided -/
    ⟩

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

def Com.letPure (e : Expr d Γ .pure t) (body : Com d (e.outContext) eff u) : Com d Γ eff u :=
  body.var (e.castPureToEff eff)

def shl_and_and_fail_before := [llvm|
{
^0(%arg170 : i8, %arg171 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.mlir.constant(5 : i8) : i8
  %2 = llvm.mlir.constant(88 : i8) : i8
  %3 = llvm.shl %arg170, %0 : i8
  %4 = llvm.shl %arg171, %1 : i8
  %5 = llvm.and %4, %2 : i8
  %6 = llvm.and %3, %5 : i8
  "llvm.return"(%6) : (i8) -> ()
}
]

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

def or_xor_tree_1010_after := [llvm|
{
^0(%arg15 : i32, %arg16 : i32, %arg17 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mul %arg15, %0 : i32
  %2 = llvm.mul %arg16, %0 : i32
  %3 = llvm.mul %arg17, %0 : i32
  %4 = llvm.xor %1, %2 : i32
  %5 = llvm.or %4, %3 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def test6_before := [llvm|
{
^0(%arg51 : i1023):
  %0 = llvm.mlir.constant(64 : i1023) : i1023
  %1 = llvm.mlir.constant(0 : i1023) : i1023
  %2 = llvm.and %arg51, %0 : i1023
  %3 = llvm.icmp "ne" %2, %1 : i1023
  %4 = "llvm.select"(%3, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1023, i1023) -> i1023
  "llvm.return"(%4) : (i1023) -> ()
}
]

def positive_samevar_before := [llvm|
{
^0(%arg62 : i8, %arg63 : i8):
  %0 = llvm.lshr %arg62, %arg63 : i8
  %1 = llvm.shl %0, %arg63 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def and_or3_before := [llvm|
{
^0(%arg168 : i1, %arg169 : i1, %arg170 : i32, %arg171 : i32):
  %0 = llvm.icmp "eq" %arg170, %arg171 : i32
  %1 = llvm.and %arg169, %0 : i1
  %2 = "llvm.select"(%1, %arg168, %arg169) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%2) : (i1) -> ()
}
]

def trunc_equality_nsw_zext_after := [llvm|
{
^0(%arg16 : i32, %arg17 : i8):
  %0 = llvm.zext %arg17 : i8 to i32
  %1 = llvm.icmp "ne" %arg16, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def eq_umin1_before := [llvm|
{
^0(%arg60 : i32, %arg61 : i32):
  %0 = llvm.icmp "ult" %arg60, %arg61 : i32
  %1 = "llvm.select"(%0, %arg60, %arg61) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "eq" %1, %arg60 : i32
  "llvm.return"(%2) : (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 udiv_i32_after := [llvm|
{
^0(%arg29 : i8, %arg30 : i8):
  %0 = llvm.udiv %arg29, %arg30 : i8
  %1 = llvm.zext %0 : i8 to i32
  "llvm.return"(%1) : (i32) -> ()
}
]

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

def demorgan_nand_before := [llvm|
{
^0(%arg38 : i8, %arg39 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.xor %arg38, %0 : i8
  %2 = llvm.and %1, %arg39 : i8
  %3 = llvm.xor %2, %0 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

partial def reflectFactor (e : Expr) : M Factor := do
  match_expr e with
  | HAnd.hAnd _bv _bv _bv _inst a b =>
     return Factor.and (← reflectFactor a) (← reflectFactor b)
  | HOr.hOr _bv _bv _bv _inst a b =>
     return Factor.or (← reflectFactor a) (← reflectFactor b)
  | HXor.hXor _bv _bv _bv _inst a b =>
     return Factor.xor (← reflectFactor a) (← reflectFactor b)
  | Complement.complement _bv _inst a =>
     return Factor.not (← reflectFactor a)
  | _ =>
    let s ← get
    match s.e2ix[e]? with
    | .some ix => return Factor.var ix
    | .none => do
       let ix := s.e2ix.size
       set { s with e2ix := s.e2ix.insert e ix }
       return .var ix

def llvm_const_lower_riscv_li49 : LLVMPeepholeRewriteRefine 64 [] :=
  {lhs := constLLVM49, rhs:= liRiscv49,
   correct := by admit /- proof elided -/

def test9_after := [llvm|
{
^0(%arg5 : i1005):
  "llvm.return"(%arg5) : (i1005) -> ()
}
]

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

def p_commutative0_after := [llvm|
{
^0(%arg32 : i32, %arg33 : i32, %arg34 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg34, %arg32 : i32
  %2 = llvm.xor %arg34, %0 : i32
  %3 = llvm.and %arg33, %2 : i32
  %4 = llvm.or disjoint %1, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def or_logic_or_logic_and_8_before := [llvm|
{
^0(%arg27 : i1, %arg28 : i1, %arg29 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.or %arg28, %arg27 : i1
  %3 = "llvm.select"(%arg29, %0, %arg27) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%3, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def test3_after := [llvm|
{
^0(%arg2 : i32, %arg3 : i32):
  %0 = llvm.add %arg2, %arg3 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def processOneElem_mot (s : State) (sa : S) (n : ℕ) (st : worklist.St A S) : Prop :=
  st.map[sa]? = some s ∧
  sa ∈ st.visited ∧
  StInv A S st.m st.map ∧
  st.sim inits final f  {(sa1, a, sa') | sa1 = sa ∧ ∃ k ≥ n, (f sa)[k]? = some (a, sa') }

def ugt_and_min_logical_before := [llvm|
{
^0(%arg334 : i8, %arg335 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "ugt" %arg334, %arg335 : i8
  %3 = llvm.icmp "eq" %arg334, %0 : i8
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

def t0_after := [llvm|
{
^0(%arg206 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.add %arg206, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

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

def sub_ult_zext_before := [llvm|
{
^0(%arg161 : i1, %arg162 : i8, %arg163 : i8):
  %0 = llvm.zext %arg161 : i1 to i8
  %1 = llvm.sub %arg162, %arg163 : i8
  %2 = llvm.icmp "ult" %1, %0 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

@[simp_denote]
def lshr_llvm_exact_64 := [LV| {
  ^entry (%x: i64, %amount: i64):
    %1 = llvm.lshr exact %x, %amount : i64
    llvm.return %1 : i64
  }]

def or_simplify_ule_fail_before := [llvm|
{
^0(%arg13 : i8, %arg14 : i8):
  %0 = llvm.mlir.constant(64 : i8) : i8
  %1 = llvm.mlir.constant(127 : i8) : i8
  %2 = llvm.or %arg13, %0 : i8
  %3 = llvm.and %arg14, %1 : i8
  %4 = llvm.or %2, %3 : i8
  %5 = llvm.icmp "ule" %4, %3 : i8
  "llvm.return"(%5) : (i1) -> ()
}
]

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

def pr51551_neg1_after := [llvm|
{
^0(%arg4 : i32, %arg5 : i32):
  %0 = llvm.mlir.constant(4 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.mlir.constant(7 : i32) : i32
  %3 = llvm.mlir.constant(0 : i32) : i32
  %4 = llvm.and %arg5, %0 : i32
  %5 = llvm.or disjoint %4, %1 : i32
  %6 = llvm.mul %5, %arg4 : i32
  %7 = llvm.and %6, %2 : i32
  %8 = llvm.icmp "eq" %7, %3 : i32
  "llvm.return"(%8) : (i1) -> ()
}
]

def udiv_common_divisor_before := [llvm|
{
^0(%arg65 : i1, %arg66 : i5, %arg67 : i5, %arg68 : i5):
  %0 = llvm.udiv %arg67, %arg66 : i5
  %1 = llvm.udiv %arg68, %arg66 : i5
  %2 = "llvm.select"(%arg65, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i5, i5) -> i5
  "llvm.return"(%2) : (i5) -> ()
}
]

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

def logic_or_logic_and_7_before := [llvm|
{
^0(%arg69 : i1, %arg70 : i1, %arg71 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.mlir.constant(false) : i1
  %2 = "llvm.select"(%arg70, %0, %arg69) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = "llvm.select"(%arg71, %0, %arg69) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%3, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def ashrslt_03_00_exact_before := [llvm|
{
^0(%arg21 : i4):
  %0 = llvm.mlir.constant(3 : i4) : i4
  %1 = llvm.mlir.constant(0 : i4) : i4
  %2 = llvm.ashr exact %arg21, %0 : i4
  %3 = llvm.icmp "slt" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def test5_after := [llvm|
{
^0(%arg95 : i32, %arg96 : i8):
  %0 = llvm.mlir.constant(32 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.zext nneg %arg96 : i8 to i32
  %3 = llvm.shl %0, %2 overflow<nuw> : i32
  %4 = llvm.add %3, %1 : i32
  %5 = llvm.and %arg95, %4 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def ashrslt_02_00_exact_before := [llvm|
{
^0(%arg37 : i4):
  %0 = llvm.mlir.constant(2 : i4) : i4
  %1 = llvm.mlir.constant(0 : i4) : i4
  %2 = llvm.ashr exact %arg37, %0 : i4
  %3 = llvm.icmp "slt" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def t1_sub_from_falseval_after := [llvm|
{
^0(%arg10 : i1, %arg11 : i8, %arg12 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %arg12, %arg11 : i8
  %2 = "llvm.select"(%arg10, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def t0_ult_slt_65536_after := [llvm|
{
^0(%arg66 : i32, %arg67 : i32, %arg68 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(65535 : i32) : i32
  %2 = llvm.icmp "slt" %arg66, %0 : i32
  %3 = llvm.icmp "sgt" %arg66, %1 : i32
  %4 = "llvm.select"(%2, %arg67, %arg66) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %5 = "llvm.select"(%3, %arg68, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def icmp_ne_zext_ne_non_boolean_after := [llvm|
{
^0(%arg33 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.icmp "ne" %arg33, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

@[simp_denote]
def select_llvm_64 := [LV| {
  ^entry (%cond : i1, %arg0: i64, %arg1: i64):
    %0 = "llvm.select"(%cond, %arg0, %arg1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
    llvm.return %0 : i64
  }]

Function.LeftInverse in Init.Data.Function

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

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

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

def select_sub_icmp_after := [llvm|
{
^0(%arg214 : i32, %arg215 : i32, %arg216 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "eq" %arg214, %0 : i32
  %2 = "llvm.select"(%1, %arg216, %arg215) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def not_signbit_trunc_before := [llvm|
{
^0(%arg16 : i16):
  %0 = llvm.mlir.constant(-1 : i16) : i16
  %1 = llvm.mlir.constant(15 : i16) : i16
  %2 = llvm.xor %arg16, %0 : i16
  %3 = llvm.lshr %2, %1 : i16
  %4 = llvm.trunc %3 : i16 to i8
  "llvm.return"(%4) : (i8) -> ()
}
]

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

def main12_logical_before := [llvm|
{
^0(%arg19 : i32):
  %0 = llvm.mlir.constant(0 : i16) : i16
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.mlir.constant(true) : i1
  %3 = llvm.mlir.constant(2 : i32) : i32
  %4 = llvm.mlir.constant(1 : i32) : i32
  %5 = llvm.trunc %arg19 : i32 to i16
  %6 = llvm.icmp "slt" %5, %0 : i16
  %7 = llvm.trunc %arg19 : i32 to i8
  %8 = llvm.icmp "slt" %7, %1 : i8
  %9 = "llvm.select"(%6, %2, %8) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %10 = "llvm.select"(%9, %3, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%10) : (i32) -> ()
}
]

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

repr in Init.Data.Repr
</all_available_defs>

<all_available_lemmas>
NFA.eval_append_singleton in Mathlib.Computability.NFA
NFA.eval_nil in Mathlib.Computability.NFA

@[ext]
theorem ext {x y : BitStream} (h : ∀ i, x i = y i) : x = y

theorem and_orn_cmp_1_logical_proof : and_orn_cmp_1_logical_before ⊑ and_orn_cmp_1_logical_after

theorem and_not_or_wrong_c_proof : and_not_or_wrong_c_before ⊑ and_not_or_wrong_c_after

theorem AvoidCollision_toFin_signExtend_of_le {x : BitVec w} (hv : v ≤ w):
    (x.signExtend v).toFin = Fin.ofNat (2 ^ v) x.toNat

theorem add_nsw_const_const_sub_nsw_thm (e : IntW 8) :
  sub (const? 8 (-127)) (add e (const? 8 1) { «nsw» := true, «nuw» := false }) { «nsw» := true, «nuw» := false } ⊑
    sub (const? 8 (-128)) e { «nsw» := true, «nuw» := false }

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

theorem ashrsgt_01_01_proof : ashrsgt_01_01_before ⊑ ashrsgt_01_01_after

theorem logical_and_icmps2_proof : logical_and_icmps2_before ⊑ logical_and_icmps2_after

theorem no_shift_xor_multiuse_cmp_xor_thm.extracted_1._4 : ∀ (x x_1 x_2 x_3 : BitVec 32),
  ¬ofBool (0#32 != x_3 &&& 4096#32) = 1#1 →
    ¬ofBool (x_3 &&& 4096#32 == 0#32) = 1#1 →
      (x_2 ^^^ 4096#32) * x * (x_2 ^^^ 4096#32) = x_2 * x_1 * (x_2 ^^^ 4096#32)

theorem shift_xor_multiuse_cmp_proof : shift_xor_multiuse_cmp_before ⊑ shift_xor_multiuse_cmp_after

theorem select_icmp_slt_zero_smin_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (x <ₛ 0#8) = 1#1 → x = x ||

theorem not_cond_proof : not_cond_before ⊑ not_cond_after

theorem lshrugt_03_08_exact_proof : lshrugt_03_08_exact_before ⊑ lshrugt_03_08_exact_after

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

theorem sge_to_ult_proof : sge_to_ult_before ⊑ sge_to_ult_after

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

lemma eval_bind : ∀ (c : Circuit α) (f : α → Circuit β) (g : β → Bool),
    eval (bind c f) g = eval c (λ a => eval (f a) g)

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

theorem select_icmp_eq_and_32_0_xor_8_thm.extracted_1._3 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x_1 &&& 32#32 == 0#32) = 1#1 → 2#32 ≥ ↑32 → False

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

theorem bitwise_and_bitwise_and_icmps_comm1_thm (e e_1 e_2 : IntW 8) :
  LLVM.and (icmp IntPred.ne (LLVM.and e_2 (shl (const? 8 1) e_1)) (const? 8 0))
      (LLVM.and (icmp IntPred.eq e (const? 8 42))
        (icmp IntPred.ne (LLVM.and e_2 (const? 8 1)) (const? 8 0))) ⊑
    LLVM.and (icmp IntPred.eq e (const? 8 42))
      (icmp IntPred.eq
        (LLVM.and e_2 (LLVM.or (shl (const? 8 1) e_1 { «nsw» := false, «nuw» := true }) (const? 8 1)))
        (LLVM.or (shl (const? 8 1) e_1 { «nsw» := false, «nuw» := true }) (const? 8 1)))

theorem test1_thm (e : IntW 33) : LLVM.xor (LLVM.xor e (const? 33 (-1))) (const? 33 (-1)) ⊑ e

theorem negative_not_power_of_two_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (-1#32 <ₛ x) = 1#1 → 0#1 = ofBool (x == 0#32)

theorem sle_smax4_proof : sle_smax4_before ⊑ sle_smax4_after

theorem lshr_shl_pow2_const_case1_proof : lshr_shl_pow2_const_case1_before ⊑ lshr_shl_pow2_const_case1_after

theorem negative_not_power_of_two_logical_proof : negative_not_power_of_two_logical_before ⊑ negative_not_power_of_two_logical_after

theorem xor_icmp_to_icmp_add_thm (e : IntW 32) :
  LLVM.xor (icmp IntPred.sgt e (const? 32 3)) (icmp IntPred.slt e (const? 32 6)) ⊑
    icmp IntPred.ult (add e (const? 32 (-6))) (const? 32 (-2))

theorem lor_land_right1_thm (e e_1 : IntW 1) : select e_1 (select e_1 (const? 1 1) e) (const? 1 0) ⊑ e_1

theorem e_2399 :
     - 1 * (f &&& (d ^^^ e)) + 1 * ((d ^^^ e) |||  ~~~(d ^^^ f)) + 3 * ((d &&& e) |||  ~~~(d ^^^ (e ^^^ f))) - 5 * (f ^^^ (d &&& e)) - 5 * (e ^^^ ( ~~~d &&& (e ||| f))) + 11 * (d ^^^ e) - 2 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) - 7 * (f ^^^  ~~~(d &&& (e &&& f))) + 5 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) - 5 * ((d &&& e) ^^^ (e ||| f)) + 1 * (e |||  ~~~(d ^^^ f)) - 5 * (e ^^^ ( ~~~d ||| (e &&& f))) + 1 * (f ^^^  ~~~(d ||| (e &&& f))) - 3 * (f ^^^ (d ||| ( ~~~e ||| f))) + 3 * (e ||| (d &&&  ~~~f)) + 2 * (f |||  ~~~(d |||  ~~~e)) - 5 * (f &&&  ~~~(d ^^^ e)) + 4 * ( ~~~f |||  ~~~(d ^^^ e)) + 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) - 7 * ((e &&&  ~~~f) ^^^ ( ~~~d ||| (e ^^^ f))) + 7 * (f ^^^ (d ||| e)) - 3 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) - 1 * (e |||  ~~~(d ||| f)) - 11 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) + 3 * (f ^^^ ( ~~~d &&& (e ||| f))) + 11 * (d ^^^ ( ~~~e &&& f)) - 7 * (e &&& (d ^^^ f)) + 1 * (f ^^^ (d |||  ~~~e)) - 11 * ( ~~~f &&&  ~~~(d ^^^ e)) + 2 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) + 4 *  ~~~( ~~~d &&& (e &&& f)) - 2 * (e &&&  ~~~(d &&& f)) - 11 * (f ^^^  ~~~(d &&&  ~~~e)) - 2 *  ~~~(e &&&  ~~~f) - 2 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) - 1 * (f ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) - 3 *  ~~~(d &&& e) - 11 * ( ~~~(d &&& e) &&& (e ^^^ f)) - 1 * (f ^^^ ( ~~~d &&& ( ~~~e ||| f))) + 1 * e - 3 * (f |||  ~~~(d ||| e)) + 5 * ( ~~~e ||| (d ^^^ f)) - 1 * (e ^^^  ~~~(d ||| (e &&& f))) + 4 * (d &&& e) - 1 * ((d ^^^ e) ||| (d ^^^ f)) - 5 * (e ^^^  ~~~(d &&&  ~~~f)) + 2 * (e &&&  ~~~(d &&&  ~~~f)) - 1 * (e ^^^ (d ||| (e ||| f))) + 4 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 1 * (f ^^^  ~~~(d ||| e)) + 3 *  ~~~(e ^^^ f) - 11 * (d ||| (e &&& f)) - 7 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) - 3 * (f ||| (d ^^^ e)) - 2 * ( ~~~(d |||  ~~~e) |||  ~~~(e ^^^ f)) - 11 * ((d ||| e) &&&  ~~~(e ^^^ f)) - 7 * (f ||| (d &&& e)) + 3 * (f ||| (d &&&  ~~~e)) - 6 * ((d &&& f) ^^^ (d ^^^ (e &&& f))) + 1 *  ~~~( ~~~d ||| ( ~~~e &&& f)) + 11 *  ~~~(d ^^^ (e ||| f)) - 1 * (e ^^^  ~~~( ~~~d &&& (e ^^^ f))) + 4 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) + 3 * (f &&& (d ||| e)) + 2 * (f ^^^  ~~~(d |||  ~~~e)) + 47 *  ~~~(d ||| (e ||| f)) + 12 *  ~~~(d ||| ( ~~~e ||| f)) + 6 *  ~~~( ~~~d ||| (e ||| f)) + 34 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 48 * ( ~~~d &&& ( ~~~e &&& f)) + 38 * (d &&& ( ~~~e &&& f)) + 6 * (d &&& (e &&& f)) =  - 42 * ( ~~~d &&& (e &&& f))

theorem trunc_sandwich_max_sum_shift2_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(30#32 ≥ ↑32 ∨ 1#12 ≥ ↑12) →
    31#32 ≥ ↑32 ∨
        True ∧ signExtend 32 (truncate 12 (x >>> 31#32)) ≠ x >>> 31#32 ∨
          True ∧ zeroExtend 32 (truncate 12 (x >>> 31#32)) ≠ x >>> 31#32 →
      False

theorem xor_2_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 1) (x_2 : BitVec 8),
  x_1 = 1#1 → x_2 ^^^ (x ^^^ -1#8) ^^^ -1#8 = x_2 ^^^ x

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

theorem isRefinedBy_ite_iff {x? y? z? : PoisonOr α} :
    x? ⊑ ite c y? z?
    ↔ let c := c
      (c → x? ⊑ y?) ∧ (¬c → x? ⊑ z?)

theorem test_or3_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 &&& 2147483647#32 ≤ₛ x) ||

theorem ashr_ult_11_proof : ashr_ult_11_before ⊑ ashr_ult_11_after

theorem e_1360 :
    7 *  ~~~(z ^^^ t) - 5 *  ~~~(z &&&  ~~~z) - 3 * (z ||| t) - 6 *  ~~~(z &&&  ~~~t) - 1 *  ~~~(z &&& t) + 11 *  ~~~t + 2 * (z ^^^ t) - 6 *  ~~~(z ||| t) + 14 *  ~~~(z |||  ~~~t) + 8 * (z &&& t) = 4 * (z &&&  ~~~t) + 1 * t

theorem ult_swap_or_not_max_commute_logical_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (x != -1#8) = 1#1 → 1#1 = ofBool (x != -1#8)

theorem ashrslt_03_03_proof : ashrslt_03_03_before ⊑ ashrslt_03_03_after

theorem n10_thm (e : IntW 8) :
  icmp IntPred.sgt (sub (const? 8 0) e) e ⊑ icmp IntPred.slt e (sub (const? 8 0) e)

theorem no_shift_no_xor_multiuse_cmp_xor_thm (e e_1 e_2 e_3 : IntW 32) :
  mul
      (mul
        (select (icmp IntPred.eq (LLVM.and e_3 (const? 32 4096)) (const? 32 0)) e_2
          (LLVM.xor e_2 (const? 32 4096)))
        (select (icmp IntPred.eq (LLVM.and e_3 (const? 32 4096)) (const? 32 0)) e_1 e))
      (LLVM.xor e_2 (const? 32 4096)) ⊑
    mul
      (mul (LLVM.xor e_2 (LLVM.and e_3 (const? 32 4096)))
        (select (icmp IntPred.eq (LLVM.and e_3 (const? 32 4096)) (const? 32 0)) e_1 e))
      (LLVM.xor e_2 (const? 32 4096))

theorem test8_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬16#32 ≥ ↑32 → 16#32 ≥ ↑32 ∨ True ∧ (x.sshiftRight' 16#32).smulOverflow 32767#32 = true → False

theorem zext_zext_ule_op0_wide_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 9),
  ofBool (zeroExtend 32 x_1 ≤ᵤ zeroExtend 32 x) = ofBool (x_1 ≤ᵤ zeroExtend 9 x)

theorem test_mul_nuw__all_are_safe_proof : test_mul_nuw__all_are_safe_before ⊑ test_mul_nuw__all_are_safe_after

theorem test2_thm.extracted_1._1 : ∀ (x : BitVec 1005), x ^^^ 0#1005 = x

theorem sle_and_min_proof : sle_and_min_before ⊑ sle_and_min_after

theorem test22_logical_proof : test22_logical_before ⊑ test22_logical_after

theorem t4_proof : t4_before ⊑ t4_after

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

theorem icmp_select_var_select_thm.extracted_1._16 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1),
  ¬x_2 = 1#1 → ¬(ofBool (x_1 == 0#8) = 1#1 ∧ x_2 = 1#1) → ofBool (x_1 == 0#8) = 1#1 → True → ofBool (x == x) = 1#1

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

theorem ashrsgt_01_15_exact_proof : ashrsgt_01_15_exact_before ⊑ ashrsgt_01_15_exact_after

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

@[simp] theorem MatchVarM.liftM_eq_some_iff (x? : Option α) :
    (liftM x? : no_index MatchVarM Δ Γ α) mapIn = some (x, mapOut)
    ↔ x? = some x ∧ mapIn = mapOut

theorem and_consts_thm (e : IntW 32) :
  LLVM.or (icmp IntPred.eq (LLVM.and (const? 32 4) e) (const? 32 0))
      (icmp IntPred.eq (LLVM.and (const? 32 8) e) (const? 32 0)) ⊑
    icmp IntPred.ne (LLVM.and e (const? 32 12)) (const? 32 12)

theorem bv_AndOrXor_887_2 :
    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.icmp LLVM.IntPred.eq e e_1) (LLVM.icmp LLVM.IntPred.ne e e_1) ⊑ LLVM.const? 1 0

theorem test8_thm (e e_1 : IntW 32) :
  trunc 64 (LLVM.or (shl (zext 128 e_1) (const? 128 32)) (zext 128 e)) ⊑
    LLVM.or (shl (zext 64 e_1) (const? 64 32) { «nsw» := false, «nuw» := true }) (zext 64 e)
      { «disjoint» := true }

theorem select_icmp_ne_0_and_8_xor_1073741824_thm.extracted_1._1 : ∀ (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 = x ^^^ 1073741824#32

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

theorem test23_logical_thm (e : IntW 32) :
  select (icmp IntPred.sgt e (const? 32 1)) (icmp IntPred.sle e (const? 32 2)) (const? 1 0) ⊑
    icmp IntPred.eq e (const? 32 2)

theorem PR38021_proof : PR38021_before ⊑ PR38021_after

theorem icmp_ne_and_pow2_shl1_proof : icmp_ne_and_pow2_shl1_before ⊑ icmp_ne_and_pow2_shl1_after

theorem add_nosignbit_shl_thm (e : IntW 32) :
  shl (add e (const? 32 2147418112)) (const? 32 8) ⊑ add (shl e (const? 32 8)) (const? 32 (-16777216))

theorem sge_and_max_commute_thm (e e_1 : IntW 8) :
  LLVM.and (icmp IntPred.eq e_1 (const? 8 127)) (icmp IntPred.sge e_1 e) ⊑
    icmp IntPred.eq e_1 (const? 8 127)

theorem e_2316 :
    3 *  ~~~(d &&& ( ~~~e ||| f)) + 1 * (f &&&  ~~~(d &&& e)) + 7 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 2 *  ~~~( ~~~d &&& (e &&& f)) - 1 * (e ^^^  ~~~(d |||  ~~~f)) - 1 * (f ^^^ (d &&& ( ~~~e ||| f))) - 1 * (e |||  ~~~(d ||| f)) - 7 * (e ^^^ ( ~~~d ||| (e ||| f))) - 7 * ( ~~~(d ||| e) ||| (e ^^^ f)) - 1 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) - 11 * (d ^^^ (e ||| f)) + 5 *  ~~~(e &&&  ~~~f) + 7 * (e ^^^ (d ||| (e &&& f))) - 6 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) - 5 * (f ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 5 *  ~~~(d |||  ~~~f) - 1 *  ~~~(d ^^^ e) + 1 *  ~~~d - 2 * ( ~~~d ||| (e &&& f)) + 2 * ( ~~~(d ^^^ e) &&& (d ^^^ f)) + 1 * (e &&&  ~~~f) - 11 * (e ^^^  ~~~(d &&& ( ~~~e ||| f))) + 1 * (f ^^^ ( ~~~d ||| ( ~~~e ||| f))) + 3 * (e ^^^ (d &&& ( ~~~e ||| f))) - 2 * (f &&&  ~~~(d &&&  ~~~e)) - 2 *  ~~~(e ||| f) + 11 *  ~~~(d &&&  ~~~f) - 11 * ((d &&& e) ^^^ (e |||  ~~~f)) + 3 * (d ||| ( ~~~e &&& f)) + 1 * (f ^^^ (d &&& e)) + 2 * (d |||  ~~~e) + 2 * (e ^^^ (d &&& (e ||| f))) - 11 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) - 7 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) + 1 * (d &&&  ~~~f) - 1 * ( ~~~(d ||| e) |||  ~~~(e ^^^ f)) + 1 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) + 7 * (f |||  ~~~(d |||  ~~~e)) + 2 * ((d ||| e) &&& (e ^^^ f)) + 1 * (e ||| (d &&& f)) + 5 * (e ^^^  ~~~(d &&& (e ||| f))) - 5 *  ~~~( ~~~d ||| (e ^^^ f)) - 1 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 2 * ( ~~~d ||| (e ||| f)) - 3 *  ~~~(d ^^^ (e ||| f)) - 6 * (e ^^^ (d &&& f)) + 1 * ((d &&& e) ||| (d ^^^ (e ^^^ f))) - 2 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) + 11 * ((d &&& e) |||  ~~~(e ^^^ f)) - 3 * ( ~~~e &&&  ~~~(d ^^^ f)) - 2 * (d ||| (e ^^^ f)) + 3 * (e ^^^ (d ||| (e ||| f))) - 3 * ((d &&& e) |||  ~~~(e ||| f)) + 3 * ((d ^^^ e) &&& (d ^^^ f)) + 5 * (f ^^^ ( ~~~d ||| (e ||| f))) - 1 * (e ^^^  ~~~(d &&&  ~~~f)) + 24 *  ~~~(d ||| (e ||| f)) + 28 *  ~~~(d ||| ( ~~~e ||| f)) + 1 *  ~~~( ~~~d ||| (e ||| f)) - 6 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 26 * ( ~~~d &&& ( ~~~e &&& f)) - 3 * ( ~~~d &&& (e &&& f)) - 11 * (d &&& ( ~~~e &&& f)) - 16 * (d &&& (e &&& f)) =  - 11 * (e &&& f)

theorem e_1022 :
     - 3 * (z ^^^ t) + 1 *  ~~~(z &&&  ~~~t) + 4 *  ~~~t + 7 *  ~~~z - 5 *  ~~~(z |||  ~~~t) - 1 * (z &&&  ~~~t) - 1 * (z &&& t) = 12 *  ~~~(z ||| t)

theorem test16_thm (e e_1 : IntW 32) :
  add (add e_1 (const? 32 1) { «nsw» := true, «nuw» := false })
      (LLVM.xor (LLVM.and e (const? 32 (-1431655767))) (const? 32 (-1431655767))) { «nsw» := true, «nuw» := false } ⊑
    sub e_1 (LLVM.or e (const? 32 1431655766))

theorem t0_basic_proof : t0_basic_before ⊑ t0_basic_after

theorem t2_proof : t2_before ⊑ t2_after

theorem narrow_zext_sub_proof : narrow_zext_sub_before ⊑ narrow_zext_sub_after

theorem select_mul_icmp_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 32), ofBool (x_2 == 1#32) = 1#1 → x_2 * x_1 = x_1

theorem lowmask_add_zext_thm.extracted_1._1 : ∀ (x : BitVec 32) (x_1 : BitVec 8),
  zeroExtend 32 x_1 + x &&& 255#32 = zeroExtend 32 (x_1 + truncate 8 x)

theorem lshrult_01_09_exact_proof : lshrult_01_09_exact_before ⊑ lshrult_01_09_exact_after

theorem test1_proof : test1_before ⊑ test1_after
</all_available_lemmas>

<local_ctx>
import Batteries.Data.Fin.Basic

import Batteries.Data.Fin.Lemmas

import Blase.SingleWidth.Defs

import Blase.AutoStructs.Constructions

import Blase.AutoStructs.Defs

import Blase.AutoStructs.FiniteStateMachine

import Mathlib.Tactic.Ring

import Mathlib.Data.Nat.Size -- TODO: remove and get rid of shiftLeft_eq_mul_pow use

import Mathlib.Data.BitVec

import Mathlib.Tactic.FinCases

open Fin.NatCast

open Mathlib

def NFA.sa (_ : NFA α σ) := σ → Language α

structure NFA.correct (M : NFA α σ) (ζ : M.sa) (L : Language α) where
  cond1 : ∀ w, (w ∈ L ↔ ∃ q ∈ M.accept, w ∈ ζ q)
  cond2 : ∀ w q, q ∈ M.eval w ↔ w ∈ ζ q

abbrev BVNRel n := ∀ ⦃w⦄, List.Vector (BitVec w) n → Prop

def NFA'.sa (M : NFA' n) := M.σ → BVNRel n

def langRel (R : BVNRel n) : Set (BitVecs n) :=
  { bvs | R bvs.bvs }

structure NFA'.correct (M : NFA' n) (ζ : M.sa) (L : BVNRel n) where
  cond1 : ∀ ⦃w⦄ (bvn : List.Vector (BitVec w) n), (L bvn ↔ ∃ q ∈ M.M.accept, ζ q bvn)
  cond2 q : q ∈ M.M.start ↔ ζ q (List.Vector.replicate n .nil)
  cond3 q a {w} (bvn : List.Vector (BitVec w) n) : q ∈ M.M.stepSet { q | ζ q bvn } a ↔
              ζ q (List.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) (bvn.get k))

structure NFA'.correct2 (M : NFA' 2) (ζ : M.sa2) (L : BVRel) where
  cond1 : ∀ (bv1 bv2 : BitVec w), (L bv1 bv2 ↔ ∃ q ∈ M.M.accept, ζ q bv1 bv2)
  cond2 q : q ∈ M.M.start ↔ ζ q .nil .nil
  cond3 q a w (bv1 bv2 : BitVec w) : q ∈ M.M.stepSet { q | ζ q bv1 bv2 } a ↔
              ζ q (BitVec.cons (a.getLsbD 0) bv1) (BitVec.cons (a.getLsbD 1) bv2)
</local_ctx>

<target_theorem>
lemma NFA'.correct_spec {M : NFA' n} {ζ : M.sa} {L : BVNRel n} :
    M.correct ζ L → M.accepts = langRel L :=
</target_theorem>

