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
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
Array in Init.Prelude
List.map in Init.Prelude
SetRel in Mathlib.Data.Rel
Set in Mathlib.Data.Set.Defs
NFA in Mathlib.Computability.NFA
Bool in Init.Prelude
List in Init.Prelude
Finset in Mathlib.Data.Finset.Defs
Option in Init.Prelude
Prod in Init.Prelude
Prod.mk in Init.Prelude
Finset.range in Mathlib.Data.Finset.Range
Fintype in Mathlib.Data.Fintype.Defs
SetRel.inv in Mathlib.Data.Rel
LawfulBEq in Init.Core
List.next in Mathlib.Data.List.Cycle
LawfulHashable in Init.Data.LawfulHashable
Inhabited in Init.Prelude
List.insert in Init.Data.List.Basic

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

abbrev State := Nat

structure RawCNFA.WF (m : RawCNFA A) where
  initials_lt : ∀ {s}, s ∈ m.initials → s ∈ m.states
  finals_lt : ∀ {s}, s ∈ m.finals → s ∈ m.states
  trans_src_lt : ∀ s_a ∈ m.trans, s_a.1 ∈ m.states
  trans_tgt_lt : s' ∈ m.tr s a → s' ∈ m.states

@[inline]
def RawCNFA.tr (m : RawCNFA A) s a := m.trans.getD (s, a) ∅

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

def RawCNFA.addFinal (m : RawCNFA A) (s : State) : RawCNFA A :=
  { m with finals := m.finals.insert s }

def RawCNFA.newState (m : RawCNFA A) : State × RawCNFA A :=
  let old := m.stateMax
  let m := { m with stateMax := old + 1 }
  (old, m)

