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

syntax "neg" : MLIR.Pretty.uniform_op

macro_rules
  | `(mlir_op| $res:mlir_op_operand = const ($x)
      $[: $outer_type]? ) => do
      let outer_type ← outer_type.getDM `(mlir_type| _)
      `(mlir_op| $res:mlir_op_operand = "const"()
          {val = $x:num : $outer_type} : ($outer_type) -> ($outer_type) )

macro_rules
  | `(mlir_op| $res:mlir_op_operand = li ($x)
     $[: $outer_type]?  ) => do
      let outer_type ← outer_type.getDM `(mlir_type| _ )
      `(mlir_op| $res:mlir_op_operand = "li"()
          {imm = $x:num : $outer_type } : ($outer_type) -> ($outer_type))

macro_rules
| `(mlir_op| $res:mlir_op_operand = $op1:MLIR.Pretty.RV.opWithImmediate $reg1 , $x : $t)  => do
    let some opName := MLIR.EDSL.Pretty.extractOpName op1.raw
      | Macro.throwUnsupported
    `(mlir_op| $res:mlir_op_operand = $opName ($reg1) {imm = $x:num : $t} : ($t) -> ($t) )

macro_rules
| `(mlir_op| $res:mlir_op_operand = $op1:MLIR.Pretty.RV.opWithShamt $reg1 , $x  : $t )  => do
    let some opName := MLIR.EDSL.Pretty.extractOpName op1.raw
      | Macro.throwUnsupported
    `(mlir_op| $res:mlir_op_operand = $opName ($reg1) {shamt = $x:num : $t}  : ($t) -> ($t) )

