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
Subtype in Init.Prelude
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 Hom.append {ζ : Ctxt Ty} (f : Γ.Hom Δ) : Hom (ζ ++ Γ) (ζ ++ Δ) :=
  fun _ => Var.appendCases
    (fun v => v.appendInl)
    (fun v => (f v).appendInr)

@[elab_as_elim]
def appendCases
    {motive : (Γ ++ Δ).Var t → Sort u}
    (left : (v : Var Γ t) → motive (appendInl v))
    (right : (v : Var Δ t) → motive (appendInr v)) :
    (v : (Γ ++ Δ).Var t) → motive v
  | ⟨idx, h⟩ =>
    if hv : idx < Γ.length then
      left ⟨idx, by admit /- proof elided -/
      ⟩
    else
      let v' : Var _ _ := ⟨idx - Γ.length, by admit /- proof elided -/
      ⟩
      have eq : v'.appendInr = ⟨idx, h⟩ := by admit /- proof elided -/

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 toHom (d : Diff Γ₁ Γ₂) : Hom Γ₁ Γ₂ :=
  fun _ v => ⟨v.val + d.val, d.property v.property⟩

abbrev Hom (Γ Γ' : Ctxt Ty) := ⦃t : Ty⦄ → Γ.Var t → Γ'.Var t

def Diff (Γ₁ Γ₂ : Ctxt Ty) : Type :=
  {d : Nat // Diff.Valid Γ₁ Γ₂ d}

@[simp]
abbrev Diff.Valid (Γ₁ Γ₂ : Ctxt Ty) (d : Nat) : Prop :=
  ∀ {i t}, Γ₁[i]? = some t → Γ₂[i+d]? = some t

def positive_biggerashr_shlnsw_before := [llvm|
{
^0(%arg50 : i8):
  %0 = llvm.mlir.constant(6 : i8) : i8
  %1 = llvm.mlir.constant(3 : i8) : i8
  %2 = llvm.ashr %arg50, %0 : i8
  %3 = llvm.shl %2, %1 overflow<nsw> : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

def and_two_ranges_to_mask_and_range_after := [llvm|
{
^0(%arg252 : i8):
  %0 = llvm.mlir.constant(-33 : i8) : i8
  %1 = llvm.mlir.constant(-91 : i8) : i8
  %2 = llvm.mlir.constant(-26 : i8) : i8
  %3 = llvm.and %arg252, %0 : i8
  %4 = llvm.add %3, %1 : i8
  %5 = llvm.icmp "ult" %4, %2 : i8
  "llvm.return"(%5) : (i1) -> ()
}
]

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

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

def printPrefix (x : BitStream) : Nat → String
  | 0   => "0b"
  | n+1 =>
    let h := if x.head then "1" else "0"
    let t := x.tail.printPrefix n
    t ++ h

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

def test_sgt_xor_after := [llvm|
{
^0(%arg40 : i32, %arg41 : i32):
  %0 = llvm.xor %arg41, %arg40 : i32
  %1 = llvm.icmp "slt" %0, %arg40 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def test9_after := [llvm|
{
^0(%arg200 : i8):
  %0 = llvm.mlir.constant(89 : i8) : i8
  %1 = llvm.icmp "eq" %arg200, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

Lean.Meta.Context in Lean.Meta.Basic

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

@[nospecialize]
partial def decideIfZerosAuxVerified' {arity : Type _}
    [DecidableEq arity] [Fintype arity] [Hashable arity]
    (iter : Nat) (maxIter : Nat) (startVerifyAtIter : Nat := 0)
    (fsm : FSM arity)
    (circs : KInductionCircuits fsm iter)
    (stats : Array CircuitStats) :
    TermElabM (DecideIfZerosOutput × Array CircuitStats) := do
  withTraceNode `trace.Bits.Fast (fun _ => return s!"K-induction (iter={iter})") do
    if iter ≥ maxIter && maxIter != 0 then
      return (.exhaustedIterations maxIter, stats.push circs.stats)
    let tStart ← IO.monoMsNow
    let cSafety : Circuit (Vars fsm.α arity (iter+2)) := circs.mkSafetyCircuit
    let tEnd ← IO.monoMsNow
    let tElapsedMs := (tEnd - tStart)
    trace[Bits.FastVerif] m!"Built new safety circuit in '{tElapsedMs}ms'"
    trace[Bits.FastVerif] m!"safety circuit size : {cSafety.size}"
    trace[Bits.FastVerif] s!"Building induction circuit..."
    let tStart ← IO.monoMsNow
    let cIndHyp := circs.mkIndHypCycleBreaking
    let tEnd ← IO.monoMsNow
    let tElapsedMs := (tEnd - tStart)
    trace[Bits.FastVerif] m!"Built induction circuit in '{tElapsedMs}ms'"

def dec_sub_before := [llvm|
{
^0(%arg16 : i8, %arg17 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.sub %arg16, %arg17 : i8
  %2 = llvm.add %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

def foo_after := [llvm|
{
^0(%arg2 : i32, %arg3 : i32):
  %0 = llvm.mul %arg2, %arg3 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def negative_not_next_power_of_two_before := [llvm|
{
^0(%arg5 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.mlir.constant(64 : i32) : i32
  %2 = llvm.mlir.constant(256 : i32) : i32
  %3 = llvm.icmp "sgt" %arg5, %0 : i32
  %4 = llvm.add %arg5, %1 : i32
  %5 = llvm.icmp "ult" %4, %2 : i32
  %6 = llvm.and %3, %5 : i1
  "llvm.return"(%6) : (i1) -> ()
}
]

def test29_after := [llvm|
{
^0(%arg173 : i1):
  %0 = llvm.mlir.constant(915 : i32) : i32
  %1 = llvm.mlir.constant(113 : i32) : i32
  %2 = "llvm.select"(%arg173, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def map (f : Ty₁ → Ty₂) : Ctxt Ty₁ → Ctxt Ty₂ :=
  ofList ∘ (List.map f) ∘ toList

def shl_lshr_pow2_not_const_case2_after := [llvm|
{
^0(%arg71 : i16):
  %0 = llvm.mlir.constant(2 : i16) : i16
  %1 = llvm.mlir.constant(0 : i16) : i16
  %2 = llvm.mlir.constant(8 : i16) : i16
  %3 = llvm.icmp "eq" %arg71, %0 : i16
  %4 = "llvm.select"(%3, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i16, i16) -> i16
  "llvm.return"(%4) : (i16) -> ()
}
]

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

def ult_rem_zero_after := [llvm|
{
^0(%arg174 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.icmp "ult" %arg174, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def multiuse2_after := [llvm|
{
^0(%arg10 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(12 : i32) : i32
  %2 = llvm.mlir.constant(48 : i32) : i32
  %3 = llvm.mlir.constant(192 : i32) : i32
  %4 = llvm.mlir.constant(8 : i32) : i32
  %5 = llvm.mlir.constant(32256 : i32) : i32
  %6 = llvm.shl %arg10, %0 : i32
  %7 = llvm.and %6, %1 : i32
  %8 = llvm.shl %arg10, %0 : i32
  %9 = llvm.and %8, %2 : i32
  %10 = llvm.shl %arg10, %0 : i32
  %11 = llvm.and %10, %3 : i32
  %12 = llvm.shl %arg10, %4 : i32
  %13 = llvm.and %12, %5 : i32
  %14 = llvm.or disjoint %11, %9 : i32
  %15 = llvm.or disjoint %7, %14 : i32
  %16 = llvm.or disjoint %13, %15 : i32
  "llvm.return"(%16) : (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 zext_mul_before := [llvm|
{
^0(%arg13 : i8):
  %0 = llvm.mlir.constant(3 : i16) : i16
  %1 = llvm.zext %arg13 : i8 to i16
  %2 = llvm.mul %1, %0 : i16
  %3 = llvm.and %2, %1 : i16
  "llvm.return"(%3) : (i16) -> ()
}
]

instance : Inhabited BVExprWrapper where
  default := {bvExpr := GenBVExpr.const (BitVec.ofNat 0 0), width := 0}

def source : Expr (DC) Γ .pure (.tokenstream) :=
  Expr.mk
    (op := .source)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .nil)
    (regArgs := .nil)

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

def lshr_shl_pow2_const_case1_before := [llvm|
{
^0(%arg60 : i16):
  %0 = llvm.mlir.constant(256 : i16) : i16
  %1 = llvm.mlir.constant(2 : i16) : i16
  %2 = llvm.mlir.constant(8 : i16) : i16
  %3 = llvm.lshr %0, %arg60 : i16
  %4 = llvm.shl %3, %1 : i16
  %5 = llvm.and %4, %2 : i16
  "llvm.return"(%5) : (i16) -> ()
}
]

noncomputable def R.fromTensor {q n} (coeffs : List Int) : R q n :=
  coeffs.zipIdx.foldl (init := 0) fun res (c, i) =>
    res + R.monomial ↑c i

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 or_logic_or_logic_and_5_before := [llvm|
{
^0(%arg36 : i1, %arg37 : i1, %arg38 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.or %arg37, %arg36 : i1
  %3 = "llvm.select"(%arg36, %0, %arg38) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

def sgt_negative_multip_rem_zero_after := [llvm|
{
^0(%arg169 : i8):
  %0 = llvm.mlir.constant(-3 : i8) : i8
  %1 = llvm.icmp "slt" %arg169, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def no_shift_xor_multiuse_cmp_xor_before := [llvm|
{
^0(%arg44 : i32, %arg45 : i32, %arg46 : i32, %arg47 : i32):
  %0 = llvm.mlir.constant(4096 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.and %arg44, %0 : i32
  %3 = llvm.icmp "ne" %1, %2 : i32
  %4 = llvm.xor %arg45, %0 : i32
  %5 = "llvm.select"(%3, %arg45, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %6 = "llvm.select"(%3, %arg46, %arg47) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %7 = llvm.mul %5, %6 : i32
  %8 = llvm.mul %7, %4 : i32
  "llvm.return"(%8) : (i32) -> ()
}
]

Equiv in Mathlib.Logic.Equiv.Defs

def narrow_zext_ashr_keep_trunc3_before := [llvm|
{
^0(%arg4 : i8, %arg5 : i8):
  %0 = llvm.mlir.constant(1) : i64
  %1 = llvm.sext %arg4 : i8 to i64
  %2 = llvm.sext %arg5 : i8 to i64
  %3 = llvm.add %1, %2 overflow<nsw> : i64
  %4 = llvm.ashr %3, %0 : i64
  %5 = llvm.trunc %4 : i64 to i7
  "llvm.return"(%5) : (i7) -> ()
}
]

def mul_add_to_mul_6_before := [llvm|
{
^0(%arg26 : i32, %arg27 : i32):
  %0 = llvm.mlir.constant(5 : i32) : i32
  %1 = llvm.mul %arg26, %arg27 overflow<nsw> : i32
  %2 = llvm.mul %1, %0 overflow<nsw> : i32
  %3 = llvm.add %1, %2 overflow<nsw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def prove_exact_with_high_mask_limit_before := [llvm|
{
^0(%arg6 : i8, %arg7 : i8):
  %0 = llvm.mlir.constant(-32 : i8) : i8
  %1 = llvm.and %arg6, %0 : i8
  %2 = llvm.sdiv %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def sgt_or_not_min_before := [llvm|
{
^0(%arg30 : i8, %arg31 : i8):
  %0 = llvm.mlir.constant(-128 : i8) : i8
  %1 = llvm.icmp "sgt" %arg30, %arg31 : i8
  %2 = llvm.icmp "ne" %arg30, %0 : i8
  %3 = llvm.or %1, %2 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

def fst {Γ : Ctxt _} (a : Var Γ (.stream2 r)) : Expr (Handshake) Γ .pure (.stream r)  :=
  Expr.mk
    (op := .fst r)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons a <| .nil)
    (regArgs := .nil)

def p_after := [llvm|
{
^0(%arg73 : i32, %arg74 : i32, %arg75 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg75, %0 : i32
  %2 = llvm.or %arg73, %1 : i32
  %3 = llvm.or %arg74, %arg75 : i32
  %4 = llvm.and %2, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def test9_after := [llvm|
{
^0(%arg72 : i32):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.trunc %arg72 : i32 to i8
  %2 = llvm.and %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

def test_sdiv_canonicalize_op0_before := [llvm|
{
^0(%arg15 : i32, %arg16 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.sub %0, %arg15 overflow<nsw> : i32
  %2 = llvm.sdiv %1, %arg16 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

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

def a_or_b_const2_after := [llvm|
{
^0(%arg6 : i32, %arg7 : i32, %arg8 : i32, %arg9 : i32):
  %0 = llvm.icmp "eq" %arg6, %arg8 : i32
  %1 = llvm.icmp "eq" %arg7, %arg9 : i32
  %2 = llvm.xor %0, %1 : i1
  "llvm.return"(%2) : (i1) -> ()
}
]

let var := {name := name, width := resultWidth, id := var.id}
      displayNameToShrinkedVar := displayNameToShrinkedVar.insert name var

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

def sub_from_constant_of_sub_from_constant_before := [llvm|
{
^0(%arg170 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(11 : i8) : i8
  %2 = llvm.sub %0, %arg170 : i8
  %3 = llvm.sub %1, %2 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def ashr_ugt_7_before := [llvm|
{
^0(%arg107 : i4):
  %0 = llvm.mlir.constant(1 : i4) : i4
  %1 = llvm.mlir.constant(7 : i4) : i4
  %2 = llvm.ashr %arg107, %0 : i4
  %3 = llvm.icmp "ugt" %2, %1 : i4
  "llvm.return"(%3) : (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 different_size_zext_zext_eq_after := [llvm|
{
^0(%arg22 : i4, %arg23 : i7):
  %0 = llvm.zext %arg22 : i4 to i7
  %1 = llvm.icmp "eq" %arg23, %0 : i7
  "llvm.return"(%1) : (i1) -> ()
}
]

def sle_or_min_logical_after := [llvm|
{
^0(%arg156 : i8, %arg157 : i8):
  %0 = llvm.icmp "sle" %arg156, %arg157 : i8
  "llvm.return"(%0) : (i1) -> ()
}
]

def visitADD_APlusBNegCPlusA : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%a: i64, %b: i64, %c: i64):
      %0 = llvm.add %c, %a : i64
      %1 = llvm.sub %b, %0 : i64
      %2 = llvm.add %a, %1 : i64
      llvm.return %2 : i64
  }]
  rhs := [LV| {
    ^entry (%a: i64, %b: i64, %c: i64):
      %0 = llvm.sub %b, %c : i64
      llvm.return %0 : i64
  }]

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

def xor_icmp_true_signed_commuted_before := [llvm|
{
^0(%arg8 : i32):
  %0 = llvm.mlir.constant(5 : i32) : i32
  %1 = llvm.mlir.constant(6 : i32) : i32
  %2 = llvm.icmp "sgt" %arg8, %0 : i32
  %3 = llvm.icmp "slt" %arg8, %1 : i32
  %4 = llvm.xor %3, %2 : i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

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

def or_xor_or_before := [llvm|
{
^0(%arg156 : i8):
  %0 = llvm.mlir.constant(33 : i8) : i8
  %1 = llvm.mlir.constant(12 : i8) : i8
  %2 = llvm.mlir.constant(7 : i8) : i8
  %3 = llvm.or %arg156, %0 : i8
  %4 = llvm.xor %3, %1 : i8
  %5 = llvm.or %4, %2 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

Lean.Expr.numeral? in Mathlib.Lean.Expr.Basic

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

def test2_before := [llvm|
{
^0(%arg0 : i167):
  %0 = llvm.mlir.constant(9 : i577) : i577
  %1 = llvm.mlir.constant(8 : i577) : i577
  %2 = llvm.zext %arg0 : i167 to i577
  %3 = llvm.lshr %2, %0 : i577
  %4 = llvm.shl %2, %1 : i577
  %5 = llvm.or %3, %4 : i577
  %6 = llvm.trunc %5 : i577 to i167
  "llvm.return"(%6) : (i167) -> ()
}
]

def neg_not_signbit3_after := [llvm|
{
^0(%arg3 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.ashr %arg3, %0 : i8
  %3 = llvm.zext %2 : i8 to i32
  %4 = llvm.sub %1, %3 overflow<nsw> : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def sext_diff_i1_xor_sub_1_after := [llvm|
{
^0(%arg12 : i64, %arg13 : i1, %arg14 : i1):
  %0 = llvm.sext %arg13 : i1 to i64
  %1 = llvm.zext %arg14 : i1 to i64
  %2 = llvm.add %1, %0 overflow<nsw> : i64
  "llvm.return"(%2) : (i64) -> ()
}
]

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

def and_or_not_not_before := [llvm|
{
^0(%arg375 : i32, %arg376 : i32, %arg377 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg376, %arg375 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.and %arg375, %arg377 : i32
  %4 = llvm.xor %3, %0 : i32
  %5 = llvm.or %4, %arg376 : i32
  %6 = llvm.and %5, %2 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

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

def masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_3_logical_after := [llvm|
{
^0(%arg21 : i32):
  %0 = llvm.mlir.constant(15 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.and %arg21, %0 : i32
  %3 = llvm.icmp "ne" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def select_xor_icmp_bad_3_after := [llvm|
{
^0(%arg179 : i32, %arg180 : i32, %arg181 : i32):
  %0 = llvm.mlir.constant(3 : i32) : i32
  %1 = llvm.icmp "eq" %arg179, %0 : i32
  %2 = llvm.xor %arg181, %0 : i32
  %3 = "llvm.select"(%1, %2, %arg180) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def test65_after := [llvm|
{
^0(%arg43 : i64):
  %0 = llvm.mlir.constant(16) : i64
  %1 = llvm.mlir.constant(0) : i64
  %2 = llvm.mlir.constant(42 : i32) : i32
  %3 = llvm.mlir.constant(40 : i32) : i32
  %4 = llvm.and %arg43, %0 : i64
  %5 = llvm.icmp "eq" %4, %1 : i64
  %6 = "llvm.select"(%5, %2, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%6) : (i32) -> ()
}
]

@[simp_denote]
def shl_llvm_16 := [LV| {
  ^entry (%x: i16, %y: i16):
    %1 = llvm.shl %x, %y : i16
    llvm.return %1 : i16
  }]

structure Item where
 name : String
 tac : Syntax

def negate_sext_after := [llvm|
{
^0(%arg98 : i8, %arg99 : i1):
  %0 = llvm.zext %arg99 : i1 to i8
  %1 = llvm.add %arg98, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

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

def slt_zero_sgt_minus1_after := [llvm|
{
^0(%arg22 : i4, %arg23 : i4):
  %0 = llvm.mlir.constant(-1 : i4) : i4
  %1 = llvm.xor %arg22, %arg23 : i4
  %2 = llvm.icmp "sgt" %1, %0 : i4
  "llvm.return"(%2) : (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 val_lt (v : Γ.Var t) : v.val < Γ.length

@[simp, grind=] theorem castCtxt_rfl (h : Γ = Γ) : v.castCtxt h = v

@[simp, grind=] theorem val_castCtxt : (castCtxt h v).val = v.val

theorem icmp_select_implied_cond_ne_proof : icmp_select_implied_cond_ne_before ⊑ icmp_select_implied_cond_ne_after

theorem shl_trunc_bigger_lshr_thm (e : IntW 32) :
  shl (trunc 8 (lshr e (const? 32 5))) (const? 8 3) ⊑ LLVM.and (trunc 8 (lshr e (const? 32 2))) (const? 8 (-8))

theorem substitute_constant_or_ne_swap_sle_proof : substitute_constant_or_ne_swap_sle_before ⊑ substitute_constant_or_ne_swap_sle_after

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

theorem n6_thm.extracted_1._3 : ∀ (x : BitVec 32),
  ¬ofBool (x &&& 1#32 != 0#32) = 1#1 → ¬ofBool (x &&& 1#32 == 0#32) = 1#1 → ¬2#32 ≥ ↑32 → 1#32 = x >>> 2#32 &&& 1#32

theorem not_invert_signbit_splat_mask1_thm.extracted_1._1 : ∀ (x : BitVec 16) (x_1 : BitVec 8),
  ¬7#8 ≥ ↑8 →
    zeroExtend 16 (x_1.sshiftRight' 7#8 ^^^ -1#8) &&& x = x &&& zeroExtend 16 (signExtend 8 (ofBool (-1#8 <ₛ x_1)))

theorem e_880 :
     - 1 *  ~~~z - 5 * (z |||  ~~~t) + 1 * z + 6 *  ~~~(z ||| t) + 1 *  ~~~(z |||  ~~~t) + 4 * (z &&& t) =  - 4 * (z &&&  ~~~t)

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

theorem test_const_shr_exact_and_1_ne_0_proof : test_const_shr_exact_and_1_ne_0_before ⊑ test_const_shr_exact_and_1_ne_0_after

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

theorem main7d_logical_thm.extracted_1._12 : ∀ (x x_1 x_2 x_3 x_4 : BitVec 32),
  ofBool (x_4 &&& (x_3 &&& x_2) == x_3 &&& x_2) = 1#1 →
    ¬ofBool (x_4 &&& (x_3 &&& x_2) != x_3 &&& x_2) = 1#1 →
      ¬ofBool (x_4 &&& (x_1 &&& x) == x_1 &&& x) = 1#1 →
        1#32 = zeroExtend 32 (ofBool (x_4 &&& (x_1 &&& x) != x_1 &&& x))

theorem urem_i1_is_zero_proof : urem_i1_is_zero_before ⊑ urem_i1_is_zero_after

theorem ashr_lshr_shift_base_mismatch_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (0#32 ≤ₛ x_1) = 1#1 → ¬x ≥ ↑32 → ofBool (x_1 <ₛ 0#32) = 1#1 ∨ x ≥ ↑32 → False

theorem negative_not_next_power_of_two_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (-1#32 <ₛ x) &&& ofBool (x + 64#32 <ᵤ 256#32) = ofBool (x <ᵤ 192#32)

theorem eval_eq_outputWith_carryWith (p : FSM arity) :
  p.eval x n =
  p.outputWith (p.carryWith p.initCarry x n) (fun a => x a n)

theorem e_1361 :
    4 *  ~~~z + 2 * t + 1 *  ~~~(z &&&  ~~~z) - 3 *  ~~~(z ^^^ t) + 2 *  ~~~(z &&&  ~~~t) + 7 *  ~~~(z &&& t) + 4 *  ~~~t + 5 * (z ^^^ t) - 21 *  ~~~(z |||  ~~~t) - 17 * (z &&&  ~~~t) = 2 * (z &&& t) + 15 *  ~~~(z ||| t)

theorem sext_diff_i1_xor_sub_1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1),
  ¬(True ∧ (zeroExtend 64 x).saddOverflow (signExtend 64 x_1) = true) →
    signExtend 64 x_1 - signExtend 64 x = zeroExtend 64 x + signExtend 64 x_1

theorem e_1193 :
     - 6 *  ~~~(z &&&  ~~~z) - 7 * z - 3 * (z ^^^ t) - 6 *  ~~~z + 13 *  ~~~(z ||| t) + 15 *  ~~~(z |||  ~~~t) + 17 * (z &&&  ~~~t) + 14 * (z &&& t) = 1 * (z |||  ~~~t)

theorem test16_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ((x_1 ^^^ 33#8 ^^^ x) &&& (x ^^^ x_1)) * (x_1 ^^^ 33#8 ^^^ x) =
    ((x_1 ^^^ x ^^^ 33#8) &&& (x ^^^ x_1)) * (x_1 ^^^ x ^^^ 33#8)

@[simp]
theorem none_left :
  Refinement none x?

theorem test_invert_demorgan_or3_proof : test_invert_demorgan_or3_before ⊑ test_invert_demorgan_or3_after

theorem squared_nsw_sgt0_thm.extracted_1._1 : ∀ (x : BitVec 5),
  ¬(True ∧ x.smulOverflow x = true) → ofBool (0#5 <ₛ x * x) = ofBool (x != 0#5)

theorem test_logical_proof : test_logical_before ⊑ test_logical_after

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

theorem in_constant_mone_vary_proof : in_constant_mone_vary_before ⊑ in_constant_mone_vary_after

theorem smear_sign_and_widen_proof : smear_sign_and_widen_before ⊑ smear_sign_and_widen_after

theorem mul_constant_eq_nsw_thm (e e_1 : IntW 32) :
  icmp IntPred.eq (mul e_1 (const? 32 6) { «nsw» := true, «nuw» := false })
      (mul e (const? 32 6) { «nsw» := true, «nuw» := false }) ⊑
    icmp IntPred.eq e_1 e

theorem prop_eq (w : Nat) (x y: BitVec w) :
  let wenv

@[grind =, simp]
lemma RawCNFA.same_stateMax (m : RawCNFA A) x y (z : Std.HashMap (State × A) (Std.HashSet State)) :
    (RawCNFA.mk m.stateMax x y z).states = m.states

theorem e_232 :
    5 *  ~~~(x ^^^ y) + 2 *  ~~~(x &&&  ~~~y) + 5 * (x |||  ~~~y) - 2 *  ~~~(x &&&  ~~~x) - 10 *  ~~~(x ||| y) - 14 * (x &&&  ~~~y) - 10 * (x &&& y) =  - 11 * (x ^^^ y) + 11 *  ~~~(x |||  ~~~y)

theorem icmp_shl_nsw_sge0_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(True ∧ (x <<< 21#32).sshiftRight' 21#32 ≠ x ∨ 21#32 ≥ ↑32) → ofBool (0#32 ≤ₛ x <<< 21#32) = ofBool (-1#32 <ₛ x)

theorem positive_biggerlshr_proof : positive_biggerlshr_before ⊑ positive_biggerlshr_after

theorem e_1883 :
     - 11 * (b &&& (a |||  ~~~c)) - 2 * (b ^^^  ~~~( ~~~a &&& (b ||| c))) - 1 * ((b &&& c) ^^^  ~~~(a &&& (b ^^^ c))) - 1 * ( ~~~(a ^^^ b) |||  ~~~(a ^^^ c)) + 1 * (a ||| (b &&& c)) + 3 * (b |||  ~~~(a ^^^ c)) + 11 * (a ^^^ (b ^^^ c)) - 6 *  ~~~(a ^^^ b) + 3 * (b ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) + 4 * (b ^^^  ~~~(a &&& c)) - 2 * (b ^^^  ~~~(a ||| ( ~~~b &&& c))) + 1 * (c ^^^  ~~~(a &&& ( ~~~b &&& c))) - 2 *  ~~~(a ^^^ ( ~~~b ||| c)) - 2 *  ~~~(a &&&  ~~~c) - 1 * (a ||| b) - 1 * (b ^^^ ( ~~~a &&& (b ^^^ c))) + 11 * ( ~~~(a &&& b) &&& (b ^^^ c)) - 2 * (a ^^^ (b &&& c)) + 3 * ((a &&& b) ||| (b ^^^ c)) - 1 * (c ^^^ ( ~~~a &&& ( ~~~b ||| c))) - 1 * (a ^^^ ( ~~~b &&& c)) + 2 *  ~~~(a ||| (b ^^^ c)) - 1 * ((a &&&  ~~~b) |||  ~~~(a ^^^ (b ^^^ c))) - 1 *  ~~~(a ||| c) - 1 *  ~~~b - 1 * ( ~~~c &&&  ~~~(a ^^^ b)) - 3 * (c ^^^  ~~~(a &&& (b &&& c))) + 1 * (c ^^^ ( ~~~a ||| (b &&& c))) - 2 * (c ^^^ (a ||| b)) - 11 * (b ^^^  ~~~( ~~~a ||| (b ^^^ c))) + 7 *  ~~~(a &&&  ~~~b) + 1 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) + 1 * (c &&& (a |||  ~~~b)) + 4 *  ~~~(a &&& b) - 7 * (b ^^^  ~~~(a ||| (b ^^^ c))) - 2 * ( ~~~b &&&  ~~~(a ^^^ c)) + 2 * (b ^^^ c) - 3 * (c ^^^  ~~~(a &&& b)) + 11 * ((b &&&  ~~~c) ^^^ (a ||| (b ^^^ c))) - 11 * (a &&& c) + 8 *  ~~~(a ||| (b ||| c)) + 4 *  ~~~(a ||| ( ~~~b ||| c)) - 3 *  ~~~( ~~~a ||| (b ||| c)) + 22 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 40 * ( ~~~a &&& ( ~~~b &&& c)) + 5 * ( ~~~a &&& (b &&& c)) - 13 * (a &&& ( ~~~b &&& c)) - 1 * (a &&& (b &&& c)) =  - 11 * (a &&& b) + 2 * (b ^^^  ~~~( ~~~a &&& ( ~~~b ||| c)))

theorem masked_icmps_mask_notallzeros_bmask_mixed_7b_proof : masked_icmps_mask_notallzeros_bmask_mixed_7b_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_7b_after

theorem srem_constant_dividend_select_of_constants_divisor_proof : srem_constant_dividend_select_of_constants_divisor_before ⊑ srem_constant_dividend_select_of_constants_divisor_after

theorem splat_mul_unknown_lz_proof : splat_mul_unknown_lz_before ⊑ splat_mul_unknown_lz_after

theorem sgt_and_min_commute_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 == BitVec.ofInt 8 (-128)) = 1#1 → ofBool (x <ₛ x_1) = 0#1

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

theorem setWidth_eq_zext (x : BitVec v) : x.zeroExtend w = x.setWidth w

theorem lshr_and_add_thm (e e_1 : IntW 8) :
  shl (add (LLVM.srem e_1 (const? 8 42)) (LLVM.and (lshr e (const? 8 3)) (const? 8 12))) (const? 8 3) ⊑
    add (LLVM.and e (const? 8 96)) (shl (LLVM.srem e_1 (const? 8 42)) (const? 8 3))

theorem add_const_sub_const_thm.extracted_1._1 : ∀ (x : BitVec 32), x + 8#32 - 2#32 = x + 6#32

theorem test_ashr_exact__exact_is_safe_thm (e : IntW 64) (e_1 : IntW 32) :
  select (icmp IntPred.eq (LLVM.and e_1 (const? 32 (-2147483588))) (const? 32 0)) e
      (ashr e (zext 64 (ashr (LLVM.and e_1 (const? 32 (-2147483588))) (const? 32 2) { «exact» := true }))) ⊑
    ashr e (zext 64 (LLVM.and (ashr e_1 (const? 32 2)) (const? 32 (-536870897))) { «nneg» := true })

theorem udiv_common_divisor_defined_cond_thm.extracted_1._2 : ∀ (x x_1 : BitVec 5) (x_2 : BitVec 1),
  ¬(x_2 = 1#1 ∨ x_1 = 0) → x_2 = 1#1 → ¬x_1 = 0 → False

theorem test48_thm (e : IntW 8) :
  zext 64 (LLVM.or (shl (zext 32 e) (const? 32 8)) (zext 32 e)) ⊑
    zext 64
      (LLVM.or (shl (zext 32 e) (const? 32 8) { «nsw» := true, «nuw» := true }) (zext 32 e) { «disjoint» := true })
      { «nneg» := true }

theorem add_nuw_const_const_sub_nuw_thm (e : IntW 8) :
  sub (const? 8 (-127)) (add e (const? 8 1) { «nsw» := false, «nuw» := true }) { «nsw» := false, «nuw» := true } ⊑
    sub (const? 8 (-128)) e { «nsw» := false, «nuw» := true }

theorem not_logicalOr_not_op1_thm.extracted_1._5 : ∀ (x x_1 : BitVec 1),
  ¬x_1 = 1#1 → x_1 ^^^ 1#1 = 1#1 → x ^^^ 1#1 ^^^ 1#1 = x

theorem and_logic_and_logic_or_7_proof : and_logic_and_logic_or_7_before ⊑ and_logic_and_logic_or_7_after

theorem test_add_nuw__all_are_safe_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x &&& 1073741823#32 == 3#32) = 1#1 →
    ¬(True ∧ (x &&& 1073741823#32).saddOverflow 1#32 = true ∨ True ∧ (x &&& 1073741823#32).uaddOverflow 1#32 = true) →
      4#32 = (x &&& 1073741823#32) + 1#32

theorem test3_thm.extracted_1._1 : ∀ (x : BitVec 32), ofBool (x <ₛ x) = 0#1

theorem p0_proof : p0_before ⊑ p0_after

theorem t6_no_extrause_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), ofBool (x_1 + x <ᵤ x) = ofBool (x ^^^ -1#8 <ᵤ x_1)

theorem sub_shl_same_amount_nuw_proof : sub_shl_same_amount_nuw_before ⊑ sub_shl_same_amount_nuw_after

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

theorem n2_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬x_1 ≥ ↑8 →
    ¬(True ∧ ((-1#8) <<< x_1).sshiftRight' x_1 ≠ -1#8 ∨ x_1 ≥ ↑8) →
      ofBool (((-1#8) <<< x_1 ^^^ 1#8) &&& x != x) = ofBool (x &&& ((-1#8) <<< x_1 ^^^ BitVec.ofInt 8 (-2)) != 0#8)

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 e_1257 :
     - 11 * (z ||| t) - 1 *  ~~~t - 3 *  ~~~(z &&&  ~~~z) + 11 * (z ^^^ t) + 5 * t - 2 *  ~~~(z &&& t) + 5 *  ~~~(z ||| t) + 13 * (z &&&  ~~~t) + 15 * (z &&& t) =  - 1 *  ~~~(z ^^^ t) + 7 * z

@[simp] theorem hasType_push_of_neq {Γ : Context Ty} (h : w ≠ v) :
    (Γ.push v ty).hasType w ty' ↔ Γ.hasType w ty'

theorem icmp_shl_ne_2_proof : icmp_shl_ne_2_before ⊑ icmp_shl_ne_2_after

theorem add_eq_sll (a : Nat) : a + a = a <<< 1

theorem no_shift_xor_multiuse_cmp_with_xor_proof : no_shift_xor_multiuse_cmp_with_xor_before ⊑ no_shift_xor_multiuse_cmp_with_xor_after

theorem select_1_proof : select_1_before ⊑ select_1_after

theorem fixed (x : BitVec 4) (y : BitVec 7) : 
    (BitVec.signExtend 32 x < BitVec.signExtend 32 y) ↔ (BitVec.signExtend 7 x < y)

theorem or_xor_tree_0011_thm (e e_1 e_2 : IntW 32) :
  LLVM.or (LLVM.xor (mul e_2 (const? 32 42)) (mul e_1 (const? 32 42)))
      (LLVM.xor (LLVM.xor (mul e (const? 32 42)) (mul e_2 (const? 32 42))) (mul e_1 (const? 32 42))) ⊑
    LLVM.or (LLVM.xor (mul e_2 (const? 32 42)) (mul e_1 (const? 32 42))) (mul e (const? 32 42))

theorem shl_add_proof : shl_add_before ⊑ shl_add_after

theorem test9_proof : test9_before ⊑ test9_after

theorem test7_proof : test7_before ⊑ test7_after

theorem p0_proof : p0_before ⊑ p0_after

@[simp]
lemma neg_accepts (M : NFA' n) :
    M.neg.accepts = M.acceptsᶜ

theorem invert_both_cmp_operands_complex_proof : invert_both_cmp_operands_complex_before ⊑ invert_both_cmp_operands_complex_after

theorem lshr_lshr_pow2_const_negative_nopow2_2_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬(x ≥ ↑16 ∨ 6#16 ≥ ↑16) → x ≥ ↑16 → False

theorem absdiff_proof : absdiff_before ⊑ absdiff_after

theorem eq_umax1_proof : eq_umax1_before ⊑ eq_umax1_after

theorem scalar_i8_lshr_and_negC_eq_not_negatedPowerOf2_thm (e e_1 : IntW 8) :
  icmp IntPred.eq (LLVM.and (lshr e_1 e) (const? 8 (-3))) (const? 8 0) ⊑
    icmp IntPred.eq (LLVM.and e_1 (shl (const? 8 (-3)) e)) (const? 8 0)

theorem e_1936 :
     - 1 * (c ^^^ ( ~~~a ||| (b &&& c))) + 2 * ((a &&& b) ^^^ (b |||  ~~~c)) + 5 * (b ^^^  ~~~( ~~~a &&& (b &&& c))) - 1 * ((b &&&  ~~~c) ^^^ ( ~~~a ||| (b ^^^ c))) + 2 * (b ^^^ (a &&& ( ~~~b ||| c))) - 5 * ( ~~~b ||| (a ^^^ c)) - 11 * (b ^^^  ~~~(a &&& (b ||| c))) + 5 * (b ^^^ (a &&& (b ||| c))) - 6 *  ~~~(a &&& c) + 4 * (c &&&  ~~~(a ^^^ b)) + 3 * (c ^^^ ( ~~~a &&& (b ||| c))) + 1 * c - 1 * ((a &&& b) |||  ~~~(b |||  ~~~c)) - 11 * (b ^^^  ~~~(a &&&  ~~~c)) + 7 *  ~~~a - 1 * ( ~~~a ||| (b ||| c)) + 11 * (a &&& c) - 7 * (b &&&  ~~~(a ^^^ c)) + 4 *  ~~~(a &&& (b ^^^ c)) - 7 * (c &&& (a ^^^ b)) + 3 * ( ~~~c &&&  ~~~(a ^^^ b)) + 11 * (c ^^^  ~~~(a &&& (b ||| c))) + 5 * ((a |||  ~~~b) &&& (a ^^^ (b ^^^ c))) - 3 * (a ^^^ (b ||| c)) + 11 * (c ^^^  ~~~( ~~~a &&& ( ~~~b ||| c))) - 2 * (a ^^^ (b &&& c)) - 1 * ( ~~~(a |||  ~~~b) |||  ~~~(a ^^^ (b ^^^ c))) - 2 * ((a &&& c) ||| (b &&&  ~~~c)) + 5 * (b ^^^  ~~~( ~~~a ||| (b ^^^ c))) + 4 * ( ~~~(a |||  ~~~b) |||  ~~~(b ^^^ c)) + 5 * (b ^^^ (a |||  ~~~c)) - 2 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) + 2 * ((a &&& b) ||| (b ^^^ c)) + 4 * ( ~~~c |||  ~~~(a ^^^ b)) - 6 * ((a ^^^ b) ||| (a ^^^ c)) - 3 * (a ^^^ ( ~~~b ||| c)) + 1 * (c ^^^  ~~~(a &&&  ~~~b)) - 1 * ((a &&& c) ^^^  ~~~(b &&&  ~~~c)) + 11 * (c ^^^  ~~~( ~~~a &&& (b ||| c))) + 1 *  ~~~(b |||  ~~~c) - 7 * (c ^^^ ( ~~~a ||| ( ~~~b &&& c))) + 5 *  ~~~(a ||| ( ~~~b &&& c)) - 11 *  ~~~(a &&&  ~~~a) + 1 *  ~~~(a ^^^ ( ~~~b ||| c)) + 3 * (b ^^^  ~~~(a ||| ( ~~~b &&& c))) + 4 * (b &&& (a ||| c)) - 4 *  ~~~(a ||| (b ||| c)) - 22 *  ~~~(a ||| ( ~~~b ||| c)) + 14 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 7 * ( ~~~a &&& ( ~~~b &&& c)) + 1 * (a &&& ( ~~~b &&& c)) - 15 * (a &&& (b &&& c)) = 25 *  ~~~( ~~~a ||| (b ||| c)) + 24 * ( ~~~a &&& (b &&& c))

theorem basic_preserve_nuw_nsw_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬(True ∧ (x_1 ^^^ -1#8).saddOverflow x = true ∨ True ∧ (x_1 ^^^ -1#8).uaddOverflow x = true) →
    True ∧ x_1.ssubOverflow x = true ∨ True ∧ x_1.usubOverflow x = true → False

theorem lsb_mask_sign_zext_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_zext_different_condition_thm.extracted_1._1 : ∀ (x x_1 : BitVec 1),
  x_1 = 1#1 →
    True ∧ (64#64).saddOverflow (zeroExtend 64 x) = true ∨ True ∧ (64#64).uaddOverflow (zeroExtend 64 x) = true →
      False

theorem ashr_lshr_no_ashr_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (0#32 ≤ₛ x_1) = 1#1 → ¬ofBool (x_1 <ₛ 0#32) = 1#1 → x ≥ ↑32 → False

theorem multiuse_lshr_lshr_proof : multiuse_lshr_lshr_before ⊑ multiuse_lshr_lshr_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]

section Lemmas

variable {Γ : Ctxt Ty}

end Lemmas

def Hom.delete {Γ : Ctxt Ty} (delv : DeleteRange Γ) : Hom (Γ.delete delv) Γ :=
  fun t' v =>
    let idx :=
      if v.val < delv.start then
        v.val
      else
        v.val + delv.num
    ⟨idx, by admit /- proof elided -/
    ⟩

def Deleted (Γ: Ctxt Ty) (vs : DeleteRange Γ) (Γ' : Ctxt Ty) : Prop :=
  Γ' = Γ.delete vs

def Deleted.toHom (h : Deleted Γ r Γ') : Γ'.Hom Γ :=
  fun _ v => Hom.delete r (v.castCtxt h)
</local_ctx>

<target_theorem>
@[simp] lemma Deleted.toHom_append {Γ Γ' : Ctxt Ty} {vs : DeleteRange Γ}
    (DEL : Deleted (⟨us⟩ ++ Γ) vs.appendInl (⟨us⟩ ++ Γ')) :
    DEL.toHom
    = have DEL' : Deleted Γ vs Γ' :=
</target_theorem>