def RawCNFA.addTrans (m : RawCNFA A) (a : A) (s s' : State) : RawCNFA A :=
  let ns := m.trans.getD (s, a) ∅
  let ns := ns.insert s'
  { m with trans :=  m.trans.insert (s, a) ns }

def and_logic_and_logic_or_3_before := [llvm|
{
^0(%arg132 : i1, %arg133 : i1, %arg134 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.and %arg133, %arg132 : i1
  %3 = "llvm.select"(%arg132, %arg134, %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 PR42691_6_logical_before := [llvm|
{
^0(%arg332 : i32):
  %0 = llvm.mlir.constant(-2147483647 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.mlir.constant(true) : i1
  %3 = llvm.icmp "ult" %arg332, %0 : i32
  %4 = llvm.icmp "eq" %arg332, %1 : i32
  %5 = "llvm.select"(%3, %2, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def or_not_and_commute9_before := [llvm|
{
^0(%arg510 : i32, %arg511 : i32, %arg512 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sdiv %0, %arg510 : i32
  %3 = llvm.sdiv %0, %arg511 : i32
  %4 = llvm.sdiv %0, %arg512 : i32
  %5 = llvm.or %2, %3 : i32
  %6 = llvm.xor %5, %1 : i32
  %7 = llvm.and %6, %4 : i32
  %8 = llvm.or %2, %4 : i32
  %9 = llvm.xor %8, %1 : i32
  %10 = llvm.and %3, %9 : i32
  %11 = llvm.or %7, %10 : i32
  "llvm.return"(%11) : (i32) -> ()
}
]

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

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

def ashr_mul_times_3_div_2_exact_2_after := [llvm|
{
^0(%arg17 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.ashr exact %arg17, %0 : i32
  %2 = llvm.add %arg17, %1 overflow<nsw> : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def t13_x_is_one_after := [llvm|
{
^0(%arg8 : i64, %arg9 : i32):
  %0 = llvm.mlir.constant(65536) : i64
  %1 = llvm.mlir.constant(0) : i64
  %2 = llvm.and %arg8, %0 : i64
  %3 = llvm.icmp "ne" %2, %1 : i64
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def shl_and_xor_after := [llvm|
{
^0(%arg158 : i8, %arg159 : i8):
  %0 = llvm.mlir.constant(10 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.and %arg158, %0 : i8
  %3 = llvm.xor %arg159, %2 : i8
  %4 = llvm.shl %3, %1 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

def lshr_and_after := [llvm|
{
^0(%arg73 : i8, %arg74 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(6 : i8) : i8
  %2 = llvm.srem %arg73, %0 : i8
  %3 = llvm.shl %2, %1 : i8
  %4 = llvm.and %arg74, %3 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

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

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

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

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

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

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

def example01 := [RV64_com| {
^bb0(%0 : !i64, %1 : !i64):
  
  
 
    %5 = "add"(%0, %0) : (!i64, !i64) -> (!i64)
  
  "ret" (%0) : (!i64) -> ()
 }]

def sub_ashr_and_i16_before := [llvm|
{
^0(%arg29 : i16, %arg30 : i16):
  %0 = llvm.mlir.constant(15 : i16) : i16
  %1 = llvm.sub %arg30, %arg29 overflow<nsw> : i16
  %2 = llvm.ashr %1, %0 : i16
  %3 = llvm.and %2, %arg29 : i16
  "llvm.return"(%3) : (i16) -> ()
}
]

@[simp_denote]
def trunc_llvm_64_to_32_nuw := [LV| {
  ^entry (%lhs: i64):
    %0 = llvm.trunc %lhs overflow<nuw> : i64 to i32
    llvm.return %0 : i32
  }]

inductive Ty
| int : Ty
| ix : Ty
| tensor2d : Ty
deriving DecidableEq, Inhabited

def icmp_ne1_before := [llvm|
{
^0(%arg0 : i8):
  %0 = llvm.mlir.constant(6 : i8) : i8
  %1 = llvm.mlir.constant(-128 : i8) : i8
  %2 = llvm.shl %arg0, %0 overflow<nsw> : i8
  %3 = llvm.icmp "ne" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

def and_or2_wrong_operand_before := [llvm|
{
^0(%arg172 : i1, %arg173 : i1, %arg174 : i1, %arg175 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.xor %arg174, %0 : i1
  %2 = llvm.and %1, %arg173 : i1
  %3 = "llvm.select"(%2, %arg172, %arg175) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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 bools_logical_commute1_after := [llvm|
{
^0(%arg96 : i1, %arg97 : i1, %arg98 : i1):
  %0 = "llvm.select"(%arg98, %arg97, %arg96) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def test_after := [llvm|
{
^0(%arg0 : i26):
  "llvm.return"(%arg0) : (i26) -> ()
}
]

def test37_after := [llvm|
{
^0(%arg241 : i32):
  %0 = llvm.mlir.constant(7 : i32) : i32
  %1 = llvm.mlir.constant(240 : i32) : i32
  %2 = llvm.mul %arg241, %0 : i32
  %3 = llvm.and %2, %1 : i32
  %4 = llvm.zext nneg %3 : i32 to i64
  "llvm.return"(%4) : (i64) -> ()
}
]

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)⟩]

def sle_swap_and_min_logical_after := [llvm|
{
^0(%arg212 : i8, %arg213 : i8):
  %0 = llvm.mlir.constant(-128 : i8) : i8
  %1 = llvm.icmp "eq" %arg212, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def or_and3_after := [llvm|
{
^0(%arg104 : i1, %arg105 : i1, %arg106 : i32, %arg107 : i32):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.icmp "ne" %arg106, %arg107 : i32
  %3 = "llvm.select"(%2, %arg105, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%arg104, %1, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

inductive Circuit (α : Type u) : Type u
  | tru : Circuit α
  | fals : Circuit α
   
  | var : (positive: Bool) → α → Circuit α
  | and : Circuit α → Circuit α → Circuit α
  | or : Circuit α → Circuit α → Circuit α
  | xor : Circuit α → Circuit α → Circuit α
deriving Repr, DecidableEq

def ule_umax2_after := [llvm|
{
^0(%arg50 : i32, %arg51 : i32):
  %0 = llvm.icmp "ule" %arg51, %arg50 : i32
  "llvm.return"(%0) : (i1) -> ()
}
]

def xor_icmp_to_icmp_add_after := [llvm|
{
^0(%arg4 : i32):
  %0 = llvm.mlir.constant(-6 : i32) : i32
  %1 = llvm.mlir.constant(-2 : i32) : i32
  %2 = llvm.add %arg4, %0 : i32
  %3 = llvm.icmp "ult" %2, %1 : i32
  "llvm.return"(%3) : (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 and_logic_and_logic_or_3_before := [llvm|
{
^0(%arg132 : i1, %arg133 : i1, %arg134 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.and %arg133, %arg132 : i1
  %3 = "llvm.select"(%arg132, %arg134, %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 uadd_sat_flipped_wrong_bounds6_before := [llvm|
{
^0(%arg91 : i32):
  %0 = llvm.mlir.constant(-12 : i32) : i32
  %1 = llvm.mlir.constant(9 : i32) : i32
  %2 = llvm.mlir.constant(-1 : i32) : i32
  %3 = llvm.icmp "ule" %arg91, %0 : i32
  %4 = llvm.add %arg91, %1 : i32
  %5 = "llvm.select"(%3, %4, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

@[simp_denote]
def sext_llvm_i8_to_32 := [LV| {
  ^entry (%arg: i8):
    %0 = llvm.sext %arg: i8 to i32
    llvm.return %0: i32
  }]

def icmp_x_slt_0_and_icmp_y_sgt_neg1_i32_fail_after := [llvm|
{
^0(%arg40 : i32, %arg41 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.icmp "sgt" %arg40, %0 : i32
  %3 = llvm.icmp "slt" %arg41, %1 : i32
  %4 = llvm.and %3, %2 : i1
  %5 = llvm.zext %4 : i1 to i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def State.get? (e : Expr) : GenM (Option Expr) := do
  let s ← get
  match ← s.mapping.getMatch e with
  | #[x] => return x
  | #[] => return none
  | _ => unreachable!

@[simp_denote]
def sltu_llvm_i64 := [LV| {
    ^entry (%a: i64, %b: i64):
    %0 = llvm.icmp.ult %a, %b : i64
    %1 = llvm.zext %0 : i1 to i64
    llvm.return %1 : i64
  }]

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

def eq_3210_before := [llvm|
{
^0(%arg126 : i32, %arg127 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(16 : i32) : i32
  %2 = llvm.mlir.constant(24 : i32) : i32
  %3 = llvm.trunc %arg126 : i32 to i8
  %4 = llvm.lshr %arg126, %0 : i32
  %5 = llvm.trunc %4 : i32 to i8
  %6 = llvm.lshr %arg126, %1 : i32
  %7 = llvm.trunc %6 : i32 to i8
  %8 = llvm.lshr %arg126, %2 : i32
  %9 = llvm.trunc %8 : i32 to i8
  %10 = llvm.trunc %arg127 : i32 to i8
  %11 = llvm.lshr %arg127, %0 : i32
  %12 = llvm.trunc %11 : i32 to i8
  %13 = llvm.lshr %arg127, %1 : i32
  %14 = llvm.trunc %13 : i32 to i8
  %15 = llvm.lshr %arg127, %2 : i32
  %16 = llvm.trunc %15 : i32 to i8
  %17 = llvm.icmp "eq" %3, %10 : i8
  %18 = llvm.icmp "eq" %5, %12 : i8
  %19 = llvm.icmp "eq" %7, %14 : i8
  %20 = llvm.icmp "eq" %9, %16 : i8
  %21 = llvm.and %17, %18 : i1
  %22 = llvm.and %19, %21 : i1
  %23 = llvm.and %20, %22 : i1
  "llvm.return"(%23) : (i1) -> ()
}
]

def sub_ashr_or_i16_after := [llvm|
{
^0(%arg37 : i16, %arg38 : i16):
  %0 = llvm.mlir.constant(-1 : i16) : i16
  %1 = llvm.icmp "slt" %arg38, %arg37 : i16
  %2 = "llvm.select"(%1, %0, %arg37) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i16, i16) -> i16
  "llvm.return"(%2) : (i16) -> ()
}
]

def PR42691_8_logical_after := [llvm|
{
^0(%arg328 : i32):
  %0 = llvm.mlir.constant(2147483647 : i32) : i32
  %1 = llvm.mlir.constant(-2147483635 : i32) : i32
  %2 = llvm.add %arg328, %0 : i32
  %3 = llvm.icmp "ult" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def xor_icmp_invalid_range_before := [llvm|
{
^0(%arg3 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(4 : i8) : i8
  %2 = llvm.icmp "eq" %arg3, %0 : i8
  %3 = llvm.icmp "ne" %arg3, %1 : i8
  %4 = llvm.xor %2, %3 : i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def elabOp (env : Lean.Environment) (stx : Lean.Syntax) : EIO ParseError (MLIR.AST.Op 0) :=
  unsafe elabIntoEIO (α := MLIR.AST.Op 0) env op0Expr stx

def a_or_b_const_after := [llvm|
{
^0(%arg10 : i32, %arg11 : i32, %arg12 : i32):
  %0 = llvm.icmp "eq" %arg10, %arg12 : i32
  %1 = llvm.icmp "eq" %arg11, %arg12 : i32
  %2 = llvm.xor %0, %1 : i1
  "llvm.return"(%2) : (i1) -> ()
}
]

@[combinator_parenthesizer MLIR.EDSL.balancedBrackets]
def MLIR.EDSL.balancedBracketsParenthesizer : Parenthesizer := pure ()

def Body.return : (body : Body Op Γ ty) → Var body.returnContext ty
  | ⟨⟨_, ret⟩, h⟩ => ⟨ret, by admit /- proof elided -/
  ⟩

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

def src_is_mask_and_before := [llvm|
{
^0(%arg122 : i8, %arg123 : i8, %arg124 : i8):
  %0 = llvm.mlir.constant(123 : i8) : i8
  %1 = llvm.mlir.constant(7 : i8) : i8
  %2 = llvm.mlir.constant(-1 : i8) : i8
  %3 = llvm.xor %arg122, %0 : i8
  %4 = llvm.ashr %1, %arg123 : i8
  %5 = llvm.lshr %2, %arg124 : i8
  %6 = llvm.and %4, %5 : i8
  %7 = llvm.and %3, %6 : i8
  %8 = llvm.icmp "eq" %3, %7 : i8
  "llvm.return"(%8) : (i1) -> ()
}
]

inductive NatPredicate (wcard : Nat) : Type
| eq : WidthExpr wcard → WidthExpr wcard → NatPredicate wcard

def lshr_exact_after := [llvm|
{
^0(%arg183 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.mlir.constant(63 : i8) : i8
  %2 = llvm.add %arg183, %0 : i8
  %3 = llvm.and %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

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

def test_ult_nuw_before := [llvm|
{
^0(%arg2 : i32, %arg3 : i16):
  %0 = llvm.trunc %arg2 overflow<nsw,nuw> : i32 to i8
  %1 = llvm.trunc %arg3 overflow<nsw,nuw> : i16 to i8
  %2 = llvm.icmp "ult" %0, %1 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def llvm_sext_lower_riscv_i16_to_32 : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 16)] :=
  {lhs:= sext_llvm_i16_to_32, rhs:= sext_riscv_i16_to_32}

def lshr_by_const_cmp_sge_value_before := [llvm|
{
^0(%arg7 : i32):
  %0 = llvm.mlir.constant(3 : i32) : i32
  %1 = llvm.lshr %arg7, %0 : i32
  %2 = llvm.icmp "sge" %1, %arg7 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

|
</all_available_defs>

<all_available_lemmas>
Std.HashMap.getElem?_insert in Std.Data.HashMap.Lemmas
getElem?_eq_none_iff in Init.GetElem
Set.mem_setOf_eq in Mathlib.Data.Set.Operations
true_and in Init.SimpLemmas
Array.mem_of_getElem? in Init.Data.Array.Lemmas
Prod.mk.eta in Mathlib.Data.Prod.Basic
Std.HashSet.mem_insert in Std.Data.HashSet.Lemmas
beq_iff_eq in Init.Core
ge_iff_le in Init.Core
not_and in Init.SimpLemmas
not_exists in Init.PropLemmas
or_true in Init.SimpLemmas
true_or in Init.SimpLemmas

@[aesop 50% unsafe]
theorem Std.HashMap.get?_none_not_mem [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} : m.get? k = none → k ∉ m

@[aesop 50% unsafe]
theorem Std.HashMap.mem_of_getElem? [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} :
    m[k]? = some v → k ∈ m

theorem Std.HashMap.mem_iff_getElem? [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] [Inhabited V] {m : Std.HashMap K V} {k : K} :
     k ∈ m ↔ ∃ v, m[k]? = some v

@[grind =, simp]
lemma addTrans_tr_eq (m : RawCNFA A) [LawfulBEq A] (a : A) (s₁ s₂ : State) :
    (m.addTrans a s₁ s₂).tr s₁ a = (m.tr s₁ a).insert s₂

@[grind =] -- TODO: should I?
lemma addTrans_tr (m : RawCNFA A) [LawfulBEq A] {a b : A} {s₁ s₁' s₂ : State} :
    (m.addTrans a s₁ s₂).tr s₁' b = if s₁ = s₁' ∧ a = b then (m.tr s₁ a).insert s₂ else m.tr s₁' b

@[grind ., simp, aesop 50% unsafe]
lemma RawCNFA.WF.trans_src_lt'' [LawfulBEq A] {m : RawCNFA A} (hwf : m.WF) :
    ∀ {s a s'}, s' ∈ m.tr s a → s ∈ m.states

@[grind ., simp, aesop 50% unsafe]
lemma RawCNFA.WF.trans_src_lt' {m : RawCNFA A} (hwf : m.WF) :
    ∀ {s a}, (s, a) ∈ m.trans → s ∈ m.states

@[aesop 50% unsafe]
theorem Std.HashMap.getElem?_none_not_mem [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} :
    m[k]? = none → k ∉ m

theorem e_2231 :
     - 1 * (d ^^^ ( ~~~e ||| f)) - 5 * ((e &&& f) ^^^  ~~~(d &&& (e ^^^ f))) + 5 * (d ||| ( ~~~e &&& f)) - 2 * (e ^^^ (d ||| (e &&& f))) + 2 * (d ||| (e &&& f)) - 3 * (f ^^^  ~~~(d &&&  ~~~e)) + 1 * (d ^^^ (e ^^^ f)) - 7 * (e &&&  ~~~(d ^^^ f)) - 7 * ((d &&& f) ^^^  ~~~(d ^^^ ( ~~~e &&& f))) - 3 * ((d ||| e) &&&  ~~~(e ^^^ f)) - 3 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) - 1 * ((d &&& e) |||  ~~~(e ^^^ f)) + 5 * (e ^^^  ~~~( ~~~d &&& (e ^^^ f))) - 1 *  ~~~( ~~~d &&& ( ~~~e &&& f)) - 11 *  ~~~(d &&& e) - 11 * (e ^^^  ~~~(d &&& (e ||| f))) + 1 * ( ~~~f |||  ~~~(d ^^^ e)) - 1 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) - 6 * ( ~~~d &&& (e ^^^ f)) + 2 * (e &&&  ~~~(d &&& f)) + 3 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) - 2 * (e &&&  ~~~f) + 11 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) + 3 * (e |||  ~~~f) - 6 * (f ^^^ ( ~~~d ||| (e &&& f))) - 1 * (e ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) - 2 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) + 11 * ((d &&& e) |||  ~~~(e |||  ~~~f)) - 5 * ( ~~~d ||| (e ^^^ f)) - 7 * (f ^^^  ~~~(d |||  ~~~e)) + 1 * ((d |||  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 7 * ( ~~~(d |||  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) + 2 *  ~~~( ~~~d &&& (e ^^^ f)) + 7 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) + 11 * (f ^^^ (d |||  ~~~e)) + 1 * (e ^^^  ~~~( ~~~d ||| (e &&& f))) - 2 * (f ^^^ (d ||| ( ~~~e ||| f))) + 7 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) + 3 * (e ||| (d &&& f)) - 2 * (e ^^^  ~~~(d |||  ~~~f)) - 1 * (e ^^^  ~~~(d &&& (e ^^^ f))) - 11 * (e ^^^  ~~~(d ||| (e ^^^ f))) + 3 *  ~~~(e &&& f) + 1 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 1 * (f |||  ~~~(d |||  ~~~e)) - 2 * (f ^^^  ~~~( ~~~d &&& (e &&& f))) + 5 * (e ^^^ (d ||| ( ~~~e &&& f))) + 38 *  ~~~(d ||| (e ||| f)) + 49 *  ~~~(d ||| ( ~~~e ||| f)) - 6 *  ~~~( ~~~d ||| (e ||| f)) - 15 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 6 * ( ~~~d &&& ( ~~~e &&& f)) - 14 * ( ~~~d &&& (e &&& f)) + 4 * (d &&& ( ~~~e &&& f)) + 5 * (d &&& (e &&& f)) =  - 4 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 3 * (f ^^^ (d ||| ( ~~~e &&& f)))

theorem lshrult_03_11_exact_proof : lshrult_03_11_exact_before ⊑ lshrult_03_11_exact_after

theorem test14_commuted_proof : test14_commuted_before ⊑ test14_commuted_after

theorem icmp_eq_zext_eq_non_boolean_proof : icmp_eq_zext_eq_non_boolean_before ⊑ icmp_eq_zext_eq_non_boolean_after

theorem land_band_right1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1), x_1 = 1#1 → x_1 &&& x = x

theorem icmp_sle7_thm (e : IntW 8) :
  icmp IntPred.sle (shl e (const? 8 1) { «nsw» := true, «nuw» := false }) (const? 8 124) ⊑
    icmp IntPred.slt e (const? 8 63)

theorem icmp_eq_zext_eq_non_boolean_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (zeroExtend 32 (ofBool (x == 2#32)) == x) = ofBool (x == 0#32)

theorem ofDep_xvar_eq_xvar' : MultiWidth.Nondep.Term.ofDepTerm xvar = xvar'

theorem test_invert_demorgan_or2_proof : test_invert_demorgan_or2_before ⊑ test_invert_demorgan_or2_after

theorem lshr_not_nneg2_proof : lshr_not_nneg2_before ⊑ lshr_not_nneg2_after

theorem e_2420 :
     - 2 *  ~~~(d ^^^ e) + 3 * (e ^^^  ~~~(d &&&  ~~~f)) - 1 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) - 7 * (e ^^^  ~~~( ~~~d &&& (e ^^^ f))) + 3 * (f |||  ~~~(d ^^^ e)) + 4 * (f ^^^ (d &&& ( ~~~e ||| f))) + 1 * ( ~~~(d ||| e) ||| (e ^^^ f)) + 2 * ( ~~~(d &&& e) &&& (d ^^^ (e ^^^ f))) + 2 * ((d |||  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 6 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) + 3 * (d &&& (e ||| f)) - 7 * ((d &&& e) ||| (d ^^^ (e ^^^ f))) + 3 * (e ^^^ ( ~~~d ||| ( ~~~e ||| f))) - 7 * ((d ||| e) &&&  ~~~(e ^^^ f)) - 1 * ( ~~~d &&& (e ||| f)) - 11 *  ~~~f + 1 * ( ~~~f &&& (d ^^^ e)) + 5 * ((d |||  ~~~e) &&& (e ^^^ f)) - 3 *  ~~~(d &&& ( ~~~e &&& f)) - 7 * ((d &&& f) ^^^ (e ||| f)) - 2 * (e ^^^  ~~~( ~~~d &&& (e &&& f))) - 6 * (e ^^^ (d &&& ( ~~~e ||| f))) + 7 * (d ||| e) - 11 *  ~~~(e &&& f) + 4 * ((d ^^^ e) &&& (d ^^^ f)) + 11 * (f ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) + 2 * ((d &&& e) |||  ~~~(e ^^^ f)) + 2 * ( ~~~(d ^^^ e) |||  ~~~(d ^^^ f)) - 2 * ( ~~~e ||| (d ^^^ f)) - 5 * ( ~~~(d ^^^ e) ||| (d ^^^ f)) + 1 * (f |||  ~~~(d |||  ~~~e)) - 2 *  ~~~(d ||| (e ^^^ f)) + 1 * (f ^^^ (d ||| ( ~~~e &&& f))) + 1 * (d &&&  ~~~e) - 1 * (e ||| (d &&&  ~~~f)) + 1 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) - 1 * (e ||| (d &&& f)) + 2 * (e ||| f) + 1 * (e ^^^ (d ||| f)) - 5 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) - 11 * ( ~~~d ||| (e ^^^ f)) + 1 *  ~~~(d |||  ~~~f) - 1 * (d ^^^ (e ||| f)) - 5 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) + 5 * (f &&& (d ^^^ e)) + 1 * (e &&& (d ||| f)) + 11 * ( ~~~f ||| (d ^^^ e)) + 4 * ( ~~~d ||| ( ~~~e &&& f)) + 3 * (d ^^^ e) - 3 * (f ^^^ (d ||| ( ~~~e ||| f))) - 1 * (e ^^^ (d ||| (e ^^^ f))) - 1 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) + 11 * (e ^^^  ~~~(d |||  ~~~f)) - 6 * (f |||  ~~~(d ||| e)) - 1 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) - 11 * (e &&&  ~~~(d &&&  ~~~f)) - 3 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) - 2 *  ~~~( ~~~d ||| (e ^^^ f)) + 11 * (e ^^^ ( ~~~d &&& ( ~~~e ||| f))) - 1 * ((e &&& f) ^^^  ~~~(d &&& (e ^^^ f))) - 1 * (e ^^^ ( ~~~d ||| (e ^^^ f))) + 1 * ((d &&&  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) - 2 *  ~~~( ~~~d ||| (e &&& f)) + 5 * (e ^^^ (d &&&  ~~~f)) + 1 * (e ^^^  ~~~(d ||| (e ^^^ f))) - 2 *  ~~~d + 30 *  ~~~(d ||| (e ||| f)) + 19 *  ~~~(d ||| ( ~~~e ||| f)) + 17 *  ~~~( ~~~d ||| (e ||| f)) + 3 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 4 * ( ~~~d &&& ( ~~~e &&& f)) + 20 * ( ~~~d &&& (e &&& f)) + 10 * (d &&& ( ~~~e &&& f)) + 5 * (d &&& (e &&& f)) =  - 3 * e

theorem negative_not_less_than_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (-1#32 <ₛ x) = 1#1 → ofBool (x + 256#32 <ᵤ 256#32) = 0#1

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

theorem lshrult_01_02_proof : lshrult_01_02_before ⊑ lshrult_01_02_after

theorem sextbool_add_thm (e : IntW 32) (e_1 : IntW 1) : add (sext 32 e_1) e ⊑ add e (sext 32 e_1)

theorem lshrugt_02_10_proof : lshrugt_02_10_before ⊑ lshrugt_02_10_after

theorem exact_lshr_ne_opposite_msb_proof : exact_lshr_ne_opposite_msb_before ⊑ exact_lshr_ne_opposite_msb_after

theorem or_xor_and_commuted1_thm (e e_1 : IntW 32) :
  LLVM.or (mul e_1 e_1) (LLVM.xor (LLVM.xor (mul e_1 e_1) (const? 32 (-1))) e) ⊑
    LLVM.or (mul e_1 e_1) (LLVM.xor e (const? 32 (-1)))

theorem lsb_mask_sign_zext_thm (e : IntW 32) :
  lshr (LLVM.and (add e (const? 32 (-1))) (LLVM.xor e (const? 32 (-1)))) (const? 32 31) ⊑
    zext 32 (icmp IntPred.eq e (const? 32 0))

theorem test21_thm.extracted_1._1 : ∀ (x x_1 : BitVec 256), ofBool (x_1 - x != x_1) = ofBool (x != 0#256)

theorem nonexact_ashr_ne_noexactlog_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬x ≥ ↑8 → ofBool ((BitVec.ofInt 8 (-90)).sshiftRight' x != BitVec.ofInt 8 (-30)) = 1#1

theorem alive_AndOrXor_1247_AB__AB__AB  (w : Nat)   : alive_AndOrXor_1247_AB__AB__AB_src w  ⊑ alive_AndOrXor_1247_AB__AB__AB_tgt w

theorem positive_biggershl_shlnuwnsw_thm (e : IntW 8) :
  shl (lshr e (const? 8 3)) (const? 8 6) { «nsw» := true, «nuw» := true } ⊑
    LLVM.and (shl e (const? 8 3) { «nsw» := true, «nuw» := true }) (const? 8 64)

theorem zext_add_scalar_proof : zext_add_scalar_before ⊑ zext_add_scalar_after

theorem neg_nsw_slt_n1_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ (0#8).ssubOverflow x = true) → ofBool (0#8 - x <ₛ -1#8) = ofBool (1#8 <ₛ x)

theorem c0_proof : c0_before ⊑ c0_after

theorem test12_proof : test12_before ⊑ test12_after

theorem src_proof : src_before ⊑ src_after

theorem or_logic_or_logic_and_6_thm.extracted_1._9 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 ||

theorem t15_proof : t15_before ⊑ t15_after

theorem select_xor_icmp_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), ofBool (x_1 == 0#32) = 1#1 → x_1 ^^^ x = x

theorem ashrsgt_01_12_thm (e : IntW 4) :
  icmp IntPred.sgt (ashr e (const? 4 1)) (const? 4 (-4)) ⊑ icmp IntPred.sgt e (const? 4 (-7))

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

theorem e_1040 :
     - 2 * (z |||  ~~~t) - 3 * t + 4 *  ~~~(z &&&  ~~~t) + 2 *  ~~~t - 2 *  ~~~(z ||| t) - 1 *  ~~~(z |||  ~~~t) + 3 * (z &&& t) = 2 *  ~~~(z ^^^ t)

theorem lshr_sext_i1_to_i128_thm (e : IntW 1) :
  lshr (sext 128 e) (const? 128 42) ⊑ select e (const? 128 77371252455336267181195263) (const? 128 0)

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

theorem t1_ult_slt_0_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x + 16#32 <ᵤ 144#32) = 1#1 → ofBool (127#32 <ₛ x) = 1#1 ∨ ofBool (x <ₛ BitVec.ofInt 32 (-16)) = 1#1 → False

theorem add_or_sub_comb_i8_negative_y_add_proof : add_or_sub_comb_i8_negative_y_add_before ⊑ add_or_sub_comb_i8_negative_y_add_after

theorem logical_or_logical_or_icmps_comm1_thm.extracted_1._5 : ∀ (x x_1 x_2 : BitVec 8),
  ¬x_1 ≥ ↑8 →
    ¬(ofBool (x_2 &&& 1#8 <<< x_1 == 0#8) = 1#1 ∨ ofBool (x == 42#8) = 1#1) →
      ¬(True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8) →
        ofBool (x_2 &&& 1#8 <<< x_1 == 0#8) = 1#1 → True → ofBool (x_2 &&& 1#8 == 0#8) = 1#1

theorem e_1259 :
    3 *  ~~~(z &&& t) - 3 * (z ^^^ t) + 1 *  ~~~(z &&&  ~~~t) + 1 * (z |||  ~~~t) - 7 * (z ||| t) - 14 *  ~~~(z ||| t) - 3 *  ~~~(z |||  ~~~t) + 4 * (z &&&  ~~~t) + 3 * (z &&& t) =  - 2 *  ~~~(z &&&  ~~~z) - 7 *  ~~~z

theorem tryFactorization_add_nuw_mul_nuw_int_max_proof : tryFactorization_add_nuw_mul_nuw_int_max_before ⊑ tryFactorization_add_nuw_mul_nuw_int_max_after

theorem alive_Select_858 : forall (w : Nat) (a b : Bitvec 1)
, TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec 1)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (a) %v0;
  %v2 := op:const (-1) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:xor w %v3;
  %v5 := op:const (b) %v0;
  %v6 := triple:%v1 %v4 %v5;
  %v7 := op:select w %v6
  dsl_ret %v7
  ]  ⊑
  TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec 1)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (a) %v0;
  %v2 := op:const (-1) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:xor 1 %v3;
  %v5 := op:const (b) %v0;
  %v6 := pair:%v4 %v5;
  %v7 := op:and 1 %v6
  dsl_ret %v7
  ]

theorem eq_smax1_thm (e e_1 : IntW 32) :
  icmp IntPred.eq (select (icmp IntPred.sgt e_1 e) e_1 e) e_1 ⊑ icmp IntPred.sge e_1 e

theorem exact_ashr_eq_both_equal_thm (e : IntW 8) :
  icmp IntPred.eq (ashr (const? 8 (-128)) e { «exact» := true }) (const? 8 (-128)) ⊑
    icmp IntPred.eq e (const? 8 0)

theorem or_xor_commute4_thm (e e_1 : IntW 32) :
  LLVM.xor (LLVM.udiv (const? 32 42) e_1) (LLVM.or (LLVM.udiv (const? 32 42) e) (LLVM.udiv (const? 32 42) e_1)) ⊑
    LLVM.and (LLVM.udiv (const? 32 42) e) (LLVM.xor (LLVM.udiv (const? 32 42) e_1) (const? 32 (-1)))

theorem appendInl_toCons {v : Var Γ t} :
    v.toCons (t':=t').appendInl (Δ := Δ) = v.appendInl.toCons

theorem ashr_xor_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬((42#32 == 0 || 32 != 1 && x_1 == intMin 32 && 42#32 == -1) = true ∨ 5#32 ≥ ↑32 ∨ 7#32 ≥ ↑32) →
    ¬(12#32 ≥ ↑32 ∨ (42#32 == 0 || 32 != 1 && x_1 == intMin 32 && 42#32 == -1) = true ∨ 7#32 ≥ ↑32) →
      (x_1.srem 42#32 ^^^ x.sshiftRight' 5#32).sshiftRight' 7#32 =
        x.sshiftRight' 12#32 ^^^ (x_1.srem 42#32).sshiftRight' 7#32

theorem logic_and_logic_or_7_thm.extracted_1._6 : ∀ (x x_1 x_2 : BitVec 1),
  x_2 = 1#1 → x = 1#1 → x_1 = 1#1 → 1#1 = x_1

theorem ashrslt_01_06_exact_proof : ashrslt_01_06_exact_before ⊑ ashrslt_01_06_exact_after

theorem or_and3_thm.extracted_1._6 : ∀ (x : BitVec 1) (x_1 x_2 : BitVec 32) (x_3 : BitVec 1),
  x_3 ||

theorem src_is_mask_xor_fail_notmask_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool ((x_1 ^^^ 123#8) &&& (x ^^^ x + -1#8 ^^^ -1#8) != x_1 ^^^ 123#8) =
    ofBool (x ^^^ 0#8 - x ||| x_1 ^^^ BitVec.ofInt 8 (-124) != -1#8)

theorem test4_proof : test4_before ⊑ test4_after

theorem test6_proof : test6_before ⊑ test6_after

theorem main3_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 7#32 == 0#32) = 1#1 →
    ofBool (x &&& 48#32 == 0#32) = 1#1 → 0#32 = zeroExtend 32 (ofBool (x &&& 55#32 != 0#32))

theorem test5_thm (e : IntW 8) (e_1 : IntW 32) :
  urem e_1 (shl (const? 32 32) (zext 32 e)) ⊑
    LLVM.and e_1
      (add (shl (const? 32 32) (zext 32 e { «nneg» := true }) { «nsw» := false, «nuw» := true })
        (const? 32 (-1)))

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

theorem substitute_constant_and_eq_eq_proof : substitute_constant_and_eq_eq_before ⊑ substitute_constant_and_eq_eq_after

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

theorem masked_icmps_mask_notallzeros_bmask_mixed_swapped_5_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 15#32 == 8#32) = 1#1 → ofBool (x &&& 15#32 != 0#32) = ofBool (x &&& 15#32 == 8#32)

theorem bor_land_right1_proof : bor_land_right1_before ⊑ bor_land_right1_after

theorem and_sgt_to_mask_thm (e : IntW 8) :
  LLVM.and (icmp IntPred.sgt e (const? 8 123)) (icmp IntPred.eq (LLVM.and e (const? 8 2)) (const? 8 0)) ⊑
    icmp IntPred.eq (LLVM.and e (const? 8 (-2))) (const? 8 124)

theorem select2_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1),
  x_2 = 1#1 → truncate 8 (zeroExtend 32 x_1) = x_1
</all_available_lemmas>

<local_ctx>
import Blase.AutoStructs.Basic

open SetRel

section nfa

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

variable {S : Type} [Fintype S] [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S]

variable (inits : Array S) (final : S → Bool) (f : S → Array (A × S))

def nfa : NFA A S where
  start := { sa | sa ∈ inits }
  accept := { sa | final sa }
  step sa a := { sa' | (a, sa') ∈ f sa }

end nfa

section nfa'

variable {S : Type} [Fintype S] [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S]

variable (inits : Array S) (final : S → Bool) (f : S → Array (BitVec n × S))

end nfa'

section worklist

variable (A : Type) [BEq A] [LawfulBEq A] [Hashable A] [DecidableEq A] [FinEnum A]

variable (S : Type) [Fintype S] [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S]

structure worklist.St where
  m : RawCNFA A
  map : Std.HashMap S State := ∅
  worklist : Array S := ∅
  worklist_nodup : worklist.toList.Nodup
  worklist_incl : ∀ sa ∈ worklist, sa ∈ map

open List in

def worklist.St.addOrCreateState (st : worklist.St A S) (final? : Bool) (sa : S) : State × worklist.St A S :=
  match heq : st.map[sa]? with
  | some s => (s, st)
  | none =>
    let (s, m) := st.m.newState
    let m := if final? then m.addFinal s else m
    let map := st.map.insert sa s
    let worklist := st.worklist.push sa
    have worklist_nodup : worklist.toList.Nodup := by admit /- proof elided -/

def processOneElem (final : S → Bool) (s : State) (st : worklist.St A S) : A × S → worklist.St A S :=
  fun (a', sa') =>
    let (s', st') := st.addOrCreateState _ _ (final sa') sa'
    let m := st'.m.addTrans a' s s'
    { st' with m }

      open List in
      have hgrow : ∃ sas, st2.map.keys ~ (sas ++ st1.map.keys) ∧ st2.worklist.toList = st1.worklist.toList ++ sas := by
        rcases a with ⟨al⟩
        unfold st2
        generalize hst1 : st1 = x; clear hst1; revert x
        induction al with
        | nil => simp
        | cons asa al ih =>
          simp; simp at ih; intros st
          let wl' := processOneElem A S final s st asa
          rcases ih wl' with ⟨sas', h1', h2'⟩; clear ih
          rcases processOneElem_grow _ _ st final asa.1 asa.2 s with ⟨sas, h1, h2⟩
          use (sas ++ sas')
          constructor
          { simp [wl'] at h1'; apply list_perm_trick; exact h1'; exact h1 }
          { simp [wl', h2] at h2'; aesop }
      have hincl : ∀ k, k ∈ st1.map → k ∈ st2.map := by
        intros k; rcases hgrow with ⟨sas, hkeys, -⟩;
        have := @(List.perm_subset_iff_right hkeys st1.map.keys).mpr (by aesop) k; aesop
      have : st1.meas < st0.meas := by
        rcases heq' : sa? with ⟨⟩ | ⟨sa⟩
        { simp_all }
        apply Finset.card_lt_card
        simp [Finset.ssubset_iff, Finset.subset_iff]
        use sa
        simp [sa?] at heq'
        constructor
        { constructor
          { apply Array.mem_of_back? at heq'; apply st0.worklist_incl; assumption }
          { apply Array.not_elem_back_pop at heq' <;> simp_all +zetaDelta [Array.pop] } }
        constructor
        { right; apply Array.mem_of_back? at heq'; assumption }
        rintro sa hh; rcases hh with hnin | hin
        { simp +zetaDelta [hnin] }
        right
        exact Array.mem_of_mem_pop st0.worklist sa hin
      have : st2.meas ≤ st1.meas := by
        apply Finset.card_le_card
        simp +zetaDelta [Finset.subset_iff]
        intros sa' h
        rcases h with hnin | hin
        { left; simp [st1] at hincl; intros hc; apply hnin; apply hincl; assumption }
        by_cases hnew : sa' ∈ st0.map
        all_goals try (left; trivial)
        right
        simp [st1] at hgrow
        rcases hgrow with ⟨sas, hkeys2, hwl2⟩
        have hnin : sa'∉ sas := by
          intros hc
          have hdisj : st0.map.keys.Disjoint sas := by
            have : (sas ++ st0.map.keys).Nodup := by
              apply List.Perm.nodup
              assumption
              apply st2.map.keys_nodup
            simp [List.nodup_append_comm, List.disjoint_of_nodup_append, this]
          apply hdisj
          { simp_all [Std.HashMap.mem_keys]; apply hnew }
          { apply hc }
        rcases hin with ⟨hin⟩; simp_all +zetaDelta
      have : st2.meas < st0.meas := by omega
      go st2
    else
      st0.m -- never happens
  | none => st0.m -- never happens
  termination_by st0.meas

def worklist.St.visited (st : worklist.St A S) : Set S := { s : S | s ∈ st.map ∧ s ∉ st.worklist }

structure StInv (m : RawCNFA A) (map : Std.HashMap S State) where
  wf : m.WF
  map_states : ∀ (sa : S) s, map[sa]? = some s → s ∈ m.states
  map_surj : ∀ s : m.states, ∃ (sa : S), map[sa]? = some s.val
  map_inj : ∀ {s} {sa sa' : S}, map[sa]? = some s → map[sa']? = some s → sa = sa'

end worklist

section worklist_correct

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

variable {S : Type} [Fintype S] [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S]

variable (inits : Array S) (final : S → Bool) (f : S → Array (A × S))

def worklist.St.rel (st : worklist.St A S) : SetRel State S := {(s, sa) | st.map[sa]? = some s }

def worklist.St.D (st : worklist.St A S) : Set S := st.visited

abbrev worklist.St.sim {st : worklist.St A S} (T : Set (S × A × S)) :=
  st.m.Simul (nfa inits final f) st.rel st.D T

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

def processOneElem_inv {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) :
    ∀ a sa', (f sa)[k]? = some (a, sa') →
    processOneElem_mot inits final f s sa k st →
    let st' := processOneElem A S final s st (a, sa')
    StInv A S st'.m st'.map :=
</local_ctx>

<target_theorem>
omit [Fintype S] in
lemma processOneElem_spec {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) :
    ∀ a sa', (f sa)[k]? = some (a, sa') →
    processOneElem_mot inits final f s sa k st →
    processOneElem_mot inits final f s sa (k+1) (processOneElem A S final s st (a, sa')) :=
</target_theorem>

