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>
Array in Init.Prelude
Nat in Init.Prelude
BEq in Init.Prelude
DecidableEq in Init.Prelude
FinEnum in Mathlib.Data.FinEnum
Hashable in Init.Prelude
Repr in Init.Data.Repr
Std.HashMap in Std.Data.HashMap.Basic
Std.HashSet in Std.Data.HashSet.Basic
BitVec in Init.Prelude
FinEnum.toList in Mathlib.Data.FinEnum
List in Init.Prelude
List.Nodup in Init.Data.List.Basic
Subtype in Init.Prelude
Set in Mathlib.Data.Set.Defs
LawfulBEq in Init.Core
Function.Injective2 in Mathlib.Logic.Function.Basic

structure CNFA (n : Nat) where
  m : RawCNFA (BitVec n)
  wf : m.WF

instance RawCNFA.statesFinset (m : RawCNFA A) : Fintype m.states := (Finset.range m.stateMax).fintypeCoeSort

abbrev State := Nat

def Std.HashSet.toSet [BEq α] [Hashable α] (m : HashSet α) : Set α := { x | x ∈ m }

axiom hashMap_missing : ∀ {P : Prop}, P

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

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

def PoisonOr.getOrUB  : PoisonOr α → m α
  | .value x => pure x
  | .poison => throwUB

RV64.sh3adduw in RISCV.Instructions

def test53_after := [llvm|
{
^0(%arg131 : i32):
  %0 = llvm.mlir.constant(7224 : i16) : i16
  %1 = llvm.mlir.constant(-32574 : i16) : i16
  %2 = llvm.trunc %arg131 : i32 to i16
  %3 = llvm.and %2, %0 : i16
  %4 = llvm.or disjoint %3, %1 : i16
  %5 = llvm.zext %4 : i16 to i64
  "llvm.return"(%5) : (i64) -> ()
}
]

