You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
Inhabited in Init.Prelude
Lean.ToExpr in Lean.ToExpr
Nat in Init.Prelude
Repr in Init.Data.Repr
Bool in Init.Prelude
Int.xor in Mathlib.Data.Int.Bitwise
BitVec in Init.Prelude
BitVec.adcb in Init.Data.BitVec.Bitblast
Prod in Init.Prelude
Fin in Init.Prelude
Fin.last in Init.Data.Fin.Basic
List in Init.Prelude
List.Vector in Mathlib.Data.Vector.Defs
BitVec.ofNat in Init.Prelude
BitVec.zero in Init.Data.BitVec.Basic
Fin.castLE in Init.Data.Fin.Basic
Set in Mathlib.Data.Set.Defs
Eq in Init.Prelude
Fin.natAdd in Init.Data.Fin.Basic
List.Vector.nil in Mathlib.Data.Vector.Defs
NeZero in Init.Data.NeZero
BitVec.iunfoldr in Init.Data.BitVec.Folds
Vector in Init.Data.Vector.Basic
Vector.ofFn in Init.Data.Vector.Basic

syntax "xor" : MLIR.Pretty.uniform_op

syntax "max" : MLIR.Pretty.uniform_op

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

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

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

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

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

| shiftL : Term → Nat → Term

deriving Repr, Inhabited, Lean.ToExpr

def sub (x y : BitStream) : BitStream :=
  fun n => (subAux x y n).1

def subAux (x y : BitStream) : Nat → Bool × Bool
  | 0 => (xor (x 0) (y 0), !(x 0) && y 0)
  | n+1 =>
    let borrow := (subAux x y n).2
    let a := x (n + 1)
    let b := y (n + 1)
    (xor a (xor b borrow), !a && b || ((!(xor a b)) && borrow))

def BitStream : Type := Nat → Bool

def add (x y : BitStream) : BitStream :=
  fun n => (addAux x y n).1

def addAux (x y : BitStream) (i : Nat) :  Bool × Bool :=
  let carryIn : Bool := match i with
    | 0 => false
    | i + 1 => (addAux x y i).2
  Prod.swap (BitVec.adcb (x i) (y i) carryIn)

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

def negAux (x : BitStream) : Nat → Bool × Bool
  | 0 => (x 0, !(x 0))
  | n+1 =>
    let borrow := (negAux x n).2
    let a := x (n + 1)
    (xor (!a) borrow, !a && borrow)

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 }

def Valuation.cons {Γ : Ctxt Ty} {t : Ty} (x : toType t) (V : Γ.Valuation) :
    (Γ.cons t).Valuation :=

def Term.language (t : Term) : Set (BitVecs (t.arity + 1)) :=
  { bvs : BitVecs (t.arity + 1) | t.evalFinBV (fun n => bvs.bvs.get n) = bvs.bvs.get t.arity }

@[simp]
def Formula.arity : Formula → Nat
| width _ _ => 0
| atom _ t1 t2 => max t1.arity t2.arity
| msbSet t => t.arity
| unop _ φ => φ.arity
| binop _ φ1 φ2 => max φ1.arity φ2.arity

@[simp] def Term.evalFinBV (t : Term) (vars : Fin (arity t) → BitVec w) : BitVec w :=
  match t with
  | .var n => vars (Fin.last n)
  | .zero    => BitVec.zero w
  | .one     => 1
  | .negOne  => -1
  | .ofNat n => BitVec.ofNat _ n
  | .and t₁ t₂ =>
      let x₁ := t₁.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ &&& x₂
  | .or t₁ t₂ =>
      let x₁ := t₁.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ ||| x₂
  | .xor t₁ t₂ =>
      let x₁ := t₁.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ ^^^ x₂
  | .not t     => ~~~(t.evalFinBV vars)
  
  | .add t₁ t₂ =>
      let x₁ := t₁.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ + x₂
  | .sub t₁ t₂ =>
      let x₁ := t₁.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      let x₂ := t₂.evalFinBV (fun i => vars (Fin.castLE (by admit /- proof elided -/
      ) i))
      x₁ - x₂
  | .neg t       => -(t.evalFinBV vars)
  | .shiftL a n => (a.evalFinBV vars) <<< n

@[simp] def Term.arity : Term → Nat
| (var n) => n+1
| zero => 0
| one => 0
| negOne => 0
| ofNat _ => 0
| Term.and t₁ t₂ => max (arity t₁) (arity t₂)
| Term.or t₁ t₂ => max (arity t₁) (arity t₂)
| Term.xor t₁ t₂ => max (arity t₁) (arity t₂)
| Term.not t => arity t
| add t₁ t₂ => max (arity t₁) (arity t₂)
| sub t₁ t₂ => max (arity t₁) (arity t₂)
| neg t => arity t

| shiftL t .. => arity t

