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>
Bool in Init.Prelude

inductive Term : Type
| var : Nat → Term
 
| zero : Term
 
| negOne : Term
 
| one : Term
 
| ofNat (n : Nat) : Term
 
| and : Term → Term → Term
 
| or : Term → Term → Term
 
| xor : Term → Term → Term
 
| not : Term → Term
 
| add : Term → Term → Term
 
| sub : Term → Term → Term
 
| neg : Term → Term

| shiftL : Term → Nat → Term

deriving Repr, Inhabited, Lean.ToExpr

def ugt_or_not_min_logical_before := [llvm|
{
^0(%arg12 : i8, %arg13 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.icmp "ugt" %arg12, %arg13 : i8
  %3 = llvm.icmp "ne" %arg12, %0 : i8
  %4 = "llvm.select"(%2, %1, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def and_or_not_not_commute6_before := [llvm|
{
^0(%arg357 : i32, %arg358 : i32, %arg359 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sdiv %0, %arg358 : i32
  %3 = llvm.and %2, %arg357 : i32
  %4 = llvm.xor %3, %1 : i32
  %5 = llvm.and %arg359, %arg357 : i32
  %6 = llvm.xor %5, %1 : i32
  %7 = llvm.or %2, %6 : i32
  %8 = llvm.and %7, %4 : i32
  "llvm.return"(%8) : (i32) -> ()
}
]

def State.cseCom {α}
  {lets : Lets d Γstart .pure Γ}
  (s : State d lets)
  (com: Com d Γ .pure α) :
  { com' : Com d Γ .pure α
    // ∀ (V : Ctxt.Valuation Γstart), com.denote (lets.denote V) = com'.denote (lets.denote V) } :=
  match com with
  | .rets vs =>
      let ⟨vs', hvs'⟩ := s.vars2vars vs
      ⟨.rets vs', by admit /- proof elided -/
        ⟩
  | .var e body =>
      let ⟨⟨e', he'⟩, v'?⟩ := s.cseExpr e
      match v'? with
      | .none =>  
        let s' := s.consNewExpr2Cache (e := e')
         
        let ⟨body', hbody'⟩ := s'.cseCom body
        ⟨.var e' body',  by admit /- proof elided -/
            ⟩
      | .some ⟨v', hv'⟩ =>
        let s' := s.consOldExpr2Cache (enew := e') (eold := e) (henew := by admit /- proof elided -/
        )
          (vold := v') (hv := by admit /- proof elided -/
          )
          
        let ⟨body', hbody'⟩ := s'.cseCom body
        
        ⟨.var e body' 
        , by admit /- proof elided -/
        ⟩

for (const, val) in positiveExamples[0]!.toArray do
        let bvExprVar := GenBVExpr.var const
        let powerOf2Expr :=  GenBVExpr.bin bvExprVar BVBinOp.and (GenBVExpr.bin bvExprVar BVBinOp.add (minusOne val.w))
        let powerOfTwoResults := positiveExamples.map (λ pos => evalBVExpr pos powerOf2Expr)

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

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

@[simp_llvm_option]
def udiv {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW w := do
  let x' ← x
  let y' ← y
  if flag.exact ∧ x'.umod y' ≠ 0 then
    .poison
  else
    udiv? x' y'

def icmp_sge_riscv_eq_icmp_sge_llvm_32 : LLVMPeepholeRewriteRefine 1 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] :=
  {lhs:= icmp_sge_llvm_32, rhs:= icmp_sge_riscv_32}

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

def isCloseBracket(c: Char):Option Bracket :=
match c with
| ')' => some .Round
| ']' => some .Square
| '{' => some .Curly
| '<' => some .Angle
| _ => none

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

def alive_AddSub_1043_tgt  (w : Nat)  :=
[llvm( w )| {
^bb0(%C1 : _, %Z : _, %RHS : _):
  %v1 = llvm.not %C1
  %v2 = llvm.or %Z, %v1
  %v3 = llvm.and %Z, %C1
  %v4 = llvm.xor %v3, %C1
  %v5 = llvm.mlir.constant 1
  %v6 = llvm.add %v4, %v5
  %v7 = llvm.sub %RHS, %v2
  llvm.return %v7
}]

def lor_lor_left2_after := [llvm|
{
^0(%arg68 : i1, %arg69 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = "llvm.select"(%arg69, %0, %arg68) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%1) : (i1) -> ()
}
]

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

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 p0_before := [llvm|
{
^0(%arg16 : i8, %arg17 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.shl %0, %arg17 : i8
  %2 = llvm.icmp "ugt" %1, %arg16 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def andn_or_cmp_1_logical_after := [llvm|
{
^0(%arg173 : i37, %arg174 : i37, %arg175 : i37):
  %0 = llvm.mlir.constant(42 : i37) : i37
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "sle" %arg173, %arg174 : i37
  %3 = llvm.icmp "ugt" %arg175, %0 : i37
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def ripple_nsw1_before := [llvm|
{
^0(%arg23 : i16, %arg24 : i16):
  %0 = llvm.mlir.constant(1 : i16) : i16
  %1 = llvm.mlir.constant(-16385 : i16) : i16
  %2 = llvm.and %arg24, %0 : i16
  %3 = llvm.and %arg23, %1 : i16
  %4 = llvm.add %2, %3 : i16
  "llvm.return"(%4) : (i16) -> ()
}
]

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

HAnd in Init.Prelude

def List.Vector.transport (v : Vector α m) (f : Fin n → Fin m) : Vector α n :=
  Vector.ofFn fun i => v.get (f i)

def src_srem_shl_demand_min_signbit_before := [llvm|
{
^0(%arg23 : i32):
  %0 = llvm.mlir.constant(1073741823 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.mlir.constant(-2147483648 : i32) : i32
  %3 = llvm.srem %arg23, %0 : i32
  %4 = llvm.shl %3, %1 : i32
  %5 = llvm.and %4, %2 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def urem? {w : Nat} (x y : BitVec w) : IntW w :=
  if y = 0 then
    .poison
  else
    .value <| x % y

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

def mul_of_bools_before := [llvm|
{
^0(%arg91 : i32, %arg92 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.and %arg91, %0 : i32
  %3 = llvm.and %arg92, %0 : i32
  %4 = llvm.mul %2, %3 : i32
  %5 = llvm.icmp "ult" %4, %1 : i32
  "llvm.return"(%5) : (i1) -> ()
}
]

def mulo_by_2_unsigned : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (2) : i64
      %0 = llvm.mul %x, %c overflow<nuw> : i64
      llvm.return %0 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %0 = llvm.add %x, %x overflow<nuw> : i64
      llvm.return %0 : i64
  }]

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

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

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

def test4b_after := [llvm|
{
^0(%arg8 : i64):
  %0 = llvm.mlir.constant(1) : i64
  %1 = llvm.icmp "slt" %arg8, %0 : i64
  "llvm.return"(%1) : (i1) -> ()
}
]

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

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

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

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

def or_ugt_after := [llvm|
{
^0(%arg58 : i8, %arg59 : i8):
  %0 = llvm.or %arg58, %arg59 : i8
  %1 = llvm.icmp "ne" %0, %arg58 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

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

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

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

def icmp_ne_and_pow2_lshr_pow2_before := [llvm|
{
^0(%arg41 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(4 : i32) : i32
  %2 = llvm.mlir.constant(0 : i32) : i32
  %3 = llvm.lshr %0, %arg41 : 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 pr4917_3_before := [llvm|
{
^0(%arg25 : i32, %arg26 : i32):
  %0 = llvm.mlir.constant(4294967295) : i64
  %1 = llvm.mlir.constant(111) : i64
  %2 = llvm.zext %arg25 : i32 to i64
  %3 = llvm.zext %arg26 : i32 to i64
  %4 = llvm.mul %2, %3 : i64
  %5 = llvm.icmp "ugt" %4, %0 : i64
  %6 = "llvm.select"(%5, %4, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  "llvm.return"(%6) : (i64) -> ()
}
]

def shl_or_disjoint_lshr_after := [llvm|
{
^0(%arg109 : i32, %arg110 : i32, %arg111 : i32):
  %0 = llvm.lshr %arg111, %arg110 : i32
  %1 = llvm.or disjoint %0, %arg109 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

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

def neg (x : BitStream) : BitStream :=
  fun n => (negAux x n).1

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

def ExtEq (Γ Δ : Context Ty) : Prop :=
  ∀ v, Γ.lookup v = Δ.lookup v

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 subMax (a : BitVec v) (b : BitVec w) : BitVec (max v w + 1) :=
   a.signExtend _ - b.signExtend _

def ConcreteCliTest.printSignature (test : ConcreteCliTest) : String :=
  s!"{test.context.toList.reverse} → {test.ty}"

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

def sext_zext_nneg_uge_op0_wide_after := [llvm|
{
^0(%arg26 : i16, %arg27 : i8):
  %0 = llvm.sext %arg27 : i8 to i16
  %1 = llvm.icmp "uge" %arg26, %0 : i16
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def and_slt_to_mask_before := [llvm|
{
^0(%arg5 : i8):
  %0 = llvm.mlir.constant(-124 : i8) : i8
  %1 = llvm.mlir.constant(2 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = llvm.icmp "slt" %arg5, %0 : i8
  %4 = llvm.and %arg5, %1 : i8
  %5 = llvm.icmp "eq" %4, %2 : i8
  %6 = llvm.and %3, %5 : i1
  "llvm.return"(%6) : (i1) -> ()
}
]

let mut bitwidth := negativeExamples[0]!.values[0]!.w

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

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

def test35_with_trunc_before := [llvm|
{
^0(%arg48 : i64):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(60 : i32) : i32
  %2 = llvm.mlir.constant(100 : i32) : i32
  %3 = llvm.trunc %arg48 : i64 to i32
  %4 = llvm.icmp "sge" %3, %0 : i32
  %5 = "llvm.select"(%4, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

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

def trunc_shl_zext_64_before := [llvm|
{
^0(%arg0 : i64):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.trunc %arg0 : i64 to i8
  %2 = llvm.shl %1, %0 : i8
  %3 = llvm.zext %2 : i8 to i64
  "llvm.return"(%3) : (i64) -> ()
}
]

@[simp_denote]
def zext_llvm_1_to_8 := [LV| {
  ^entry (%arg: i1):
    %0 = llvm.zext %arg: i1 to i8
    llvm.return %0: i8
  }]

def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .nat) : Expr Γ .nat :=
  Expr.mk
    (op := .add)
    (ty_eq := rfl)
    (eff_le := EffectKind.pure_le _)
    (args := .cons e₁ <| .cons e₂ .nil)
    (regArgs := .nil)

@[simp_denote]
def add_hi_and_lo_negone_llvm_i64 := [LV| {
    ^entry (%arg: i64):
    %1 = llvm.mlir.constant (-1) : i64
    %0 = llvm.add %arg, %1 overflow<nsw> : i64
    llvm.return %0 : i64
  }]

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

checkTimeout

def test_sub_nuw__nsw_is_safe_before := [llvm|
{
^0(%arg22 : i32):
  %0 = llvm.mlir.constant(-2147483648 : i32) : i32
  %1 = llvm.mlir.constant(-2147483647 : i32) : i32
  %2 = llvm.mlir.constant(-1 : i32) : i32
  %3 = llvm.or %arg22, %0 : i32
  %4 = llvm.icmp "eq" %3, %1 : i32
  %5 = llvm.sub %0, %3 overflow<nuw> : i32
  %6 = "llvm.select"(%4, %2, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def different_size_zext_zext_sgt_after := [llvm|
{
^0(%arg16 : i7, %arg17 : i4):
  %0 = llvm.zext %arg17 : i4 to i7
  %1 = llvm.icmp "ugt" %arg16, %0 : i7
  "llvm.return"(%1) : (i1) -> ()
}
]

def trunc_equality_both_before := [llvm|
{
^0(%arg40 : i16, %arg41 : i16):
  %0 = llvm.trunc %arg40 overflow<nsw,nuw> : i16 to i8
  %1 = llvm.trunc %arg41 overflow<nsw,nuw> : i16 to i8
  %2 = llvm.icmp "eq" %0, %1 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

match_expr hExpr with
    | Eq w lhsExpr rhsExpr =>

def main4_before := [llvm|
{
^0(%arg135 : i32):
  %0 = llvm.mlir.constant(7 : i32) : i32
  %1 = llvm.mlir.constant(48 : i32) : i32
  %2 = llvm.mlir.constant(0 : i32) : i32
  %3 = llvm.mlir.constant(1 : i32) : i32
  %4 = llvm.and %arg135, %0 : i32
  %5 = llvm.icmp "eq" %4, %0 : i32
  %6 = llvm.and %arg135, %1 : i32
  %7 = llvm.icmp "eq" %6, %1 : i32
  %8 = llvm.and %5, %7 : i1
  %9 = "llvm.select"(%8, %2, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%9) : (i32) -> ()
}
]

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

pure validCandidates
</all_available_defs>

<all_available_lemmas>
...

theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]

theorem test9_logical_thm (e : IntW 32) :
  select (icmp IntPred.ne (LLVM.and e (const? 32 1073741824)) (const? 32 0))
      (icmp IntPred.sgt e (const? 32 (-1))) (const? 1 0) ⊑
    icmp IntPred.eq (LLVM.and e (const? 32 (-1073741824))) (const? 32 1073741824)

theorem mul_splat_fold_no_nuw_proof : mul_splat_fold_no_nuw_before ⊑ mul_splat_fold_no_nuw_after

theorem testtrunclowhigh_thm (e e_1 : IntW 16) (e_2 : IntW 32) :
  select (icmp IntPred.ult (add e_2 (const? 32 128)) (const? 32 256)) (trunc 16 e_2)
      (select (icmp IntPred.sgt e_2 (const? 32 (-1))) e_1 e) ⊑
    select (icmp IntPred.ult (add e_2 (const? 32 128)) (const? 32 256)) (trunc 16 e_2)
      (select (icmp IntPred.slt e_2 (const? 32 0)) e e_1)

theorem test4_thm.extracted_1._4 : ∀ (x : BitVec 1023),
  ¬ofBool (x <ₛ 0#1023) = 1#1 → ¬1022#1023 ≥ ↑1023 → 0#1023 = x.sshiftRight' 1022#1023

@[simp] theorem carry'_zero
    (initCarry : Bool) (x y : BitStream) :
  (carry' initCarry x y 0) = initCarry

theorem src_is_notmask_neg_p2_fail_not_invertable_proof : src_is_notmask_neg_p2_fail_not_invertable_before ⊑ src_is_notmask_neg_p2_fail_not_invertable_after

theorem badimm3_thm.extracted_1._2 : ∀ (x : BitVec 16),
  ¬(7#8 ≥ ↑8 ∨ 8#16 ≥ ↑16) →
    ofBool ((truncate 8 x).sshiftRight' 7#8 == truncate 8 (x >>> 8#16)) = 1#1 →
      ¬ofBool (x + 128#16 <ᵤ 256#16) = 1#1 →
        ¬(14#16 ≥ ↑16 ∨ True ∧ signExtend 16 (truncate 8 (x.sshiftRight' 14#16)) ≠ x.sshiftRight' 14#16) →
          truncate 8 x = truncate 8 (x.sshiftRight' 14#16) ^^^ 127#8

theorem select_ashr_icmp_bad_thm.extracted_1._3 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 == 1#32) = 1#1 → ¬x_2 ≥ ↑32 → 1#32 ≥ ↑32 → False

theorem xor_icmp_to_icmp_add_proof : xor_icmp_to_icmp_add_before ⊑ xor_icmp_to_icmp_add_after

theorem bv_AndOrXor_135 :
    ∀ (e e_1 e_2 : LLVM.IntW w), LLVM.and (LLVM.xor e e_1) e_2 ⊑ LLVM.xor (LLVM.and e e_2) (LLVM.and e_1 e_2)

theorem e_1517 :
     - 11 * ((b &&&  ~~~c) |||  ~~~(a ||| ( ~~~b &&& c))) - 5 * (c ^^^ (a ||| (b &&& c))) + 18 *  ~~~(a ||| (b ||| c)) + 11 *  ~~~(a ||| ( ~~~b ||| c)) + 12 *  ~~~( ~~~a ||| (b ||| c)) + 16 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 12 * ( ~~~a &&& ( ~~~b &&& c)) + 11 * ( ~~~a &&& (b &&& c)) + 7 * (a &&& ( ~~~b &&& c)) + 7 * (a &&& (b &&& c)) = 7 * (b ^^^  ~~~(a &&& (b &&& c)))

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

theorem sub_mask1_trunc_lshr_thm (e : IntW 64) :
  sub (const? 8 10) (LLVM.and (trunc 8 (lshr e (const? 64 15))) (const? 8 1)) ⊑
    add (trunc 8 (ashr (shl e (const? 64 48)) (const? 64 63)) { «nsw» := true, «nuw» := false }) (const? 8 10)
      { «nsw» := true, «nuw» := false }

theorem and_nosignbit_select_shl_proof : and_nosignbit_select_shl_before ⊑ and_nosignbit_select_shl_after

theorem xor_notand_to_or_not3_proof : xor_notand_to_or_not3_before ⊑ xor_notand_to_or_not3_after

theorem test_invert_demorgan_or3_thm (e e_1 : IntW 32) :
  LLVM.xor
      (LLVM.or
        (LLVM.or
          (LLVM.or (icmp IntPred.eq e_1 (const? 32 178206))
            (icmp IntPred.ult (add e (const? 32 (-195102))) (const? 32 1506)))
          (icmp IntPred.ult (add e (const? 32 (-201547))) (const? 32 716213)))
        (icmp IntPred.ult (add e (const? 32 (-918000))) (const? 32 196112)))
      (const? 1 1) ⊑
    LLVM.and
      (LLVM.and
        (LLVM.and (icmp IntPred.ne e_1 (const? 32 178206))
          (icmp IntPred.ult (add e (const? 32 (-196608))) (const? 32 (-1506))))
        (icmp IntPred.ult (add e (const? 32 (-917760))) (const? 32 (-716213))))
      (icmp IntPred.ult (add e (const? 32 (-1114112))) (const? 32 (-196112)))

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

theorem mul_of_pow2_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 32),
  ofBool (510#32 <ᵤ (x_1 &&& 2#32) * zeroExtend 32 x) = 0#1

theorem bv_AddSub_1043 :
    ∀ (e e_1 e_2 : LLVM.IntW w),
      LLVM.add (LLVM.add (LLVM.xor (LLVM.and e_1 e) e) (LLVM.const? w 1)) e_2 ⊑ LLVM.sub e_2 (LLVM.or e_1 (LLVM.not e))

@[simp, simp_denote, simp_sllvm]
lemma run_pure : StateT.run (pure x : EffectM α) s = .value (x, s)

@[grind =, simp]
lemma createSink_finals [LawfulBEq A] {m : RawCNFA A} : m.createSink.2.finals = m.finals

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

theorem test_sdiv_canonicalize_op0_exact_thm (e e_1 : IntW 32) :
  LLVM.sdiv (sub (const? 32 0) e_1 { «nsw» := true, «nuw» := false }) e { «exact» := true } ⊑
    sub (const? 32 0) (LLVM.sdiv e_1 e { «exact» := true }) { «nsw» := true, «nuw» := false }

theorem icmp_eq_sext_ne_zero_proof : icmp_eq_sext_ne_zero_before ⊑ icmp_eq_sext_ne_zero_after

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

theorem test11_thm (e : IntW 737) :
  icmp IntPred.ne (LLVM.and e (const? 737 (-2147483648))) (const? 737 0) ⊑
    icmp IntPred.ugt e (const? 737 2147483647)

theorem lshrult_02_14_exact_proof : lshrult_02_14_exact_before ⊑ lshrult_02_14_exact_after

theorem udiv_shl_pair3_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 32),
  ¬(True ∧ x_2 <<< x_1 >>> x_1 ≠ x_2 ∨
        x_1 ≥ ↑32 ∨ True ∧ (x_2 <<< x).sshiftRight' x ≠ x_2 ∨ True ∧ x_2 <<< x >>> x ≠ x_2 ∨ x ≥ ↑32 ∨ x_2 <<< x = 0) →
    ¬(True ∧ 1#32 <<< x_1 >>> x_1 ≠ 1#32 ∨ x_1 ≥ ↑32 ∨ x ≥ ↑32) → x_2 <<< x_1 / x_2 <<< x = 1#32 <<< x_1 >>> x

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

theorem alive_Select_700 : 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 (B) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:icmp slt  w %v3;
  %v5 := triple:%v4 %v1 %v2;
  %v6 := op:select 1 %v5;
  %v7 := pair:%v6 %v2;
  %v8 := op:icmp slt  w %v7;
  %v9 := triple:%v8 %v6 %v2;
  %v10 := op:select 1 %v9
  dsl_ret %v10
  ]  ⊑
  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 (B) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:icmp slt  1 %v3;
  %v5 := triple:%v4 %v1 %v2;
  %v6 := op:select 1 %v5;
  %v7 := pair:%v6 %v2;
  %v8 := op:icmp slt  1 %v7;
  %v9 := triple:%v4 %v1 %v2;
  %v10 := op:select 1 %v9
  dsl_ret %v10
  ]

theorem test35_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(True ∧ (0#32 - x &&& 240#32).msb = true) →
    0#64 - zeroExtend 64 x &&& 240#64 = zeroExtend 64 (0#32 - x &&& 240#32)

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'))

theorem test6_proof : test6_before ⊑ test6_after

theorem ashrsgt_03_03_thm (e : IntW 4) : icmp IntPred.sgt (ashr e (const? 4 3)) (const? 4 3) ⊑ const? 1 0

theorem trunc_shl_15_i16_i32_proof : trunc_shl_15_i16_i32_before ⊑ trunc_shl_15_i16_i32_after

theorem icmp_sle2_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ (x <<< 1#8).sshiftRight' 1#8 ≠ x ∨ 1#8 ≥ ↑8) →
    ofBool (x <<< 1#8 ≤ₛ BitVec.ofInt 8 (-127)) = ofBool (x <ₛ BitVec.ofInt 8 (-63))

lemma neg_eq {M : NFA' n} : M.neg = M.determinize.flipAccept

theorem lsb_mask_sign_zext_commuted_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 → ((x ^^^ -1#32) &&& x + -1#32) >>> 31#32 = zeroExtend 32 (ofBool (x == 0#32))

theorem select_constants_and_icmp_eq0_zero_tval_proof : select_constants_and_icmp_eq0_zero_tval_before ⊑ select_constants_and_icmp_eq0_zero_tval_after

theorem cmpeq_xor_cst1_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 ^^^ 10#32 == x) = ofBool (x_1 ^^^ x == 10#32)

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

theorem select_constants_and_icmp_eq0_zero_fval_proof : select_constants_and_icmp_eq0_zero_fval_before ⊑ select_constants_and_icmp_eq0_zero_fval_after

theorem main5_like_thm (e e_1 : IntW 32) :
  select
      (LLVM.and (icmp IntPred.eq (LLVM.and e_1 (const? 32 7)) (const? 32 7))
        (icmp IntPred.eq (LLVM.and e (const? 32 7)) (const? 32 7)))
      (const? 32 0) (const? 32 1) ⊑
    zext 32 (icmp IntPred.ne (LLVM.and (LLVM.and e_1 e) (const? 32 7)) (const? 32 7))

theorem nonexact_ashr_eq_noexactdiv_proof : nonexact_ashr_eq_noexactdiv_before ⊑ nonexact_ashr_eq_noexactdiv_after

theorem not_thm.extracted_1._1 : ∀ (x : BitVec 8), ¬42#8 = 0 → (-1#8 ^^^ x) * (x / 42#8) = x / 42#8 * (x ^^^ -1#8)

theorem test18_proof : test18_before ⊑ test18_after

theorem e_168 :
     - 1 *  ~~~x + 2 *  ~~~y - 2 * (x ^^^ y) - 12 *  ~~~(x ||| y) - 11 * (x &&&  ~~~y) - 11 * (x &&& y) =  - 11 * (x |||  ~~~y) - 3 *  ~~~(x |||  ~~~y)

theorem shl_lshr_demand1_thm.extracted_1._1 : ∀ (x : BitVec 8), ¬(x ≥ ↑8 ∨ 3#8 ≥ ↑8) → x ≥ ↑8 → False

theorem test33b_proof : test33b_before ⊑ test33b_after

theorem test_add_nsw__none_are_safe_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x == 3#32) = 1#1 → 4#32 = x + 1#32

theorem PR42691_3_thm (e : IntW 32) :
  LLVM.or (icmp IntPred.sge e (const? 32 0)) (icmp IntPred.eq e (const? 32 (-2147483648))) ⊑
    icmp IntPred.ult e (const? 32 (-2147483647))

theorem test2_proof : test2_before ⊑ test2_after

@[simp] theorem size_rets  : (rets v : Com d Γ eff t).size = 0

theorem or_not_xor_common_op_commute2_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 8),
  x_2 ^^^ x_1 ||

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

theorem xor_or_thm.extracted_1._1 : ∀ (x : BitVec 8), x ^^^ 32#8 ||

theorem udiv_shl_mul_nuw_swap_thm (e e_1 e_2 : IntW 5) :
  LLVM.udiv (shl e_2 e_1 { «nsw» := false, «nuw» := true }) (mul e e_2 { «nsw» := false, «nuw» := true }) ⊑
    LLVM.udiv (shl (const? 5 1) e_1 { «nsw» := false, «nuw» := true }) e

theorem ashrsgt_01_09_proof : ashrsgt_01_09_before ⊑ ashrsgt_01_09_after

theorem e_2449 :
     - 1 * (e ^^^  ~~~(d &&& (e ||| f))) - 5 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) - 5 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) + 1 * ( ~~~d ||| (e ||| f)) + 1 * ( ~~~e |||  ~~~(d ^^^ f)) + 5 * (e &&&  ~~~(d &&&  ~~~f)) + 1 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 2 * (e &&& (d ^^^ f)) + 1 * ( ~~~d ||| (e &&& f)) - 1 * (d ||| e) - 11 * (d &&& f) - 1 * (e ^^^  ~~~(d &&& ( ~~~e ||| f))) + 1 * ((e &&&  ~~~f) ^^^ ( ~~~d ||| (e ^^^ f))) + 3 * (f ^^^ ( ~~~d &&& ( ~~~e ||| f))) - 2 *  ~~~f + 11 *  ~~~(d &&& f) + 5 * ((d &&& f) ||| (e &&&  ~~~f)) + 4 * (e ^^^  ~~~(d |||  ~~~f)) + 5 * ((d &&& e) |||  ~~~(d ^^^ (e ^^^ f))) - 1 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) - 7 * (d ^^^ (e &&& f)) + 11 * (e ^^^  ~~~(d &&& f)) - 7 * (e ^^^ (d ||| (e ||| f))) + 2 * (d &&&  ~~~f) + 4 *  ~~~( ~~~d ||| (e ^^^ f)) + 11 * (d ^^^ f) - 1 * (e &&& (d |||  ~~~f)) + 3 *  ~~~( ~~~d &&& (e ^^^ f)) - 11 * (e ^^^  ~~~(d ||| f)) - 1 * (d ||| (e ||| f)) - 1 * (e ^^^  ~~~(d &&& (e &&& f))) - 1 * (f ^^^  ~~~( ~~~d &&& (e &&& f))) - 1 * e + 1 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) + 2 * (d ^^^ (e ||| f)) + 2 * (e ||| (d &&& f)) + 1 * ((d &&& e) ||| (d ^^^ (e ^^^ f))) + 4 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) + 7 * ((d &&& f) ^^^ (d ^^^ (e &&& f))) + 2 * (d ^^^ (e ^^^ f)) + 2 * ((d ^^^ e) &&& (d ^^^ f)) - 1 * (f ^^^ (d ||| (e &&& f))) + 7 * ((d &&& e) |||  ~~~(e ^^^ f)) + 5 * (e ^^^ ( ~~~d &&& (e ||| f))) - 3 *  ~~~(e ^^^ f) - 6 * (e ^^^ ( ~~~d ||| (e &&& f))) - 6 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) - 7 * (d ||| ( ~~~e ||| f)) - 6 * (e ^^^ ( ~~~d &&& ( ~~~e ||| f))) - 1 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 3 * (e |||  ~~~(d ||| f)) + 5 * (f ||| (d &&&  ~~~e)) - 6 * (e ||| f) - 6 *  ~~~(d ||| f) + 4 * ((d ^^^ e) &&&  ~~~(d ^^^ f)) - 11 * (d &&& (e ||| f)) - 11 * (d ^^^ ( ~~~e &&& f)) - 7 * (d &&& ( ~~~e ||| f)) - 7 * (f &&&  ~~~(d &&& e)) - 2 * ( ~~~d ||| ( ~~~e ||| f)) + 1 * ( ~~~f &&&  ~~~(d ^^^ e)) - 1 * (f ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) + 7 * ((d &&& e) ||| (e ^^^ f)) + 7 * (d ^^^ ( ~~~e ||| f)) + 2 * ((e &&&  ~~~f) ^^^ (d ||| (e ^^^ f))) + 2 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) + 1 * ((d |||  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 7 * (f ^^^  ~~~(d &&& (e ||| f))) - 5 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) + 7 *  ~~~(d ||| (e ||| f)) - 7 *  ~~~(d ||| ( ~~~e ||| f)) - 4 *  ~~~( ~~~d ||| (e ||| f)) + 18 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 6 * ( ~~~d &&& ( ~~~e &&& f)) - 7 * ( ~~~d &&& (e &&& f)) + 41 * (d &&& ( ~~~e &&& f)) + 8 * (d &&& (e &&& f)) = 3 * (e ^^^  ~~~(d ||| (e ^^^ f))) + 11 *  ~~~( ~~~d ||| (e &&& f))

theorem ashrslt_03_08_exact_proof : ashrslt_03_08_exact_before ⊑ ashrslt_03_08_exact_after

theorem sub_to_xor_or_commuted_proof : sub_to_xor_or_commuted_before ⊑ sub_to_xor_or_commuted_after

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

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

theorem absdiff1_proof : absdiff1_before ⊑ absdiff1_after

theorem or_nosignbit_lshr_proof : or_nosignbit_lshr_before ⊑ or_nosignbit_lshr_after

theorem e_433 :
    1 * y + 2 *  ~~~(x &&& y) - 1 * (x |||  ~~~y) - 7 *  ~~~(x &&&  ~~~y) + 1 *  ~~~(x &&&  ~~~x) + 5 *  ~~~(x ||| y) + 3 *  ~~~(x |||  ~~~y) - 2 * (x &&&  ~~~y) =  - 6 * (x &&& y)

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

theorem and_ne_with_one_bit_diff_constants3_logical_thm (e : IntW 8) :
  select (icmp IntPred.ne e (const? 8 65)) (icmp IntPred.ne e (const? 8 (-63))) (const? 1 0) ⊑
    icmp IntPred.ne (LLVM.and e (const? 8 127)) (const? 8 65)

theorem tryFactorization_xor_lshr_ashr_proof : tryFactorization_xor_lshr_ashr_before ⊑ tryFactorization_xor_lshr_ashr_after

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

theorem main5c_like_logical_thm.extracted_1._7 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 &&& 7#32 != 7#32) = 1#1 → ¬ofBool (x_1 &&& 7#32 == 7#32) = 1#1 → True → 0#32 = zeroExtend 32 0#1

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

theorem or_ranges_single_elem_left_proof : or_ranges_single_elem_left_before ⊑ or_ranges_single_elem_left_after

theorem ashrsgt_02_01_exact_proof : ashrsgt_02_01_exact_before ⊑ ashrsgt_02_01_exact_after

theorem test2_proof : test2_before ⊑ test2_after

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

theorem mul_sel_op0_thm (e : IntW 32) (e_1 : IntW 1) :
  mul (select e_1 (const? 32 0) (LLVM.udiv (const? 32 42) e { «exact» := true })) e ⊑
    select e_1 (const? 32 0) (const? 32 42)

theorem Option.some_bind'' (x : α) (f : α → Option β) : some x >>= f = f x

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

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

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

theorem pv_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬x_1 ≥ ↑8 → ofBool ((-1#8) >>> x_1 &&& x != x) = ofBool ((-1#8) >>> x_1 <ᵤ x)

theorem xor_notand_to_or_not4_thm (e e_1 e_2 : IntW 3) :
  LLVM.xor (LLVM.xor (LLVM.and e_2 e_1) (const? 3 (-1))) (LLVM.or e e_2) ⊑
    LLVM.or (LLVM.and e_2 e_1) (LLVM.xor (LLVM.or e e_2) (const? 3 (-1)))

theorem select_replace_udiv_non_speculatable_proof : select_replace_udiv_non_speculatable_before ⊑ select_replace_udiv_non_speculatable_after

theorem t9_c0_c2_thm.extracted_1._1 : ∀ (x : BitVec 8), 42#8 - x - 24#8 = 18#8 - x

theorem PR28476_logical_thm.extracted_1._5 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x_1 != 0#32) = 1#1 → ofBool (x_1 == 0#32) = 1#1 → zeroExtend 32 0#1 ^^^ 1#32 = zeroExtend 32 1#1

@[simp]
lemma swapLastTwo_eq2 : swapLastTwo (n := n) n = Fin.last (n+1)

theorem and_or1_thm.extracted_1._4 : ∀ (x x_1 x_2 : BitVec 1),
  x_2 ^^^ 1#1 ||

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

lemma CNFA.determinize_bv_language {m : CNFA n} :
    m.bv_recognizes L → m.determinize.bv_recognizes L

theorem bitwise_or_logical_or_icmps_comm1_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 8),
  ¬x_1 ≥ ↑8 → ofBool (x == 42#8) = 1#1 → ofBool (x_2 &&& 1#8 <<< x_1 == 0#8) ||

theorem fold_add_udiv_urem_commuted_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(10#32 = 0 ∨ 10#32 = 0 ∨ 4#32 ≥ ↑32) → 10#32 = 0 ∨ True ∧ (x / 10#32).umulOverflow 6#32 = true → False

theorem and_nosignbit_select_ashr_proof : and_nosignbit_select_ashr_before ⊑ and_nosignbit_select_ashr_after
</all_available_lemmas>

<local_ctx>
import Mathlib.Data.Bool.Basic

import Mathlib.Data.Fin.Basic

import Blase.Fast.BitStream

import Blase.SingleWidth.Defs

open Term

open BitStream in

open BitStream in

section Predicate

end Predicate
</local_ctx>

<target_theorem>
theorem eq_true_iff_of_eq_false_iff (b : Bool) (rhs : Prop) (h : (b = false) ↔ rhs) :
    (b = true) ↔ ¬ rhs :=
</target_theorem>