def negate_select_of_op_vs_negated_op_nsw_commuted_before := [llvm|
{
^0(%arg18 : i8, %arg19 : i8, %arg20 : i1):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %0, %arg18 overflow<nsw> : i8
  %2 = "llvm.select"(%arg20, %arg18, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %3 = llvm.sub %arg19, %2 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def test23_before := [llvm|
{
^0(%arg185 : i32, %arg186 : i32):
  %0 = llvm.xor %arg186, %arg185 : i32
  %1 = llvm.icmp "eq" %0, %arg185 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def llvm_mul_lower_riscv_nsw_flag_32 : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] where
  lhs := mul_llvm_nsw_32
  rhs := mul_riscv_32

def test_sub_nsw__all_are_safe_before := [llvm|
{
^0(%arg29 : i32):
  %0 = llvm.mlir.constant(255 : i32) : i32
  %1 = llvm.mlir.constant(6 : i32) : i32
  %2 = llvm.mlir.constant(-254 : i32) : i32
  %3 = llvm.mlir.constant(-260 : i32) : i32
  %4 = llvm.and %arg29, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.sub %2, %4 overflow<nsw> : i32
  %7 = "llvm.select"(%5, %3, %6) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%7) : (i32) -> ()
}
]

def llvm_add_lower_riscv_nuw_flag_8 : LLVMPeepholeRewriteRefine 8 [Ty.llvm (.bitvec 8), Ty.llvm (.bitvec 8)] where
  lhs:= add_llvm_nuw_flags_8
  rhs:= add_riscv_8

def land_lor_right1_after := [llvm|
{
^0(%arg46 : i1, %arg47 : i1):
  "llvm.return"(%arg46) : (i1) -> ()
}
]

def and_nosignbit_shl_before := [llvm|
{
^0(%arg22 : i32):
  %0 = llvm.mlir.constant(2147418112 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.and %arg22, %0 : i32
  %3 = llvm.shl %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

instance : DialectToExpr LLVM where
  toExprM := .const ``Id [0]
  toExprDialect := .const ``LLVM []

def ne_21_logical_before := [llvm|
{
^0(%arg52 : i32, %arg53 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(16 : i32) : i32
  %2 = llvm.mlir.constant(true) : i1
  %3 = llvm.lshr %arg52, %0 : i32
  %4 = llvm.trunc %3 : i32 to i8
  %5 = llvm.lshr %arg52, %1 : i32
  %6 = llvm.trunc %5 : i32 to i8
  %7 = llvm.lshr %arg53, %0 : i32
  %8 = llvm.trunc %7 : i32 to i8
  %9 = llvm.lshr %arg53, %1 : i32
  %10 = llvm.trunc %9 : i32 to i8
  %11 = llvm.icmp "ne" %4, %8 : i8
  %12 = llvm.icmp "ne" %6, %10 : i8
  %13 = "llvm.select"(%12, %2, %11) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%13) : (i1) -> ()
}
]

def _root_.Blase.dummy : Unit := ()

def logical_and_cond_reuse_after := [llvm|
{
^0(%arg258 : i1, %arg259 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = "llvm.select"(%arg258, %arg259, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%1) : (i1) -> ()
}
]

def getEqRhs (eq : Expr) : MetaM Expr := do
  check eq
  let eq ← whnf <| ← inferType eq
  let some (_ty, _lhs, rhs) := eq.eq? | throwError m!"unable to infer RHS for equality {eq}"
  let rhs ← instantiateMVars rhs
  rhs.ensureHasNoMVars
  return rhs

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

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

def select_match : List (Σ Γ, Σ ty, PeepholeRewrite LLVMPlusRiscV Γ ty) :=
  [⟨[Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64),Ty.llvm (.bitvec 1)],
   [Ty.llvm (.bitvec 64)],(LLVMToRiscvPeepholeRewriteRefine.toPeepholeUNSOUND select_riscv_select_llvm_64)⟩,
  ⟨[Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32),Ty.llvm (.bitvec 1)],
   [Ty.llvm (.bitvec 32)],(LLVMToRiscvPeepholeRewriteRefine.toPeepholeUNSOUND select_riscv_select_llvm_32)⟩,
   ⟨[Ty.llvm (.bitvec 8), Ty.llvm (.bitvec 8),Ty.llvm (.bitvec 1)],
   [Ty.llvm (.bitvec 8)],(LLVMToRiscvPeepholeRewriteRefine.toPeepholeUNSOUND select_riscv_select_llvm_8)⟩]

@[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 ashr_can_be_lshr_before := [llvm|
{
^0(%arg1 : i32):
  %0 = llvm.mlir.constant(16 : i32) : i32
  %1 = llvm.ashr exact %arg1, %0 : i32
  %2 = llvm.trunc %1 overflow<nsw> : i32 to i16
  "llvm.return"(%2) : (i16) -> ()
}
]

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

def sge_smin1_before := [llvm|
{
^0(%arg79 : i32, %arg80 : i32):
  %0 = llvm.icmp "slt" %arg79, %arg80 : i32
  %1 = "llvm.select"(%0, %arg79, %arg80) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "sge" %1, %arg79 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def basic_before := [llvm|
{
^0(%arg25 : i8, %arg26 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.xor %arg25, %0 : i8
  %2 = llvm.add %1, %arg26 : i8
  %3 = llvm.xor %2, %0 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

structure Tensor2d' (α : Type) where
  dim₀ : Index
  dim₁ : Index
  mat : Matrix (Fin dim₀) (Fin dim₁) α

def test_lshr_exact__exact_is_safe_before := [llvm|
{
^0(%arg62 : i32, %arg63 : i64):
  %0 = llvm.mlir.constant(60 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.mlir.constant(0 : i32) : i32
  %3 = llvm.and %arg62, %0 : i32
  %4 = llvm.lshr exact %3, %1 : i32
  %5 = llvm.zext %4 : i32 to i64
  %6 = llvm.icmp "eq" %3, %2 : i32
  %7 = llvm.ashr %arg63, %5 : i64
  %8 = "llvm.select"(%6, %arg63, %7) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  "llvm.return"(%8) : (i64) -> ()
}
]

def xor_or_xor_common_op_commute5_after := [llvm|
{
^0(%arg68 : i32, %arg69 : i32, %arg70 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg68, %0 : i32
  %2 = llvm.and %arg69, %1 : i32
  %3 = llvm.xor %2, %arg70 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

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

def Com.changeEffect {eff₁ eff₂ : EffectKind} (h : eff₁ ≤ eff₂) :
    Com d Γ eff₁ t → Com d Γ eff₂ t := fun com =>
  Com.rec' (motive := @fun Γ _ => eff₁ ≤ eff₂ → Com d Γ eff₂ t)
            (fun v _h               => rets v)
      (fun e _body castBody h => var (e.changeEffect h) (castBody h))
    com h

def land_land_right1_before := [llvm|
{
^0(%arg54 : i1, %arg55 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = "llvm.select"(%arg54, %arg55, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %2 = "llvm.select"(%arg54, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%2) : (i1) -> ()
}
]

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

def slt_zero_ult_i1_fail2_after := [llvm|
{
^0(%arg6 : i32, %arg7 : i1):
  %0 = llvm.mlir.constant(31 : i32) : i32
  %1 = llvm.zext %arg7 : i1 to i32
  %2 = llvm.ashr %arg6, %0 : i32
  %3 = llvm.icmp "ugt" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def src_x_and_nmask_uge_before := [llvm|
{
^0(%arg21 : i8, %arg22 : i8, %arg23 : i1):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.shl %0, %arg22 : i8
  %3 = "llvm.select"(%arg23, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %4 = llvm.and %arg21, %3 : i8
  %5 = llvm.icmp "uge" %4, %3 : i8
  "llvm.return"(%5) : (i1) -> ()
}
]

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

OptionT.run in Init.Control.Option

def and_two_ranges_to_mask_and_range_no_add_on_one_range_before := [llvm|
{
^0(%arg249 : i16):
  %0 = llvm.mlir.constant(12 : i16) : i16
  %1 = llvm.mlir.constant(16 : i16) : i16
  %2 = llvm.mlir.constant(28 : i16) : i16
  %3 = llvm.icmp "uge" %arg249, %0 : i16
  %4 = llvm.icmp "ult" %arg249, %1 : i16
  %5 = llvm.icmp "uge" %arg249, %2 : i16
  %6 = llvm.or %4, %5 : i1
  %7 = llvm.and %3, %6 : i1
  "llvm.return"(%7) : (i1) -> ()
}
]

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

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

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

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

def llvm_shl_lower_riscv_nuw_64: LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] where
  lhs := shl_llvm_nuw_64
  rhs := shl_riscv_64

def not_cmp_constant_before := [llvm|
{
^0(%arg144 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.mlir.constant(42 : i32) : i32
  %2 = llvm.xor %arg144, %0 : i32
  %3 = llvm.icmp "ugt" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

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

def xor_ashr_not_fail_invalid_xor_constant_after := [llvm|
{
^0(%arg15 : i8, %arg16 : i8, %arg17 : i8):
  %0 = llvm.mlir.constant(-2 : i8) : i8
  %1 = llvm.xor %arg16, %arg15 : i8
  %2 = llvm.ashr %1, %arg17 : i8
  %3 = llvm.xor %2, %0 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

def and_or_not_not_commute7_after := [llvm|
{
^0(%arg354 : i32, %arg355 : i32, %arg356 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.or %arg356, %arg355 : i32
  %2 = llvm.and %1, %arg354 : i32
  %3 = llvm.xor %2, %0 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def reassoc_x2_add_nuw_before := [llvm|
{
^0(%arg20 : i32, %arg21 : i32):
  %0 = llvm.mlir.constant(4 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.add %arg20, %0 overflow<nuw> : i32
  %3 = llvm.add %arg21, %1 overflow<nuw> : i32
  %4 = llvm.add %2, %3 overflow<nuw> : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def positive_sameconst_shlnuwnsw_lshrexact_after := [llvm|
{
^0(%arg26 : i8):
  "llvm.return"(%arg26) : (i8) -> ()
}
]

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

def sll_i32_test : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] where
  lhs := sll_llvm_i64
  rhs := sll_riscv_i64

def or_xor_tree_1001_before := [llvm|
{
^0(%arg18 : i32, %arg19 : i32, %arg20 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mul %arg18, %0 : i32
  %2 = llvm.mul %arg19, %0 : i32
  %3 = llvm.mul %arg20, %0 : i32
  %4 = llvm.xor %2, %1 : i32
  %5 = llvm.xor %2, %3 : i32
  %6 = llvm.xor %5, %1 : i32
  %7 = llvm.or %6, %4 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

def example_program := [DCPlus_com| {
  ^entry(%0 : !TokenStream, %1 : !ValueStream_1):
    %branch = "DCPlus.branch" (%1, %0) : (!ValueStream_1, !TokenStream) -> (!TokenStream2)
    %fst = "DCPlus.fst" (%branch) :  (!TokenStream2) -> (!TokenStream)
    "return" (%fst) : (!TokenStream) -> ()
  }]

def squared_nsw_eq0_after := [llvm|
{
^0(%arg185 : i5):
  %0 = llvm.mlir.constant(0 : i5) : i5
  %1 = llvm.icmp "eq" %arg185, %0 : i5
  "llvm.return"(%1) : (i1) -> ()
}
]

def scalar_i32_shl_and_negC_eq_before := [llvm|
{
^0(%arg31 : i32, %arg32 : i32):
  %0 = llvm.mlir.constant(-262144 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.shl %arg31, %arg32 : i32
  %3 = llvm.and %2, %0 : i32
  %4 = llvm.icmp "eq" %3, %1 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

def sext_sub_nuw_after := [llvm|
{
^0(%arg14 : i8, %arg15 : i1):
  %0 = llvm.zext %arg15 : i1 to i8
  %1 = llvm.add %arg14, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def alive_InstCombineShift__279_src :=
[sllvm| {
^bb0(%X : i64, %C : i64):
  %v1 = llvm.lshr %X, %C : i64
  %v2 = llvm.shl %v1, %C : i64
  llvm.return %v2 : i64
}]

def test_logical_or_eq_a_b_after := [llvm|
{
^0(%arg9 : i1, %arg10 : i8, %arg11 : i8):
  %0 = "llvm.select"(%arg9, %arg10, %arg11) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%0) : (i8) -> ()
}
]

@[simp_denote] def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr ScfArith Γ .pure .int :=
  Expr.mk
    (op := .coe <| .add)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons e₁ <| .cons e₂ .nil)
    (regArgs := .nil)

def sle_smax3_after := [llvm|
{
^0(%arg51 : i32, %arg52 : i32):
  %0 = llvm.mlir.constant(3 : i32) : i32
  %1 = llvm.add %arg51, %0 : i32
  %2 = llvm.icmp "sle" %arg52, %1 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

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

def xor_or_xor_common_op_commute6_before := [llvm|
{
^0(%arg65 : i32, %arg66 : i32, %arg67 : i32):
  %0 = llvm.xor %arg67, %arg65 : i32
  %1 = llvm.or %arg65, %arg66 : i32
  %2 = llvm.xor %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def mkEqRflNativeDecideProof (lhsExpr : Expr) (rhs : Bool) : TermElabM Expr := do
    
  let auxDeclName ← Term.mkAuxName `_mkEqRflNativeDecideProof
  let decl := Declaration.defnDecl {
    name := auxDeclName
    levelParams := []
    type := mkConst ``Bool
    value := lhsExpr
    hints := .abbrev
    safety := .safe
  }
  addAndCompile decl
  let lhsDef : Expr := mkConst auxDeclName
  let rflProof ← mkEqRefl (toExpr rhs)
  mkAppM ``Lean.ofReduceBool #[lhsDef, toExpr rhs, rflProof]

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

def add_const_const_sub_nsw_after := [llvm|
{
^0(%arg58 : i8):
  %0 = llvm.mlir.constant(-128 : i8) : i8
  %1 = llvm.sub %0, %arg58 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def test12commuted_after := [llvm|
{
^0(%arg87 : i32, %arg88 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg87, %arg88 : i32
  %2 = llvm.xor %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def src_is_mask_select_before := [llvm|
{
^0(%arg110 : i8, %arg111 : i8, %arg112 : i1):
  %0 = llvm.mlir.constant(123 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.mlir.constant(15 : i8) : i8
  %3 = llvm.xor %arg110, %0 : i8
  %4 = llvm.add %arg111, %1 : i8
  %5 = llvm.xor %arg111, %4 : i8
  %6 = "llvm.select"(%arg112, %5, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %7 = llvm.and %6, %3 : i8
  %8 = llvm.icmp "ne" %7, %3 : i8
  "llvm.return"(%8) : (i1) -> ()
}
]

structure Item where
 name : String
 tac : Syntax

|
</all_available_defs>

<all_available_lemmas>
Array.mem_push in Init.Data.Array.Lemmas
Array.mem_toList_iff in Init.Data.Array.Lemmas
Array.toList_push in Init.Data.Array.Bootstrap
Function.Injective2.eq_iff in Mathlib.Logic.Function.Basic
List.Nodup.append in Mathlib.Data.List.Nodup
List.append_assoc in Init.Data.List.Basic
List.disjoint_singleton in Batteries.Data.List.Lemmas
List.mem_append in Init.Data.List.Lemmas
List.mem_singleton in Init.Data.List.Lemmas
Set.mem_empty_iff_false in Mathlib.Data.Set.Basic
Set.mem_insert_iff in Mathlib.Data.Set.Insert
Set.union_singleton in Mathlib.Data.Set.Insert
and_false in Init.SimpLemmas
iff_and_self in Init.SimpLemmas
ne_eq in Init.SimpLemmas
or_false in Init.SimpLemmas
true_and in Init.SimpLemmas
ne_or_eq in Mathlib.Logic.Basic
Array.mem_def in Init.Data.Array.Basic
Array.not_mem_empty in Init.Data.Array.Lemmas
FinEnum.nodup_toList in Mathlib.Data.FinEnum
List.Nodup.notMem in Mathlib.Data.List.Nodup
List.dedup_eq_self in Mathlib.Data.List.Dedup
List.foldl_nil in Init.Data.List.Basic
List.mem_cons in Init.Data.List.Lemmas
List.nodup_cons in Init.Data.List.Pairwise
List.not_mem_nil in Init.Data.List.Lemmas
false_and in Init.SimpLemmas
false_or in Init.SimpLemmas

theorem Std.HashSet.fold_induction [BEq α] [LawfulBEq α] [Hashable α]
  {f : β → α → β} {m : HashSet α} {motive : β → Set α → Prop} :
    motive b ∅ →
    (∀ b x s, x ∉ s → motive b s → motive (f b x) (s ∪ {x})) →
    motive (m.fold f b) m.toSet

theorem Std.HashSet.toSet_toList[BEq α] [LawfulBEq α] [Hashable α] (m : HashSet α) : m.toSet = { x | x ∈ m.toList }

@[simp]
lemma Std.HashSet.mem_toSet [BEq α] [Hashable α] (m : HashSet α) : x ∈ m.toSet ↔ x ∈ m

@[simp]
theorem Std.HashSet.mem_attachWith_mem [BEq α] [Hashable α] [LawfulBEq α] (m : HashSet α) {P H} (x : α) h :
    ⟨x, h⟩ ∈ m.attachWith P H ↔ x ∈ m

@[symm] theorem Bisim.symm {a b : Stream α} : a ~ b → b ~ a

theorem select_or_disjoint_or_proof : select_or_disjoint_or_before ⊑ select_or_disjoint_or_after

theorem sext_thm.extracted_1._2 : ∀ (x : BitVec 1), ¬x = 1#1 → 0#41 = signExtend 41 x

theorem ashr_slt_exact_near_pow2_cmpval_thm (e : IntW 8) :
  icmp IntPred.slt (ashr e (const? 8 1) { «exact» := true }) (const? 8 5) ⊑
    icmp IntPred.slt e (const? 8 9)

theorem n9_wrong_x0_proof : n9_wrong_x0_before ⊑ n9_wrong_x0_after

theorem fold_icmp_shl_nuw_c2_div_non_pow2_proof : fold_icmp_shl_nuw_c2_div_non_pow2_before ⊑ fold_icmp_shl_nuw_c2_div_non_pow2_after

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

theorem scalar_i32_udiv_and_negC_eq_X_is_constant3_thm (e : IntW 32) :
  icmp IntPred.ne (LLVM.and (LLVM.udiv (const? 32 12345) e) (const? 32 16376)) (const? 32 0) ⊑
    icmp IntPred.ult e (const? 32 1544)

theorem ofBitVec_one_eqTo_ofNat : @ofBitVecSext w 1 ≈ʷ ofNat 1

theorem ashr_lshr_cst2_proof : ashr_lshr_cst2_before ⊑ ashr_lshr_cst2_after

theorem width5 (w : Nat) (a b : BitVec w) : (a + b = a - a) → a = - b

theorem test36_thm.extracted_1._1 : ∀ (x : BitVec 32), True ∧ (x + 7#32 &&& 240#32).msb = true → False

@[simp] lemma swapLastTwoBlock_Sn {n : Nat} : swapLastTwoBlock (n := n) (n+1) = Fin.last _

theorem shr_umax_proof : shr_umax_before ⊑ shr_umax_after

theorem test_shift_and_cmp_changed1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬(5#8 ≥ ↑8 ∨ 5#8 ≥ ↑8) →
    ¬5#8 ≥ ↑8 →
      ofBool (((x_1 &&& 8#8 ||| x &&& 6#8) <<< 5#8).sshiftRight' 5#8 <ₛ 1#8) =
        ofBool (x <<< 5#8 &&& BitVec.ofInt 8 (-64) <ₛ 32#8)

theorem src_is_mask_shl_lshr_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), ¬(x ≥ ↑8 ∨ x ≥ ↑8) → x ≥ ↑8 → False

theorem t0_proof : t0_before ⊑ t0_after

theorem test_add_nuw_nsw__none_are_safe_proof : test_add_nuw_nsw__none_are_safe_before ⊑ test_add_nuw_nsw__none_are_safe_after

theorem slt_zero_eq_i1_fail_thm (e : IntW 32) (e_1 : IntW 1) :
  icmp IntPred.eq (zext 32 e_1) (ashr e (const? 32 31)) ⊑
    icmp IntPred.eq (ashr e (const? 32 31)) (zext 32 e_1)

theorem ashr_ult_9_proof : ashr_ult_9_before ⊑ ashr_ult_9_after

theorem sle_swap_or_min_logical_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬ofBool (x ≤ₛ x_1) = 1#1 → ofBool (x == BitVec.ofInt 8 (-128)) = ofBool (x ≤ₛ x_1)

theorem icmp_eq_zext_ne_zero_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (zeroExtend 32 (ofBool (x != 0#32)) == x) = ofBool (x <ᵤ 2#32)

theorem select2_thm.extracted_1._5 : ∀ (x x_1 x_2 : BitVec 8) (x_3 : BitVec 1),
  ¬x_3 = 1#1 → truncate 8 (zeroExtend 32 x_1 + zeroExtend 32 x) = x_1 + x

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

theorem and_umax_less_thm (e : IntW 32) :
  LLVM.and (select (icmp IntPred.ugt (const? 32 31) e) (const? 32 31) e) (const? 32 (-32)) ⊑
    LLVM.and e (const? 32 (-32))

theorem PR42691_9_logical_proof : PR42691_9_logical_before ⊑ PR42691_9_logical_after

theorem or_not_and_and_not_and_xor_commute4_proof : or_not_and_and_not_and_xor_commute4_before ⊑ or_not_and_and_not_and_xor_commute4_after

theorem add_and_or_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), (x_1 &&& x) + (x_1 ||| x) = x_1 + x

theorem main4f_like_logical_thm.extracted_1._6 : ∀ (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 t0_ult_slt_128_thm.extracted_1._11 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 + 16#32 <ᵤ 144#32) = 1#1 →
    ¬ofBool (127#32 <ₛ x_2) = 1#1 → ofBool (x_2 <ₛ BitVec.ofInt 32 (-16)) = 1#1 → x_2 = x_1

theorem test48_proof : test48_before ⊑ test48_after

theorem shl_nsw_nuw_uge_Csle0_thm (e e_1 : IntW 8) :
  icmp IntPred.uge (shl e_1 e { «nsw» := true, «nuw» := true }) (const? 8 (-120)) ⊑
    icmp IntPred.ugt e_1 (const? 8 (-121))

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

theorem sel_false_val_is_a_masked_ashr_of_true_val2_thm.extracted_1._2 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬2#32 ≥ ↑32 →
    ofBool ((x_1 &&& BitVec.ofInt 32 (-2147483588)).sshiftRight' 2#32 == 0#32) = 1#1 →
      ¬(2#32 ≥ ↑32 ∨
            True ∧ (x_1.sshiftRight' 2#32 &&& BitVec.ofInt 32 (-536870897)).msb = true ∨
              zeroExtend 64 (x_1.sshiftRight' 2#32 &&& BitVec.ofInt 32 (-536870897)) ≥ ↑64) →
        x = x.sshiftRight' (zeroExtend 64 (x_1.sshiftRight' 2#32 &&& BitVec.ofInt 32 (-536870897)))

theorem test1_proof : test1_before ⊑ test1_after

lemma complete_stepSet_sink {M : NFA α σ} :
    .inr () ∈ S → .inr () ∈ M.complete.stepSet S a

theorem no_shift_xor_multiuse_cmp_xor_thm.extracted_1._2 : ∀ (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 toTensor_length_eq_rep_length [Fact (q > 1)] (a : R q n) :
  a.toTensor.length = a.repLength

theorem trunc_ashr_trunc_outofrange_thm (e : IntW 64) :
  trunc 8 (ashr (trunc 32 e) (const? 32 25)) ⊑
    trunc 8 (ashr (trunc 32 e) (const? 32 25)) { «nsw» := true, «nuw» := false }

theorem uge_or_not_max_commute_thm (e e_1 : IntW 8) :
  LLVM.or (icmp IntPred.ne e_1 (const? 8 (-1))) (icmp IntPred.uge e_1 e) ⊑ const? 1 1

theorem test1_thm (e : IntW 17) :
  trunc 17 (LLVM.or (lshr (zext 37 e) (const? 37 8)) (shl (zext 37 e) (const? 37 8))) ⊑
    LLVM.or (lshr e (const? 17 8)) (shl e (const? 17 8))

theorem e_1390 :
     - 6 *  ~~~(z ^^^ t) + 5 * t + 2 *  ~~~z - 11 *  ~~~(z &&&  ~~~z) + 11 * (z ||| t) - 6 * (z ^^^ t) - 7 * (z |||  ~~~t) - 1 *  ~~~(z |||  ~~~t) + 18 * (z &&&  ~~~t) + 13 * (z &&& t) = 5 * z - 22 *  ~~~(z ||| t)

theorem sdiv_exact_ne_1_thm (e e_1 : IntW 8) :
  icmp IntPred.eq (LLVM.sdiv e_1 e { «exact» := true }) (const? 8 0) ⊑
    icmp IntPred.eq e_1 (const? 8 0)

theorem e_1726 :
     - 5 * ((a |||  ~~~b) &&& (a ^^^ (b ^^^ c))) - 6 * c - 1 *  ~~~(a |||  ~~~c) - 1 * ((a &&& b) ^^^ (b |||  ~~~c)) - 5 * (b ^^^  ~~~( ~~~a &&& (b &&& c))) + 4 * (c ^^^ (a ||| (b &&& c))) - 1 *  ~~~(a &&&  ~~~a) + 1 * (b ^^^ (a ||| c)) - 1 * ( ~~~(a ||| b) |||  ~~~(a ^^^ (b ^^^ c))) - 3 * ( ~~~(a ^^^ b) &&&  ~~~(a ^^^ c)) + 5 * (b ^^^ (a &&&  ~~~c)) - 1 * ((a ^^^ b) &&& (a ^^^ c)) + 11 * (c ^^^ ( ~~~a ||| ( ~~~b ||| c))) + 2 * (a ^^^ ( ~~~b &&& c)) - 11 * ((a ||| b) &&&  ~~~(b ^^^ c)) + 1 *  ~~~(a ^^^ ( ~~~b ||| c)) - 1 *  ~~~(a ^^^ (b ||| c)) + 1 * (b ^^^  ~~~( ~~~a &&& (b ||| c))) + 1 *  ~~~( ~~~a ||| (b ^^^ c)) - 11 * (b ^^^  ~~~(a &&& (b ||| c))) + 11 * (c ^^^  ~~~(a &&&  ~~~b)) + 3 * (c ^^^  ~~~( ~~~a &&& (b &&& c))) - 11 * (a &&&  ~~~b) + 8 *  ~~~(a ||| (b ||| c)) - 20 *  ~~~(a ||| ( ~~~b ||| c)) + 17 *  ~~~( ~~~a ||| (b ||| c)) - 6 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 34 * ( ~~~a &&& ( ~~~b &&& c)) + 18 * ( ~~~a &&& (b &&& c)) + 11 * (a &&& ( ~~~b &&& c)) + 29 * (a &&& (b &&& c)) = 11 *  ~~~(a ||| (b &&& c))

theorem lshr_neg_sgt_minus_1_thm (e : IntW 8) :
  icmp IntPred.sgt (lshr (const? 8 (-17)) e) (const? 8 (-1)) ⊑ icmp IntPred.ne e (const? 8 0)

theorem in_constant_6_vary_invmask_thm (e e_1 : IntW 4) :
  LLVM.xor (LLVM.and (LLVM.xor e_1 (const? 4 6)) (LLVM.xor e (const? 4 (-1)))) e_1 ⊑
    LLVM.xor (LLVM.and (LLVM.xor e_1 (const? 4 6)) e) (const? 4 6)

theorem ugt_or_not_min_commute_logical_thm.extracted_1._3 : ∀ (x x_1 : BitVec 8),
  ¬ofBool (x_1 != 0#8) = 1#1 → ofBool (x <ᵤ x_1) = ofBool (x_1 != 0#8)

theorem addhshlhsdivhscalar1_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬((BitVec.ofInt 8 (-64) == 0 || 8 != 1 && x == intMin 8 && BitVec.ofInt 8 (-64) == -1) = true ∨ 6#8 ≥ ↑8) →
    ¬(64#8 == 0 || 8 != 1 && x == intMin 8 && 64#8 == -1) = true →
      x.sdiv (BitVec.ofInt 8 (-64)) <<< 6#8 + x = x.srem 64#8

theorem shl_mul_mask_proof : shl_mul_mask_before ⊑ shl_mul_mask_after

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

lemma CNFA.autWidth_bv_language :
    (autWidth wp n).bv_recognizes { bv | wp.sat bv.w n }

theorem test_with_5_proof : test_with_5_before ⊑ test_with_5_after

theorem test_mul_nsw__nsw_is_safe_proof : test_mul_nsw__nsw_is_safe_before ⊑ test_mul_nsw__nsw_is_safe_after

theorem e_2025 :
    3 * (f ^^^ (d &&& (e ||| f))) + 4 * ((d &&& e) ^^^ (d ^^^ ( ~~~e ||| f))) - 1 * ((d ^^^ e) &&& (d ^^^ f)) - 1 * (e ^^^  ~~~(d |||  ~~~f)) - 6 *  ~~~(d |||  ~~~e) - 5 * (e ^^^  ~~~(d ||| f)) + 1 * ((d ^^^ e) |||  ~~~(d ^^^ f)) + 5 * d - 1 *  ~~~f - 5 * (e ^^^  ~~~(d &&& (e &&& f))) + 2 * (e ^^^ ( ~~~d &&& (e ||| f))) - 1 * e - 11 * (e ^^^ ( ~~~d ||| (e ||| f))) + 2 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) + 11 * (d ^^^ (e ^^^ f)) + 1 *  ~~~(d ||| (e &&& f)) + 4 * (e &&&  ~~~(d ^^^ f)) + 1 * (f &&& (d ||| e)) + 5 * (f &&&  ~~~(d &&& e)) - 1 * ((d &&& e) ||| (e ^^^ f)) + 2 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) + 7 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) + 1 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) + 1 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) + 5 * (f ^^^ (d ||| (e ||| f))) - 2 * (f ^^^  ~~~(d |||  ~~~e)) - 2 * ( ~~~(d &&& e) &&& (e ^^^ f)) + 4 *  ~~~(d ||| (e ||| f)) - 17 *  ~~~(d ||| ( ~~~e ||| f)) - 18 *  ~~~( ~~~d ||| (e ||| f)) - 6 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 13 * ( ~~~d &&& ( ~~~e &&& f)) - 4 * ( ~~~d &&& (e &&& f)) + 2 * (d &&& ( ~~~e &&& f)) - 21 * (d &&& (e &&& f)) = 2 * (d ||| f) - 1 * (f ^^^ (d ||| (e &&& f)))

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

theorem ashr_ult_6_proof : ashr_ult_6_before ⊑ ashr_ult_6_after

theorem ne_umin2_proof : ne_umin2_before ⊑ ne_umin2_after

theorem ashrsgt_01_01_exact_proof : ashrsgt_01_01_exact_before ⊑ ashrsgt_01_01_exact_after

theorem test2_proof : test2_before ⊑ test2_after

theorem t3_exact_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬(True ∧ x >>> 63#64 <<< 63#64 ≠ x ∨ 63#64 ≥ ↑64) →
    ¬(True ∧ x >>> 63#64 <<< 63#64 ≠ x ∨
          63#64 ≥ ↑64 ∨
            True ∧ signExtend 64 (truncate 32 (x >>> 63#64)) ≠ x >>> 63#64 ∨
              True ∧ zeroExtend 64 (truncate 32 (x >>> 63#64)) ≠ x >>> 63#64) →
      0#32 - truncate 32 (x.sshiftRight' 63#64) = truncate 32 (x >>> 63#64)

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

theorem masked_icmps_mask_notallzeros_bmask_mixed_1b_logical_proof : masked_icmps_mask_notallzeros_bmask_mixed_1b_logical_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_1b_logical_after

theorem mul130_low_thm (e e_1 : IntW 130) :
  add
      (shl
        (add (mul (lshr e_1 (const? 130 65)) (LLVM.and e (const? 130 36893488147419103231)))
          (mul (LLVM.and e_1 (const? 130 36893488147419103231)) (lshr e (const? 130 65))))
        (const? 130 65))
      (mul (LLVM.and e_1 (const? 130 36893488147419103231)) (LLVM.and e (const? 130 36893488147419103231))) ⊑
    mul e e_1

theorem ule_swap_and_min_commute_logical_proof : ule_swap_and_min_commute_logical_before ⊑ ule_swap_and_min_commute_logical_after

theorem icmp_eq_or_z_or_pow2orz_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 == 0#8 - x &&& x) ||

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

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

theorem sle_and_min_proof : sle_and_min_before ⊑ sle_and_min_after

theorem sge_or_not_max_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), ofBool (x ≤ₛ x_1) ||

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

theorem exact_lshr_eq_opposite_msb_thm (e : IntW 8) :
  icmp IntPred.eq (lshr (const? 8 (-128)) e { «exact» := true }) (const? 8 1) ⊑
    icmp IntPred.eq e (const? 8 7)

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

theorem test_shift_nonnegative_thm (e : IntW 32) :
  icmp IntPred.sge (shl (lshr e (const? 32 2)) (const? 32 3) { «nsw» := true, «nuw» := false }) (const? 32 0) ⊑
    const? 1 1

theorem positive_with_signbit_proof : positive_with_signbit_before ⊑ positive_with_signbit_after

theorem test5_proof : test5_before ⊑ test5_after

theorem test23_logical_proof : test23_logical_before ⊑ test23_logical_after

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

theorem e_1189 :
     - 11 *  ~~~(z ^^^ t) + 4 * z + 1 * (z |||  ~~~t) - 5 *  ~~~(z &&& t) + 3 *  ~~~(z &&&  ~~~t) + 23 *  ~~~(z ||| t) + 13 *  ~~~(z |||  ~~~t) + 14 * (z &&& t) =  - 11 * (z &&&  ~~~t) + 11 *  ~~~(z &&&  ~~~z)

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

theorem test3_thm.extracted_1._1 : ∀ (x : BitVec 32), ¬8#32 = 0 → x % 8#32 = x &&& 7#32

theorem urem_i8_proof : urem_i8_before ⊑ urem_i8_after

theorem bv_AndOrXor_2647 :
    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.and e e_1) (LLVM.xor e e_1) ⊑ LLVM.or e e_1
</all_available_lemmas>

<local_ctx>
import Mathlib.Data.Fintype.Prod

import Blase.AutoStructs.Worklist

import Mathlib.Tactic.ApplyFun

open SetRel

section sink

variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A]

end sink

section generic_prod

variable {α} [BEq α] [Hashable α] [LawfulBEq α]

variable {β} [BEq β] [Hashable β] [LawfulBEq β]

variable {S₁ : Finset α} {S₂ : Finset β}

variable {γ} (f : S₁ → S₂ → γ) (hinj : Function.Injective2 f)

variable {m₁ : Std.HashSet α} (hm₁ : ∀ s₁ ∈ m₁, s₁ ∈ S₁)

variable {m₂ : Std.HashSet β} (hm₂ : ∀ s₂ ∈ m₂, s₂ ∈ S₂)

@[inline]
def product.prodArray' (a : Array γ) :=
  m₁.attachWith _ hm₁ |>.fold (init := a) fun is s1 =>
    m₂.attachWith _ hm₂ |>.fold (init := is) fun is s2 =>
      is.push (f s1 s2)

end generic_prod

section product

variable {A : Type} [BEq A] [LawfulBEq A] [Hashable A] [DecidableEq A] [FinEnum A]

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

<target_theorem>
lemma product.f_spec {m₁ m₂ : CNFA n} {s₁ : m₁.m.states} {s₂ : m₂.m.states} :
    ∀ a s₁' s₂',
      (a, (s₁', s₂')) ∈ f m₁ m₂ (s₁, s₂) ↔ s₁'.val ∈ m₁.m.tr s₁ a ∧ s₂'.val ∈ m₂.m.tr s₂ a :=
</target_theorem>

