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>
DecidableEq in Init.Prelude
Lean.ToExpr in Lean.ToExpr
List in Init.Prelude
Repr in Init.Data.Repr
Nat in Init.Prelude
String in Init.Prelude
Fin in Init.Prelude
List.ofFn in Init.Data.List.OfFn
Option in Init.Prelude
List.length in Init.Prelude

structure Ctxt (Ty : Type) : Type where
  ofList :: toList : List Ty
  
  deriving Repr, Lean.ToExpr, DecidableEq

@[grind=]
def length (Γ : Ctxt Ty) : Nat := Γ.toList.length

inductive Ty (q : Nat) (n : Nat)
  | index : Ty q n
  | integer : Ty q n
  | tensor : Ty q n
  | polynomialLike : Ty q n
  deriving DecidableEq, Repr

def appendInl (v : Γ.Var t) : (Γ ++ Δ).Var t :=
  ⟨v.val, by admit /- proof elided -/
  ⟩

def Var (Γ : Ctxt Ty) (t : Ty) : Type :=
  { i : Nat // Γ[i]? = some t }

def sgt_swap_and_min_commute_logical_after := [llvm|
{
^0(%arg338 : i8, %arg339 : i8):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

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

def negative_trunc_not_arg_logical_after := [llvm|
{
^0(%arg20 : i32, %arg21 : i32):
  %0 = llvm.mlir.constant(128 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(256 : i32) : i32
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.and %arg20, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.add %arg21, %0 : i32
  %7 = llvm.icmp "ult" %6, %2 : i32
  %8 = "llvm.select"(%5, %7, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%8) : (i1) -> ()
}
]

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

def test3_after := [llvm|
{
^0(%arg207 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def and_or3_commuted_after := [llvm|
{
^0(%arg164 : i1, %arg165 : i1, %arg166 : i32, %arg167 : i32):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "ne" %arg166, %arg167 : i32
  %3 = "llvm.select"(%2, %0, %arg164) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%arg165, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def test_after := [llvm|
{
  %0 = llvm.mlir.constant(0 : i32) : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

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

def test15_after := [llvm|
{
^0(%arg6 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.ashr %arg6, %0 : i32
  %3 = llvm.sub %1, %2 overflow<nsw> : i32
  %4 = llvm.sext %3 : i32 to i64
  "llvm.return"(%4) : (i64) -> ()
}
]

def bools2_logical_commute0_before := [llvm|
{
^0(%arg64 : i1, %arg65 : i1, %arg66 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.xor %arg66, %0 : i1
  %3 = "llvm.select"(%arg66, %arg64, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%2, %arg65, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %5 = "llvm.select"(%3, %0, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def extractOpName : Syntax → Option (TSyntax `str)
  | .node _ _ ⟨.atom _ name :: _⟩ => some <| Syntax.mkStrLit name
  | _ => none

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

def urem_common_dividend_defined_cond_before := [llvm|
{
^0(%arg13 : i1, %arg14 : i5, %arg15 : i5, %arg16 : i5):
  %0 = llvm.urem %arg14, %arg15 : i5
  %1 = llvm.urem %arg14, %arg16 : i5
  %2 = "llvm.select"(%arg13, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i5, i5) -> i5
  "llvm.return"(%2) : (i5) -> ()
}
]

def n2_before := [llvm|
{
^0(%arg19 : i1, %arg20 : i8, %arg21 : i8, %arg22 : i8, %arg23 : i8):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.icmp "eq" %arg20, %arg21 : i8
  %2 = llvm.xor %arg19, %0 : i1
  %3 = llvm.or %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

instance [ToString w] : ToString (Option w) where
  toString
    | some x => s!"(some {toString x})"
    | none   => "(none)"

def and_orn_cmp_3_logical_before := [llvm|
{
^0(%arg182 : i72, %arg183 : i72, %arg184 : i72):
  %0 = llvm.mlir.constant(42 : i72) : i72
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.mlir.constant(false) : i1
  %3 = llvm.icmp "ugt" %arg182, %arg183 : i72
  %4 = llvm.icmp "ule" %arg182, %arg183 : i72
  %5 = llvm.icmp "ugt" %arg184, %0 : i72
  %6 = "llvm.select"(%4, %1, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %7 = "llvm.select"(%3, %6, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%7) : (i1) -> ()
}
]

instance : MLIR.AST.TransformExpr (HSxComb) 0 where
  mkExpr := mkExpr

One in Init.Prelude

def not_invert_signbit_splat_mask2_before := [llvm|
{
^0(%arg81 : i8, %arg82 : i16):
  %0 = llvm.mlir.constant(6 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.ashr %arg81, %0 : i8
  %3 = llvm.xor %2, %1 : i8
  %4 = llvm.sext %3 : i8 to i16
  %5 = llvm.and %4, %arg82 : i16
  "llvm.return"(%5) : (i16) -> ()
}
]

@[simp_denote]
def shl_riscv_64 := [LV| {
  ^entry (%reg1: i64, %reg2: i64 ):
    %0 = "builtin.unrealized_conversion_cast"(%reg1) : (i64) -> (!i64)
    %1 = "builtin.unrealized_conversion_cast"(%reg2) : (i64) -> (!i64)
    %2 = sll %0, %1 : !i64
    %3 = "builtin.unrealized_conversion_cast"(%2) : (!i64) -> (i64)
    llvm.return %3 : i64
  }]

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 scalar_i8_shl_and_negC_eq_after := [llvm|
{
^0(%arg35 : i8, %arg36 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.shl %arg35, %arg36 : i8
  %2 = llvm.icmp "ult" %1, %0 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

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

def rewrite_patterns : List (Σ Γ, Σ ty, PeepholeRewrite DCPlus Γ ty) :=[
  mkRewrite rewrite_a_T,
  mkRewrite rewrite_a_F,
  mkRewrite rewrite_c_A,
  mkRewrite rewrite_c_B,
  mkRewrite rewrite_h_A,
  mkRewrite rewrite_h_B,
  mkRewrite rewrite_g,
  mkRewrite rewrite_e,
]

def ne_irregular_bit_widths_before := [llvm|
{
^0(%arg62 : i31, %arg63 : i31):
  %0 = llvm.mlir.constant(7 : i31) : i31
  %1 = llvm.mlir.constant(13 : i31) : i31
  %2 = llvm.lshr %arg62, %0 : i31
  %3 = llvm.trunc %2 : i31 to i6
  %4 = llvm.lshr %arg62, %1 : i31
  %5 = llvm.trunc %4 : i31 to i5
  %6 = llvm.lshr %arg63, %0 : i31
  %7 = llvm.trunc %6 : i31 to i6
  %8 = llvm.lshr %arg63, %1 : i31
  %9 = llvm.trunc %8 : i31 to i5
  %10 = llvm.icmp "ne" %3, %7 : i6
  %11 = llvm.icmp "ne" %5, %9 : i5
  %12 = llvm.or %11, %10 : i1
  "llvm.return"(%12) : (i1) -> ()
}
]

def test_shl_nuw__nuw_is_safe_after := [llvm|
{
^0(%arg80 : i32, %arg81 : i64):
  %0 = llvm.mlir.constant(2 : i32) : i32
  %1 = llvm.mlir.constant(-8 : i32) : i32
  %2 = llvm.shl %arg80, %0 : i32
  %3 = llvm.and %2, %1 : i32
  %4 = llvm.zext nneg %3 : i32 to i64
  %5 = llvm.ashr %arg81, %4 : i64
  "llvm.return"(%5) : (i64) -> ()
}
]

@[simp] abbrev FlatCom.denote [DialectDenote d]
    (flatCom : FlatCom d Γ eff Γ_out ts)
    (V : Γ.Valuation) : eff.toMonad d.m (HVector toType ts) :=
  flatCom.lets.denote V >>= (return flatCom.rets.map ·)

@[simp_denote]
def sltu_riscv_i32 :=
  [LV| {
    ^entry (%arg0: i32, %arg1: i32):
    %a = "builtin.unrealized_conversion_cast" (%arg0) : (i32) -> (!i64)
    %b = "builtin.unrealized_conversion_cast" (%arg1) : (i32) -> (!i64)
    %0 = "sext.w" (%a) : (!i64) -> (!i64)
    %1 = "sext.w" (%b) : (!i64) -> (!i64)
    %2 = sltu %0, %1 : !i64
    %3 = "builtin.unrealized_conversion_cast" (%2) : (!i64) -> (i32)
    llvm.return %3 : i32
  }]

def add_nsw_poison_constant_fold_after := [llvm|
{
^0(%arg2 : i1, %arg3 : i8):
  %0 = llvm.mlir.constant(64 : i8) : i8
  %1 = llvm.mlir.constant(-127 : i8) : i8
  %2 = llvm.add %arg3, %0 overflow<nsw> : i8
  %3 = "llvm.select"(%arg2, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

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

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 xor_icmp_to_ne_before := [llvm|
{
^0(%arg6 : i32):
  %0 = llvm.mlir.constant(4 : i32) : i32
  %1 = llvm.mlir.constant(6 : i32) : i32
  %2 = llvm.icmp "sgt" %arg6, %0 : i32
  %3 = llvm.icmp "slt" %arg6, %1 : i32
  %4 = llvm.xor %2, %3 : i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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 ExprRemapVar [DecidableEq d.Ty] [DecidableEq d.Op]
    {Γstart Γ Γ' : Ctxt d.Ty} {α}
    (lets : Lets d Γstart .pure Γ)
    (hom : Ctxt.Hom Γ' Γ)
    (vold : HVector Γ.Var α)
    (vnew : HVector Γ'.Var α)
    (VNEW: ∀ (Vstart : Ctxt.Valuation Γstart), vold.map (lets.denote Vstart) =
      vnew.map ((lets.denote Vstart).comap hom))
    (e' : Expr d Γ' .pure β) :
    {e : Expr d Γ .pure β // ∀ (V : Ctxt.Valuation Γstart),
          e.denoteOp (lets.denote V)
          = e'.denoteOp ((lets.denote V).comap hom) } :=
  match e' with
  | ⟨op, ty_eq, eff_le, args, regArgs⟩ =>
    let ⟨args', hargs'⟩ := VarRemapVar lets hom vold vnew VNEW args
    ⟨.mk op ty_eq eff_le args' regArgs, by admit /- proof elided -/
    ⟩

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

@[combinator_formatter MLIR.EDSL.balancedBrackets]
def MLIR.EDSL.balancedBrackets.formatter : Formatter := pure ()

\n Input expression: {hExpr} has generalization: {pretty}"
                          | GeneralizeContext.Tactic _name =>
                            match cfg.output with
                            | .thmStmt =>
                              let name := Name.mkSimple "foo"
                              pure m! "{H.prettifyAsTheorem name res allVariables widthVals}"
                            | .sexpr =>
                              throwError (H.prettifyAsSexpr res allVariables) widthVals|> format
            | none => throwError m! "Could not generalize {bvLogicalExpr}"
    | _ => throwError m!"The top level constructor is not an equality predicate in {hExpr}"

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

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

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

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

instance : DialectPrint Handshake where
  printOpName := reprStr
  printTy := reprStr
  printAttributes _ := ""
  dialectName := "handshake"
  printReturn _ := "return"

def uge_and_max_commute_before := [llvm|
{
^0(%arg234 : i8, %arg235 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.icmp "uge" %arg234, %arg235 : i8
  %2 = llvm.icmp "eq" %arg234, %0 : i8
  %3 = llvm.and %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def n2_before := [llvm|
{
^0(%arg0 : i8, %arg1 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.shl %0, %arg1 : i8
  %3 = llvm.xor %2, %1 : i8
  %4 = llvm.and %3, %arg0 : i8
  %5 = llvm.icmp "eq" %4, %arg0 : i8
  "llvm.return"(%5) : (i1) -> ()
}
]

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

def scalar_i16_shl_ult_const_before := [llvm|
{
^0(%arg16 : i16):
  %0 = llvm.mlir.constant(8 : i16) : i16
  %1 = llvm.mlir.constant(1024 : i16) : i16
  %2 = llvm.shl %arg16, %0 : i16
  %3 = llvm.icmp "ult" %2, %1 : i16
  "llvm.return"(%3) : (i1) -> ()
}
]

def sdiv_exact_eq_9_no_of_before := [llvm|
{
^0(%arg8 : i8, %arg9 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.mlir.constant(9 : i8) : i8
  %2 = llvm.and %arg9, %0 : i8
  %3 = llvm.sdiv exact %arg8, %2 : i8
  %4 = llvm.icmp "eq" %3, %1 : i8
  "llvm.return"(%4) : (i1) -> ()
}
]

def different_size_zext_zext_slt_before := [llvm|
{
^0(%arg18 : i7, %arg19 : i4):
  %0 = llvm.zext %arg18 : i7 to i25
  %1 = llvm.zext %arg19 : i4 to i25
  %2 = llvm.icmp "slt" %0, %1 : i25
  "llvm.return"(%2) : (i1) -> ()
}
]

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

@[simp_denote]
def add_llvm_nsw_nuw_flags_8 := [LV| {
   ^entry (%lhs: i8, %rhs: i8):
    %1 = llvm.add %lhs, %rhs overflow<nsw,nuw> : i8
    llvm.return %1 : i8
  }]

def src_x_and_nmask_sge_fail_maybe_z_before := [llvm|
{
^0(%arg11 : i8, %arg12 : i8, %arg13 : i1):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.shl %0, %arg12 : i8
  %3 = "llvm.select"(%arg13, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %4 = llvm.and %arg11, %3 : i8
  %5 = llvm.icmp "sge" %4, %3 : i8
  "llvm.return"(%5) : (i1) -> ()
}
]

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

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

def mul_select_zext_before := [llvm|
{
^0(%arg18 : i1, %arg19 : i64):
  %0 = llvm.mlir.constant(1) : i64
  %1 = "llvm.select"(%arg18, %arg19, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  %2 = llvm.zext %arg18 : i1 to i64
  %3 = llvm.mul %1, %2 : i64
  "llvm.return"(%3) : (i64) -> ()
}
]

def andcond.010.inv.inner.cond.in.inner.sel_before := [llvm|
{
^0(%arg65 : i1, %arg66 : i1, %arg67 : i1, %arg68 : i1, %arg69 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = "llvm.select"(%arg65, %arg66, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = llvm.xor %arg65, %1 : i1
  %4 = "llvm.select"(%3, %arg68, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %5 = "llvm.select"(%2, %arg69, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def neg_not_signbit2_before := [llvm|
{
^0(%arg4 : i8):
  %0 = llvm.mlir.constant(6 : i8) : i8
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.lshr %arg4, %0 : i8
  %3 = llvm.zext %2 : i8 to i32
  %4 = llvm.sub %1, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def a_before := [llvm|
{
^0(%arg48 : i1, %arg49 : i1):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.zext %arg48 : i1 to i32
  %3 = llvm.zext %arg49 : i1 to i32
  %4 = llvm.sub %0, %3 : i32
  %5 = llvm.add %2, %1 : i32
  %6 = llvm.add %5, %4 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def logic_or_logic_and_5_after := [llvm|
{
^0(%arg75 : i1, %arg76 : i1, %arg77 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = "llvm.select"(%arg77, %arg76, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = "llvm.select"(%arg75, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

|
</all_available_defs>

<all_available_lemmas>
Fin.coe_cast in Init.Data.Fin.Lemmas
List.getElem?_append in Init.Data.List.Lemmas
List.getElem?_ofFn in Init.Data.List.OfFn
List.getElem_append_right in Init.Data.List.BasicAux
List.length_append in Init.Data.List.Basic
Nat.ge_of_not_lt in Init.Data.Nat.Basic
Option.dite_none_right_eq_some in Init.Data.Option.Lemmas
Valuation.ext in Mathlib.RingTheory.Valuation.Basic
dite_eq_ite in Init.ByCases

@[simp] theorem ofList_append {ts us : List Ty} :
    Ctxt.ofList ts ++ Ctxt.ofList us = Ctxt.ofList (ts ++ us)

@[simp, grind=] theorem length_ofList : (ofList ts).length = ts.length

@[simp, grind=] theorem getElem?_ofList (i : Nat) : (ofList ts)[i]? = ts[i]?

@[simp, grind=] theorem getElem_ofList (i : Nat) (h : _) : (ofList ts)[i]'h = ts[i]'h

theorem t3_no_extrause_proof : t3_no_extrause_before ⊑ t3_no_extrause_after

theorem a_false_implies_b_false2_comm_thm.extracted_1._6 : ∀ (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 icmp_eq_and1_lshr_pow2_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬x ≥ ↑32 → zeroExtend 32 (ofBool (8#32 >>> x &&& 1#32 == 0#32)) = zeroExtend 32 (ofBool (x != 3#32))

theorem test51_thm.extracted_1._1 : ∀ (x : BitVec 64) (x_1 : BitVec 1),
  x_1 = 1#1 → True ∧ (truncate 32 x &&& BitVec.ofInt 32 (-2) &&& zeroExtend 32 (x_1 ^^^ 1#1) != 0) = true → False

theorem t_1_10_thm (e : IntW 8) :
  LLVM.and (select (icmp IntPred.ugt e (const? 8 1)) e (const? 8 1)) (const? 8 10) ⊑
    LLVM.and e (const? 8 10)

theorem test_add_nuw__nuw_is_safe_proof : test_add_nuw__nuw_is_safe_before ⊑ test_add_nuw__nuw_is_safe_after

theorem shl_xor_xor_bad_mask_distribute_proof : shl_xor_xor_bad_mask_distribute_before ⊑ shl_xor_xor_bad_mask_distribute_after

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

theorem test_add__nsw_is_safe_proof : test_add__nsw_is_safe_before ⊑ test_add__nsw_is_safe_after

theorem PR42691_8_proof : PR42691_8_before ⊑ PR42691_8_after

theorem lshrult_03_08_proof : lshrult_03_08_before ⊑ lshrult_03_08_after

theorem scalar_i16_shl_and_signbit_eq_thm (e e_1 : IntW 16) :
  icmp IntPred.eq (LLVM.and (shl e_1 e) (const? 16 (-32768))) (const? 16 0) ⊑
    icmp IntPred.sgt (shl e_1 e) (const? 16 (-1))

theorem ashrslt_03_00_thm (e : IntW 4) :
  icmp IntPred.slt (ashr e (const? 4 3)) (const? 4 0) ⊑ icmp IntPred.slt e (const? 4 0)

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

theorem lshrult_01_11_thm (e : IntW 4) : icmp IntPred.ult (lshr e (const? 4 1)) (const? 4 (-5)) ⊑ const? 1 1

theorem slt3 (w : Nat) (a b : BitVec w) : ((a.sle b) ∧ (b.sle a)) → a = b

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

theorem test2_proof : test2_before ⊑ test2_after

theorem toTensor_length_eq_rep_length [Fact (q > 1)] (a : R q n) :
  a.toTensor.length = a.repLength

theorem t0_sub_of_trueval_thm (e e_1 : IntW 8) (e_2 : IntW 1) :
  sub (select e_2 e_1 e) e_1 ⊑ select e_2 (const? 8 0) (sub e e_1)

theorem test_mul_nuw__nsw_is_safe_thm.extracted_1._3 : ∀ (x : BitVec 32),
  ¬ofBool (x ||| BitVec.ofInt 32 (-83886080) == BitVec.ofInt 32 (-83886079)) = 1#1 →
    ¬(True ∧ (x ||| BitVec.ofInt 32 (-83886080)).umulOverflow 9#32 = true) →
      True ∧ (x ||| BitVec.ofInt 32 (-83886080)).smulOverflow 9#32 = true → False

theorem bv_AndOrXor_1253_A__AB___A__B :
    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.xor e e_1) e ⊑ LLVM.and e (LLVM.xor e_1 (LLVM.const? w (-1)))

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

theorem zext_nneg_i1_proof : zext_nneg_i1_before ⊑ zext_nneg_i1_after

theorem ult_and_not_max_commute_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 != -1#8) &&& ofBool (x_1 <ᵤ x) = ofBool (x_1 <ᵤ x)

theorem sel_zext_thm.extracted_1._1 : ∀ (x : BitVec 1), ¬x = 1#1 → zeroExtend 64 42#32 = 42#64

theorem and_min_7_8_proof : and_min_7_8_before ⊑ and_min_7_8_after

theorem shl_nuw_add_nuw_thm (e : IntW 32) :
  shl (const? 32 1) (add e (const? 32 1) { «nsw» := false, «nuw» := true }) { «nsw» := false, «nuw» := true } ⊑
    shl (const? 32 2) e { «nsw» := false, «nuw» := true }

theorem e_2190 :
     - 7 * (e ^^^ ( ~~~d ||| (e &&& f))) - 5 * (e &&& (d ^^^ f)) - 2 *  ~~~(d ||| ( ~~~e &&& f)) + 5 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) + 1 * ( ~~~(d &&& e) &&& (e ^^^ f)) - 1 * (f ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 1 * (f ^^^  ~~~(d &&& (e &&& f))) - 2 * (e ^^^  ~~~( ~~~d &&& (e ||| f))) - 1 * (e ^^^ (d ||| ( ~~~e ||| f))) + 11 * (f ^^^ (d &&&  ~~~e)) - 11 * ( ~~~(d &&& e) &&&  ~~~(d ^^^ (e ^^^ f))) - 2 * (d ^^^ ( ~~~e ||| f)) + 1 * (d &&&  ~~~f) - 6 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) - 5 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) + 2 * (f ||| (d &&&  ~~~e)) + 3 * (e ^^^  ~~~(d &&& (e ^^^ f))) - 6 * ((e &&&  ~~~f) |||  ~~~( ~~~d ||| ( ~~~e &&& f))) - 1 * ((d |||  ~~~e) &&& (d ^^^ (e ^^^ f))) - 11 * ((d &&& e) ^^^ (d ^^^ ( ~~~e ||| f))) + 2 * (f &&&  ~~~(d ^^^ e)) - 1 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f)) - 1 * ( ~~~d &&& ( ~~~e ||| f)) + 1 * (e ^^^ (d &&& (e ||| f))) - 2 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) - 3 * (e &&& (d ||| f)) - 1 * ( ~~~f &&&  ~~~(d ^^^ e)) - 2 * (e |||  ~~~(d ^^^ f)) - 6 * (e ^^^  ~~~(d &&& (e ||| f))) + 2 * ((d &&& f) ^^^  ~~~(d ^^^ ( ~~~e &&& f))) + 1 *  ~~~( ~~~d &&& (e ||| f)) + 1 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) - 6 * (e |||  ~~~(d ||| f)) + 11 * ((e &&&  ~~~f) ^^^ ( ~~~d ||| (e ^^^ f))) + 3 *  ~~~(e ^^^ f) - 1 * (f ^^^  ~~~(d &&& (e ||| f))) - 2 * ((d &&& e) ^^^ (e ||| f)) - 1 *  ~~~(d &&& f) - 7 *  ~~~(e &&& f) + 2 * ( ~~~e &&& (d ^^^ f)) + 5 * (f ^^^ ( ~~~d ||| (e &&& f))) + 5 * (e ^^^ ( ~~~d &&& (e ^^^ f))) + 2 * (f ^^^  ~~~(d &&&  ~~~e)) - 11 * (d ^^^ e) + 39 *  ~~~(d ||| (e ||| f)) + 32 *  ~~~(d ||| ( ~~~e ||| f)) + 10 *  ~~~( ~~~d ||| (e ||| f)) + 35 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 25 * ( ~~~d &&& (e &&& f)) + 21 * (d &&& ( ~~~e &&& f)) + 9 * (d &&& (e &&& f)) =  - 2 * (e &&&  ~~~(d ^^^ f)) - 5 * ( ~~~(d ||| e) ||| (d ^^^ (e ^^^ f)))

theorem zext_sub_thm.extracted_1._1 : ∀ (x : BitVec 8),
  BitVec.ofInt 16 (-5) - zeroExtend 16 x &&& zeroExtend 16 x = zeroExtend 16 (BitVec.ofInt 8 (-5) - x &&& x)

theorem const_sub_add_const_proof : const_sub_add_const_before ⊑ const_sub_add_const_after

theorem ugt_rem_nz_thm (e : IntW 8) :
  icmp IntPred.ugt (mul e (const? 8 5) { «nsw» := false, «nuw» := true }) (const? 8 21) ⊑
    icmp IntPred.ugt e (const? 8 4)

theorem test3_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), ¬x = 0 → ofBool (x_1 / x != 0#32) = ofBool (x ≤ᵤ x_1)

theorem sle_smax4_proof : sle_smax4_before ⊑ sle_smax4_after

theorem e_7 :
    11 *  ~~~(x &&&  ~~~y) - 11 * x + 11 * (x &&&  ~~~y) + 11 * (x &&& y) = 11 *  ~~~(x ||| y) + 11 * y

theorem e_855 :
    7 * (z ||| t) - 2 * z + 4 * (z ^^^ t) - 1 *  ~~~(z ||| t) - 11 *  ~~~(z |||  ~~~t) - 10 * (z &&&  ~~~t) = 6 * (z &&& t) - 1 * (z |||  ~~~t)

theorem test_thm.extracted_1._1 : zeroExtend 32 (ofBool (1#32 == 2#32)) = 0#32

theorem e_1800 :
     - 1 * (b ^^^ (a |||  ~~~c)) - 6 * (c ||| (a &&& b)) + 3 * ((a |||  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) - 7 *  ~~~(b |||  ~~~c) - 1 *  ~~~(b &&&  ~~~c) + 5 *  ~~~(a ||| b) + 1 * (b ^^^  ~~~(a &&& (b &&& c))) - 5 * (c ^^^ (a &&& b)) - 11 * (c ^^^ (a &&&  ~~~b)) - 2 * (c ^^^ (a ||| (b &&& c))) - 11 * ((b &&& c) ||| (a &&& (b ||| c))) + 4 * (b ^^^ (a &&&  ~~~c)) - 5 * ((a &&& c) ^^^ (a ^^^ ( ~~~b &&& c))) - 2 * ((b &&&  ~~~c) |||  ~~~( ~~~a ||| ( ~~~b &&& c))) - 1 * (b &&& (a ||| c)) - 1 * (b &&&  ~~~c) + 2 * (c ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) - 2 * ( ~~~a ||| (b ||| c)) - 5 * ((b &&&  ~~~c) ^^^ ( ~~~a ||| (b ^^^ c))) - 2 *  ~~~b + 5 *  ~~~(a |||  ~~~c) + 4 * (b ^^^  ~~~(a |||  ~~~c)) - 2 * (b ^^^ (a ||| c)) + 4 * (a &&& ( ~~~b ||| c)) - 3 * ((a &&& b) |||  ~~~(b ||| c)) + 3 * ( ~~~(a |||  ~~~b) |||  ~~~(a ^^^ (b ^^^ c))) + 5 * (a &&&  ~~~b) - 1 * (c &&&  ~~~(a ^^^ b)) + 5 * ((a ||| b) &&& (b ^^^ c)) + 2 *  ~~~(a &&& ( ~~~b ||| c)) + 3 * ((b &&&  ~~~c) ^^^ (a ||| (b ^^^ c))) - 7 * (a ||| (b &&& c)) + 1 * ( ~~~(a &&&  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) - 3 *  ~~~(a ||| (b ||| c)) - 13 *  ~~~(a ||| ( ~~~b ||| c)) + 17 *  ~~~( ~~~a ||| (b ||| c)) + 25 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 35 * ( ~~~a &&& (b &&& c)) + 30 * (a &&& ( ~~~b &&& c)) + 29 * (a &&& (b &&& c)) =  - 27 * ( ~~~a &&& ( ~~~b &&& c))

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

theorem bools_logical_commute0_and2_thm.extracted_1._18 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 ^^^ 1#1 = 1#1 → ¬x_2 = 1#1 → ¬0#1 = 1#1 → x_2 &&& x = x_1

@[simp] theorem eval_trueUptoExcluding (n : Nat) {env : Fin 0 → BitStream} :
    (trueUptoExcluding n).eval env = fun i => decide (i < n)

theorem udiv_illegal_type_thm.extracted_1._1 : ∀ (x x_1 : BitVec 9), ¬zeroExtend 32 x = 0 → x = 0 → False

theorem badimm4_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬(7#8 ≥ ↑8 ∨ 8#16 ≥ ↑16) →
    ofBool ((truncate 8 x).sshiftRight' 7#8 == truncate 8 (x >>> 8#16)) = 1#1 →
      ofBool (127#16 <ₛ x) = 1#1 → truncate 8 x = 126#8

theorem test11_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬(True ∧ (x &&& BitVec.ofInt 8 (-13) &&& 8#8 != 0) = true) →
    (x ||| 12#8) ^^^ 4#8 = x &&& BitVec.ofInt 8 (-13) ||

theorem t15_and_with_const1_proof : t15_and_with_const1_before ⊑ t15_and_with_const1_after

theorem not_signbit_zext_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬15#16 ≥ ↑16 → zeroExtend 32 ((x ^^^ -1#16) >>> 15#16) = zeroExtend 32 (ofBool (-1#16 <ₛ x))

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

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

theorem ashrsgt_01_13_proof : ashrsgt_01_13_before ⊑ ashrsgt_01_13_after

theorem c_0_1_0_proof : c_0_1_0_before ⊑ c_0_1_0_after

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

theorem test9b_proof : test9b_before ⊑ test9b_after

theorem test11_proof : test11_before ⊑ test11_after

theorem lshr_or_thm (e : IntW 8) :
  LLVM.or (lshr (const? 8 16) e) (lshr (const? 8 3) (add e (const? 8 1))) ⊑ lshr (const? 8 17) e

theorem thisdoesnotloop_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x <ₛ BitVec.ofInt 32 (-128)) = 1#1 → truncate 8 128#32 = BitVec.ofInt 8 (-128)

theorem eval_sext_multi_use_in_one_inst_thm (e : IntW 32) :
  sext 32
      (LLVM.or
        (mul (LLVM.and (trunc 16 e) (const? 16 14)) (LLVM.and (trunc 16 e) (const? 16 14))
          { «nsw» := true, «nuw» := true })
        (const? 16 (-32768))) ⊑
    sext 32
      (LLVM.or
        (mul (LLVM.and (trunc 16 e) (const? 16 14)) (LLVM.and (trunc 16 e) (const? 16 14))
          { «nsw» := true, «nuw» := true })
        (const? 16 (-32768)) { «disjoint» := true })

@[symm]
theorem equal_up_to_symm (e : a ≈ʷ b) : b ≈ʷ a

theorem ashr_exact_poison_constant_fold_thm.extracted_1._1 : ∀ (x : BitVec 1),
  ¬x = 1#1 → ¬(True ∧ 42#8 >>> 3#8 <<< 3#8 ≠ 42#8 ∨ 3#8 ≥ ↑8) → (42#8).sshiftRight' 3#8 = 5#8

theorem main13_proof : main13_before ⊑ main13_after

theorem ne_umax3_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x <ᵤ x_1 + 3#32) = 1#1 → ofBool (x_1 + 3#32 != x) = ofBool (x_1 + 3#32 <ᵤ x)

theorem eval_fsmUltUnary_eq_decide
    (a : NatFSM wcard tcard bcard ncard icard pcard (.ofDep v))
    (b : NatFSM wcard tcard bcard ncard icard pcard (.ofDep w))
    {wenv : WidthExpr.Env wcard}
    {fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream}
    (henv : HWidthEnv fsmEnv wenv)
    (ha : HNatFSMToBitstream a) (hb : HNatFSMToBitstream b) :
    ((fsmUltUnary a b).eval fsmEnv) i =
   (decide (min i (v.toNat wenv) < min i (w.toNat wenv)))

theorem n10_wrong_pred2_thm (e e_1 : IntW 8) :
  icmp IntPred.eq (add e_1 e) e ⊑ icmp IntPred.eq e_1 (const? 8 0)

theorem eq_10_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32) →
    ofBool (truncate 8 x_1 == truncate 8 x) &&& ofBool (truncate 8 (x_1 >>> 8#32) == truncate 8 (x >>> 8#32)) =
      ofBool (truncate 16 x_1 == truncate 16 x)

theorem alive_Select_1100  (w : Nat)   : alive_Select_1100_src w  ⊑ alive_Select_1100_tgt w

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

theorem t3_ult_sgt_neg1_thm.extracted_1._6 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 <ᵤ 65536#32) = 1#1 → ofBool (65535#32 <ₛ x_1) = 1#1 → False

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

theorem e_1876 :
     - 2 *  ~~~(a &&& b) + 2 * (c ||| (a &&&  ~~~b)) - 6 * ( ~~~a &&& (b ||| c)) - 1 * ( ~~~a ||| (b &&& c)) - 5 * (b ^^^ (a &&& c)) - 5 * ((a &&& c) ^^^  ~~~(a ^^^ (b &&& c))) + 2 *  ~~~c + 1 * ((a &&& b) ^^^ (b ||| c)) + 7 * (a ||| (b ||| c)) + 4 * (a ^^^ c) - 3 * (c ^^^  ~~~(a &&& ( ~~~b &&& c))) - 7 *  ~~~(a &&&  ~~~c) - 1 * ( ~~~(a ||| b) |||  ~~~(a ^^^ (b ^^^ c))) - 3 *  ~~~(a ||| (b ^^^ c)) - 1 * (c ^^^ ( ~~~a ||| ( ~~~b &&& c))) - 1 *  ~~~(a ^^^ ( ~~~b ||| c)) + 1 * (b ^^^ (a ||| (b ^^^ c))) + 1 *  ~~~(a ||| ( ~~~b &&& c)) + 1 *  ~~~( ~~~a &&& ( ~~~b &&& c)) - 7 * (b ^^^  ~~~(a ||| c)) - 1 * (c ||| (a ^^^ b)) - 2 * ( ~~~c ||| (a ^^^ b)) + 1 * (c ^^^ (a ||| ( ~~~b &&& c))) + 1 * ((a &&& b) ||| (a ^^^ (b ^^^ c))) + 4 * (b ^^^ (a &&& ( ~~~b ||| c))) - 7 * ((a &&&  ~~~b) ||| (b ^^^ c)) + 1 * ((b &&&  ~~~c) ^^^ ( ~~~a ||| (b ^^^ c))) + 11 * ( ~~~(a &&&  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) - 6 * ((a ^^^ b) ||| (a ^^^ c)) - 6 * ((a ^^^ b) |||  ~~~(a ^^^ c)) - 7 *  ~~~(a |||  ~~~b) - 1 * (b ^^^  ~~~(a &&& (b &&& c))) - 3 * ( ~~~(a |||  ~~~b) |||  ~~~(b ^^^ c)) + 5 *  ~~~(a ^^^ c) - 1 * (c &&& (a ||| b)) + 2 * ((a ^^^ b) &&& (a ^^^ c)) + 2 *  ~~~( ~~~a &&& (b ^^^ c)) + 1 * ((a ^^^ b) &&&  ~~~(a ^^^ c)) - 1 * (c ^^^ (a ||| b)) + 15 *  ~~~(a ||| (b ||| c)) + 40 *  ~~~(a ||| ( ~~~b ||| c)) + 1 *  ~~~( ~~~a ||| (b ||| c)) - 5 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 16 * ( ~~~a &&& ( ~~~b &&& c)) + 20 * ( ~~~a &&& (b &&& c)) + 22 * (a &&& ( ~~~b &&& c)) + 6 * (a &&& (b &&& c)) =  - 1 * ((a &&&  ~~~b) ||| (a ^^^ (b ^^^ c))) - 4 * (b ^^^  ~~~(a &&& (b ||| c)))

theorem PR96857_xor_without_noundef_proof : PR96857_xor_without_noundef_before ⊑ PR96857_xor_without_noundef_after

theorem src_srem_shl_demand_max_signbit_proof : src_srem_shl_demand_max_signbit_before ⊑ src_srem_shl_demand_max_signbit_after

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

theorem test20_thm.extracted_1._1 : ∀ (x : BitVec 13), ¬12#13 ≥ ↑13 → ofBool (x.sshiftRight' 12#13 == 123#13) = 0#1

theorem zext_zext_ule_op0_wide_proof : zext_zext_ule_op0_wide_before ⊑ zext_zext_ule_op0_wide_after

theorem testtrunclowhigh_proof : testtrunclowhigh_before ⊑ testtrunclowhigh_after

theorem sdiv_shl_pair_const_thm (e : IntW 32) :
  LLVM.sdiv (shl e (const? 32 2) { «nsw» := true, «nuw» := false })
      (shl e (const? 32 1) { «nsw» := true, «nuw» := false }) ⊑
    const? 32 2

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

theorem fold_sext_to_and_wrong6_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (signExtend 32 x &&& BitVec.ofInt 32 (-2147483647) != -1#32) = 1#1

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

theorem test3_proof : test3_before ⊑ test3_after
</all_available_lemmas>

<local_ctx>
import LeanMLIR.Framework

import Mathlib.Tactic.Linarith

import Mathlib.Tactic.DepRewrite

open Ctxt (Var Valuation Hom)

namespace DCE

structure DeleteRange (Γ : Ctxt Ty) where
   
  start : Fin (Γ.length + 1)
   
  num : Fin (Γ.length + 1 - start.val)

open DCE (DeleteRange)

namespace DeleteRange

def appendInl {Γ : Ctxt Ty} {ts : List Ty}
    (r : DeleteRange Γ) : DeleteRange (⟨ts⟩ ++ Γ) where
  start := ⟨r.start + ts.length, by admit /- proof elided -/
  ⟩
  num := ⟨r.num, by admit /- proof elided -/
  ⟩

section Lemmas

end Lemmas

end DeleteRange

end DCE

open DCE (DeleteRange)

def Ctxt.delete (Γ : Ctxt Ty) (vs : DeleteRange Γ) : Ctxt Ty :=
  Ctxt.ofList <| List.ofFn (n := Γ.length - vs.num.val) fun i =>
    have := vs.start.prop
    if hi : i.val < vs.start then
      Γ[i.val]
    else
      Γ[i.val + vs.num]
</local_ctx>

<target_theorem>
@[simp] theorem Ctxt.delete_append_appendInl {Γ : Ctxt Ty} {us : List Ty}
    {r : DeleteRange Γ} :
    (⟨us⟩ ++ Γ).delete r.appendInl = ⟨us⟩ ++ (Γ.delete r) :=
</target_theorem>