def BitVec.transport (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2 :=
  BitVec.ofFn fun i => bv.getLsbD (f i)

def BitVec.ofFn {w : Nat} (f : Fin w → Bool) : BitVec w :=
  BitVec.iunfoldr (fun i _ => ((), f i)) () |>.2

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

def BitVecs'.transport (f : Fin n → Fin m) (bvs' : BitVecs' m): BitVecs' n :=
  bvs'.map fun bv => bv.transport f

def BitVecs.transport (f : Fin n → Fin m) (bvs : BitVecs m) : BitVecs n :=
  { w := bvs.w, bvs := bvs.bvs.transport f }

infixr:67 "::ᵥ" => Valuation.cons

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 main4f_like_logical_after := [llvm|
{
^0(%arg115 : i32, %arg116 : i32, %arg117 : i32):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.and %arg115, %arg116 : i32
  %2 = llvm.icmp "eq" %1, %arg116 : i32
  %3 = llvm.and %arg115, %arg117 : i32
  %4 = llvm.icmp "eq" %3, %arg117 : i32
  %5 = "llvm.select"(%2, %4, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %6 = llvm.zext %5 : i1 to i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def icmp_slt_0_and_icmp_ne_neg2_i32_fail_before := [llvm|
{
^0(%arg44 : i32):
  %0 = llvm.mlir.constant(-2 : i32) : i32
  %1 = llvm.mlir.constant(31 : i32) : i32
  %2 = llvm.icmp "ne" %arg44, %0 : i32
  %3 = llvm.zext %2 : i1 to i32
  %4 = llvm.lshr %arg44, %1 : i32
  %5 = llvm.and %4, %3 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

instance : Refinement (BitVec w) := .ofEq

def pr33078_2_after := [llvm|
{
^0(%arg4 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.ashr %arg4, %0 : i8
  %2 = llvm.sext %1 : i8 to i12
  "llvm.return"(%2) : (i12) -> ()
}
]

@[simp_denote]
def add_b31_test : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := add_b31_llvm_i64
  rhs := add_b31_riscv_i64

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

def sdiv_common_divisor_defined_cond_before := [llvm|
{
^0(%arg41 : i1, %arg42 : i5, %arg43 : i5, %arg44 : i5):
  %0 = llvm.sdiv %arg43, %arg42 : i5
  %1 = llvm.sdiv %arg44, %arg42 : i5
  %2 = "llvm.select"(%arg41, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i5, i5) -> i5
  "llvm.return"(%2) : (i5) -> ()
}
]

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

def xor_or_xor_common_op_commute1_after := [llvm|
{
^0(%arg80 : i32, %arg81 : i32, %arg82 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg80, %0 : i32
  %2 = llvm.and %arg81, %1 : i32
  %3 = llvm.xor %2, %arg82 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def shl_mul_mask_wrong_mul_const_after := [llvm|
{
^0(%arg0 : i32):
  %0 = llvm.mlir.constant(255 : i32) : i32
  %1 = llvm.mlir.constant(65535 : i32) : i32
  %2 = llvm.mlir.constant(8 : i32) : i32
  %3 = llvm.and %arg0, %0 : i32
  %4 = llvm.mul %3, %1 overflow<nsw,nuw> : i32
  %5 = llvm.shl %3, %2 overflow<nsw,nuw> : i32
  %6 = llvm.or %4, %5 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

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

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

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

BitVec.allOnes in Init.Data.BitVec.Basic

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

RV64.sexth in RISCV.Instructions

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

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

def or_min_31_30_after := [llvm|
{
^0(%arg3 : i8):
  %0 = llvm.mlir.constant(31 : i8) : i8
  %1 = llvm.or %arg3, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def NFA'.autMsbSet : NFA' 1 := ⟨_, NFA.autMsbSet⟩

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

def visitADD_Sameop : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 1)] where
  lhs := [LV| {
    ^entry (%x: i1):
      %c = llvm.mlir.constant (1) : i64
      %0 = llvm.sext %x : i1 to i64
      %1 = llvm.add %0, %c : i64
      llvm.return %1 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i1):
      %0 = llvm.not %x : i1
      %1 = llvm.zext %0 : i1 to i64
      llvm.return %1 : i64
  }]

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

def select_xor_icmp_bad_5_after := [llvm|
{
^0(%arg172 : i32, %arg173 : i32, %arg174 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "eq" %arg172, %0 : i32
  %2 = llvm.xor %arg172, %arg174 : i32
  %3 = "llvm.select"(%1, %arg173, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%3) : (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) -> ()
}
]

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

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 -/
    ⟩

instance : ToString DCOp.TokenStream where
  toString s := toString (Stream.toList 10 s)

def mul_add_to_mul_1_before := [llvm|
{
^0(%arg32 : i16):
  %0 = llvm.mlir.constant(8 : i16) : i16
  %1 = llvm.mul %arg32, %0 overflow<nsw> : i16
  %2 = llvm.add %arg32, %1 overflow<nsw> : i16
  "llvm.return"(%2) : (i16) -> ()
}
]

def llvm_const_lower_riscv_li_49 : LLVMPeepholeRewriteRefine 64 [] :=
  {lhs := constLLVM_49, rhs:= liRiscv_49,
   correct := by admit /- proof elided -/

def test24_after := [llvm|
{
^0(%arg273 : i32):
  %0 = llvm.mlir.constant(2 : i32) : i32
  %1 = llvm.icmp "sgt" %arg273, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def commutativity_constant_14_vary_after := [llvm|
{
^0(%arg12 : i4, %arg13 : i4):
  %0 = llvm.mlir.constant(-2 : i4) : i4
  %1 = llvm.and %arg12, %0 : i4
  "llvm.return"(%1) : (i4) -> ()
}
]

def positive_biggerShl_before := [llvm|
{
^0(%arg34 : i32):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.mlir.constant(5 : i32) : i32
  %2 = llvm.shl %arg34, %0 : i32
  %3 = llvm.lshr %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def main3d_after := [llvm|
{
^0(%arg143 : i32):
  %0 = llvm.mlir.constant(23 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.and %arg143, %0 : i32
  %3 = llvm.icmp "eq" %2, %1 : i32
  %4 = llvm.zext %3 : i1 to i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

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

def test2_after := [llvm|
{
^0(%arg0 : i52, %arg1 : i52):
  %0 = llvm.icmp "ugt" %arg0, %arg1 : i52
  "llvm.return"(%0) : (i1) -> ()
}
]

def prove_exact_with_high_mask_after := [llvm|
{
^0(%arg8 : i8, %arg9 : i8):
  %0 = llvm.mlir.constant(2 : i8) : i8
  %1 = llvm.mlir.constant(-2 : i8) : i8
  %2 = llvm.ashr %arg8, %0 : i8
  %3 = llvm.and %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

List.next in Mathlib.Data.List.Cycle

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

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

def eq_shift_in_zeros_after := [llvm|
{
^0(%arg84 : i32, %arg85 : i32):
  %0 = llvm.mlir.constant(256 : i32) : i32
  %1 = llvm.xor %arg84, %arg85 : i32
  %2 = llvm.icmp "ult" %1, %0 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def t4_before := [llvm|
{
^0(%arg9 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %0, %arg9 overflow<nsw> : i8
  %2 = llvm.icmp "ugt" %1, %arg9 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def zext_nneg_sext_sle_op0_narrow_before := [llvm|
{
^0(%arg50 : i8, %arg51 : i16):
  %0 = llvm.zext nneg %arg50 : i8 to i32
  %1 = llvm.sext %arg51 : i16 to i32
  %2 = llvm.icmp "sle" %0, %1 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def sext_shl_trunc_smaller_after := [llvm|
{
^0(%arg11 : i16, %arg12 : i32):
  %0 = llvm.zext %arg11 : i16 to i32
  %1 = llvm.shl %0, %arg12 : i32
  %2 = llvm.trunc %1 : i32 to i5
  "llvm.return"(%2) : (i5) -> ()
}
]

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

def ripple_nsw3_after := [llvm|
{
^0(%arg19 : i16, %arg20 : i16):
  %0 = llvm.mlir.constant(-21845 : i16) : i16
  %1 = llvm.mlir.constant(21843 : i16) : i16
  %2 = llvm.and %arg20, %0 : i16
  %3 = llvm.and %arg19, %1 : i16
  %4 = llvm.add %2, %3 overflow<nsw,nuw> : i16
  "llvm.return"(%4) : (i16) -> ()
}
]

def binop_left_to_zero_srem : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (0) : i64
      %0 = llvm.srem %c, %x : i64
      llvm.return %0 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (0) : i64
      llvm.return %c : i64
  }]

def t2_symmetry_after := [llvm|
{
^0(%arg37 : i8, %arg38 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.xor %arg37, %0 : i8
  %2 = llvm.icmp "ule" %arg38, %1 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

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

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

@[simp_denote]
def shl_llvm_nsw_32 := [LV| {
  ^entry (%x: i32, %y: i32):
    %1 = llvm.shl %x, %y overflow<nsw> : i32
    llvm.return %1 : i32
  }]

def n12_after := [llvm|
{
^0(%arg0 : i8, %arg1 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %0, %arg0 overflow<nsw> : i8
  %2 = llvm.icmp "slt" %arg1, %1 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def or_xor_tree_1100_after := [llvm|
{
^0(%arg9 : i32, %arg10 : i32, %arg11 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mul %arg9, %0 : i32
  %2 = llvm.mul %arg10, %0 : i32
  %3 = llvm.mul %arg11, %0 : i32
  %4 = llvm.xor %1, %2 : i32
  %5 = llvm.or %4, %3 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def trunc_shl_zext_32_before := [llvm|
{
^0(%arg1 : i32):
  %0 = llvm.mlir.constant(4 : i16) : i16
  %1 = llvm.trunc %arg1 : i32 to i16
  %2 = llvm.shl %1, %0 : i16
  %3 = llvm.zext %2 : i16 to i32
  "llvm.return"(%3) : (i32) -> ()
}
]

@[elab_as_elim, induction_eliminator]
def recOn' {motive : Ctxt Ty → Sort*}
    (nil  : motive empty)
    (cons : (Γ : Ctxt Ty) → (t : Ty) → motive Γ → motive (Γ.cons t)) :
    ∀ Γ, motive Γ
  | ⟨[]⟩        => nil
  | ⟨ty :: tys⟩ => cons ⟨tys⟩ ty (recOn' nil cons ⟨tys⟩)

def combined_sdiv_srem := [LV| {
  ^entry (%a: i64, %b: i64):
    %0= llvm.sdiv exact %a, %b : i64
    %1 = llvm.mul %b, %0 : i64
    %2 = llvm.sub %a, %1 : i64
    llvm.return %2 : i64
  }]

def positive_biggershl_shlnuwnsw_lshrexact_before := [llvm|
{
^0(%arg24 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.mlir.constant(6 : i8) : i8
  %2 = llvm.lshr exact %arg24, %0 : i8
  %3 = llvm.shl %2, %1 overflow<nsw,nuw> : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

Nat in Init.Prelude

|
</all_available_defs>

<all_available_lemmas>
Nat.mod_eq_of_lt in Init.Data.Nat.Div.Basic
Nat.add_comm in Init.Data.Nat.Basic
Fin.ext_iff in Init.Data.Fin.Lemmas
Nat.mod_le in Init.Data.Nat.Div.Basic
eq_iff_iff in Init.Core
iff_true in Init.SimpLemmas
ite_cond_eq_true in Init.SimpLemmas

@[ext]
theorem ext {x y : BitStream} (h : ∀ i, x i = y i) : x = y

@[simp]
lemma List.Vector.append_get_ge {x : List.Vector α n} {y : List.Vector α m} {i : Fin (n+m)} (hlt: n ≤ i) :
    (x ++ y).get i = y.get ((i.cast (Nat.add_comm n m) |>.subNat n hlt))

@[simp]
lemma List.Vector.append_get_lt {x : List.Vector α n} {y : List.Vector α m} {i : Fin (n+m)} (hlt: i < n) :
    (x ++ y).get i = x.get (i.castLT hlt)

@[simp]
lemma BitVecs.transport_getElem {bvs : BitVecs m} (f : Fin n → Fin m) (i : Fin n) :
    (bvs.transport f).bvs.get i = bvs.bvs.get (f i)

theorem test_proof : test_before ⊑ test_after

theorem ashrslt_01_13_exact_thm (e : IntW 4) :
  icmp IntPred.slt (ashr e (const? 4 1) { «exact» := true }) (const? 4 (-3)) ⊑
    icmp IntPred.slt e (const? 4 (-6))

theorem e_1721 :
     - 1 * ( ~~~(a &&&  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) - 2 * (a ^^^ c) - 3 * ((a ^^^ b) ||| (a ^^^ c)) - 5 * ((a |||  ~~~b) &&& (b ^^^ c)) - 1 * (c ^^^ (a &&& ( ~~~b ||| c))) + 5 * ( ~~~a ||| (b ^^^ c)) - 7 * ((b &&&  ~~~c) |||  ~~~(a ||| ( ~~~b &&& c))) + 2 * (a ^^^ ( ~~~b &&& c)) + 2 * ( ~~~(a &&&  ~~~b) &&&  ~~~(b ^^^ c)) - 7 * (c |||  ~~~(a ||| b)) + 7 * ( ~~~(a |||  ~~~b) |||  ~~~(a ^^^ (b ^^^ c))) - 6 * (b ^^^ ( ~~~a ||| (b &&& c))) + 11 * (c &&&  ~~~(a ^^^ b)) + 1 * (a ^^^ ( ~~~b ||| c)) - 1 * (a ||| (b ^^^ c)) - 5 * (b ^^^ (a &&& c)) - 6 * (b |||  ~~~(a |||  ~~~c)) + 5 * ((a &&&  ~~~b) ||| (a ^^^ (b ^^^ c))) + 2 * (a &&& (b ||| c)) - 1 * ((a &&& c) ||| (b &&&  ~~~c)) - 3 * (a |||  ~~~c) - 7 * (c ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) - 11 * (c ||| (a &&& b)) + 16 *  ~~~(a ||| (b ||| c)) + 16 *  ~~~(a ||| ( ~~~b ||| c)) + 13 *  ~~~( ~~~a ||| (b ||| c)) + 41 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 25 * ( ~~~a &&& ( ~~~b &&& c)) + 28 * ( ~~~a &&& (b &&& c)) + 20 * (a &&& ( ~~~b &&& c)) + 10 * (a &&& (b &&& c)) = 3 * (a &&& ( ~~~b ||| c))

theorem ne_smax2_proof : ne_smax2_before ⊑ ne_smax2_after

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

theorem ne_umin2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 <ᵤ x) = 1#1 → ofBool (x_1 != x) = ofBool (x_1 <ᵤ x)

theorem e_1079 :
    3 *  ~~~z - 5 * (z ^^^ t) + 5 *  ~~~t - 6 * (z ||| t) - 3 *  ~~~(z &&&  ~~~t) - 8 *  ~~~(z ||| t) + 11 *  ~~~(z |||  ~~~t) + 6 * (z &&& t) =  - 3 * (z &&&  ~~~t) - 3 * (z |||  ~~~t)

theorem e_1720 :
    3 * ( ~~~(a ^^^ b) &&& (a ^^^ c)) - 5 * (c ^^^ (a &&& ( ~~~b ||| c))) - 3 * ((a &&&  ~~~b) |||  ~~~(b ^^^ c)) - 3 * (c ^^^  ~~~(a &&& (b &&& c))) - 1 *  ~~~( ~~~a ||| (b ^^^ c)) + 7 * (a &&&  ~~~c) + 7 * (b ^^^  ~~~(a &&& c)) - 1 * ((a &&& c) ^^^ (a ^^^ ( ~~~b &&& c))) - 1 * ((a &&& b) ^^^  ~~~(a ^^^ ( ~~~b ||| c))) - 2 * (b ^^^  ~~~(a ||| (b &&& c))) - 1 * (b ^^^  ~~~(a ||| (b ^^^ c))) - 7 * (c ^^^  ~~~( ~~~a ||| (b &&& c))) + 4 * ((a &&& b) ||| (b ^^^ c)) - 5 * (a &&& ( ~~~b ||| c)) + 1 * ((a ^^^ b) ||| (a ^^^ c)) - 5 * (a |||  ~~~b) + 5 * (a ^^^ (b ^^^ c)) - 11 *  ~~~(a &&& (b &&& c)) - 1 *  ~~~( ~~~a ||| (b &&& c)) + 4 * (c ^^^  ~~~(a &&&  ~~~b)) - 1 * (b &&&  ~~~c) + 5 * (c ^^^ ( ~~~a &&& ( ~~~b ||| c))) - 2 * (b ^^^  ~~~( ~~~a ||| (b &&& c))) + 2 * ( ~~~b ||| (a ^^^ c)) + 4 *  ~~~(a ||| (b ||| c)) + 5 *  ~~~(a ||| ( ~~~b ||| c)) + 23 *  ~~~( ~~~a ||| (b ||| c)) + 12 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 9 * ( ~~~a &&& ( ~~~b &&& c)) + 10 * (a &&& ( ~~~b &&& c)) + 8 * (a &&& (b &&& c)) =  - 24 * ( ~~~a &&& (b &&& c)) - 3 * ( ~~~(a &&& b) &&&  ~~~(a ^^^ (b ^^^ c)))

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

theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q)

theorem ule_or_min_commute_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 == 0#8) ||

theorem positive_samevar_shlnuwnsw_ashrexact_proof : positive_samevar_shlnuwnsw_ashrexact_before ⊑ positive_samevar_shlnuwnsw_ashrexact_after

@[simp] theorem Valuation.ofHVector_apply (xs : HVector toType ts)
    (v : Var ⟨ts⟩ t) :
    ofHVector xs v = xs[v]

theorem dec_mask_commute_neg_i32_proof : dec_mask_commute_neg_i32_before ⊑ dec_mask_commute_neg_i32_after

theorem lshr_add_xor_fail_thm (e e_1 : IntW 8) :
  LLVM.xor (lshr e_1 (const? 8 1)) (add (lshr e (const? 8 1)) (const? 8 123)) ⊑
    LLVM.xor (lshr e_1 (const? 8 1))
      (add (lshr e (const? 8 1)) (const? 8 123) { «nsw» := false, «nuw» := true })

theorem ashrslt_02_09_proof : ashrslt_02_09_before ⊑ ashrslt_02_09_after

theorem add_and_or_commutative_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), (x_1 &&& x) + (x ||| x_1) = x + x_1

theorem masked_icmps_mask_notallzeros_bmask_mixed_1b_logical_proof : masked_icmps_mask_notallzeros_bmask_mixed_1b_logical_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_1b_logical_after

theorem icmp_ne_sext_sgt_zero_nofold_thm (e : IntW 32) :
  icmp IntPred.ne (sext 32 (icmp IntPred.sgt e (const? 32 0))) e ⊑
    icmp IntPred.ne e (sext 32 (icmp IntPred.sgt e (const? 32 0)))

theorem test38_proof : test38_before ⊑ test38_after

theorem xor_i8_to_i64_shl_save_and_ne_thm.extracted_1._2 : ∀ (x : BitVec 64) (x_1 : BitVec 8),
  ofBool (x_1 &&& 1#8 != 0#8) = 1#1 →
    ¬63#64 ≥ ↑64 → x ^^^ BitVec.ofInt 64 (-9223372036854775808) = x ^^^ zeroExtend 64 x_1 <<< 63#64

theorem e_2018 :
    1 * ((e &&& f) ^^^  ~~~( ~~~d &&& (e ^^^ f))) + 11 * ((d &&& f) ||| (e &&&  ~~~f)) - 6 * (e ^^^  ~~~(d &&& (e &&& f))) + 1 * (e ^^^ (d |||  ~~~f)) - 1 * (f ^^^ (d &&&  ~~~e)) - 1 * f + 5 * (f |||  ~~~(d ^^^ e)) + 7 * (e |||  ~~~(d ||| f)) - 1 *  ~~~(d &&&  ~~~f) + 2 * (e ^^^  ~~~(d &&& (e ||| f))) + 2 * ( ~~~f &&&  ~~~(d ^^^ e)) - 7 * (d &&&  ~~~e) + 7 * (e ^^^ f) + 7 * ( ~~~e ||| (d ^^^ f)) - 1 * e - 1 * ((d ^^^ e) |||  ~~~(d ^^^ f)) - 6 *  ~~~( ~~~d ||| (e ^^^ f)) + 11 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) + 2 * (f &&& (d |||  ~~~e)) - 1 * (d ^^^ f) - 1 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) - 5 * (f ^^^ ( ~~~d ||| (e &&& f))) - 7 * (e ^^^ (d &&& ( ~~~e ||| f))) - 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) + 1 * (e ^^^  ~~~(d &&& f)) + 1 * ((e &&& f) ^^^  ~~~(d &&& (e ^^^ f))) - 24 *  ~~~(d ||| (e ||| f)) - 13 *  ~~~(d ||| ( ~~~e ||| f)) + 3 *  ~~~( ~~~d ||| (e ||| f)) - 33 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 27 * ( ~~~d &&& ( ~~~e &&& f)) - 9 * ( ~~~d &&& (e &&& f)) - 6 * (d &&& ( ~~~e &&& f)) - 12 * (d &&& (e &&& f)) =  - 1 * ( ~~~(d ||| e) |||  ~~~(e ^^^ f)) - 2 * (e ^^^ (d &&&  ~~~f))

theorem icmp_sgt6_thm (e : IntW 8) :
  icmp IntPred.sgt (shl e (const? 8 1) { «nsw» := true, «nuw» := false }) (const? 8 16) ⊑
    icmp IntPred.sgt e (const? 8 8)

theorem or_to_nxor_multiuse_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  True ∧ (x_1 &&& x &&& ((x_1 ||| x) ^^^ -1#32) != 0) = true → False

theorem test3_proof : test3_before ⊑ test3_after

theorem lshrult_01_13_exact_proof : lshrult_01_13_exact_before ⊑ lshrult_01_13_exact_after

theorem e_678 :
    1 * x + 1 * y - 1 * (x |||  ~~~y) - 1 * (x ||| y) - 7 *  ~~~(x ^^^ y) - 7 *  ~~~x + 22 *  ~~~(x ||| y) + 8 *  ~~~(x |||  ~~~y) + 7 * (x &&&  ~~~y) + 8 * (x &&& y) = 6 *  ~~~y + 1 *  ~~~(x &&&  ~~~y)

theorem lshr_add_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬(5#8 ≥ ↑8 ∨ (42#8 == 0 || 8 != 1 && x == intMin 8 && 42#8 == -1) = true ∨ 5#8 ≥ ↑8) →
    ¬((42#8 == 0 || 8 != 1 && x == intMin 8 && 42#8 == -1) = true ∨ 5#8 ≥ ↑8) →
      (x_1 >>> 5#8 + x.srem 42#8) <<< 5#8 = x_1 + x.srem 42#8 <<< 5#8 &&& BitVec.ofInt 8 (-32)

theorem select_icmp_ne_0_and_1073741824_or_8_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 32),
  ofBool (0#32 != x_1 &&& 1073741824#32) = 1#1 → ofBool (x_1 &&& 1073741824#32 == 0#32) = 1#1 → x = x ||

theorem shl_and_thm (e : IntW 8) :
  LLVM.and (shl (const? 8 48) e) (shl (const? 8 8) (add e (const? 8 1))) ⊑ shl (const? 8 16) e

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

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

theorem icmp_eq_mul_nsw_nonequal_proof : icmp_eq_mul_nsw_nonequal_before ⊑ icmp_eq_mul_nsw_nonequal_after

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

theorem main7a_logical_thm.extracted_1._4 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x_1 &&& x == x_1) = 1#1 → ¬ofBool (x_1 &&& x != x_1) = 1#1 → ¬0#1 = 1#1 → False

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

theorem lshrugt_02_12_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬2#4 ≥ ↑4 → ofBool (BitVec.ofInt 4 (-4) <ᵤ x >>> 2#4) = 0#1

theorem test3a_proof : test3a_before ⊑ test3a_after

theorem select_2_thm.extracted_1._10 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1),
  ¬x_2 = 1#1 → x ^^^ 45#8 ^^^ -1#8 = x ^^^ BitVec.ofInt 8 (-46)

theorem uge_and_max_commute_logical_thm (e e_1 : IntW 8) :
  select (icmp IntPred.eq e_1 (const? 8 (-1))) (icmp IntPred.uge e_1 e) (const? 1 0) ⊑
    icmp IntPred.eq e_1 (const? 8 (-1))

theorem add_smax_simplify2_proof : add_smax_simplify2_before ⊑ add_smax_simplify2_after

theorem test_add_nuw_nsw__nsw_is_safe_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x ||| BitVec.ofInt 32 (-2147483648) == -1#32) = 1#1 →
    True ∧ (x ||| BitVec.ofInt 32 (-2147483648)).saddOverflow 1#32 = true → False

theorem substitute_constant_and_ne_ugt_swap_logical_proof : substitute_constant_and_ne_ugt_swap_logical_before ⊑ substitute_constant_and_ne_ugt_swap_logical_after

theorem mkOutEqZeroCircuitLeN_eval_eq_false_iff {arity : Type _}
  [DecidableEq arity] [Fintype arity] [Hashable arity] (p : FSM arity) (n : Nat)
  (env : Vars p.α arity (n + 1) → Bool) :
  ((mkOutEqZeroCircuitLeN p n).eval env = false) ↔
  (∀ (i : Nat) (hi : i < n + 1),
    env (Vars.outputs ⟨i, by omega⟩) = false)

theorem e_1665 :
    2 *  ~~~(a ||| c) + 11 * ((a &&& b) |||  ~~~(b |||  ~~~c)) + 4 *  ~~~(a &&& ( ~~~b ||| c)) - 1 * ((a |||  ~~~b) &&& (a ^^^ (b ^^^ c))) + 4 * ( ~~~(a &&&  ~~~b) &&& (a ^^^ (b ^^^ c))) + 7 *  ~~~(a &&&  ~~~a) + 2 * (b ^^^  ~~~( ~~~a ||| (b &&& c))) - 1 * (c ^^^  ~~~(a &&& (b ||| c))) + 1 * (a ^^^ ( ~~~b &&& c)) - 7 *  ~~~(b |||  ~~~c) + 11 * (c &&&  ~~~(a ^^^ b)) - 5 * ((a &&& c) ^^^  ~~~(b &&&  ~~~c)) - 11 * (c ^^^ (a ||| (b ||| c))) + 1 *  ~~~(a ^^^ ( ~~~b ||| c)) - 5 *  ~~~(a &&& c) + 1 * ((a &&& c) |||  ~~~(b ||| c)) + 5 * (b ^^^  ~~~( ~~~a &&& (b ||| c))) - 8 *  ~~~(a ||| (b ||| c)) - 7 *  ~~~(a ||| ( ~~~b ||| c)) + 7 *  ~~~( ~~~a ||| (b ||| c)) - 6 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 19 * ( ~~~a &&& ( ~~~b &&& c)) - 7 * ( ~~~a &&& (b &&& c)) - 18 * (a &&& ( ~~~b &&& c)) - 35 * (a &&& (b &&& c)) = 1 * (a ||| (b ||| c))

theorem alive_Select_740 : forall (w : Nat) (A : Bitvec 1)
, TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec 1)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (A) %v0;
  %v2 := op:const (0) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:icmp sgt  w %v3;
  %v5 := op:const (0) %v0;
  %v6 := pair:%v5 %v1;
  %v7 := op:sub 1 %v6;
  %v8 := triple:%v4 %v1 %v7;
  %v9 := op:select w %v8;
  %v10 := op:const (-1) %v0;
  %v11 := pair:%v9 %v10;
  %v12 := op:icmp sgt  w %v11;
  %v13 := op:const (0) %v0;
  %v14 := pair:%v13 %v9;
  %v15 := op:sub w %v14;
  %v16 := triple:%v12 %v9 %v15;
  %v17 := op:select w %v16
  dsl_ret %v17
  ]  ⊑
  TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec 1)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (A) %v0;
  %v2 := op:const (0) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:icmp sgt  1 %v3;
  %v5 := op:const (0) %v0;
  %v6 := pair:%v5 %v1;
  %v7 := op:sub 1 %v6;
  %v8 := triple:%v4 %v1 %v7;
  %v9 := op:select 1 %v8;
  %v10 := op:const (-1) %v0;
  %v11 := pair:%v9 %v10;
  %v12 := op:icmp sgt  1 %v11;
  %v13 := op:const (0) %v0;
  %v14 := pair:%v13 %v9;
  %v15 := op:sub 1 %v14;
  %v16 := triple:%v4 %v1 %v7;
  %v17 := op:select 1 %v16
  dsl_ret %v17
  ]

theorem src_srem_shl_demand_max_signbit_mask_hit_first_demand_proof : src_srem_shl_demand_max_signbit_mask_hit_first_demand_before ⊑ src_srem_shl_demand_max_signbit_mask_hit_first_demand_after

theorem test_cast_select_proof : test_cast_select_before ⊑ test_cast_select_after

theorem Id.map_eq' (x : Id α) (f : α → β) : f <$> x = f x

@[simp] theorem Com.castPureToEff_var {com : Com d _ .pure ty} {e : Expr d Γ _ eTy} :
    (var e com).castPureToEff eff = var (e.castPureToEff eff) (com.castPureToEff eff)

theorem icmp_slt_0_and_icmp_sge_neg1_i64_fail_thm (e : IntW 64) :
  LLVM.and (lshr e (const? 64 62)) (zext 64 (icmp IntPred.sge e (const? 64 (-1)))) ⊑
    select (icmp IntPred.sgt e (const? 64 (-2))) (LLVM.and (lshr e (const? 64 62)) (const? 64 1))
      (const? 64 0)

theorem alive_275   : alive_275_src ⊑ alive_275_tgt

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

theorem ashrslt_03_06_exact_proof : ashrslt_03_06_exact_before ⊑ ashrslt_03_06_exact_after

theorem test_negative_nsw_and_unsigned_pred_proof : test_negative_nsw_and_unsigned_pred_before ⊑ test_negative_nsw_and_unsigned_pred_after

theorem mul_of_sdiv_fail_ub_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ x.smod 6#8 ≠ 0 ∨ (6#8 == 0 || 8 != 1 && x == intMin 8 && 6#8 == -1) = true) →
    x.sdiv 6#8 * BitVec.ofInt 8 (-6) = 0#8 - x

theorem sext_diff_i1_xor_sub_1_thm (e e_1 : IntW 1) :
  sub (sext 64 e_1) (sext 64 e) ⊑ add (zext 64 e) (sext 64 e_1) { «nsw» := true, «nuw» := false }

theorem test9_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), x_1 ||

theorem ashr_C1_add_A_C2_i32_proof : ashr_C1_add_A_C2_i32_before ⊑ ashr_C1_add_A_C2_i32_after

theorem f_var1_commutative_and_proof : f_var1_commutative_and_before ⊑ f_var1_commutative_and_after

theorem test3_proof : test3_before ⊑ test3_after

theorem append_valid {Γ₁ Γ₂ Γ₃  : Ctxt Ty} {d₁ d₂ : Nat} :
  Diff.Valid Γ₁ Γ₂ d₁ →  Diff.Valid Γ₂ Γ₃ d₂ → Diff.Valid Γ₁ Γ₃ (d₁ + d₂)

theorem bools_thm (e e_1 e_2 : IntW 1) :
  LLVM.or (LLVM.and (LLVM.xor e_2 (const? 1 1)) e_1) (LLVM.and e_2 e) ⊑ select e_2 e e_1

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

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

theorem test_mul_nuw_nsw__nsw_is_safe_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x ||| BitVec.ofInt 32 (-83886080) == BitVec.ofInt 32 (-83886079)) = 1#1 →
    ¬(True ∧ (x ||| BitVec.ofInt 32 (-83886080)).smulOverflow 9#32 = true) →
      BitVec.ofInt 32 (-754974711) = (x ||| BitVec.ofInt 32 (-83886080)) * 9#32

theorem PR42691_1_logical_proof : PR42691_1_logical_before ⊑ PR42691_1_logical_after

theorem alive_AndOrXor_698  (w : Nat)   : alive_AndOrXor_698_src w  ⊑ alive_AndOrXor_698_tgt w

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

theorem ugt_sext_proof : ugt_sext_before ⊑ ugt_sext_after

theorem and_xor_or5_proof : and_xor_or5_before ⊑ and_xor_or5_after

theorem bools2_logical_commute2_thm.extracted_1._13 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 = 1#1 → x = 1#1 → ¬0#1 = 1#1 → x_2 ^^^ 1#1 = x

theorem AvoidCollision_signExtend_not {x : BitVec w} (h : 0 < w) :
    (~~~x).signExtend v = ~~~(x.signExtend v)

theorem and_logic_and_logic_or_6_thm.extracted_1._7 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 = 1#1 → 0#1 = 1#1 → 1#1 = x_1 &&& x

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

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

theorem t1_sshr_thm (e e_1 : IntW 32) :
  ashr (LLVM.and (shl (const? 32 (-1)) e_1) e) e_1 { «exact» := true } ⊑
    ashr (LLVM.and (shl (const? 32 (-1)) e_1 { «nsw» := true, «nuw» := false }) e) e_1 { «exact» := true }

theorem shl_lshr_demand3_proof : shl_lshr_demand3_before ⊑ shl_lshr_demand3_after

theorem test14_proof : test14_before ⊑ test14_after
</all_available_lemmas>

<local_ctx>
import Batteries.Data.Fin.Basic

import Batteries.Data.Fin.Lemmas

import Blase.SingleWidth.Defs

import Blase.AutoStructs.Constructions

import Blase.AutoStructs.Defs

import Blase.AutoStructs.FiniteStateMachine

import Mathlib.Tactic.Ring

import Mathlib.Data.Nat.Size -- TODO: remove and get rid of shiftLeft_eq_mul_pow use

import Mathlib.Data.BitVec

import Mathlib.Tactic.FinCases

open Fin.NatCast

open Mathlib

section fsm

variable {arity : Type} [FinEnum arity]

open BitStream in

end fsm

section nfas_relations

inductive NFA.msbState : Type where
| i | f
deriving DecidableEq, Fintype

end nfas_relations

def liftUnop n : Fin (n + 1) → Fin (n + 2) :=
  fun k =>
    if k = n then Fin.last (n+1) else k.castLE (by admit /- proof elided -/
    )

inductive TermBinop where
| and | or | xor | add | sub

def TermBinop.subst (op : TermBinop) (t₁ t₂ : Term) : Term :=
  match op with
  | .and => .and t₁ t₂
  | .or => .or t₁ t₂
  | .xor => .xor t₁ t₂
  | .add => .add t₁ t₂
  | .sub => .sub t₁ t₂

def TermBinop.openTerm (op : TermBinop) : Term := op.subst (.var 0) (.var 1)

inductive TermUnop where
| neg | not | shiftL (k : Nat)

def TermUnop.openTerm (op : TermUnop) : Term :=
  match op with
  | .neg => .neg (.var 0)
  | .not => .not (.var 0)
  | .shiftL k => .shiftL (.var 0) k

@[simp]
def TermUnop.openTerm_arity' (op : TermUnop) : op.openTerm.arity + 1 = 2 :=

def TermUnop.subst (op : TermUnop) (t : Term) : Term :=
  match op with
  | .neg => .neg t
  | .not => .not t
  | .shiftL k => .shiftL t k

def swapLastTwo (x : Fin (n + 2)) : Fin (n + 2) :=
  if x = Fin.last (n + 1) then n else if x = n then Fin.last (n + 1) else x
</local_ctx>

<target_theorem>
lemma TermUnop.alt_lang {t : Term} (op : TermUnop) :
  (op.subst_arity' ▸ (op.subst t).language) =
    let lop : Set (BitVecs 2) :=
</target_theorem>

