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>
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
ZMod in Mathlib.Data.ZMod.Defs
NFA in Mathlib.Computability.NFA
DecidableEq in Init.Prelude
Fintype in Mathlib.Data.Fintype.Defs
BitVec in Init.Prelude
List in Init.Prelude
NFA.accept in Mathlib.Computability.NFA
NFA.start in Mathlib.Computability.NFA
NFA.step in Mathlib.Computability.NFA
Language in Mathlib.Computability.Language
FinEnum in Mathlib.Data.FinEnum
BitVec.ofFin in Init.Prelude
List.reverseRecOn in Mathlib.Data.List.Induction
NFA.stepSet in Mathlib.Computability.NFA
Nat in Init.Prelude
List.Vector in Mathlib.Data.Vector.Defs
Set in Mathlib.Data.Set.Defs
Bool in Init.Prelude
Fin in Init.Prelude
BitVec.iunfoldr in Init.Data.BitVec.Folds
List.finRange in Init.Data.List.FinRange
List.Vector.ofFn in Mathlib.Data.Vector.Defs
BitVec.cons in Init.Data.BitVec.Basic
List.Vector.replicate in Mathlib.Data.Vector.Defs
Function.RightInverse in Init.Data.Function

noncomputable def f : (ZMod q)[X] := X^(2^n) + 1