macro "[mlir_attr_entry|" entry:mlir_attr_entry "]" : term => do
  let `(mlir_attr_entry| $key $[= $val]?) := entry | Macro.throwUnsupported
  let key ← match key.raw[0] with
    | .ident _ key _ _ => pure key.toString
    
    
    
    | .node _ `str ⟨(.atom _ val)::[]⟩ => pure val
    
    | _ => Macro.throwUnsupported
  let value ← match val with
    | none      => `(AttrValue.unit)
    | some val  => `([mlir_attr_val| $val])
  `(AttrEntry.mk $(Lean.quote key) $value)

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

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)

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

def eq_smin1_after := [llvm|
{
^0(%arg87 : i32, %arg88 : i32):
  %0 = llvm.icmp "sle" %arg87, %arg88 : i32
  "llvm.return"(%0) : (i1) -> ()
}
]

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

def testi64i32_ne_before := [llvm|
{
^0(%arg7 : i64):
  %0 = llvm.mlir.constant(32) : i64
  %1 = llvm.mlir.constant(31 : i32) : i32
  %2 = llvm.lshr %arg7, %0 : i64
  %3 = llvm.trunc %2 : i64 to i32
  %4 = llvm.trunc %arg7 : i64 to i32
  %5 = llvm.ashr %4, %1 : i32
  %6 = llvm.icmp "ne" %5, %3 : i32
  "llvm.return"(%6) : (i1) -> ()
}
]

structure RawCNFA.SimulFun (m : RawCNFA A) (M : NFA A Q) (f : m.states ≃ Q)  where
  accept {q} : ((f.invFun q).val ∈ m.finals ↔ q ∈ M.accept)
  initial {q} : q ∈ M.start ↔ (f.invFun q).val ∈ m.initials
  trans_match {a q q'} : q' ∈ M.step q a ↔ (f.invFun q').val ∈ m.tr (f.invFun q) a

def test_mul_nuw_nsw__nsw_is_safe_before := [llvm|
{
^0(%arg7 : i32):
  %0 = llvm.mlir.constant(-83886080 : i32) : i32
  %1 = llvm.mlir.constant(-83886079 : i32) : i32
  %2 = llvm.mlir.constant(9 : i32) : i32
  %3 = llvm.mlir.constant(-754974711 : i32) : i32
  %4 = llvm.or %arg7, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.mul %4, %2 overflow<nsw,nuw> : i32
  %7 = "llvm.select"(%5, %3, %6) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%7) : (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 add_constant_equal_with_the_top_bit_of_demandedbits_pass_after := [llvm|
{
^0(%arg9 : i32):
  %0 = llvm.mlir.constant(24 : i32) : i32
  %1 = llvm.mlir.constant(16 : i32) : i32
  %2 = llvm.and %arg9, %0 : i32
  %3 = llvm.xor %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

@[instance] def instReprTy := instPrint.instReprTy

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) -> ()
}
]

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 uadd_sat_flipped_wrong_bounds_before := [llvm|
{
^0(%arg96 : 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 "uge" %arg96, %0 : i32
  %4 = llvm.add %arg96, %1 : i32
  %5 = "llvm.select"(%3, %2, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def fold_add_udiv_urem_or_disjoint_after := [llvm|
{
^0(%arg5 : i32):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.mlir.constant(6 : i32) : i32
  %2 = llvm.udiv %arg5, %0 : i32
  %3 = llvm.mul %2, %1 overflow<nuw> : i32
  %4 = llvm.add %3, %arg5 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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 llvm_const_lower_riscv_li_7 : LLVMPeepholeRewriteRefine 64 [] :=
  {lhs := constLLVM_7, rhs:= liRiscv_7,
   correct := by admit /- proof elided -/

def t2_before := [llvm|
{
^0(%arg220 : i8, %arg221 : i8):
  %0 = llvm.mlir.constant(-42 : i8) : i8
  %1 = llvm.shl %0, %arg221 : i8
  %2 = llvm.sub %arg220, %1 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def udiv_common_divisor_before := [llvm|
{
^0(%arg65 : i1, %arg66 : i5, %arg67 : i5, %arg68 : i5):
  %0 = llvm.udiv %arg67, %arg66 : i5
  %1 = llvm.udiv %arg68, %arg66 : i5
  %2 = "llvm.select"(%arg65, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i5, i5) -> i5
  "llvm.return"(%2) : (i5) -> ()
}
]

def different_size_zext_zext_eq_before := [llvm|
{
^0(%arg22 : i4, %arg23 : i7):
  %0 = llvm.zext %arg22 : i4 to i25
  %1 = llvm.zext %arg23 : i7 to i25
  %2 = llvm.icmp "eq" %0, %1 : i25
  "llvm.return"(%2) : (i1) -> ()
}
]

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

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

def one_side_fold_eq_before := [llvm|
{
^0(%arg25 : i32, %arg26 : i32, %arg27 : i32, %arg28 : i1):
  %0 = "llvm.select"(%arg28, %arg25, %arg27) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %1 = "llvm.select"(%arg28, %arg26, %arg27) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "eq" %1, %0 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def udiv_i32_multiuse_before := [llvm|
{
^0(%arg25 : i8, %arg26 : i8):
  %0 = llvm.zext %arg25 : i8 to i32
  %1 = llvm.zext %arg26 : i8 to i32
  %2 = llvm.udiv %0, %1 : i32
  %3 = llvm.add %0, %1 : i32
  %4 = llvm.mul %2, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

LawfulMonad in Init.Control.Lawful.Basic

@[simp_llvm]
def not? {w : Nat} (x : BitVec w) : IntW w := do
  .value (~~~x)

abbrev EnumerativeSearchCache :=  Std.HashMap BVExprWrapper BVExpr.PackedBitVec

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

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 lshr_lshr_pow2_const_after := [llvm|
{
^0(%arg65 : i16):
  %0 = llvm.mlir.constant(3 : i16) : i16
  %1 = llvm.mlir.constant(4 : i16) : i16
  %2 = llvm.mlir.constant(0 : i16) : i16
  %3 = llvm.icmp "eq" %arg65, %0 : i16
  %4 = "llvm.select"(%3, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i16, i16) -> i16
  "llvm.return"(%4) : (i16) -> ()
}
]

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

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

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

def ashr_and_after := [llvm|
{
^0(%arg17 : i8):
  %0 = llvm.mlir.constant(-64 : i8) : i8
  %1 = llvm.ashr %0, %arg17 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

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) -> ()
}
]

let some width ← H.getWidth w  | throwError m! "Could not determine the rewrite width from {w}"
          let startTime ← Core.liftIOCore IO.monoMsNow

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

def 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 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 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 ugt_swap_and_not_min_logical_before := [llvm|
{
^0(%arg68 : i8, %arg69 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "ult" %arg69, %arg68 : i8
  %3 = llvm.icmp "ne" %arg68, %0 : i8
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def t1_ult_slt_0_after := [llvm|
{
^0(%arg63 : i32, %arg64 : i32, %arg65 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(65535 : i32) : i32
  %2 = llvm.icmp "slt" %arg63, %0 : i32
  %3 = llvm.icmp "sgt" %arg63, %1 : i32
  %4 = "llvm.select"(%2, %arg64, %arg63) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %5 = "llvm.select"(%3, %arg65, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

DecidableRel in Init.Prelude

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

def no_masks_with_logical_or2_after := [llvm|
{
^0(%arg7 : i32, %arg8 : i32, %arg9 : i32):
  %0 = llvm.mlir.constant(63 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.mlir.constant(true) : i1
  %3 = llvm.icmp "ne" %arg8, %0 : i32
  %4 = llvm.and %arg7, %arg9 : i32
  %5 = llvm.icmp "ne" %4, %1 : i32
  %6 = "llvm.select"(%5, %2, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%6) : (i1) -> ()
}
]

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

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

def sub_to_add_5 : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant 5 : i64
      %1 = llvm.sub %x, %c : i64
      llvm.return %1 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant -5 : i64
      %1 = llvm.add %x, %c : i64
      llvm.return %1 : i64
  }]

def alive_Select_1105_src  (w : Nat)   :=
[llvm( w )| {
^bb0(%Y : _, %X : _):
  %v1 = llvm.mlir.constant 0 :  i1
  %v2 = llvm.select %v1,%X, %Y
  llvm.return %v2
}]

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

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

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

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

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

checkTimeout

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

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) -> ()
}
]

IO.FS.Handle in Init.System.IO

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) -> ()
}
]
</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 ashrsgt_01_15_thm (e : IntW 4) :
  icmp IntPred.sgt (ashr e (const? 4 1)) (const? 4 (-1)) ⊑ icmp IntPred.sgt e (const? 4 (-1))

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

theorem nonexact_lshr_eq_noexactlog_proof : nonexact_lshr_eq_noexactlog_before ⊑ nonexact_lshr_eq_noexactlog_after

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

theorem e_2475 :
     - 2 * ( ~~~e &&& (d ^^^ f)) - 3 * (f ^^^ (d |||  ~~~e)) - 6 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 6 * (e &&&  ~~~(d &&& f)) + 3 *  ~~~( ~~~d &&& (e ||| f)) - 11 * (e ^^^  ~~~(d &&&  ~~~f)) + 11 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) - 6 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) + 4 * (f |||  ~~~(d ^^^ e)) - 5 * (f &&&  ~~~(d &&&  ~~~e)) + 4 *  ~~~(d ^^^ ( ~~~e &&& f)) - 2 * (e &&&  ~~~(d ^^^ f)) - 1 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 1 * (f ||| (d &&&  ~~~e)) - 1 * (e ^^^ ( ~~~d ||| (e ||| f))) + 11 * ((e &&& f) ||| (d &&& (e ||| f))) + 1 *  ~~~(e &&&  ~~~f) + 5 *  ~~~(e ||| f) - 1 * (f ^^^ (d ||| (e ||| f))) - 2 * (e ^^^ ( ~~~d &&& ( ~~~e ||| f))) + 3 * (f ^^^  ~~~(d &&& (e ||| f))) + 1 * ( ~~~(d &&& e) &&& (e ^^^ f)) - 11 * (d &&& (e ^^^ f)) + 2 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) + 2 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 2 * (f ^^^ (d ||| ( ~~~e &&& f))) - 2 * ((d |||  ~~~e) &&& (d ^^^ (e ^^^ f))) + 5 * (d &&&  ~~~f) - 1 * ((e &&& f) ^^^  ~~~( ~~~d &&& (e ^^^ f))) - 1 *  ~~~( ~~~d &&& ( ~~~e ||| f)) - 3 *  ~~~(d ||| (e &&& f)) + 4 *  ~~~(d ^^^ (e &&& f)) + 2 * ((d &&& e) |||  ~~~(d ^^^ (e ^^^ f))) - 7 * (e &&& f) - 7 *  ~~~(d ^^^ e) + 1 * (e ^^^ ( ~~~d &&& (e ^^^ f))) + 1 *  ~~~(d &&& e) - 1 *  ~~~(d &&& (e ^^^ f)) + 3 * (f ^^^ (d ||| e)) - 5 * (f ^^^  ~~~(d &&& (e &&& f))) + 1 * (e ^^^  ~~~(d |||  ~~~f)) - 7 * ( ~~~d &&& (e ^^^ f)) + 11 * (f ^^^ (d ||| ( ~~~e ||| f))) - 2 * ( ~~~d ||| (e &&& f)) - 11 * ((d &&&  ~~~e) ||| (e ^^^ f)) + 7 * (e |||  ~~~(d ||| f)) - 1 * ( ~~~(d ||| e) ||| (d ^^^ (e ^^^ f))) + 7 * ((d ^^^ e) |||  ~~~(d ^^^ f)) + 1 * (f ^^^ ( ~~~d ||| (e &&& f))) - 5 *  ~~~e + 2 * ( ~~~d &&& ( ~~~e ||| f)) + 2 * (e ^^^ ( ~~~d &&& (e ||| f))) + 11 * (f ^^^ (d &&& (e ||| f))) + 1 *  ~~~(d &&& ( ~~~e ||| f)) + 7 * (e |||  ~~~(d |||  ~~~f)) + 5 * ((d ||| e) &&&  ~~~(e ^^^ f)) - 5 * (e |||  ~~~(d ^^^ f)) + 5 *  ~~~(d ||| f) - 2 * (f ^^^  ~~~(d &&&  ~~~e)) - 1 * ((d &&& f) ^^^ (d ^^^ ( ~~~e &&& f))) - 1 * f - 3 * ((d &&& f) ^^^ (d ^^^ (e &&& f))) - 3 * (e ^^^ (d &&& (e ^^^ f))) - 7 * (e ^^^ ( ~~~d ||| ( ~~~e ||| f))) - 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) - 1 *  ~~~( ~~~d ||| (e &&& f)) + 2 *  ~~~(d &&&  ~~~d) - 1 * (e ^^^ (d ||| ( ~~~e ||| f))) + 1 * ((d ^^^ e) ||| (d ^^^ f)) + 1 * ((e &&&  ~~~f) ^^^ ( ~~~d ||| (e ^^^ f))) - 1 * ( ~~~(d ^^^ e) ||| (d ^^^ f)) - 6 * (e ||| (d &&& f)) - 6 * (d ^^^ ( ~~~e &&& f)) - 7 *  ~~~(d ||| (e ||| f)) + 3 *  ~~~(d ||| ( ~~~e ||| f)) + 27 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 47 * ( ~~~d &&& ( ~~~e &&& f)) - 25 * ( ~~~d &&& (e &&& f)) + 39 * (d &&& ( ~~~e &&& f)) + 17 * (d &&& (e &&& f)) =  - 23 *  ~~~( ~~~d ||| (e ||| f)) + 7 * (d |||  ~~~f)

theorem or_signbit_lshr_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬8#32 ≥ ↑32 → (x ||| BitVec.ofInt 32 (-65536)) >>> 8#32 = x >>> 8#32 ||

theorem e_2064 :
    1 * (e ^^^ ( ~~~d &&& ( ~~~e ||| f))) - 1 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) - 5 * (e ^^^  ~~~(d |||  ~~~f)) + 11 * (f |||  ~~~(d |||  ~~~e)) - 1 *  ~~~(d ||| e) - 3 * (e ^^^  ~~~(d &&& f)) + 3 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) + 4 * ( ~~~d ||| (e ^^^ f)) - 2 *  ~~~(e &&& f) + 1 * ( ~~~f ||| (d ^^^ e)) - 11 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 2 * ((d &&& f) ^^^ (d ^^^ ( ~~~e &&& f))) - 3 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) - 11 * (e ^^^ (d ||| (e ||| f))) - 3 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) + 2 *  ~~~( ~~~d ||| (e &&& f)) - 1 * (f ^^^  ~~~(d ||| e)) - 7 * ((d &&& e) |||  ~~~(e ^^^ f)) - 7 * (e &&& (d |||  ~~~f)) + 1 * (f &&& (d |||  ~~~e)) + 5 * e + 2 * (e ^^^ (d &&& f)) + 11 * (d &&&  ~~~e) + 1 * (e ^^^ (d &&& ( ~~~e ||| f))) + 7 * ( ~~~(d &&& e) &&&  ~~~(d ^^^ (e ^^^ f))) - 7 * (e ^^^ ( ~~~d ||| (e ^^^ f))) + 1 * (e ^^^ (d ||| (e ^^^ f))) + 1 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) + 3 *  ~~~(d ^^^ (e ^^^ f)) + 11 * (f |||  ~~~(d ||| e)) + 9 *  ~~~(d ||| (e ||| f)) - 2 *  ~~~(d ||| ( ~~~e ||| f)) + 16 *  ~~~( ~~~d ||| (e ||| f)) + 6 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 3 * ( ~~~d &&& ( ~~~e &&& f)) - 34 * ( ~~~d &&& (e &&& f)) - 32 * (d &&& ( ~~~e &&& f)) + 15 * (d &&& (e &&& f)) = 1 *  ~~~(d &&& f)

theorem select_exact_lshr_icmp_const_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (31#32 <ᵤ x) = 1#1 → 5#32 ≥ ↑32 → False

@[simp, aesop 50% unsafe]
theorem evalFrom_mono (M : NFA α σ) (S₁ S₂ : Set σ) (x : List α) (h : S₁ ⊆ S₂) :
    M.evalFrom S₁ x ⊆ M.evalFrom S₂ x

theorem select_icmp_sgt_allones_smin_flipped_proof : select_icmp_sgt_allones_smin_flipped_before ⊑ select_icmp_sgt_allones_smin_flipped_after

theorem e_1074 :
    5 *  ~~~z - 11 *  ~~~(z ^^^ t) - 2 * t - 2 * (z ^^^ t) + 3 *  ~~~t - 4 *  ~~~(z |||  ~~~t) - 1 * (z &&&  ~~~t) =  - 10 * (z &&& t) - 3 *  ~~~(z &&&  ~~~t)

theorem e_512 :
    4 *  ~~~(x &&&  ~~~x) - 1 *  ~~~x + 7 * y + 1 *  ~~~(x &&& y) - 1 * (x |||  ~~~y) + 7 *  ~~~(x &&&  ~~~y) - 10 *  ~~~(x ||| y) - 3 * (x &&&  ~~~y) - 17 * (x &&& y) = 17 *  ~~~(x |||  ~~~y) + 1 * (x ^^^ y)

theorem test_sub_nuw_nsw__nsw_is_safe_thm.extracted_1._3 : ∀ (x : BitVec 32),
  ¬ofBool (x ||| BitVec.ofInt 32 (-2147483648) == BitVec.ofInt 32 (-2147483647)) = 1#1 →
    ¬(True ∧ (BitVec.ofInt 32 (-2147483648)).ssubOverflow (x ||| BitVec.ofInt 32 (-2147483648)) = true ∨
          True ∧ (BitVec.ofInt 32 (-2147483648)).usubOverflow (x ||| BitVec.ofInt 32 (-2147483648)) = true) →
      True ∧ (BitVec.ofInt 32 (-2147483648)).ssubOverflow (x ||| BitVec.ofInt 32 (-2147483648)) = true → False

theorem not_not_true_proof : not_not_true_before ⊑ not_not_true_after

theorem shl_nsw_slt_1_proof : shl_nsw_slt_1_before ⊑ shl_nsw_slt_1_after

theorem zext_eq_sext_thm.extracted_1._1 : ∀ (x x_1 : BitVec 1),
  ofBool (zeroExtend 32 x_1 == signExtend 32 x) = (x_1 ||| x) ^^^ 1#1

theorem a_false_implies_b_false2_comm_thm.extracted_1._5 : ∀ (x x_1 : BitVec 1) (x_2 : BitVec 8),
  ofBool (20#8 <ᵤ x_2) = 1#1 → ofBool (10#8 <ᵤ x_2) = 1#1 → x_1 ||

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

theorem nonexact_lshr_eq_proof : nonexact_lshr_eq_before ⊑ nonexact_lshr_eq_after

theorem mul_select_zext_proof : mul_select_zext_before ⊑ mul_select_zext_after

theorem udiv_shl_mul_nuw_proof : udiv_shl_mul_nuw_before ⊑ udiv_shl_mul_nuw_after

theorem ashr_ult_2_proof : ashr_ult_2_before ⊑ ashr_ult_2_after

theorem e_253 :
    11 * (x ||| y) + 2 *  ~~~y - 1 * (x |||  ~~~y) + 4 * y - 3 *  ~~~(x ||| y) - 12 * (x &&&  ~~~y) - 14 * (x &&& y) = 17 *  ~~~(x |||  ~~~y) - 2 *  ~~~x

theorem t0_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬63#64 ≥ ↑64 →
    63#64 ≥ ↑64 ∨ True ∧ signExtend 64 (truncate 32 (x.sshiftRight' 63#64)) ≠ x.sshiftRight' 63#64 → False

theorem select_icmp_ne_0_and_32_or_4096_thm (e e_1 : IntW 32) :
  select (icmp IntPred.ne (const? 32 0) (LLVM.and e_1 (const? 32 32))) e (LLVM.or e (const? 32 4096)) ⊑
    LLVM.or e (LLVM.xor (LLVM.and (shl e_1 (const? 32 7)) (const? 32 4096)) (const? 32 4096))

theorem lor_lor_left2_thm (e e_1 : IntW 1) :
  select (select e_1 (const? 1 1) e) (const? 1 1) e ⊑ select e_1 (const? 1 1) e

theorem and_or_not_not_commute5_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  (x_2 &&& x_1 ^^^ -1#32) &&& (x_1 &&& x ^^^ -1#32 ||| x_2) = (x ||| x_2) &&& x_1 ^^^ -1#32

theorem trunc_shl_ashr_infloop_thm (e : IntW 64) :
  trunc 32 (shl (ashr e (const? 64 3)) (const? 64 2)) ⊑
    LLVM.and (trunc 32 (lshr e (const? 64 1))) (const? 32 (-4))

@[simp]
theorem Expr.regArgs_mk {Γ : Ctxt d.Ty} {ty eff op}
    (ty_eq : ty = DialectSignature.returnTypes op)
    (eff_le : DialectSignature.effectKind op ≤ eff)
    (args : HVector (Var Γ) (DialectSignature.sig op)) (regArgs) :
    (Expr.mk op ty_eq eff_le args regArgs).regArgs = regArgs

theorem fold_and_zext_icmp_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 64),
  zeroExtend 8 (ofBool (x_1 <ₛ x_2)) &&& zeroExtend 8 (ofBool (x_2 <ₛ x)) =
    zeroExtend 8 (ofBool (x_1 <ₛ x_2) &&& ofBool (x_2 <ₛ x))

theorem ne_nuw_rem_zero_thm (e : IntW 8) :
  icmp IntPred.ne (mul e (const? 8 5) { «nsw» := false, «nuw» := true }) (const? 8 (-126)) ⊑
    icmp IntPred.ne e (const? 8 26)

theorem or_ranges_single_elem_right_proof : or_ranges_single_elem_right_before ⊑ or_ranges_single_elem_right_after

theorem e_1124 :
    5 * z - 1 *  ~~~(z &&&  ~~~t) - 1 * (z ^^^ t) + 7 *  ~~~t + 1 * t - 5 *  ~~~(z ^^^ t) - 2 *  ~~~(z ||| t) - 11 * (z &&&  ~~~t) =  - 1 *  ~~~z

theorem and_xor_commute4_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(x_1 = 0 ∨ x = 0 ∨ x_1 = 0) → x_1 = 0 ∨ x = 0 → False

@[simp]
lemma reduce_accepts {M : NFA' n} : M.reduce.accepts = M.accepts

theorem BitVec.even_mul_eq_shiftLeft_mul_of_eq_mul_two
    (w : Nat) (x : BitVec w) (n e : Nat) (he : e = n * 2) :
    (BitVec.ofNat w e) * x = (BitVec.ofNat w n) * (x <<< (1 : Nat))

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

theorem and_lshr_and_thm (e : IntW 32) :
  select (icmp IntPred.eq (LLVM.and e (const? 32 1)) (const? 32 0)) (LLVM.and (lshr e (const? 32 1)) (const? 32 1))
      (const? 32 1) ⊑
    zext 32 (icmp IntPred.ne (LLVM.and e (const? 32 3)) (const? 32 0))

theorem ashr_lshr_exact_both_proof : ashr_lshr_exact_both_before ⊑ ashr_lshr_exact_both_after

theorem MatchVar.isMonotone_unifyVars  : IsMonotone (unifyVars w v)

theorem sub_ashr_or_i32_commute_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬(True ∧ x.ssubOverflow x_1 = true ∨ 31#32 ≥ ↑32) →
    ¬ofBool (x <ₛ x_1) = 1#1 → x_1 ||

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

@[bv_automata_nnf] theorem imp_self_eq (p : Prop) : (p → p) = True

theorem e_1078 :
     - 2 *  ~~~z + 1 *  ~~~(z &&&  ~~~z) - 3 * z - 1 *  ~~~(z &&&  ~~~t) + 7 * (z ||| t) + 2 *  ~~~(z ||| t) + 6 *  ~~~(z |||  ~~~t) - 5 * (z &&&  ~~~t) =  - 7 * (z &&& t) + 11 * t

theorem lshrult_03_03_exact_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬(True ∧ x >>> 3#4 <<< 3#4 ≠ x ∨ 3#4 ≥ ↑4) → ofBool (x >>> 3#4 <ᵤ 3#4) = 1#1

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

theorem test6_proof : test6_before ⊑ test6_after

theorem test1_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 57), ¬(x_1 ≥ ↑57 ∨ x_1 ≥ ↑57) → x_1 ≥ ↑57 → False

theorem bar_proof : bar_before ⊑ bar_after

theorem neg_slt_42_proof : neg_slt_42_before ⊑ neg_slt_42_after

theorem PR42691_3_proof : PR42691_3_before ⊑ PR42691_3_after

@[simp]
theorem toBitVec_neg (a : BitStream) :
    (- a).toBitVec w = - (a.toBitVec w)

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

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

@[simp]
lemma complete_cast {M : NFA α σ} (h : σ = ς) : (h ▸ M).Complete ↔ M.Complete

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

theorem slt_swap_or_not_max_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x <ₛ x_1) = 1#1 → 1#1 = ofBool (x != 127#8)

theorem e_2218 :
    4 * ((d &&& e) ^^^  ~~~(d ^^^ ( ~~~e ||| f))) + 2 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) + 5 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 1 * ( ~~~d &&& (e ^^^ f)) + 7 * (f ^^^ (d ||| ( ~~~e ||| f))) - 1 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) + 2 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) - 2 * (d ||| ( ~~~e ||| f)) + 1 * (d ||| (e ^^^ f)) - 11 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) - 7 *  ~~~(d &&& ( ~~~e &&& f)) + 5 * (e ^^^  ~~~(d &&& ( ~~~e ||| f))) + 1 * (e ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) - 5 * (e ^^^  ~~~(d ||| f)) - 2 * (e |||  ~~~(d ^^^ f)) + 1 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) - 6 * (d &&& (e ^^^ f)) - 1 * (e ^^^ (d ||| (e ^^^ f))) - 2 * ( ~~~(d ^^^ e) &&& (d ^^^ f)) - 3 * (e ^^^ ( ~~~d ||| (e &&& f))) - 1 * (f ||| (d &&& e)) + 7 *  ~~~(d |||  ~~~f) + 1 * ((e &&& f) ^^^  ~~~( ~~~d &&& (e ^^^ f))) - 1 * (e ^^^ (d |||  ~~~f)) + 2 * (f ^^^  ~~~(d &&& (e &&& f))) + 1 * ( ~~~d &&& (e ||| f)) + 2 * ( ~~~e &&& (d ^^^ f)) - 7 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) + 5 *  ~~~(d |||  ~~~e) + 2 * (f ^^^  ~~~(d ||| e)) + 1 * ( ~~~d ||| (e ||| f)) - 6 * (f &&&  ~~~(d &&& e)) + 11 * (f ||| (d &&&  ~~~e)) + 2 * (e ^^^  ~~~( ~~~d &&& (e ||| f))) - 1 * ( ~~~(d ||| e) ||| (d ^^^ (e ^^^ f))) - 3 *  ~~~d - 7 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 1 * (f ^^^  ~~~(d &&& (e ||| f))) - 7 * (e ^^^  ~~~(d &&& (e &&& f))) + 2 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) + 11 *  ~~~(e ^^^ f) - 1 * (d ^^^ (e ||| f)) + 3 * (e ^^^  ~~~( ~~~d ||| (e &&& f))) - 5 * (f |||  ~~~(d ||| e)) - 2 * (f ^^^ (d &&& e)) - 11 * (e &&& f) + 31 *  ~~~(d ||| (e ||| f)) - 20 *  ~~~( ~~~d ||| (e ||| f)) + 33 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 13 * ( ~~~d &&& ( ~~~e &&& f)) + 18 * ( ~~~d &&& (e &&& f)) + 22 * (d &&& ( ~~~e &&& f)) + 19 * (d &&& (e &&& f)) = 11 * (e ^^^ ( ~~~d ||| ( ~~~e ||| f)))

theorem test_shl_nuw__nsw_is_safe_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (x ||| BitVec.ofInt 32 (-83886080) == BitVec.ofInt 32 (-83886079)) = 1#1 →
    ¬(True ∧ (x ||| BitVec.ofInt 32 (-83886080)) <<< 2#32 >>> 2#32 ≠ x ||| BitVec.ofInt 32 (-83886080) ∨ 2#32 ≥ ↑32) →
      (x ||| BitVec.ofInt 32 (-83886080)) <<< 2#32 * (x ||| BitVec.ofInt 32 (-83886080)) *
          (x ||| BitVec.ofInt 32 (-83886080)) <<< 2#32 =
        0#32

theorem icmp_eq_sext_ne_zero_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (signExtend 32 (ofBool (x != 0#32)) == x) = ofBool (x + 1#32 <ᵤ 2#32)

theorem sel_false_val_is_a_masked_lshr_of_true_val2_thm.extracted_1._2 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬2#32 ≥ ↑32 →
    ofBool ((x_1 &&& 60#32) >>> 2#32 == 0#32) = 1#1 →
      ¬(2#32 ≥ ↑32 ∨ True ∧ (x_1 >>> 2#32 &&& 15#32).msb = true ∨ zeroExtend 64 (x_1 >>> 2#32 &&& 15#32) ≥ ↑64) →
        x = x.sshiftRight' (zeroExtend 64 (x_1 >>> 2#32 &&& 15#32))

theorem bitwise_or_bitwise_or_icmps_comm1_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 8),
  ¬x_1 ≥ ↑8 → True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8 ∨ True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8 → False

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 eq_umin2_thm (e e_1 : IntW 32) :
  icmp IntPred.eq (select (icmp IntPred.ult e_1 e) e_1 e) e ⊑ icmp IntPred.ule e e_1

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

theorem f_thm (e : IntW 32) :
  select (icmp IntPred.slt e (const? 32 0)) (const? 1 1) (icmp IntPred.sgt e (ashr (const? 32 7) e)) ⊑
    select (icmp IntPred.slt e (const? 32 0)) (const? 1 1)
      (icmp IntPred.sgt e (lshr (const? 32 7) e))

theorem test0_proof : test0_before ⊑ test0_after

theorem substitute_constant_or_ne_swap_sle_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 != 42#8) ||

theorem icmp_mul_nsw_slt_proof : icmp_mul_nsw_slt_before ⊑ icmp_mul_nsw_slt_after

theorem e_2304 :
     - 1 * (f ^^^ ( ~~~d ||| ( ~~~e ||| f))) - 7 * (f ^^^ (d &&& (e ||| f))) + 1 * ((d &&& e) ^^^ (e ||| f)) - 2 * (f &&& (d |||  ~~~e)) + 2 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) - 2 * ( ~~~(d &&& e) &&& (e ^^^ f)) - 5 * (d ||| (e ^^^ f)) - 1 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) + 7 * (e ^^^  ~~~(d ||| (e &&& f))) - 2 * (e ^^^ (d &&& ( ~~~e ||| f))) - 1 * (f ^^^ (d ||| ( ~~~e &&& f))) + 11 * (e &&&  ~~~f) + 3 * (e &&&  ~~~(d &&& f)) - 2 * (e ||| (d &&&  ~~~f)) - 1 *  ~~~(d &&&  ~~~f) - 2 *  ~~~( ~~~d &&& ( ~~~e &&& f)) - 2 * ( ~~~d ||| (e ||| f)) - 11 * (f ^^^ (d &&&  ~~~e)) - 1 * (e |||  ~~~(d |||  ~~~f)) + 4 * (e ^^^  ~~~(d ||| (e ^^^ f))) + 2 * (e ^^^  ~~~(d ||| ( ~~~e &&& f))) - 3 *  ~~~(d ||| (e ^^^ f)) + 11 * ( ~~~(d &&& e) &&& (d ^^^ (e ^^^ f))) - 11 * (f ^^^  ~~~(d &&&  ~~~e)) + 5 * ((d |||  ~~~e) &&& (e ^^^ f)) - 6 * (f ^^^  ~~~(d ||| (e &&& f))) + 2 * ((d &&& f) ^^^ (d ^^^ ( ~~~e &&& f))) - 7 * (e ^^^  ~~~( ~~~d ||| (e &&& f))) + 1 * (e ^^^ ( ~~~d ||| (e ||| f))) + 3 *  ~~~( ~~~d ||| (e ^^^ f)) + 3 * ( ~~~d &&& (e ^^^ f)) - 5 * ( ~~~(d ||| e) ||| (d ^^^ (e ^^^ f))) + 2 * ((d &&&  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) - 3 * (f ^^^  ~~~(d &&& (e &&& f))) + 2 * ((d |||  ~~~e) &&& (d ^^^ (e ^^^ f))) + 5 * (f ^^^ (d ||| (e ||| f))) + 11 *  ~~~(d |||  ~~~e) - 5 * (d &&& e) - 3 *  ~~~(d ||| (e &&& f)) - 3 * ((d &&& e) |||  ~~~(e ||| f)) + 7 * ( ~~~e |||  ~~~(d ^^^ f)) - 1 * (f ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 1 * ((d &&& e) |||  ~~~(d ^^^ (e ^^^ f))) - 1 * ( ~~~(d ||| e) |||  ~~~(e ^^^ f)) - 11 * ( ~~~(d |||  ~~~e) |||  ~~~(e ^^^ f)) - 6 * (d ^^^ ( ~~~e ||| f)) + 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 1 * (e ^^^  ~~~(d &&& (e ||| f))) - 2 * ( ~~~(d &&& e) &&&  ~~~(e ^^^ f)) + 3 *  ~~~(d ^^^ ( ~~~e ||| f)) - 1 * (e ^^^ f) - 1 * (d &&& ( ~~~e ||| f)) - 1 * (e |||  ~~~(d ||| f)) - 6 * (d &&& (e ||| f)) + 2 * (e ||| (d ^^^ f)) + 26 *  ~~~(d ||| (e ||| f)) - 5 *  ~~~(d ||| ( ~~~e ||| f)) + 20 *  ~~~( ~~~d ||| (e ||| f)) + 15 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 2 * ( ~~~d &&& ( ~~~e &&& f)) + 41 * ( ~~~d &&& (e &&& f)) + 18 * (d &&& ( ~~~e &&& f)) + 35 * (d &&& (e &&& f)) = 2 * (e ^^^  ~~~(d &&& f)) - 11 * (f ^^^  ~~~(d ||| ( ~~~e &&& f)))

theorem test21_thm (e : IntW 8) : LLVM.and (ashr e (const? 8 7)) (const? 8 1) ⊑ lshr e (const? 8 7)

theorem test3_logical_proof : test3_logical_before ⊑ test3_logical_after

theorem select_xor_icmp_bad_6_thm.extracted_1._3 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x_1 != 1#32) = 1#1 → ¬ofBool (x_1 == 1#32) = 1#1 → False

theorem cmpne_xor_cst3_proof : cmpne_xor_cst3_before ⊑ cmpne_xor_cst3_after

theorem e_1701 :
    5 *  ~~~( ~~~a ||| (b &&& c)) - 5 * ((a &&& c) ^^^ (b ||| c)) + 2 * (a ^^^ c) + 5 * ((a &&& c) ^^^ (a ^^^ ( ~~~b &&& c))) - 11 * (b ^^^  ~~~( ~~~a &&& (b ||| c))) - 2 * ( ~~~a ||| ( ~~~b ||| c)) + 1 * (c ^^^  ~~~(a &&& (b &&& c))) - 5 * (b ^^^  ~~~(a ||| (b &&& c))) - 2 * (b ^^^ (a &&& c)) - 1 * ((a ||| b) &&& (a ^^^ (b ^^^ c))) + 1 * (b &&& (a ||| c)) - 2 * ( ~~~(a &&& b) &&& (a ^^^ (b ^^^ c))) + 4 *  ~~~(a ||| c) - 1 * ( ~~~(a ||| b) |||  ~~~(b ^^^ c)) + 1 * ( ~~~(a |||  ~~~b) ||| (a ^^^ (b ^^^ c))) + 1 *  ~~~(a &&& (b ^^^ c)) + 3 * (b ^^^ (a ||| c)) - 7 * (a ||| c) - 1 *  ~~~(a &&& ( ~~~b ||| c)) + 3 * (c ^^^  ~~~(a ||| ( ~~~b &&& c))) - 1 * (b |||  ~~~(a ^^^ c)) + 11 *  ~~~(a ||| (b ||| c)) + 11 *  ~~~(a ||| ( ~~~b ||| c)) + 6 *  ~~~( ~~~a ||| (b ||| c)) + 6 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 8 * ( ~~~a &&& ( ~~~b &&& c)) + 30 * ( ~~~a &&& (b &&& c)) + 6 * (a &&& ( ~~~b &&& c)) + 9 * (a &&& (b &&& c)) =  - 1 * (c ^^^  ~~~(a &&& ( ~~~b ||| c)))

theorem add_nuw_nsw_or_and_thm (e e_1 : IntW 32) :
  add (LLVM.or e_1 e) (LLVM.and e_1 e) { «nsw» := true, «nuw» := true } ⊑
    add e_1 e { «nsw» := true, «nuw» := true }

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

theorem test3_proof : test3_before ⊑ test3_after

theorem or_or_logic_and_1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1), ¬x_1 ||
</all_available_lemmas>

<local_ctx>
import LeanMLIR.Framework

import LeanMLIR.Util

import Mathlib.Tactic.Linarith

namespace Tensor1D

abbrev Index := ℕ

structure Tensor1d (α : Type) [Inhabited α] where
  size : Index
  val :  Index → α
  spec : ∀ (ix: Index), ix >= size -> val ix = default

def Tensor1d.extract [Inhabited α] (t: Tensor1d α)
  (left: Index) (len: Index) : Tensor1d α :=
  let right := if (left + len) < t.size then left + len else 0
  let size := right - left
  { size := size,
    val := fun ix =>
    if left + len < t.size
    then if (ix < len) then t.val (ix + left) else default
    else default,
    spec := by admit /- proof elided -/

def Tensor1d.insertslice  [Inhabited α] (t: Tensor1d α)
  (sliceix: Nat)
  (slice : Tensor1d α) : Tensor1d α where
  size := if sliceix > t.size then 0 else t.size + slice.size
  val := fun ix =>
    if sliceix > t.size then default 
    else if ix >= t.size + slice.size then default 
    else
      let go (ix: Nat) : α :=
        if ix < sliceix then t.val sliceix
        else if ix < sliceix + slice.size then slice.val (ix - sliceix)
        else t.val (ix - (sliceix + slice.size))
      go ix
  spec := by admit /- proof elided -/
</local_ctx>

<target_theorem>
theorem extractslice_insertslice [Inhabited α]
  (t: Tensor1d α)
  (sliceix: Nat)
  (slice: Tensor1d α)
  (CORRECT: ((t.insertslice sliceix slice).extract sliceix slice.size).size ≠ 0)
  : (t.insertslice sliceix slice).extract sliceix slice.size = slice :=
</target_theorem>

