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>
Nat in Init.Prelude
BitVec in Init.Prelude
Set in Mathlib.Data.Set.Defs
Finset in Mathlib.Data.Finset.Defs
Finset.range in Mathlib.Data.Finset.Range
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
LawfulBEq in Init.Core

abbrev State := Nat

def RawCNFA.states (m : RawCNFA A) : Finset State := Finset.range m.stateMax

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

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

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

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

def pr33078_3_before := [llvm|
{
^0(%arg3 : i8):
  %0 = llvm.mlir.constant(12 : i16) : i16
  %1 = llvm.sext %arg3 : i8 to i16
  %2 = llvm.lshr %1, %0 : i16
  %3 = llvm.trunc %2 : i16 to i4
  "llvm.return"(%3) : (i4) -> ()
}
]

Nat.reduceAdd in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat

def test10_before := [llvm|
{
^0(%arg107 : i32, %arg108 : i32):
  %0 = llvm.xor %arg107, %arg108 : i32
  %1 = llvm.and %arg107, %arg108 : i32
  %2 = llvm.xor %0, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def n2_badmask_before := [llvm|
{
^0(%arg4 : i32, %arg5 : i32, %arg6 : i32, %arg7 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg6, %arg4 : i32
  %2 = llvm.xor %arg7, %0 : i32
  %3 = llvm.and %2, %arg5 : i32
  %4 = llvm.add %1, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def test2_before := [llvm|
{
^0(%arg0 : i999, %arg1 : i999):
  %0 = llvm.mlir.constant(65280 : i999) : i999
  %1 = llvm.and %arg0, %0 : i999
  %2 = llvm.and %arg1, %0 : i999
  %3 = llvm.icmp "ne" %1, %2 : i999
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def fold_sext_to_and_wrong9_before := [llvm|
{
^0(%arg1 : i8):
  %0 = llvm.mlir.constant(128 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.sext %arg1 : i8 to i32
  %3 = llvm.and %2, %0 : i32
  %4 = llvm.icmp "ne" %3, %1 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

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

def llvm_udiv_lower_riscv_flag_32: LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] :=
  {lhs := udiv_llvm_exact_32, rhs := udiv_riscv_32, correct := sorry }

BitVec.shiftConcat in Init.Data.BitVec.Basic

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

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

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

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

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

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

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

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

def icmp_eq_and_pow2_shl_pow2_negative2_before := [llvm|
{
^0(%arg60 : i32):
  %0 = llvm.mlir.constant(2 : i32) : i32
  %1 = llvm.mlir.constant(14 : i32) : i32
  %2 = llvm.mlir.constant(0 : i32) : i32
  %3 = llvm.shl %0, %arg60 : i32
  %4 = llvm.and %3, %1 : i32
  %5 = llvm.icmp "eq" %4, %2 : i32
  %6 = llvm.zext %5 : i1 to i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def scalar_i64_shl_ult_const_before := [llvm|
{
^0(%arg14 : i64):
  %0 = llvm.mlir.constant(25) : i64
  %1 = llvm.mlir.constant(8589934592) : i64
  %2 = llvm.shl %arg14, %0 : i64
  %3 = llvm.icmp "ult" %2, %1 : i64
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def State.cseRegionArgList
  {Γstart Γ : Ctxt d.Ty}
  {lets : Lets d Γstart .pure Γ}
  (_ : State d lets)
  {ts : RegionSignature d.Ty}
  (rs : HVector ((fun t => Com d t.1 .impure t.2)) <| ts) :
  {rs' : HVector ((fun t => Com d t.1 .impure t.2)) <| ts //
    HVector.denote rs = HVector.denote rs' } :=
  let _ := HVector.map (fun _Γα com => Com.denote com) rs
  match ts, rs with
  | _, .nil => ⟨.nil, by admit /- proof elided -/
    ⟩
  | ⟨Γ, t⟩::ts, .cons region rs =>
    
    
    
    
    ⟨.cons region rs, by admit /- proof elided -/
    ⟩

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 and_logic_and_logic_or_1_before := [llvm|
{
^0(%arg138 : i1, %arg139 : i1, %arg140 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.and %arg138, %arg139 : i1
  %3 = "llvm.select"(%arg138, %arg140, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%2, %1, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def add_signbit_select_shl_before := [llvm|
{
^0(%arg34 : i32, %arg35 : i1):
  %0 = llvm.mlir.constant(-65536 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.add %arg34, %0 : i32
  %3 = "llvm.select"(%arg35, %2, %arg34) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %4 = llvm.shl %3, %1 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

def add_const_const_sub_before := [llvm|
{
^0(%arg61 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.add %arg61, %0 : i32
  %3 = llvm.sub %1, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def test7_before := [llvm|
{
^0(%arg44 : i8):
  %0 = llvm.mlir.constant(-1 : i29) : i29
  %1 = llvm.zext %arg44 : i8 to i29
  %2 = llvm.ashr %0, %1 : i29
  "llvm.return"(%2) : (i29) -> ()
}
]

def test24_before := [llvm|
{
^0(%arg53 : i32):
  %0 = llvm.mlir.constant(-2147483648 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.urem %arg53, %0 : i32
  %3 = llvm.icmp "ne" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def commutativity_constant_14_vary_before := [llvm|
{
^0(%arg12 : i4, %arg13 : i4):
  %0 = llvm.mlir.constant(-2 : i4) : i4
  %1 = llvm.mlir.constant(1 : i4) : i4
  %2 = llvm.xor %arg12, %0 : i4
  %3 = llvm.and %2, %1 : i4
  %4 = llvm.xor %arg12, %3 : i4
  "llvm.return"(%4) : (i4) -> ()
}
]

def ne_shift_in_zeros_before := [llvm|
{
^0(%arg32 : i32, %arg33 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(16 : i32) : i32
  %2 = llvm.lshr %arg32, %0 : i32
  %3 = llvm.trunc %2 : i32 to i8
  %4 = llvm.lshr %arg32, %1 : i32
  %5 = llvm.trunc %4 : i32 to i24
  %6 = llvm.lshr %arg33, %0 : i32
  %7 = llvm.trunc %6 : i32 to i8
  %8 = llvm.lshr %arg33, %1 : i32
  %9 = llvm.trunc %8 : i32 to i24
  %10 = llvm.icmp "ne" %3, %7 : i8
  %11 = llvm.icmp "ne" %5, %9 : i24
  %12 = llvm.or %11, %10 : i1
  "llvm.return"(%12) : (i1) -> ()
}
]

def test7_after := [llvm|
{
^0(%arg7 : i47):
  %0 = llvm.mlir.constant(39 : i47) : i47
  %1 = llvm.lshr %arg7, %0 : i47
  "llvm.return"(%1) : (i47) -> ()
}
]

def a_false_implies_b_true2_comm_before := [llvm|
{
^0(%arg9 : i8, %arg10 : i1, %arg11 : i1):
  %0 = llvm.mlir.constant(10 : i8) : i8
  %1 = llvm.mlir.constant(20 : i8) : i8
  %2 = llvm.icmp "ugt" %arg9, %0 : i8
  %3 = llvm.icmp "ult" %arg9, %1 : i8
  %4 = "llvm.select"(%3, %arg10, %arg11) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %5 = llvm.or %4, %2 : i1
  "llvm.return"(%5) : (i1) -> ()
}
]

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

def or_xor_and_commuted2_before := [llvm|
{
^0(%arg48 : i32, %arg49 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.mul %arg49, %arg49 : i32
  %2 = llvm.mul %arg48, %arg48 : i32
  %3 = llvm.xor %1, %0 : i32
  %4 = llvm.xor %2, %3 : i32
  %5 = llvm.or %4, %1 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

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

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

def TermUnop.openTerm (op : TermUnop) : Term :=
  match op with
  | .neg => .neg (.var 0)
  | .not => .not (.var 0)
  | .shiftL k => .shiftL (.var 0) k

structure Item where
 name : String
 tac : Syntax

def urem {w : Nat} (x y : IntW w) : IntW w := do
  let x' ← x
  let y' ← y
  urem? x' y'

Lean.ofReduceBool in Init.Core

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

def test_negative_nsw_and_unsigned_pred_before := [llvm|
{
^0(%arg52 : i64):
  %0 = llvm.mlir.constant(10) : i64
  %1 = llvm.mlir.constant(3) : i64
  %2 = llvm.sub %0, %arg52 overflow<nsw> : i64
  %3 = llvm.icmp "ult" %2, %1 : i64
  "llvm.return"(%3) : (i1) -> ()
}
]

def test88_after := [llvm|
{
^0(%arg57 : i16):
  %0 = llvm.mlir.constant(15 : i16) : i16
  %1 = llvm.ashr %arg57, %0 : i16
  "llvm.return"(%1) : (i16) -> ()
}
]

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

def ne_3210_after := [llvm|
{
^0(%arg74 : i32, %arg75 : i32):
  %0 = llvm.icmp "ne" %arg74, %arg75 : i32
  "llvm.return"(%0) : (i1) -> ()
}
]

instance : DecidableEq (IntW w) :=

instance : Inhabited (
  {lets : Lets d Γstart .pure Γ} →
  State d lets →
  (com: Com d Γ .pure α) →
  { com' : Com d Γ .pure α // ∀ (V: Ctxt.Valuation Γ), com.denote V = com'.denote V }) where
  default := fun _s com => ⟨com, by admit /- proof elided -/
  ⟩

def test12_after := [llvm|
{
^0(%arg46 : i32, %arg47 : i32):
  %0 = llvm.mlir.constant(1431655765 : i32) : i32
  %1 = llvm.and %arg46, %0 : i32
  %2 = llvm.sub %arg47, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def positive_biggerashr_shlnuwnsw_ashrexact_after := [llvm|
{
^0(%arg25 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.ashr exact %arg25, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def scalar_i32_lshr_and_negC_slt_before := [llvm|
{
^0(%arg4 : i32, %arg5 : i32):
  %0 = llvm.mlir.constant(-8 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.lshr %arg4, %arg5 : i32
  %3 = llvm.and %2, %0 : i32
  %4 = llvm.icmp "slt" %3, %1 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

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

def trunc_equality_nuw_after := [llvm|
{
^0(%arg44 : i16, %arg45 : i16):
  %0 = llvm.icmp "eq" %arg44, %arg45 : i16
  "llvm.return"(%0) : (i1) -> ()
}
]

def neg_nsw_slt_1_after := [llvm|
{
^0(%arg19 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.icmp "sgt" %arg19, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

Function.RightInverse in Init.Data.Function

def worklistRun'_spec :
    (worklistRun' A S final inits hinits f |>.Sim $ nfa inits final f) :=

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

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

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

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

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

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

def udiv_i32_c_multiuse_before := [llvm|
{
^0(%arg12 : i8):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.zext %arg12 : i8 to i32
  %2 = llvm.udiv %1, %0 : i32
  %3 = llvm.add %1, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

private def attrVal0Str : AttrVal := [mlir_attr_val| "foo"]

@[reducible]
instance : DialectDenote ExOp ExTy where
  denote
    | .add, .cons (a : Nat) (.cons b .nil), _ => a + b
    | .runK (k : Nat), (.cons (v : Nat) .nil), (.cons rgn _nil) =>
      k.iterate (fun val => rgn (fun _ty _var => val)) v

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

def and_or_not_not_wrong_a_before := [llvm|
{
^0(%arg332 : i32, %arg333 : i32, %arg334 : i32, %arg335 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg333, %arg335 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.and %arg332, %arg334 : i32
  %4 = llvm.xor %3, %0 : i32
  %5 = llvm.or %4, %arg333 : i32
  %6 = llvm.and %5, %2 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def positive_samevar_ashrexact_before := [llvm|
{
^0(%arg42 : i8, %arg43 : i8):
  %0 = llvm.ashr exact %arg42, %arg43 : i8
  %1 = llvm.shl %0, %arg43 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

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

def or_eq_with_one_bit_diff_constants2_after := [llvm|
{
^0(%arg362 : i32):
  %0 = llvm.mlir.constant(-33 : i32) : i32
  %1 = llvm.mlir.constant(65 : i32) : i32
  %2 = llvm.and %arg362, %0 : i32
  %3 = llvm.icmp "eq" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

BitVec.sdiv in Init.Data.BitVec.Basic

def getSimpData (simpsetName : Name) : MetaM (SimpTheorems × Simprocs) := do
  let some ext ← (getSimpExtension? simpsetName)
    | throwError m!"'{simpsetName}' simp attribute not found!"
  let theorems ← ext.getTheorems
  let some ext ← (Simp.getSimprocExtension? simpsetName)
    | throwError m!"'{simpsetName}' simp attribute not found!"
  let simprocs ← ext.getSimprocs
  return (theorems, simprocs)

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

@[match_pattern] def add (w : Width φ)
  (NoWrapFlags: NoWrapFlags := {nsw := false , nuw := false}) : MOp φ
    := .binary w (.add NoWrapFlags )

HAppend in Init.Prelude

def llvm_trunc_riscv_32_to_8_nuw_nsw : LLVMPeepholeRewriteRefine 8 [Ty.llvm (.bitvec 32)] :=
  {lhs:= trunc_llvm_32_to_8_nsw_nuw, rhs:= trunc_riscv_32_to_8_nsw_nuw}

def no_shift_xor_multiuse_or_after := [llvm|
{
^0(%arg134 : i32, %arg135 : i32):
  %0 = llvm.mlir.constant(4096 : i32) : i32
  %1 = llvm.and %arg134, %0 : i32
  %2 = llvm.or %arg135, %0 : i32
  %3 = llvm.xor %1, %0 : i32
  %4 = llvm.or %arg135, %3 : i32
  %5 = llvm.mul %4, %2 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

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

|

Lean.Meta.mkEq in Lean.Meta.AppBuilder

return none
</all_available_defs>

<all_available_lemmas>
Finset.mem_range in Mathlib.Data.Finset.Range
Nat.lt_of_le_of_lt in Init.Prelude
Set.mem_insert_iff in Mathlib.Data.Set.Insert
Set.union_singleton in Mathlib.Data.Set.Insert
not_lt in Mathlib.Order.Defs.LinearOrder

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 }

theorem or_and2_proof : or_and2_before ⊑ or_and2_after

theorem or_xor_common_op_commute6_thm (e e_1 e_2 : IntW 8) :
  LLVM.or (LLVM.xor e_2 e_1) (LLVM.or e_1 e) ⊑ LLVM.or (LLVM.or e_1 e) e_2

theorem e_9 :
     - 2 * (x ^^^ y) + 11 * (x ||| y) + 5 * y - 9 * (x &&&  ~~~y) = 14 *  ~~~(x |||  ~~~y) + 16 * (x &&& y)

theorem zext_or_masked_bit_test_proof : zext_or_masked_bit_test_before ⊑ zext_or_masked_bit_test_after

theorem e_786 :
     - 1 *  ~~~t - 1 * (z |||  ~~~t) - 7 * z + 2 *  ~~~(z ||| t) + 9 * (z &&&  ~~~t) =  - 8 * (z &&& t)

theorem udiv_c_i32_proof : udiv_c_i32_before ⊑ udiv_c_i32_after

theorem AvoidCollision_getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
    (x.setWidth m)[i]? = if i < m then some (x.getLsbD i) else none

theorem and_nosignbit_select_shl_thm.extracted_1._1 : ∀ (x : BitVec 32) (x_1 : BitVec 1),
  x_1 = 1#1 → ¬8#32 ≥ ↑32 → (x &&& 2147418112#32) <<< 8#32 = x <<< 8#32 &&& BitVec.ofInt 32 (-16777216)

theorem test69_xor_proof : test69_xor_before ⊑ test69_xor_after

theorem shr_umax_proof : shr_umax_before ⊑ shr_umax_after

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

theorem main3d_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 7#32 != 0#32) = 1#1 → True → 0#32 = zeroExtend 32 (ofBool (x &&& 23#32 == 0#32))

theorem sext_sub_const_thm.extracted_1._1 : ∀ (x : BitVec 1), x = 1#1 → 42#64 - signExtend 64 x = 43#64

theorem ugt_swap_or_not_min_logical_proof : ugt_swap_or_not_min_logical_before ⊑ ugt_swap_or_not_min_logical_after

theorem negtest_near_pow2_cmpval_isnt_close_to_pow2_proof : negtest_near_pow2_cmpval_isnt_close_to_pow2_before ⊑ negtest_near_pow2_cmpval_isnt_close_to_pow2_after

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

theorem test19_proof : test19_before ⊑ test19_after

theorem test3_thm.extracted_1._1 : ∀ (x : BitVec 64), zeroExtend 64 (truncate 8 x) = x &&& 255#64

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

theorem icmp_ne_sext_ne_otherwise_proof : icmp_ne_sext_ne_otherwise_before ⊑ icmp_ne_sext_ne_otherwise_after

theorem ugt_and_min_proof : ugt_and_min_before ⊑ ugt_and_min_after

theorem e_2375 :
     - 3 *  ~~~(d ^^^ ( ~~~e &&& f)) - 7 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) + 1 * (d &&& f) + 11 * (e ^^^  ~~~(d &&& (e ||| f))) + 1 * (e ^^^ (d &&&  ~~~f)) + 7 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) - 7 * ( ~~~d ||| ( ~~~e ||| f)) - 3 * (d ^^^ ( ~~~e ||| f)) - 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 6 * (f ^^^ (d ||| (e &&& f))) - 7 * (d |||  ~~~f) + 11 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) + 11 * ( ~~~e |||  ~~~(d ^^^ f)) - 1 * (d ^^^ e) - 2 * (f ^^^  ~~~(d &&& (e &&& f))) - 6 * (d ||| (e ^^^ f)) - 1 * (d &&& (e ^^^ f)) - 1 * (e &&&  ~~~(d &&& f)) - 1 * (e ^^^  ~~~(d ||| ( ~~~e &&& f))) - 3 * (f ^^^ ( ~~~d &&& (e ||| f))) + 11 * (e ^^^  ~~~( ~~~d &&& (e &&& f))) + 1 * (f |||  ~~~(d ||| e)) + 5 * (e &&& (d |||  ~~~f)) + 1 * ((d &&& e) |||  ~~~(e |||  ~~~f)) + 5 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) - 5 * (d ^^^ f) - 6 * (e ^^^ (d &&& (e ^^^ f))) - 1 * ((d ^^^ e) &&&  ~~~(d ^^^ f)) + 7 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) + 5 * ( ~~~d ||| (e ^^^ f)) - 11 *  ~~~(d &&&  ~~~d) + 5 * (d &&&  ~~~e) - 2 * (e ^^^ ( ~~~d ||| (e ||| f))) - 2 * (f ^^^  ~~~(d &&& (e ||| f))) + 11 * (f ^^^ (d ||| ( ~~~e ||| f))) + 1 * (d |||  ~~~e) - 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) - 1 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) - 2 * ( ~~~f &&&  ~~~(d ^^^ e)) - 1 *  ~~~(d ||| f) - 2 * ( ~~~(d &&& e) &&& (d ^^^ (e ^^^ f))) - 7 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) + 1 * ( ~~~(d ||| e) |||  ~~~(e ^^^ f)) - 2 * ((d &&& e) ^^^  ~~~(d ^^^ ( ~~~e ||| f))) - 6 * (f ||| (d &&& e)) - 11 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) + 4 * (e ^^^ (d ||| ( ~~~e &&& f))) + 2 * (f ^^^ (d ||| (e ||| f))) - 6 * ((d &&& e) ^^^ (d ^^^ ( ~~~e ||| f))) - 1 *  ~~~(d &&&  ~~~f) + 1 * (d &&& ( ~~~e ||| f)) + 2 * (f ^^^  ~~~(d &&&  ~~~e)) - 5 * ( ~~~d &&& (e ^^^ f)) - 3 * (e ^^^ ( ~~~d ||| (e ^^^ f))) - 3 * ((d &&&  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) + 7 *  ~~~(d ||| ( ~~~e &&& f)) + 1 * (d ^^^ (e ^^^ f)) + 1 * (e ^^^  ~~~( ~~~d &&& (e ^^^ f))) - 5 *  ~~~e + 4 * ((e &&&  ~~~f) ^^^ ( ~~~d ||| (e ^^^ f))) - 11 * (d ||| f) - 1 * (f ^^^ ( ~~~d ||| (e ||| f))) + 5 * (e ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) - 21 *  ~~~(d ||| (e ||| f)) + 35 *  ~~~(d ||| ( ~~~e ||| f)) + 9 *  ~~~( ~~~d ||| (e ||| f)) + 33 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 38 * ( ~~~d &&& ( ~~~e &&& f)) + 34 * ( ~~~d &&& (e &&& f)) + 6 * (d &&& ( ~~~e &&& f)) =  - 39 * (d &&& (e &&& f))

theorem lshr_xor_thm (e e_1 : IntW 8) :
  shl (LLVM.xor (lshr e_1 (const? 8 3)) (LLVM.srem e (const? 8 42))) (const? 8 3) ⊑
    LLVM.xor (LLVM.and e_1 (const? 8 (-8))) (shl (LLVM.srem e (const? 8 42)) (const? 8 3))

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

theorem test4_thm (e : IntW 32) :
  sext 64 (LLVM.udiv e (const? 32 3)) ⊑ zext 64 (LLVM.udiv e (const? 32 3)) { «nneg» := true }

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

theorem tail_iterate'' {α} {n} {s : Stream' α} : Stream'.iterate Stream'.tail s n m = s (n + m)

@[simp] theorem denote_mk {lets : Lets d Γ_in eff Γ_out} {com : Com d Γ_out eff ty} :
    denote ⟨lets, com⟩ = fun V => (lets.denote V) >>= com.denote

@[simp] theorem val_toArgResult (mapOut : MatchVarResult lets v (.var matchLets matchExpr) w.appendInl mapIn) :
    mapOut.toArgResult.val = mapOut.val

theorem ne_smax2_proof : ne_smax2_before ⊑ ne_smax2_after

theorem icmp_eq_sext_eq_allones_thm (e : IntW 32) :
  icmp IntPred.eq (sext 32 (icmp IntPred.eq e (const? 32 (-1)))) e ⊑
    icmp IntPred.ult (add e (const? 32 1)) (const? 32 2)

theorem lshr_xor_or_good_mask_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬(4#8 ≥ ↑8 ∨ 4#8 ≥ ↑8) →
    ¬(4#8 ≥ ↑8 ∨ True ∧ ((x ||| x_1) >>> 4#8 &&& 48#8 != 0) = true) →
      x_1 >>> 4#8 ||

@[simp]
theorem Term.toBV_boolConst {wenv : WidthExpr.Env wcard}
    {tctx : Term.Ctx wcard tcard}
    (benv : Term.BoolEnv bcard)
    (tenv : tctx.Env wenv) (b : Bool) :
  Term.toBV benv nenv ienv penv tenv (.boolConst b) = b

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

theorem alive_AndOrXor_2416 : alive_AndOrXor_2416_src ⊑ alive_AndOrXor_2416_tgt

theorem ofBitVec_sub : ofBitVecSext (x - y) ≈ʷ (ofBitVecSext x) - (ofBitVecSext y)

theorem pr51551_proof : pr51551_before ⊑ pr51551_after

theorem eq_getLsbD_toBitVec_of_lt (x : BitStream) (i : Nat) (hi : i < w) :
    x i = (x.toBitVec w).getLsbD i

theorem slt_zero_eq_ne_0_thm (e : IntW 32) :
  icmp IntPred.eq (zext 32 (icmp IntPred.ne e (const? 32 0))) (lshr e (const? 32 31)) ⊑
    icmp IntPred.slt e (const? 32 1)

theorem mul_select_zext_thm.extracted_1._3 : ∀ (x : BitVec 64) (x_1 : BitVec 1),
  ¬x_1 = 1#1 → 1#64 * zeroExtend 64 x_1 = 0#64

theorem eq_basic_proof : eq_basic_before ⊑ eq_basic_after

theorem test71_proof : test71_before ⊑ test71_after

theorem test_shl__nsw_is_safe_proof : test_shl__nsw_is_safe_before ⊑ test_shl__nsw_is_safe_after

theorem positive_samevar_shlnuwnsw_lshrexact_proof : positive_samevar_shlnuwnsw_lshrexact_before ⊑ positive_samevar_shlnuwnsw_lshrexact_after

theorem lshrult_03_14_proof : lshrult_03_14_before ⊑ lshrult_03_14_after

theorem p_constmask2_proof : p_constmask2_before ⊑ p_constmask2_after

theorem lshrult_03_12_proof : lshrult_03_12_before ⊑ lshrult_03_12_after

theorem lshrult_02_14_exact_proof : lshrult_02_14_exact_before ⊑ lshrult_02_14_exact_after

theorem test17_proof : test17_before ⊑ test17_after

theorem test2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (-1#32 <ₛ x_1) ||

theorem a_thm.extracted_1._1 : ∀ (x : BitVec 32), 8#32 - x &&& 7#32 = 0#32 - x &&& 7#32

theorem pr51551_neg2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(True ∧ (x_1 &&& BitVec.ofInt 32 (-7)).smulOverflow x = true) →
    truncate 1 x_1 ^^^ 1#1 = 1#1 → ofBool ((x_1 &&& BitVec.ofInt 32 (-7)) * x &&& 7#32 == 0#32) = 1#1

theorem and_two_ranges_to_mask_and_range_no_add_on_one_range_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ofBool (12#16 ≤ᵤ x) &&& (ofBool (x <ᵤ 16#16) ||| ofBool (28#16 ≤ᵤ x)) =
    ofBool (11#16 <ᵤ x &&& BitVec.ofInt 16 (-20))

theorem sext_multi_uses_thm.extracted_1._1 : ∀ (x : BitVec 64) (x_1 : BitVec 1) (x_2 : BitVec 64),
  x_1 = 1#1 → x_2 * signExtend 64 x_1 + ((x ^^^ signExtend 64 x_1) - signExtend 64 x_1) = 0#64 - (x_2 + x)

theorem zext_sext_add_icmp_sgt_0_thm.extracted_1._1 : ∀ (x x_1 : BitVec 1),
  ofBool (0#8 <ₛ zeroExtend 8 x_1 + signExtend 8 x) = x_1 &&& (x ^^^ 1#1)

theorem nomask_lhs_logical_thm (e : IntW 32) :
  select (icmp IntPred.eq e (const? 32 0)) (const? 1 1)
      (icmp IntPred.eq (LLVM.and e (const? 32 1)) (const? 32 0)) ⊑
    icmp IntPred.eq (LLVM.and e (const? 32 1)) (const? 32 0)

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

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

theorem test5_thm.extracted_1._1 : ∀ (x : BitVec 700),
  (x ||| 288230376151711743#700) ^^^ 288230376151711743#700 = x &&& BitVec.ofInt 700 (-288230376151711744)

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

theorem nonexact_lshr_eq_exactdiv_proof : nonexact_lshr_eq_exactdiv_before ⊑ nonexact_lshr_eq_exactdiv_after

theorem e_1557 :
     - 7 * (c ^^^ ( ~~~a ||| ( ~~~b &&& c))) - 5 * (c ^^^ (a &&& b)) + 5 * (c ^^^  ~~~(a &&& (b ||| c))) + 2 * (b ^^^ ( ~~~a ||| (b &&& c))) - 5 * ( ~~~(a ||| b) |||  ~~~(a ^^^ (b ^^^ c))) - 3 * (b ||| (a ^^^ c)) - 1 * (b ^^^  ~~~( ~~~a &&& (b ||| c))) + 7 *  ~~~(a ||| (b ||| c)) + 7 *  ~~~(a ||| ( ~~~b ||| c)) - 1 *  ~~~( ~~~a ||| (b ||| c)) + 12 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 12 * ( ~~~a &&& ( ~~~b &&& c)) + 15 * ( ~~~a &&& (b &&& c)) + 6 * (a &&& ( ~~~b &&& c)) = 1 *  ~~~(a &&& ( ~~~b ||| c)) - 5 * (a &&& (b &&& c))

theorem test_and_xor_freely_invertable_proof : test_and_xor_freely_invertable_before ⊑ test_and_xor_freely_invertable_after

theorem both_proof : both_before ⊑ both_after

theorem Lets.Γ_out_eq (l : Lets Op Γ_in Γ_out) : Γ_out = (Lets.outContext l.val Γ_in)

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

theorem n10_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬63#64 ≥ ↑64 → 1#64 - x >>> 63#64 = zeroExtend 64 (ofBool (-1#64 <ₛ x))

theorem test_ne_proof : test_ne_before ⊑ test_ne_after

theorem bools_logical_commute1_and2_proof : bools_logical_commute1_and2_before ⊑ bools_logical_commute1_and2_after

theorem uge_and_max_thm (e e_1 : IntW 8) :
  LLVM.and (icmp IntPred.uge e_1 e) (icmp IntPred.eq e_1 (const? 8 (-1))) ⊑
    icmp IntPred.eq e_1 (const? 8 (-1))

@[simp, grind =]
theorem mem_toList [LawfulBEq α] {k : α} :
    k ∈ m.toList ↔ k ∈ m

theorem bv_152 :
    ∀ (e : LLVM.IntW w), LLVM.mul e (LLVM.const? w (-1)) ⊑ LLVM.sub (LLVM.const? w 0) e

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

@[simp]
lemma proj_accepts (M : NFA' m) (f : Fin n → Fin m) :
    (M.proj f).accepts = BitVecs.transport f '' M.accepts

theorem sle_or_min_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 ≤ₛ x) = 1#1 → 1#1 = ofBool (x_1 ≤ₛ x)

theorem scalar_i32_shl_and_negC_eq_nonzero_proof : scalar_i32_shl_and_negC_eq_nonzero_before ⊑ scalar_i32_shl_and_negC_eq_nonzero_after

theorem scalar1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 4),
  ¬(True ∧ (x_1 &&& BitVec.ofInt 4 (-2) &&& (x &&& 1#4) != 0) = true) →
    (x_1 ^^^ x) &&& BitVec.ofInt 4 (-2) ^^^ x = x_1 &&& BitVec.ofInt 4 (-2) ||

theorem or_trunc_lshr_more_proof : or_trunc_lshr_more_before ⊑ or_trunc_lshr_more_after

theorem e_695 :
     - 11 * (x |||  ~~~y) + 7 *  ~~~(x &&&  ~~~x) - 11 * (x ^^^ y) - 2 * (x ||| y) - 2 *  ~~~x - 11 *  ~~~(x &&&  ~~~y) + 2 *  ~~~(x &&& y) + 12 *  ~~~(x ||| y) + 15 * (x &&&  ~~~y) + 14 * (x &&& y) =  - 17 *  ~~~(x |||  ~~~y) - 3 *  ~~~(x ^^^ y)

theorem masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_3_thm (e : IntW 32) :
  LLVM.or (icmp IntPred.ne (LLVM.and e (const? 32 7)) (const? 32 0))
      (icmp IntPred.eq (LLVM.and e (const? 32 15)) (const? 32 0)) ⊑
    icmp IntPred.ne (LLVM.and e (const? 32 15)) (const? 32 8)

@[simp]
theorem ofBitVecSextMsb_eq_concat_ofBitVec (x : BitVec w) :
    ofBitVecSextMsb x = (ofBitVecSext x).concat false

theorem ult_umin1_proof : ult_umin1_before ⊑ ult_umin1_after

theorem test2_thm (e : IntW 8) (e_1 : IntW 32) :
  LLVM.and (LLVM.or e_1 (zext 32 e)) (const? 32 65536) ⊑ LLVM.and e_1 (const? 32 65536)

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

theorem n2_proof : n2_before ⊑ n2_after

theorem lshr_exact_add_nuw_proof : lshr_exact_add_nuw_before ⊑ lshr_exact_add_nuw_after

theorem test2_proof : test2_before ⊑ test2_after

theorem test_ule_xor_proof : test_ule_xor_before ⊑ test_ule_xor_after

theorem or_and3_commuted_thm.extracted_1._3 : ∀ (x : BitVec 1) (x_1 x_2 : BitVec 32),
  ofBool (x_2 == x_1) ||

theorem ne_21_logical_proof : ne_21_logical_before ⊑ ne_21_logical_after

theorem negate_zext_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 8),
  x_1 - zeroExtend 8 x = x_1 + signExtend 8 x

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

theorem e_628 :
    5 * (x ^^^ y) + 1 *  ~~~x + 4 *  ~~~(x &&&  ~~~y) - 2 * x + 4 *  ~~~(x &&& y) + 2 *  ~~~(x ^^^ y) + 11 *  ~~~y - 22 *  ~~~(x ||| y) - 14 *  ~~~(x |||  ~~~y) - 18 * (x &&&  ~~~y) = 4 * (x &&& y)

theorem ule_swap_or_min_logical_proof : ule_swap_or_min_logical_before ⊑ ule_swap_or_min_logical_after

theorem positive_biggerlshr_shlnsw_proof : positive_biggerlshr_shlnsw_before ⊑ positive_biggerlshr_shlnsw_after

theorem test10b_proof : test10b_before ⊑ test10b_after

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

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

theorem xor_ashr_not_proof : xor_ashr_not_before ⊑ xor_ashr_not_after

theorem f_t15_t01_t09_thm.extracted_1._2 : ∀ (x : BitVec 40),
  ¬(31#40 ≥ ↑40 ∨ 16#32 ≥ ↑32) →
    ¬(15#40 ≥ ↑40 ∨ True ∧ signExtend 40 (truncate 32 (x.sshiftRight' 15#40)) ≠ x.sshiftRight' 15#40) →
      truncate 32 (x.sshiftRight' 31#40) <<< 16#32 = truncate 32 (x.sshiftRight' 15#40) &&& BitVec.ofInt 32 (-65536)

theorem udiv_shl_pair_const_proof : udiv_shl_pair_const_before ⊑ udiv_shl_pair_const_after

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

theorem ashr_mul_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬8#20 ≥ ↑20 →
    ¬(True ∧ (signExtend 16 x_1).smulOverflow (signExtend 16 x) = true ∨ 8#16 ≥ ↑16) →
      truncate 16 ((signExtend 20 x_1 * signExtend 20 x).sshiftRight' 8#20) =
        (signExtend 16 x_1 * signExtend 16 x).sshiftRight' 8#16

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

theorem f_proof : f_before ⊑ f_after

theorem trunc_shl_1_i32_i64_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬1#64 ≥ ↑64 → ¬1#32 ≥ ↑32 → truncate 32 (x <<< 1#64) = truncate 32 x <<< 1#32
</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₂)

end generic_prod

section product

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

end product

section determinization

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

private def bv_to_set (bv : BitVec w) : Set State :=
  { s | bv.getLsbD s }
</local_ctx>

<target_theorem>
@[simp]
lemma transBV_spec {m : CNFA n} {res} {s : m.m.states} :
    s' ∈ bv_to_set (m.m.transBV' res s a) ↔
      (s' ∈ bv_to_set res ∨ s' ∈ m.m.tr s a) :=
</target_theorem>