instance instFinEnumBV : FinEnum (BitVec w) where
  card := 2^w
  equiv := {
    toFun := fun x => x.toFin
    invFun := fun x => BitVec.ofFin x
    left_inv := by admit /- proof elided -/

@[simp]
def langMsb : Set (BitVecs 1) := { bvs | bvs.bvs.get 0 |>.msb }

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

def head (x : BitStream) : Bool      := x 0

def BitStream : Type := Nat → Bool

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 positive_biggerShl_before := [llvm|
{
^0(%arg34 : i32):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.mlir.constant(5 : i32) : i32
  %2 = llvm.shl %arg34, %0 : i32
  %3 = llvm.lshr %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def or_eq_with_one_bit_diff_constants1_logical_before := [llvm|
{
^0(%arg365 : i32):
  %0 = llvm.mlir.constant(50 : i32) : i32
  %1 = llvm.mlir.constant(51 : i32) : i32
  %2 = llvm.mlir.constant(true) : i1
  %3 = llvm.icmp "eq" %arg365, %0 : i32
  %4 = llvm.icmp "eq" %arg365, %1 : i32
  %5 = "llvm.select"(%3, %2, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def visitSRA : List (Σ Γ, LLVMPeepholeRewriteRefine 64 Γ) :=
  [⟨_, visitSRA_0⟩,
   ⟨_, visitSRA_Neg1⟩]

def different_size_sext_sext_eq_before := [llvm|
{
^0(%arg10 : i7, %arg11 : i4):
  %0 = llvm.sext %arg10 : i7 to i25
  %1 = llvm.sext %arg11 : i4 to i25
  %2 = llvm.icmp "eq" %0, %1 : i25
  "llvm.return"(%2) : (i1) -> ()
}
]

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

def lshr_eq_msb_low_last_zero_after := [llvm|
{
^0(%arg177 : i8):
  %0 = llvm.mlir.constant(6 : i8) : i8
  %1 = llvm.icmp "ugt" %arg177, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def and_two_ranges_to_mask_and_range_no_add_on_one_range_after := [llvm|
{
^0(%arg249 : i16):
  %0 = llvm.mlir.constant(-20 : i16) : i16
  %1 = llvm.mlir.constant(11 : i16) : i16
  %2 = llvm.and %arg249, %0 : i16
  %3 = llvm.icmp "ugt" %2, %1 : i16
  "llvm.return"(%3) : (i1) -> ()
}
]

def test44_after := [llvm|
{
^0(%arg203 : i32, %arg204 : i32):
  %0 = llvm.and %arg203, %arg204 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

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

def select_same_val_self : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 1), Ty.llvm (.bitvec 64) ] where
  lhs := [LV| {
    ^entry (%x: i64, %c: i1):
      %0 = llvm.select %c, %x, %x : i64
      llvm.return %0 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64, %c: i1):
      llvm.return %x : i64
  }]

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

def trunc_lshr_sext_exact_before := [llvm|
{
^0(%arg45 : i8):
  %0 = llvm.mlir.constant(6 : i32) : i32
  %1 = llvm.sext %arg45 : i8 to i32
  %2 = llvm.lshr exact %1, %0 : i32
  %3 = llvm.trunc %2 : i32 to i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

def test_shl_nsw__nsw_is_safe_before := [llvm|
{
^0(%arg73 : i32):
  %0 = llvm.mlir.constant(-83886080 : i32) : i32
  %1 = llvm.mlir.constant(-83886079 : i32) : i32
  %2 = llvm.mlir.constant(2 : i32) : i32
  %3 = llvm.mlir.constant(-335544316 : i32) : i32
  %4 = llvm.or %arg73, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.shl %4, %2 overflow<nsw> : i32
  %7 = "llvm.select"(%5, %3, %6) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %8 = llvm.mul %7, %4 : i32
  %9 = llvm.mul %8, %6 : i32
  "llvm.return"(%9) : (i32) -> ()
}
]

def and_signbit_select_lshr_after := [llvm|
{
^0(%arg30 : i32, %arg31 : i1):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(16776960 : i32) : i32
  %2 = llvm.lshr %arg30, %0 : i32
  %3 = llvm.and %2, %1 : i32
  %4 = "llvm.select"(%arg31, %3, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

def logical_and_logical_and_icmps_comm2_after := [llvm|
{
^0(%arg202 : i8, %arg203 : i8, %arg204 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.icmp "eq" %arg203, %0 : i8
  %5 = llvm.and %arg202, %1 : i8
  %6 = llvm.shl %1, %arg204 overflow<nuw> : i8
  %7 = llvm.and %arg202, %6 : i8
  %8 = llvm.icmp "ne" %5, %2 : i8
  %9 = llvm.icmp "ne" %7, %2 : i8
  %10 = "llvm.select"(%8, %4, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %11 = "llvm.select"(%10, %9, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%11) : (i1) -> ()
}
]

def lshr_shl_pow2_const_case1_before := [llvm|
{
^0(%arg60 : i16):
  %0 = llvm.mlir.constant(256 : i16) : i16
  %1 = llvm.mlir.constant(2 : i16) : i16
  %2 = llvm.mlir.constant(8 : i16) : i16
  %3 = llvm.lshr %0, %arg60 : i16
  %4 = llvm.shl %3, %1 : i16
  %5 = llvm.and %4, %2 : i16
  "llvm.return"(%5) : (i16) -> ()
}
]

def Valuation.singleton {t : Ty} (v : toType t) : Ctxt.Valuation ⟨[t]⟩ :=
  Ctxt.Valuation.nil.cons v

def logical_or_not_after := [llvm|
{
^0(%arg260 : i1, %arg261 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.xor %arg260, %0 : i1
  %2 = "llvm.select"(%1, %0, %arg261) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%2) : (i1) -> ()
}
]

private def pretty_test_overflow :=
  [llvm()|{
  ^bb0(%arg0: i32):
    %0 = llvm.mlir.constant 8 : i32
    %1 = llvm.add %0, %arg0 overflow<nsw> : i32
    %2 = llvm.mul %1, %arg0 : i32
    %3 = llvm.not %2 : i32
    llvm.return %3 : i32
  }]

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

def PR42691_9_logical_after := [llvm|
{
^0(%arg326 : i32):
  %0 = llvm.mlir.constant(-14 : i32) : i32
  %1 = llvm.mlir.constant(2147483633 : i32) : i32
  %2 = llvm.add %arg326, %0 : i32
  %3 = llvm.icmp "ult" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def sdiv_pow2_16 : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (16) : i64
      %0 = llvm.sdiv %x, %c : i64
      llvm.return %0 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %c0 = llvm.mlir.constant (63) : i64
      %c1 = llvm.mlir.constant (60) : i64
      %c2 = llvm.mlir.constant (4) : i64
      %0 = llvm.ashr %x, %c0 : i64
      %1 = llvm.lshr %0, %c1 : i64
      %2 = llvm.add %x, %1 : i64 
      %3 = llvm.ashr %2, %c2 : i64
      llvm.return %3 : i64
  }]

def absdiff1_before := [llvm|
{
^0(%arg2 : i64, %arg3 : i64):
  %0 = llvm.icmp "ult" %arg2, %arg3 : i64
  %1 = llvm.sext %0 : i1 to i64
  %2 = llvm.sub %arg2, %arg3 : i64
  %3 = llvm.xor %2, %1 : i64
  %4 = llvm.sub %3, %1 : i64
  "llvm.return"(%4) : (i64) -> ()
}
]

def test18_after := [llvm|
{
^0(%arg34 : i32, %arg35 : i32):
  %0 = llvm.mlir.constant(1431655765 : i32) : i32
  %1 = llvm.or %arg34, %0 : i32
  %2 = llvm.sub %arg35, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def test15_after := [llvm|
{
^0(%arg6 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.ashr %arg6, %0 : i32
  %3 = llvm.sub %1, %2 overflow<nsw> : i32
  %4 = llvm.sext %3 : i32 to i64
  "llvm.return"(%4) : (i64) -> ()
}
]

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

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

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

def mul_constant_eq_before := [llvm|
{
^0(%arg140 : i32, %arg141 : i32):
  %0 = llvm.mlir.constant(5 : i32) : i32
  %1 = llvm.mul %arg140, %0 : i32
  %2 = llvm.mul %arg141, %0 : i32
  %3 = llvm.icmp "eq" %1, %2 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def shrink_select_after := [llvm|
{
^0(%arg52 : i1, %arg53 : i32):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.trunc %arg53 : i32 to i8
  %2 = "llvm.select"(%arg52, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def xor_nosignbit_select_shl_before := [llvm|
{
^0(%arg36 : i32, %arg37 : i1):
  %0 = llvm.mlir.constant(2147418112 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.xor %arg36, %0 : i32
  %3 = "llvm.select"(%arg37, %2, %arg36) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %4 = llvm.shl %3, %1 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def shl_bad_sub_i32_before := [llvm|
{
^0(%arg12 : i32):
  %0 = llvm.mlir.constant(32 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.sub %0, %arg12 : i32
  %3 = llvm.shl %1, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def or_nosignbit_lshr_before := [llvm|
{
^0(%arg12 : i32):
  %0 = llvm.mlir.constant(2147418112 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.or %arg12, %0 : i32
  %3 = llvm.lshr %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def inter (M N : NFA' n) : NFA' n := ⟨_, M.M.inter N.M⟩

def hoist_ashr_ahead_of_sext_2_before := [llvm|
{
^0(%arg1 : i8):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.sext %arg1 : i8 to i32
  %2 = llvm.ashr %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def and_orn_cmp_3_before := [llvm|
{
^0(%arg185 : i72, %arg186 : i72, %arg187 : i72):
  %0 = llvm.mlir.constant(42 : i72) : i72
  %1 = llvm.icmp "ugt" %arg185, %arg186 : i72
  %2 = llvm.icmp "ule" %arg185, %arg186 : i72
  %3 = llvm.icmp "ugt" %arg187, %0 : i72
  %4 = llvm.or %2, %3 : i1
  %5 = llvm.and %1, %4 : i1
  "llvm.return"(%5) : (i1) -> ()
}
]

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

def doBvGeneralize (g : MVarId) : GenM (Expr × MVarId) := do
  let lctx ← getLCtx
  let mut allFVars := #[]
  for h in lctx do
    if not h.isImplementationDetail then
      allFVars := allFVars.push h.fvarId
  let (_, g) ← g.revert allFVars
  let e ← visit (← g.getType)
  let mut newVars := #[]
  for x in (←get).mapping.elements do
    newVars := newVars.push x

def or_or_and_pat4_before := [llvm|
{
^0(%arg62 : i8, %arg63 : i8, %arg64 : i8, %arg65 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.udiv %0, %arg64 : i8
  %2 = llvm.and %arg62, %arg63 : i8
  %3 = llvm.and %arg65, %arg63 : i8
  %4 = llvm.or %1, %3 : i8
  %5 = llvm.or %4, %2 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def function : Parser :=
  leading_parser argumentList >> arrow >> termParser

def mul? {w : Nat} (x y : BitVec w) : IntW w :=
  .value <| x * y

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

def shl_sub_i32_after := [llvm|
{
^0(%arg18 : i32):
  %0 = llvm.mlir.constant(-2147483648 : i32) : i32
  %1 = llvm.lshr exact %0, %arg18 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

noncomputable def R.toTensor {q n} (a : R q n) : List Int :=
  List.range a.repLength |>.map fun i =>
        a.coeff i |>.toInt

def llvm_sub_nuw_lower_riscv_16: LLVMPeepholeRewriteRefine 16 [Ty.llvm (.bitvec 16), Ty.llvm (.bitvec 16)] where
  lhs := llvm_sub_nuw_16
  rhs := sub_riscv_16

def eq_210_before := [llvm|
{
^0(%arg128 : i32, %arg129 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(16 : i32) : i32
  %2 = llvm.trunc %arg128 : i32 to i8
  %3 = llvm.lshr %arg128, %0 : i32
  %4 = llvm.trunc %3 : i32 to i8
  %5 = llvm.lshr %arg128, %1 : i32
  %6 = llvm.trunc %5 : i32 to i8
  %7 = llvm.trunc %arg129 : i32 to i8
  %8 = llvm.lshr %arg129, %0 : i32
  %9 = llvm.trunc %8 : i32 to i8
  %10 = llvm.lshr %arg129, %1 : i32
  %11 = llvm.trunc %10 : i32 to i8
  %12 = llvm.icmp "eq" %2, %7 : i8
  %13 = llvm.icmp "eq" %4, %9 : i8
  %14 = llvm.icmp "eq" %6, %11 : i8
  %15 = llvm.and %12, %13 : i1
  %16 = llvm.and %14, %15 : i1
  "llvm.return"(%16) : (i1) -> ()
}
]

def binop_left_to_zero_lshr : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (0) : i64
      %0 = llvm.lshr %c, %x : i64
      llvm.return %0 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (0) : i64
      llvm.return %c : i64
  }]

def or_logic_or_logic_and_5_after := [llvm|
{
^0(%arg36 : i1, %arg37 : i1, %arg38 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = "llvm.select"(%arg37, %arg38, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = "llvm.select"(%arg36, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

class SubstituteableTerminator (T : Type u) where
  substituteTerminator (σ : VarName → VarName) : T → T

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

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

def slt_swap_or_not_max_commute_logical_after := [llvm|
{
^0(%arg48 : i8, %arg49 : i8):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.icmp "ne" %arg48, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

|
</all_available_defs>

<all_available_lemmas>
BitVec.eq_nil in Init.Data.BitVec.Basic
BitVec.getElem_one in Init.Data.BitVec.Lemmas
BitVec.getLsbD_eq_getElem in Init.Data.BitVec.Basic
BitVec.msb_eq_getLsbD_last in Init.Data.BitVec.Lemmas
BitVec.ofNat_eq_ofNat in Init.Data.BitVec.Basic
List.getElem?_eq_getElem in Init.GetElem
List.getLast?_eq_getElem? in Init.Data.List.Lemmas
Set.mem_image in Mathlib.Data.Set.Operations
Set.mem_setOf_eq in Mathlib.Data.Set.Operations
and_true in Init.SimpLemmas
decide_true in Init.Core

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

@[simp]
lemma dec_enc' : dec (enc bvs) = bvs

@[simp]
lemma dec_enc : Function.RightInverse (α := BitVecs' n) enc dec

lemma dec_enc_w (bvs : BitVecs n) : (dec (enc bvs)).w = bvs.w

@[simp]
theorem BitVec.ofFn_getElem {w : Nat} (f : Fin w → Bool) {i : Nat} (hi : i < w) :
    (BitVec.ofFn f)[i] = f ⟨i, hi⟩

@[simp]
theorem BitVec.ofFn_getLsbD {w : Nat} {f : Fin w → Bool} {i : Nat} (hi : i < w) :
    (BitVec.ofFn f).getLsbD i = f ⟨i, hi⟩

theorem BitVec.ofFn_getLsbD_fin {w : Nat} {f : Fin w → Bool} {i : Fin w} :
    (BitVec.ofFn f).getLsbD i = f i

theorem e_772 :
    4 *  ~~~(z &&&  ~~~z) + 4 *  ~~~(z &&&  ~~~t) - 6 * (z ^^^ t) - 2 *  ~~~(z |||  ~~~t) - 8 * (z &&& t) = 8 *  ~~~(z ||| t) - 2 * (z &&&  ~~~t)

theorem slt_smin1_proof : slt_smin1_before ⊑ slt_smin1_after

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

theorem select_xor_icmp_bad_5_thm.extracted_1._4 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (x_2 != 0#32) = 1#1 → ¬ofBool (x_2 == 0#32) = 1#1 → x = x_2 ^^^ x_1

theorem select_constants_and_icmp_eq0_zero_tval_thm (e e_1 : IntW 1) :
  icmp IntPred.eq (LLVM.and (select e_1 (const? 8 0) (const? 8 12)) (select e (const? 8 0) (const? 8 12)))
      (const? 8 0) ⊑
    select e_1 (const? 1 1) e

theorem mul_of_bool_proof : mul_of_bool_before ⊑ mul_of_bool_after

theorem test88_thm.extracted_1._2 : ∀ (x : BitVec 16),
  ¬18#32 ≥ ↑32 → ¬15#16 ≥ ↑16 → truncate 16 ((signExtend 32 x).sshiftRight' 18#32) = x.sshiftRight' 15#16

theorem main1_proof : main1_before ⊑ main1_after

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

theorem fold_xor_zext_icmp_proof : fold_xor_zext_icmp_before ⊑ fold_xor_zext_icmp_after

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

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

theorem c0_proof : c0_before ⊑ c0_after

theorem test2_proof : test2_before ⊑ test2_after

theorem t14_x_is_one_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 (1#64 >>> zeroExtend 64 (x + BitVec.ofInt 32 (-16))) != 0#32) = 0#1

theorem ashrsgt_03_04_proof : ashrsgt_03_04_before ⊑ ashrsgt_03_04_after

theorem select_xor_icmp_proof : select_xor_icmp_before ⊑ select_xor_icmp_after

theorem e_2376 :
    1 * (d ||| ( ~~~e &&& f)) - 2 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) - 2 * (e ^^^ (d ||| (e ^^^ f))) - 2 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) - 1 * (f ^^^  ~~~(d &&& (e &&& f))) - 2 * ( ~~~d ||| (e &&& f)) + 2 * (f ||| (d &&& e)) + 11 * ( ~~~(d &&& e) &&&  ~~~(e ^^^ f)) - 2 * ((e &&& f) ^^^  ~~~(d &&& (e ^^^ f))) - 5 * (f ^^^  ~~~( ~~~d &&& (e &&& f))) - 2 * ( ~~~(d &&& e) &&&  ~~~(d ^^^ (e ^^^ f))) + 2 * ( ~~~e |||  ~~~(d ^^^ f)) - 1 * (d &&& (e ||| f)) + 7 * ((d |||  ~~~e) &&& (e ^^^ f)) + 1 * (d ^^^ e) + 2 * ( ~~~f &&&  ~~~(d ^^^ e)) - 6 * (f ^^^ (d ||| (e &&& f))) - 1 * (e ^^^  ~~~(d &&& (e ^^^ f))) - 5 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) - 11 *  ~~~(d &&&  ~~~f) + 2 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) - 7 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) + 1 * (f ^^^ ( ~~~d ||| (e &&& f))) - 7 * ( ~~~(d |||  ~~~e) |||  ~~~(e ^^^ f)) - 1 * (e &&&  ~~~f) + 2 * ((d &&& e) |||  ~~~(e ||| f)) - 2 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) + 3 * (e &&& (d |||  ~~~f)) - 11 * (f ^^^ ( ~~~d &&& ( ~~~e ||| f))) + 4 * ((d |||  ~~~e) &&& (d ^^^ (e ^^^ f))) + 1 * (d ||| (e &&& f)) - 3 * (f ^^^  ~~~(d ||| (e &&& f))) - 1 * ((d &&& e) ^^^ (e ||| f)) - 1 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) + 3 * (e ||| f) - 7 * ( ~~~d &&& ( ~~~e ||| f)) + 1 * ((e &&& f) ||| (d &&& (e ||| f))) - 6 *  ~~~(d &&& ( ~~~e ||| f)) - 11 * ( ~~~d ||| (e ^^^ f)) + 11 * (e &&&  ~~~(d ^^^ f)) + 5 * ((d &&& e) |||  ~~~(e |||  ~~~f)) + 1 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 1 * (d ||| (e ^^^ f)) + 2 * (e ^^^  ~~~(d &&&  ~~~f)) + 1 *  ~~~(d |||  ~~~f) - 6 * (f ^^^ (d |||  ~~~e)) - 1 *  ~~~(d &&& ( ~~~e &&& f)) + 1 * (f &&&  ~~~(d &&&  ~~~e)) + 4 * (d ^^^ (e ||| f)) - 6 * (d ^^^ f) + 2 *  ~~~(d ||| (e ^^^ f)) + 2 * (e ^^^ (d &&& f)) - 1 * (f |||  ~~~(d ^^^ e)) - 5 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) - 5 * (f ^^^ (d &&& ( ~~~e ||| f))) - 6 * ((d &&& e) ^^^  ~~~(d ^^^ ( ~~~e ||| f))) - 1 * (e ^^^  ~~~(d &&& f)) + 5 *  ~~~(d &&&  ~~~d) + 1 *  ~~~f + 1 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) + 7 * (f ^^^ ( ~~~d ||| ( ~~~e ||| f))) + 7 * (e ^^^ (d ||| (e ||| f))) - 2 * (d |||  ~~~f) + 60 *  ~~~(d ||| (e ||| f)) + 29 *  ~~~(d ||| ( ~~~e ||| f)) + 15 *  ~~~( ~~~d ||| (e ||| f)) + 17 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 33 * ( ~~~d &&& ( ~~~e &&& f)) + 17 * (d &&& ( ~~~e &&& f)) + 6 * (d &&& (e &&& f)) =  - 47 * ( ~~~d &&& (e &&& f)) + 1 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f))

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

theorem foo_thm (e : IntW 32) :
  LLVM.and (sub (const? 32 5) e) (const? 32 2) ⊑ LLVM.and (sub (const? 32 1) e) (const? 32 2)

theorem positive_easyinvert_thm.extracted_1._1 : ∀ (x : BitVec 16) (x_1 : BitVec 8),
  ofBool (x_1 <ₛ 0#8) ^^^ ofBool (x <ₛ 0#16) ^^^ 1#1 = ofBool (x_1 <ₛ 0#8) ^^^ ofBool (-1#16 <ₛ x)

theorem eq_21_proof : eq_21_before ⊑ eq_21_after

theorem or_xor_common_op_commute0_proof : or_xor_common_op_commute0_before ⊑ or_xor_common_op_commute0_after

theorem icmp_ne_zext_ne_zero_thm (e : IntW 32) :
  icmp IntPred.ne (zext 32 (icmp IntPred.ne e (const? 32 0))) e ⊑
    icmp IntPred.ugt e (const? 32 1)

theorem gt_signed_to_large_unsigned_proof : gt_signed_to_large_unsigned_before ⊑ gt_signed_to_large_unsigned_after

theorem commutativity_constant_varx_6_invmask_thm.extracted_1._1 : ∀ (x x_1 : BitVec 4),
  (x_1 ^^^ -1#4) &&& (x ^^^ 6#4) ^^^ 6#4 = (x ^^^ 6#4) &&& x_1 ^^^ x

theorem test_mul_nsw__nsw_is_safe_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x ||| BitVec.ofInt 32 (-83886080) == BitVec.ofInt 32 (-83886079)) = 1#1 →
    True ∧ (x ||| BitVec.ofInt 32 (-83886080)).smulOverflow 9#32 = true → False

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

theorem e_1682 :
     - 7 * (b &&&  ~~~(a &&&  ~~~c)) + 1 * ( ~~~(a ^^^ b) &&&  ~~~(a ^^^ c)) + 1 * (a |||  ~~~b) - 2 * (b ^^^ ( ~~~a &&& (b ||| c))) - 1 * (b ^^^  ~~~( ~~~a &&& (b ^^^ c))) - 1 * (c ^^^ (a ||| ( ~~~b &&& c))) - 7 * (b ^^^ ( ~~~a &&& ( ~~~b ||| c))) + 2 * (b &&& (a |||  ~~~c)) + 1 * ((a &&& b) ^^^ (a ^^^ (b &&& c))) - 3 * ( ~~~(a ^^^ b) &&& (a ^^^ c)) + 4 * (a ||| ( ~~~b &&& c)) - 2 * (b ^^^  ~~~(a ||| c)) - 5 * (c ^^^ ( ~~~a &&& (b ||| c))) - 11 *  ~~~( ~~~a &&& (b ^^^ c)) + 1 * (a ||| c) - 2 * ((a &&& b) ^^^ (b ||| c)) - 7 * (c ^^^  ~~~(a |||  ~~~b)) + 7 * ((b &&&  ~~~c) |||  ~~~(a ||| ( ~~~b &&& c))) + 11 * (c ^^^ (a &&& ( ~~~b ||| c))) + 7 * ( ~~~(a &&& b) &&& (b ^^^ c)) + 12 *  ~~~(a ||| (b ||| c)) + 13 *  ~~~(a ||| ( ~~~b ||| c)) - 2 *  ~~~( ~~~a ||| (b ||| c)) + 14 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 3 * ( ~~~a &&& (b &&& c)) + 12 * (a &&& ( ~~~b &&& c)) + 31 * (a &&& (b &&& c)) = 3 * (c ^^^ (a ||| (b &&& c)))

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

theorem uge_zext_thm (e : IntW 8) (e_1 : IntW 1) :
  icmp IntPred.uge (zext 8 e_1) e ⊑ icmp IntPred.ule e (zext 8 e_1)

theorem test_zext4_thm.extracted_1._3 : ∀ (x x_1 : BitVec 1),
  x_1 = 1#1 → x_1 ^^^ 1#1 = 1#1 → zeroExtend 32 x = zeroExtend 32 1#1

theorem test86_thm.extracted_1._2 : ∀ (x : BitVec 16),
  ¬4#32 ≥ ↑32 → ¬4#16 ≥ ↑16 → truncate 16 ((signExtend 32 x).sshiftRight' 4#32) = x.sshiftRight' 4#16

theorem sext_sub_nuw_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 8),
  ¬(True ∧ x_1.usubOverflow (signExtend 8 x) = true) → x_1 - signExtend 8 x = x_1 + zeroExtend 8 x

theorem and_def {α : Type _} (c d : Circuit α) :
  (c &&& d) = Circuit.simplifyAnd c d

theorem trunc_nuw_xor_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬(True ∧ zeroExtend 8 (truncate 1 (x_1 ^^^ x)) ≠ x_1 ^^^ x) → truncate 1 (x_1 ^^^ x) = ofBool (x_1 != x)

theorem select_2_thm (e e_1 e_2 : IntW 8) (e_3 e_4 : IntW 1) :
  LLVM.xor
      (select e_4 (select e_3 (LLVM.xor e_2 (const? 8 (-1))) (LLVM.xor e_1 (const? 8 123))) (LLVM.xor e (const? 8 45)))
      (const? 8 (-1)) ⊑
    select e_4 (select e_3 e_2 (LLVM.xor e_1 (const? 8 (-124)))) (LLVM.xor e (const? 8 (-46)))

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 trunc_sandwich_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(28#32 ≥ ↑32 ∨ 2#12 ≥ ↑12) →
    ¬(30#32 ≥ ↑32 ∨
          True ∧ signExtend 32 (truncate 12 (x >>> 30#32)) ≠ x >>> 30#32 ∨
            True ∧ zeroExtend 32 (truncate 12 (x >>> 30#32)) ≠ x >>> 30#32) →
      truncate 12 (x >>> 28#32) >>> 2#12 = truncate 12 (x >>> 30#32)

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

theorem shl_nsw_add_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(True ∧ (1#32 <<< x).sshiftRight' x ≠ 1#32 ∨ x ≥ ↑32) →
    True ∧ ((-1#32) <<< x).sshiftRight' x ≠ -1#32 ∨ x ≥ ↑32 → False

theorem e_588 :
    1 *  ~~~x + 3 * (x ^^^ y) + 11 *  ~~~(x &&& y) - 1 * x + 7 * (x ||| y) + 5 *  ~~~(x ^^^ y) + 2 *  ~~~(x &&&  ~~~x) - 19 *  ~~~(x ||| y) - 24 *  ~~~(x |||  ~~~y) - 22 * (x &&&  ~~~y) = 13 * (x &&& y)

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

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

theorem e_2015 :
    5 * (f ^^^ (d &&& e)) + 11 * ( ~~~e &&&  ~~~(d ^^^ f)) + 4 * (e ^^^  ~~~(d ||| ( ~~~e &&& f))) - 1 * (e |||  ~~~(d ||| f)) + 2 * (f ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) + 2 * (f ^^^  ~~~(d &&& e)) + 2 *  ~~~(d ^^^ e) + 3 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 1 * (f ^^^ (d ||| (e &&& f))) - 3 *  ~~~( ~~~d &&& (e &&& f)) + 3 * (f ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) + 1 * (e |||  ~~~f) + 1 * (e ^^^  ~~~( ~~~d ||| (e &&& f))) - 5 * (d &&& (e ^^^ f)) - 11 * ( ~~~d ||| (e ^^^ f)) - 6 * e + 1 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 2 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) - 11 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) + 3 * (e ||| (d ^^^ f)) + 4 * ((d ^^^ e) ||| (d ^^^ f)) + 11 * (d ||| e) + 1 * (d ||| (e ^^^ f)) - 11 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) + 11 *  ~~~(d &&& (e ^^^ f)) - 11 * (e &&&  ~~~(d &&& f)) - 18 *  ~~~(d ||| (e ||| f)) - 9 *  ~~~(d ||| ( ~~~e ||| f)) - 34 *  ~~~( ~~~d ||| (e ||| f)) - 7 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 18 * ( ~~~d &&& ( ~~~e &&& f)) + 1 * ( ~~~d &&& (e &&& f)) - 7 * (d &&& ( ~~~e &&& f)) - 23 * (d &&& (e &&& f)) =  - 7 * ((d &&& e) |||  ~~~(e ^^^ f))

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

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

theorem trunc_shl_32_i32_i64_proof : trunc_shl_32_i32_i64_before ⊑ trunc_shl_32_i32_i64_after

theorem ripple_nsw6_proof : ripple_nsw6_before ⊑ ripple_nsw6_after

theorem splat_mul_unknown_lz_proof : splat_mul_unknown_lz_before ⊑ splat_mul_unknown_lz_after

theorem test_proof : test_before ⊑ test_after

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

theorem lshr_eq_msb_low_last_zero_proof : lshr_eq_msb_low_last_zero_before ⊑ lshr_eq_msb_low_last_zero_after

theorem src_is_mask_shl_lshr_fail_not_allones_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬(x ≥ ↑8 ∨ x ≥ ↑8) →
    ¬x ≥ ↑8 →
      ofBool (0#8 != (x_1 ^^^ 123#8) &&& (BitVec.ofInt 8 (-2) <<< x >>> x ^^^ -1#8)) =
        ofBool (x_1 ^^^ BitVec.ofInt 8 (-124) ||| (-1#8) >>> x &&& BitVec.ofInt 8 (-2) != -1#8)

theorem logic_and_logic_or_5_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1), ¬x_1 = 1#1 → 0#1 = 1#1 → 1#1 = 0#1

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

theorem t6_ugt_sgt_128_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (143#32 <ᵤ x_1 + 16#32) = 1#1 → ofBool (127#32 <ₛ x_1) = 1#1 → x_1 = x

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

theorem test_or3_logical_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x_1 &&& 2147483647#32 ≤ₛ x) = 1#1 → ofBool (x <ₛ 0#32) = ofBool (x_1 &&& 2147483647#32 ≤ᵤ x)

theorem lshr_sub_nsw_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(True ∧ x_1.ssubOverflow x = true ∨ 31#32 ≥ ↑32) → (x_1 - x) >>> 31#32 = zeroExtend 32 (ofBool (x_1 <ₛ x))

theorem zext_false_val_must_be_zero_thm (e : IntW 1) : select e (const? 32 42) (zext 32 e) ⊑ select e (const? 32 42) (const? 32 0)

theorem shl_add_and_fail_mismatch_shift_proof : shl_add_and_fail_mismatch_shift_before ⊑ shl_add_and_fail_mismatch_shift_after

theorem shl_lshr_pow2_const_case1_thm (e : IntW 16) :
  LLVM.and (lshr (shl (const? 16 4) e) (const? 16 6)) (const? 16 8) ⊑
    select (icmp IntPred.eq e (const? 16 7)) (const? 16 8) (const? 16 0)

theorem test11_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬zeroExtend 128 x &&& 31#128 ≥ ↑128 →
    ¬(True ∧ (x &&& 31#32).msb = true ∨
          True ∧
              (zeroExtend 64 x_1 <<< zeroExtend 64 (x &&& 31#32)).sshiftRight' (zeroExtend 64 (x &&& 31#32)) ≠
                zeroExtend 64 x_1 ∨
            True ∧
                zeroExtend 64 x_1 <<< zeroExtend 64 (x &&& 31#32) >>> zeroExtend 64 (x &&& 31#32) ≠ zeroExtend 64 x_1 ∨
              zeroExtend 64 (x &&& 31#32) ≥ ↑64) →
      truncate 64 (zeroExtend 128 x_1 <<< (zeroExtend 128 x &&& 31#128)) =
        zeroExtend 64 x_1 <<< zeroExtend 64 (x &&& 31#32)

theorem e_1415 :
    5 * (z ||| t) - 3 *  ~~~t - 7 *  ~~~(z &&& t) + 2 *  ~~~z + 1 * z - 2 *  ~~~(z ^^^ t) - 6 *  ~~~(z &&&  ~~~t) + 22 *  ~~~(z ||| t) + 6 *  ~~~(z |||  ~~~t) + 8 * (z &&& t) =  - 10 * (z &&&  ~~~t) + 6 * (z |||  ~~~t)

theorem a_true_implies_b_false_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 8),
  ofBool (20#8 <ᵤ x_1) = 1#1 → ofBool (x_1 <ᵤ 10#8) = 1#1 → False

theorem icmp_eq_sext_ne_allones_thm (e : IntW 32) :
  icmp IntPred.eq (sext 32 (icmp IntPred.ne e (const? 32 (-1)))) e ⊑ const? 1 0

theorem shift_no_xor_multiuse_cmp_with_xor_proof : shift_no_xor_multiuse_cmp_with_xor_before ⊑ shift_no_xor_multiuse_cmp_with_xor_after

theorem n5_proof : n5_before ⊑ n5_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

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)

section fsm

variable {arity : Type} [FinEnum arity]

open BitStream in

end fsm

section nfas_relations

inductive NFA.msbState : Type where
| i | f
deriving DecidableEq, Fintype

def NFA.msbStep (q : NFA.msbState) (a : BitVec 1) : List NFA.msbState :=
  match q, a with
  | .i, 0 => [.i]
  | .i, 1 => [.i, .f]
  | _, _ => []

def NFA.autMsbSet : NFA (BitVec 1) msbState where
  step s a := { s' | s' ∈ msbStep s a }
  start := {.i}
  accept := {.f}

def NFA'.autMsbSet : NFA' 1 := ⟨_, NFA.autMsbSet⟩

def NFA.msbLang : Language (BitVec 1) := { bvs  | bvs.getLast? = some 1 }

def NFA.msbSA (q : msbState) : Language (BitVec 1) :=
  match q with
  | .i => ⊤
  | .f => msbLang

def NFA.msbCorrect : NFA.autMsbSet.correct msbSA msbLang :=
</local_ctx>

<target_theorem>
@[simp]
lemma autMsbSet_accepts : NFA'.autMsbSet.accepts = langMsb :=
</target_theorem>

