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

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

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

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

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

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

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

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

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

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

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

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

### Your task:
<all_available_defs>
Bool in Init.Prelude
Nat in Init.Prelude
Int.xor in Mathlib.Data.Int.Bitwise
List in Init.Prelude
Nat.testBit in Init.Data.Nat.Bitwise.Basic
BitVec in Init.Prelude
BitVec.ofNat in Init.Prelude
List.map in Init.Prelude
BitVec.ult in Init.Data.BitVec.Basic
BitVec.carry in Init.Data.BitVec.Bitblast

syntax "slt" : 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) )

def BitStream : Type := Nat → Bool

def borrow (x y : BitStream) : BitStream :=
  fun n => (subAux x y n).2

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 nxor (a b : BitStream) : BitStream := fun i => a i == b i

def scanAnd (s : BitStream) : BitStream := scanl true Bool.and s

abbrev scanl (init : Bool) (f : Bool → Bool → Bool) (s : BitStream) : BitStream :=
  fun n => match n with
    | 0 => f init (s 0)
    | n+1 => f (scanl init f s n) (s (n + 1))

def scanOr (s : BitStream) : BitStream := scanl false Bool.or s

abbrev falseIffNeq (n : Nat) : BitStream := fun i => decide (i == n)

abbrev falseIffLt (n : Nat) : BitStream := fun i => decide (i ≥ n)

abbrev falseIffGe (n : Nat) : BitStream := fun i => decide (i < n)

abbrev falseIffEq (n : Nat) : BitStream := fun i => decide (i != n)

abbrev falseIffGt (n : Nat) : BitStream := fun i => decide (i ≤ n)

def Term.width (t : Term) : WidthExpr :=
  match t with

| .ofNat w _n => w
  | .var _v w => w
  | .add w _a _b => w
  | .zext _a wnew => wnew
  | .setWidth _a wnew => wnew
  | .sext _a wnew => wnew
  | .bor w _a _b => w
  | .band w _a _b => w
  | .bxor w _a _b => w
  | .bnot w _a => w
  | .boolVar _v => WidthExpr.const 1 
  | .boolConst _b => WidthExpr.const 1
  | .shiftl w _a _k => w
  | .bvOfBool _b => WidthExpr.const 1
  | binWidthRel _k wa wb => WidthExpr.const 0
  | binRel _k w _a _b => w
  | or _p1 _p2 => WidthExpr.const 0
  | and _p1 _p2 => WidthExpr.const 0
  | pvar _v => WidthExpr.const 0
  | boolBinRel _k _a _b => WidthExpr.const 0

abbrev falseIffLe (n : Nat) : BitStream := fun i => decide (i > n)

abbrev negOne : BitStream := fun _ => true

def shiftLeft (x : BitStream) (k : Nat) : BitStream :=
  fun i => if i < k then false else x (i - k)

def ofNat (x : Nat) : BitStream :=
  Nat.testBit x

abbrev one    : BitStream := (· == 0)

abbrev zero   : BitStream := fun _ => false

def Term.denote (w : Nat) (t : Term) (vars : List (BitVec w)) : BitVec w :=
  match t with
  | ofNat n => BitVec.ofNat w n
  | var n => vars.getD n default
  | zero => 0#w
  | negOne => -1#w
  | one  => 1#w
  | and a b => (a.denote w vars) &&& (b.denote w vars)
  | or a b => (a.denote w vars) ||| (b.denote w vars)
  | xor a b => (a.denote w vars) ^^^ (b.denote w vars)
  | not a => ~~~ (a.denote w vars)
  | add a b => (a.denote w vars) + (b.denote w vars)
  | sub a b => (a.denote w vars) - (b.denote w vars)
  | neg a => - (a.denote w vars)
  
  
  | shiftL a n => (a.denote w vars) <<< n

def Predicate.denote (p : Predicate) (w : Nat) (vars : List (BitVec w)) : Prop :=
  match p with
  | .width .ge k => k ≤ w 
  | .width .gt k => k < w 
  | .width .le k => w ≤ k
  | .width .lt k => w < k
  | .width .neq k => w ≠ k
  | .width .eq k => w = k
  | .binary .eq t₁ t₂ => t₁.denote w vars = t₂.denote w vars
  | .binary .neq t₁ t₂ => t₁.denote w vars ≠ t₂.denote w vars
  | .binary .sle  t₁ t₂ => ((t₁.denote w vars).sle (t₂.denote w vars)) = true
  | .binary .slt  t₁ t₂ => ((t₁.denote w vars).slt (t₂.denote w vars)) = true
  | .binary .ule  t₁ t₂ => ((t₁.denote w vars).ule (t₂.denote w vars)) = true
  | .binary .ult  t₁ t₂ => (t₁.denote w vars).ult (t₂.denote w vars) = true
  | .land  p q => p.denote w vars ∧ q.denote w vars
  | .lor  p q => p.denote w vars ∨ q.denote w vars

inductive Predicate : Type where
 
| width (wp : WidthPredicate) (n : Nat) : Predicate
| binary (p : BinaryPredicate) (t₁ t₂ : Term)
| land  (p q : Predicate) : Predicate
| lor (p q : Predicate) : Predicate
deriving Repr, Inhabited, Lean.ToExpr

inductive WidthPredicate
| eq
| neq
| lt
| le
| gt
| ge
deriving Repr, Inhabited, Lean.ToExpr

abbrev ofBitVecSext {w} (x : BitVec w) : BitStream :=
  fun i => if i < w then x.getLsbD i else x.msb

def toBitVec (w : Nat) (x : BitStream) : BitVec w :=
  match w with
  | 0   => 0#0
  | w+1 => (x.toBitVec w).cons (x w)

instance instDCTyDenote : TyDenote Ty where
toType := fun
| Ty.tokenstream => CIRCTStream.DCOp.TokenStream
| Ty.tokenstream2 => CIRCTStream.DCOp.TokenStream × CIRCTStream.DCOp.TokenStream
| Ty.valuestream w => CIRCTStream.DCOp.ValueStream (BitVec w)
| Ty.valuestream2 w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.ValueStream (BitVec w)
| Ty.valuetokenstream w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.TokenStream
| Ty.variadicvaluetokenstream w => CIRCTStream.DCOp.VariadicValueStream w × CIRCTStream.DCOp.TokenStream

@[simp_denote]
def sll_riscv_i64 :=
  [LV| {
    ^entry (%arg0: i64, %arg1: i64):
    %a = "builtin.unrealized_conversion_cast" (%arg0) : (i64) -> (!i64)
    %b = "builtin.unrealized_conversion_cast" (%arg1) : (i64) -> (!i64)
    %0 = sll %a, %b : !i64
    %1 = "builtin.unrealized_conversion_cast" (%0) : (!i64) -> (i64)
    llvm.return %1 : i64
  }]

BitVec.ofNat in Init.Prelude

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

def lshr_add_exact_after := [llvm|
{
^0(%arg6 : i8, %arg7 : i8):
  %0 = llvm.mlir.constant(-4 : i8) : i8
  %1 = llvm.mlir.constant(2 : i8) : i8
  %2 = llvm.and %arg6, %0 : i8
  %3 = llvm.and %arg7, %1 : i8
  %4 = llvm.lshr exact %2, %3 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

def llvm_sext_lower_riscv_i1_to_32 : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 1)] :=
  {lhs:= sext_llvm_i1_to_32, rhs:= sext_riscv_i1_to_32}

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

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

def tail : Stream α → Stream α := Stream'.tail

def exact_lshr_ne_before := [llvm|
{
^0(%arg157 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.lshr exact %0, %arg157 : i8
  %3 = llvm.icmp "ne" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

def not_sub_before := [llvm|
{
^0(%arg133 : i32):
  %0 = llvm.mlir.constant(123 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sub %0, %arg133 : i32
  %3 = llvm.xor %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def neg_of_sub_from_constant_after := [llvm|
{
^0(%arg172 : i8):
  %0 = llvm.mlir.constant(-42 : i8) : i8
  %1 = llvm.add %arg172, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

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

def add_and_or_before := [llvm|
{
^0(%arg15 : i32, %arg16 : i32):
  %0 = llvm.or %arg15, %arg16 : i32
  %1 = llvm.and %arg15, %arg16 : i32
  %2 = llvm.add %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def sub_select_zext_op_swapped_non_const_args_after := [llvm|
{
^0(%arg3 : i1, %arg4 : i6, %arg5 : i6):
  %0 = llvm.mlir.constant(1 : i6) : i6
  %1 = llvm.mlir.constant(0 : i6) : i6
  %2 = llvm.sub %0, %arg4 : i6
  %3 = llvm.sub %1, %arg5 : i6
  %4 = "llvm.select"(%arg3, %2, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i6, i6) -> i6
  "llvm.return"(%4) : (i6) -> ()
}
]

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

def example00 := [RV64_com| {
^bb0(%0 : !riscv.reg, %1 : !riscv.reg):
    %2 = "slt"(%0, %1) : (!riscv.reg, !riscv.reg) -> (!riscv.reg)
    %3 = "andi" (%2){imm = 1 : !i64} : (!riscv.reg) -> (!riscv.reg)
    %4 = "sra"(%0, %0) : (!riscv.reg, !riscv.reg) -> (!riscv.reg)
    %5 = "add"(%0, %0) : (!riscv.reg, !riscv.reg) -> (!riscv.reg)
    %6 = "sra"(%2, %5) : (!riscv.reg, !riscv.reg) -> (!riscv.reg)
  "ret" (%0) : (!riscv.reg) -> ()
 }].denote

def and_or2_before := [llvm|
{
^0(%arg200 : i1, %arg201 : i1, %arg202 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.xor %arg202, %0 : i1
  %2 = llvm.and %1, %arg201 : i1
  %3 = "llvm.select"(%2, %arg200, %arg201) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def add_shl_moreOneUse_sh3add_no_ZBA_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32)] where
  lhs := add_shl_moreOneUse_sh3add
  rhs := add_shl_moreOneUse_sh3add_riscv_no_ZBA

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

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

Std.Format.nest in Init.Data.Format.Basic

def shl_and_and_after := [llvm|
{
^0(%arg172 : i8, %arg173 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.mlir.constant(80 : i8) : i8
  %2 = llvm.and %arg173, %arg172 : i8
  %3 = llvm.shl %2, %0 : i8
  %4 = llvm.and %3, %1 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

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

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

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

List.Vector.ofFn in Mathlib.Data.Vector.Defs

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

def and_not_or_commute5_after := [llvm|
{
^0(%arg466 : i32, %arg467 : i32, %arg468 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sdiv %0, %arg466 : i32
  %3 = llvm.sdiv %0, %arg468 : i32
  %4 = llvm.xor %arg467, %3 : i32
  %5 = llvm.and %4, %2 : i32
  %6 = llvm.xor %5, %1 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def test_ashr__exact_is_safe_before := [llvm|
{
^0(%arg52 : i32, %arg53 : i64):
  %0 = llvm.mlir.constant(-2147483588 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.mlir.constant(0 : i32) : i32
  %3 = llvm.and %arg52, %0 : i32
  %4 = llvm.ashr %3, %1 : i32
  %5 = llvm.zext %4 : i32 to i64
  %6 = llvm.icmp "eq" %3, %2 : i32
  %7 = llvm.ashr %arg53, %5 : i64
  %8 = "llvm.select"(%6, %arg53, %7) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  "llvm.return"(%8) : (i64) -> ()
}
]

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

def and_not_or_or_not_or_xor_commute5_before := [llvm|
{
^0(%arg310 : i32, %arg311 : i32, %arg312 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.or %arg311, %arg312 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.and %2, %arg310 : i32
  %4 = llvm.xor %arg311, %arg312 : i32
  %5 = llvm.or %4, %arg310 : i32
  %6 = llvm.xor %5, %0 : i32
  %7 = llvm.or %6, %3 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

def icmp {w : Nat} (c : IntPred) (x y : IntW w) : IntW 1 := do
  let x' ← x
  let y' ← y
  icmp? c x' y'

def src_x_and_nmask_ne_after := [llvm|
{
^0(%arg27 : i8, %arg28 : i8, %arg29 : i1):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.shl %0, %arg28 overflow<nsw> : i8
  %3 = llvm.icmp "ugt" %2, %arg27 : i8
  %4 = "llvm.select"(%arg29, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def test14_after := [llvm|
{
^0(%arg26 : i35):
  %0 = llvm.mlir.constant(-19760 : i35) : i35
  %1 = llvm.mlir.constant(19744 : i35) : i35
  %2 = llvm.and %arg26, %0 : i35
  %3 = llvm.or disjoint %2, %1 : i35
  "llvm.return"(%3) : (i35) -> ()
}
]

Array.size in Init.Prelude

def test13_before := [llvm|
{
^0(%arg87 : i32):
  %0 = llvm.srem %arg87, %arg87 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def ashr_uge_noexact_after := [llvm|
{
^0(%arg160 : i8):
  %0 = llvm.mlir.constant(79 : i8) : i8
  %1 = llvm.icmp "ugt" %arg160, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

BitVec.iunfoldr in Init.Data.BitVec.Folds

AList in Mathlib.Data.List.AList

def logical_and_bitwise_and_icmps_comm1_before := [llvm|
{
^0(%arg217 : i8, %arg218 : i8, %arg219 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.icmp "eq" %arg218, %0 : i8
  %5 = llvm.and %arg217, %1 : i8
  %6 = llvm.shl %1, %arg219 : i8
  %7 = llvm.and %arg217, %6 : i8
  %8 = llvm.icmp "ne" %5, %2 : i8
  %9 = llvm.icmp "ne" %7, %2 : i8
  %10 = llvm.and %4, %8 : i1
  %11 = "llvm.select"(%9, %10, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%11) : (i1) -> ()
}
]

def State.cseRegionArgList
  {Γstart Γ : Ctxt d.Ty}
  {lets : Lets d Γstart .pure Γ}
  (_ : State d lets)
  {ts : RegionSignature d.Ty}
  (rs : HVector ((fun t => Com d t.1 .impure t.2)) <| ts) :
  {rs' : HVector ((fun t => Com d t.1 .impure t.2)) <| ts //
    HVector.denote rs = HVector.denote rs' } :=
  let _ := HVector.map (fun _Γα com => Com.denote com) rs
  match ts, rs with
  | _, .nil => ⟨.nil, by admit /- proof elided -/
    ⟩
  | ⟨Γ, t⟩::ts, .cons region rs =>
    
    
    
    
    ⟨.cons region rs, by admit /- proof elided -/
    ⟩

instance : MLIR.AST.TransformReturn (Handshake) 0 where
  mkReturn := mkReturn

System.FilePath in Init.System.FilePath

def neg_mask_before := [llvm|
{
^0(%arg1 : i32, %arg2 : i16):
  %0 = llvm.mlir.constant(15 : i16) : i16
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.sext %arg2 : i16 to i32
  %3 = llvm.sub %arg1, %2 overflow<nsw> : i32
  %4 = llvm.lshr %arg2, %0 : i16
  %5 = llvm.zext %4 : i16 to i32
  %6 = llvm.sub %1, %5 overflow<nsw> : i32
  %7 = llvm.and %3, %6 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

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

def n11_after := [llvm|
{
^0(%arg1 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.mlir.constant(6 : i8) : i8
  %2 = llvm.shl %arg1, %0 : i8
  %3 = llvm.ashr exact %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def foo_before := [llvm|
{
^0(%arg0 : i8, %arg1 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.mlir.constant(84 : i8) : i8
  %2 = llvm.mlir.constant(-118 : i8) : i8
  %3 = llvm.mlir.constant(33 : i8) : i8
  %4 = llvm.mlir.constant(-88 : i8) : i8
  %5 = llvm.mlir.constant(5 : i8) : i8
  %6 = llvm.shl %arg0, %0 : i8
  %7 = llvm.and %arg1, %1 : i8
  %8 = llvm.and %arg1, %2 : i8
  %9 = llvm.and %arg1, %3 : i8
  %10 = llvm.sub %4, %7 : i8
  %11 = llvm.and %10, %1 : i8
  %12 = llvm.or %9, %11 : i8
  %13 = llvm.xor %6, %8 : i8
  %14 = llvm.or %12, %13 : i8
  %15 = llvm.lshr %13, %0 : i8
  %16 = llvm.shl %15, %5 : i8
  %17 = llvm.xor %16, %14 : i8
  "llvm.return"(%17) : (i8) -> ()
}
]

def n10_after := [llvm|
{
^0(%arg3 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %0, %arg3 : i8
  %2 = llvm.icmp "slt" %arg3, %1 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def test18_after := [llvm|
{
^0(%arg78 : i16, %arg79 : i32):
  %0 = llvm.mlir.constant(4 : i16) : i16
  %1 = llvm.mlir.constant(0 : i16) : i16
  %2 = llvm.mlir.constant(63 : i32) : i32
  %3 = llvm.mlir.constant(31 : i32) : i32
  %4 = llvm.and %arg78, %0 : i16
  %5 = llvm.icmp "eq" %4, %1 : i16
  %6 = "llvm.select"(%5, %2, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %7 = llvm.and %arg79, %6 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

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

def add_and_or_commutative_after := [llvm|
{
^0(%arg13 : i32, %arg14 : i32):
  %0 = llvm.add %arg13, %arg14 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def PR20945_before := [llvm|
{
^0(%arg132 : i32):
  %0 = llvm.mlir.constant(-9 : i32) : i32
  %1 = llvm.mlir.constant(-5 : i32) : i32
  %2 = llvm.ashr %0, %arg132 : i32
  %3 = llvm.icmp "ne" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def add_sub_reg_frags : List (Σ Γ, RISCVPeepholeRewrite Γ) :=
  [⟨_, add_sub_reg_frags_left⟩,
  ⟨_, add_sub_reg_frags_right⟩]

Mul in Init.Prelude

|
</all_available_defs>

<all_available_lemmas>
BitVec.lt_def in Init.Data.BitVec.Lemmas
BitVec.of_length_zero in Init.Data.BitVec.Lemmas
BitVec.ult_eq_not_carry in Init.Data.BitVec.Bitblast

@[simp] theorem subAux_eq_BitVec_carry (a b : BitStream) (w i : Nat) (hi : i < w) :
    (a.subAux b i).2 = !(BitVec.carry (i + 1) (a.toBitVec w) ((~~~b).toBitVec w) true)

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

theorem e_297 :
     - 2 * (x ||| y) - 3 * x + 1 *  ~~~y + 6 *  ~~~(x ||| y) + 2 *  ~~~(x |||  ~~~y) + 4 * (x &&&  ~~~y) + 12 * (x &&& y) = 7 *  ~~~(x ^^^ y)

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

theorem pv_proof : pv_before ⊑ pv_after

theorem e_1479 :
     - 1 * z - 6 * (z ^^^ t) + 7 *  ~~~(z &&& t) - 2 * (z ||| t) + 7 *  ~~~z - 3 *  ~~~(z &&&  ~~~z) - 7 *  ~~~t - 4 *  ~~~(z ||| t) - 4 *  ~~~(z |||  ~~~t) + 12 * (z &&&  ~~~t) + 5 * (z &&& t) =  - 1 * t

theorem main12_logical_thm.extracted_1._4 : ∀ (x : BitVec 32),
  ¬ofBool (truncate 16 x <ₛ 0#16) = 1#1 →
    ¬ofBool (x &&& 32896#32 == 0#32) = 1#1 → ¬ofBool (truncate 8 x <ₛ 0#8) = 1#1 → 1#32 = 2#32

theorem e_843 :
     - 3 *  ~~~t + 2 * (z |||  ~~~t) + 1 *  ~~~(z ||| t) - 1 * (z &&&  ~~~t) - 4 * (z &&& t) =  - 2 * z

theorem n6_proof : n6_before ⊑ n6_after

theorem bools_logical_commute1_thm.extracted_1._14 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 = 1#1 → ¬x_1 = 1#1 → ¬0#1 = 1#1 → 0#1 = x_2

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

theorem e_2429 :
     - 1 *  ~~~( ~~~d ||| (e &&& f)) + 5 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) + 1 *  ~~~( ~~~d &&& ( ~~~e ||| f)) - 2 * (e ^^^ (d &&&  ~~~f)) - 7 *  ~~~( ~~~d &&& (e ||| f)) + 4 * (e |||  ~~~(d ||| f)) + 11 *  ~~~(e ||| f) - 1 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) - 3 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) - 7 * (f ^^^  ~~~(d &&& (e &&& f))) - 5 * ((d &&& f) ^^^ (d ^^^ ( ~~~e &&& f))) - 2 * (e ^^^ (d |||  ~~~f)) + 3 * ((d &&& f) ^^^  ~~~(d ^^^ ( ~~~e &&& f))) - 2 * (e ||| (d &&&  ~~~f)) + 11 * (f ||| (d &&&  ~~~e)) + 1 * ((d &&& e) ||| (d ^^^ (e ^^^ f))) - 6 * ((e &&&  ~~~f) |||  ~~~( ~~~d ||| ( ~~~e &&& f))) - 1 *  ~~~(d &&& ( ~~~e &&& f)) - 1 * ((d ^^^ e) &&&  ~~~(d ^^^ f)) - 11 *  ~~~f - 11 * (e ^^^ (d ||| ( ~~~e &&& f))) + 7 * (f ^^^ (d ||| (e ||| f))) + 7 * (d |||  ~~~f) - 2 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 2 * (f ^^^  ~~~(d |||  ~~~e)) + 3 * ((e &&&  ~~~f) ^^^ ( ~~~d ||| (e ^^^ f))) + 3 * ((d &&& e) |||  ~~~(e |||  ~~~f)) - 7 * (e ^^^ (d &&& f)) + 2 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) - 1 * (f ||| (d ^^^ e)) + 1 * (e &&&  ~~~(d ^^^ f)) - 3 * (e ^^^ (d ||| (e &&& f))) - 1 * (d ^^^ e) - 6 * (d ^^^ (e ||| f)) + 7 *  ~~~d + 1 *  ~~~(d &&& ( ~~~e ||| f)) + 1 * ( ~~~d ||| ( ~~~e ||| f)) + 11 * (f ^^^  ~~~(d &&& e)) + 1 * (e ^^^  ~~~(d &&& f)) + 2 * ( ~~~e &&&  ~~~(d ^^^ f)) - 2 *  ~~~(d |||  ~~~f) + 1 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 6 *  ~~~(d &&& (e &&& f)) - 2 *  ~~~(d &&&  ~~~e) - 3 * ( ~~~(d |||  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) + 2 * ((d &&& e) |||  ~~~(d ^^^ (e ^^^ f))) - 1 * (f &&& (d |||  ~~~e)) + 1 * ( ~~~(d |||  ~~~e) ||| (e ^^^ f)) - 11 *  ~~~(e &&& f) - 5 * ( ~~~d ||| (e ||| f)) - 6 * (f ^^^ (d &&&  ~~~e)) - 2 * (f ^^^ ( ~~~d &&& (e ||| f))) + 1 * (e ^^^ (d &&& (e ||| f))) + 2 *  ~~~(d ||| ( ~~~e &&& f)) + 11 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) + 3 * ((d &&& f) ||| (e &&&  ~~~f)) - 5 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) - 1 * (d &&& f) - 5 * d + 4 * ((d &&& f) ^^^ (e ||| f)) + 5 * (e &&&  ~~~(d &&& f)) - 1 * (d &&& ( ~~~e ||| f)) + 2 * (d ^^^ f) - 7 * (e &&& f) + 5 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 2 * ((d ||| e) &&& (d ^^^ (e ^^^ f))) + 11 * (d ^^^ ( ~~~e &&& f)) - 9 *  ~~~(d ||| (e ||| f)) + 16 *  ~~~(d ||| ( ~~~e ||| f)) + 27 *  ~~~( ~~~d ||| (e ||| f)) + 22 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 2 * ( ~~~d &&& ( ~~~e &&& f)) + 14 * ( ~~~d &&& (e &&& f)) + 28 * (d &&& ( ~~~e &&& f)) - 20 * (d &&& (e &&& f)) =  - 2 * ( ~~~(d ||| e) ||| (e ^^^ f)) - 2 *  ~~~(d ^^^ ( ~~~e ||| f))

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

theorem or_nosignbit_shl_proof : or_nosignbit_shl_before ⊑ or_nosignbit_shl_after

theorem lor_bor_left1_proof : lor_bor_left1_before ⊑ lor_bor_left1_after

theorem mullo_variant3_proof : mullo_variant3_before ⊑ mullo_variant3_after

theorem lshrult_03_03_exact_proof : lshrult_03_03_exact_before ⊑ lshrult_03_03_exact_after

theorem or_ranges_overlap_proof : or_ranges_overlap_before ⊑ or_ranges_overlap_after

theorem add_umax_simplify2_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(True ∧ x.uaddOverflow 57#32 = true) → ¬ofBool (56#32 <ᵤ x + 57#32) = 1#1 → 56#32 = x + 57#32

theorem slt_swap_or_not_max_commute_proof : slt_swap_or_not_max_commute_before ⊑ slt_swap_or_not_max_commute_after

theorem test15f_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x &&& 128#32 != 0#32) = 1#1 → ¬1#32 ≥ ↑32 → 0#32 = x <<< 1#32 &&& 256#32 ^^^ 256#32

theorem src_srem_shl_demand_max_signbit_mask_hit_first_demand_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬((4#32 == 0 || 32 != 1 && x == intMin 32 && 4#32 == -1) = true ∨ 29#32 ≥ ↑32) →
    (4#32 == 0 || 32 != 1 && x == intMin 32 && 4#32 == -1) = true ∨
        True ∧ (x.srem 4#32 <<< 29#32).sshiftRight' 29#32 ≠ x.srem 4#32 ∨ 29#32 ≥ ↑32 →
      False

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

theorem e_580 :
    4 * y - 1 * (x ^^^ y) - 7 *  ~~~(x &&& y) - 1 *  ~~~y + 2 * x - 3 * (x |||  ~~~y) + 13 *  ~~~(x ||| y) + 12 * (x &&&  ~~~y) - 1 * (x &&& y) = 2 *  ~~~(x &&&  ~~~x) - 6 *  ~~~(x |||  ~~~y)

theorem n10_thm (e : IntW 8) :
  icmp IntPred.sgt (sub (const? 8 0) e) e ⊑ icmp IntPred.slt e (sub (const? 8 0) e)

theorem eq_shift_in_zeros_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(16#32 ≥ ↑32 ∨ 16#32 ≥ ↑32 ∨ 8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32) →
    ofBool (truncate 24 (x_1 >>> 16#32) == truncate 24 (x >>> 16#32)) &&&
        ofBool (truncate 8 (x_1 >>> 8#32) == truncate 8 (x >>> 8#32)) =
      ofBool (x_1 ^^^ x <ᵤ 256#32)

theorem sub_3_thm (e e_1 : IntW 128) (e_2 : IntW 1) (e_3 : IntW 128) :
  LLVM.xor (sub e_3 (select e_2 (LLVM.xor e_1 (const? 128 (-1))) (LLVM.xor e (const? 128 123)))) (const? 128 (-1)) ⊑
    sub (const? 128 (-2)) (add (select e_2 e_1 (LLVM.xor e (const? 128 (-124)))) e_3)

theorem sub_mask1_trunc_lshr_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬15#64 ≥ ↑64 →
    ¬(48#64 ≥ ↑64 ∨
          63#64 ≥ ↑64 ∨
            True ∧ signExtend 64 (truncate 8 ((x <<< 48#64).sshiftRight' 63#64)) ≠ (x <<< 48#64).sshiftRight' 63#64 ∨
              True ∧ (truncate 8 ((x <<< 48#64).sshiftRight' 63#64)).saddOverflow 10#8 = true) →
      10#8 - (truncate 8 (x >>> 15#64) &&& 1#8) = truncate 8 ((x <<< 48#64).sshiftRight' 63#64) + 10#8

theorem bools2_logical_commute1_and1_thm.extracted_1._3 : ∀ (x x_1 : BitVec 1),
  ¬x_1 &&& x = 1#1 → ¬x ^^^ 1#1 = 1#1 → x = 1#1 → 0#1 = x_1

theorem test15_proof : test15_before ⊑ test15_after

theorem e_939 :
    7 *  ~~~(z &&&  ~~~z) + 2 *  ~~~(z ^^^ t) - 1 * (z ||| t) - 9 *  ~~~(z ||| t) - 6 *  ~~~(z |||  ~~~t) - 6 * (z &&&  ~~~t) = 8 * (z &&& t)

theorem not_sub_eq_not_add :
    ~~~ (x - y) = ~~~x + y

theorem bools_logical_commute1_thm.extracted_1._4 : ∀ (x x_1 : BitVec 1),
  x_1 = 1#1 → ¬x = 1#1 → ¬x ^^^ 1#1 = 1#1 → 0#1 = x_1

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

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

theorem exact_lshr_eq_both_equal_thm (e : IntW 8) :
  icmp IntPred.eq (lshr (const? 8 126) e { «exact» := true }) (const? 8 126) ⊑
    icmp IntPred.eq e (const? 8 0)

theorem t3_no_extrause_proof : t3_no_extrause_before ⊑ t3_no_extrause_after

theorem substitute_constant_or_ne_swap_sle_logical_thm (e e_1 : IntW 8) :
  select (icmp IntPred.ne e_1 (const? 8 42)) (const? 1 1) (icmp IntPred.sle e e_1) ⊑
    select (icmp IntPred.ne e_1 (const? 8 42)) (const? 1 1) (icmp IntPred.slt e (const? 8 43))

theorem alive_AndOrXor_2595 : alive_AndOrXor_2595_src ⊑ alive_AndOrXor_2595_tgt

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

theorem main8_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x &&& 64#32 != 0#32) = 1#1 → ofBool (x &&& 192#32 == 0#32) = 1#1 → ¬True → 2#32 = 1#32

theorem or_xor_common_op_commute6_thm (e e_1 e_2 : IntW 8) :
  LLVM.or (LLVM.xor e_2 e_1) (LLVM.or e_1 e) ⊑ LLVM.or (LLVM.or e_1 e) e_2

theorem bools2_logical_commute0_thm.extracted_1._2 : ∀ (x : BitVec 1),
  ¬x = 1#1 → ¬x ^^^ 1#1 = 1#1 → 0#1 = 1#1 → False

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)

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

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

theorem or_logic_or_logic_and_3_thm.extracted_1._3 : ∀ (x x_1 x_2 : BitVec 1), x_2 = 1#1 → True → x_2 ||

theorem shl_sub_lshr_reverse_proof : shl_sub_lshr_reverse_before ⊑ shl_sub_lshr_reverse_after

theorem slt_zero_eq_ne_0_fail2_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬30#32 ≥ ↑32 →
    ofBool (zeroExtend 32 (ofBool (x != 0#32)) == x >>> 30#32) =
      ofBool (x >>> 30#32 == zeroExtend 32 (ofBool (x != 0#32)))

theorem shl_xor_xor_good_mask_proof : shl_xor_xor_good_mask_before ⊑ shl_xor_xor_good_mask_after

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

theorem ashr_lshr_shift_amt_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 mul32_low_proof : mul32_low_before ⊑ mul32_low_after

theorem t1_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬ofBool (x &&& 31#8 == 0#8) = 1#1 → x + 32#8 &&& BitVec.ofInt 8 (-32) = x + 31#8 &&& BitVec.ofInt 8 (-32)

theorem not_match_inconsistent_values_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬(299#64 = 0 ∨ 29#64 = 0 ∨ 64#64 = 0) →
    299#64 = 0 ∨
        29#64 = 0 ∨
          True ∧ (x / 29#64 &&& 63#64).smulOverflow 299#64 = true ∨
            True ∧ (x / 29#64 &&& 63#64).umulOverflow 299#64 = true ∨
              True ∧ (x % 299#64).saddOverflow ((x / 29#64 &&& 63#64) * 299#64) = true ∨
                True ∧ (x % 299#64).uaddOverflow ((x / 29#64 &&& 63#64) * 299#64) = true →
      False

@[simp] theorem Com.rec'_rets (v : HVector Γ.Var t) :
    (Com.rets (d:=d) (eff := eff) v).rec' (motive:=motive) rets var = rets v

theorem ule_swap_and_min_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬ofBool (x ≤ᵤ x_1) = 1#1 → 0#1 = ofBool (x == 0#8)

theorem t5_c2_thm (e e_1 : IntW 8) : sub (sub e_1 e) (const? 8 42) ⊑ add (sub e_1 e) (const? 8 (-42))

theorem trunc_sel_equal_sext_thm.extracted_1._3 : ∀ (x : BitVec 32) (x_1 : BitVec 1),
  x_1 = 1#1 →
    ¬(16#32 ≥ ↑32 ∨ True ∧ x <<< 16#32 >>> 16#32 <<< 16#32 ≠ x <<< 16#32 ∨ 16#32 ≥ ↑32) →
      signExtend 32 (truncate 16 x) = (x <<< 16#32).sshiftRight' 16#32

theorem lowmask_mul_zext_thm (e : IntW 32) (e_1 : IntW 8) :
  LLVM.and (mul (zext 32 e_1) e) (const? 32 255) ⊑ zext 32 (mul e_1 (trunc 8 e))

theorem wide_source_matching_signbits_proof : wide_source_matching_signbits_before ⊑ wide_source_matching_signbits_after

theorem main7b_logical_thm.extracted_1._7 : ∀ (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 == x_1 &&& x) = 1#1 → 0#32 = zeroExtend 32 (ofBool (x != x_1 &&& x))

theorem is_ascii_alphabetic_inverted_thm (e : IntW 32) :
  select (icmp IntPred.ult (add e (const? 32 (-91)) { «nsw» := true, «nuw» := false }) (const? 32 (-26)))
      (icmp IntPred.ult (add e (const? 32 (-123)) { «nsw» := true, «nuw» := false }) (const? 32 (-26)))
      (const? 1 0) ⊑
    icmp IntPred.ult (add (LLVM.and e (const? 32 (-33))) (const? 32 (-91))) (const? 32 (-26))

theorem select_ashr_icmp_bad_proof : select_ashr_icmp_bad_before ⊑ select_ashr_icmp_bad_after

theorem urem_common_dividend_defined_cond_proof : urem_common_dividend_defined_cond_before ⊑ urem_common_dividend_defined_cond_after

theorem add_assoc_2' 
  (hppot : ppot &&& (ppot - 1) = 0)
  (hqpot : qpot &&& (qpot - 1) = 0)
  (hrpot : rpot &&& (rpot - 1) = 0)
  (hspot : spot &&& (spot - 1) = 0)
  (htpot : tpot &&& (tpot - 1) = 0)
  (hupot : upot &&& (upot - 1) = 0)
  (hpmask : pmask = ppot - 1)
  (hqmask : qmask = qpot - 1)
  (hrmask : rmask = rpot - 1)
  (hsmask : smask = spot - 1)
  (htmask : tmask = tpot - 1)
  (humask : umask = upot - 1)
  (hr : UnaryLt rmask qmask) (hs : UnaryLt smask qmask) (hu : UnaryGe umask  tmask)
  :
  --
  (bw' tmask 
    (addMax' (bw' umask (addMax' (bw' pmask a') pmask (bw' rmask b') rmask)) umask (bw' smask c') smask))  =
  (bw' tmask (addMax' (bw' pmask a') pmask (bw' qmask (addMax' (bw' rmask b') rmask (bw' smask c') smask)) qmask))

omit [LawfulBEq A] [Fintype S] [DecidableEq S] in
lemma addOrCreateElem_visited final? (st : worklist.St A S) sa :
    st.addOrCreateState _ _ final? sa |>.2.visited = st.visited

theorem mul_constant_mismatch_wrap_eq_thm (e e_1 : IntW 32) :
  icmp IntPred.eq (mul e_1 (const? 32 54) { «nsw» := true, «nuw» := false })
      (mul e (const? 32 54) { «nsw» := false, «nuw» := true }) ⊑
    icmp IntPred.eq (LLVM.and (LLVM.xor e_1 e) (const? 32 2147483647)) (const? 32 0)

theorem test16_thm (e : IntW 8) : LLVM.and (shl e (const? 8 2)) (const? 8 3) ⊑ const? 8 0

theorem alive_AddSub_1560  (w : Nat)   : alive_AddSub_1560_src w  ⊑ alive_AddSub_1560_tgt w

theorem test0_proof : test0_before ⊑ test0_after

theorem ule_swap_or_not_min_logical_proof : ule_swap_or_not_min_logical_before ⊑ ule_swap_or_not_min_logical_after

theorem p_commutative0_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 32),
  ¬(True ∧ (x_2 &&& x_1 &&& (x &&& (x_2 ^^^ -1#32)) != 0) = true) →
    x_2 &&& x_1 ||

theorem e_603 :
     - 1 *  ~~~(x &&&  ~~~y) - 2 *  ~~~(x &&& y) + 2 * x + 7 *  ~~~(x ^^^ y) + 3 * (x |||  ~~~y) + 5 * (x ||| y) - 7 *  ~~~(x ||| y) - 3 *  ~~~(x |||  ~~~y) - 8 * (x &&&  ~~~y) - 17 * (x &&& y) =  - 1 * y

theorem not_signbit_splat_mask2_thm (e : IntW 16) (e_1 : IntW 8) :
  LLVM.and (sext 16 (ashr e_1 (const? 8 6))) e ⊑ LLVM.and e (sext 16 (ashr e_1 (const? 8 6)))

theorem xor_or_xor_common_op_commute7_proof : xor_or_xor_common_op_commute7_before ⊑ xor_or_xor_common_op_commute7_after

theorem add_signbit_select_shl_proof : add_signbit_select_shl_before ⊑ add_signbit_select_shl_after

theorem test15i_proof : test15i_before ⊑ test15i_after
</all_available_lemmas>

<local_ctx>
import Mathlib.Data.Bool.Basic

import Mathlib.Data.Fin.Basic

import Blase.Fast.BitStream

import Blase.SingleWidth.Defs

open Term

open BitStream in

def Term.eval (t : Term) (vars : List BitStream) : BitStream :=
  match t with
  | var n       => vars.getD n default
  | zero        => BitStream.zero
  | one         => BitStream.one
  | negOne      => BitStream.negOne
  | ofNat n     => BitStream.ofNat n
  | and t₁ t₂   => (t₁.eval vars) &&& (t₂.eval vars)
  | or t₁ t₂    => (t₁.eval vars) ||| (t₂.eval vars)
  | xor t₁ t₂   => (t₁.eval vars) ^^^ (t₂.eval vars)
  | not t       => ~~~(t.eval vars)
  | add t₁ t₂   => (Term.eval t₁ vars) + (Term.eval t₂ vars)
  | sub t₁ t₂   => (Term.eval t₁ vars) - (Term.eval t₂ vars)
  | neg t       => -(Term.eval t vars)


  | shiftL t n  => BitStream.shiftLeft (Term.eval t vars) n

def Predicate.evalEq (t₁ t₂ : BitStream) : BitStream := (t₁ ^^^ t₂).concat false |>.scanOr

def Predicate.evalNeq (t₁ t₂ : BitStream) : BitStream := (t₁.nxor t₂).concat true |>.scanAnd

def Predicate.evalLor (t₁ t₂ : BitStream) : BitStream := (t₁ &&& t₂)

def Predicate.evalLand (t₁ t₂ : BitStream) : BitStream := (t₁ ||| t₂)

def Predicate.evalUlt (t₁ t₂ : BitStream) : BitStream := (~~~ (t₁.borrow t₂)).concat true

def Predicate.evalMsbEq (t₁ t₂ : BitStream) : BitStream :=
  (t₁ ^^^ t₂).concat false

def Predicate.evalSlt (t₁ t₂ : BitStream) : BitStream :=
    (((Predicate.evalUlt t₁ t₂)) ^^^ (Predicate.evalMsbEq t₁ t₂))

open BitStream in

def Predicate.eval (p : Predicate) (vars : List BitStream) : BitStream :=
  match p with
  | .width .eq n => BitStream.falseIffEq n
  | .width .neq n => BitStream.falseIffNeq n
  | .width .lt n => BitStream.falseIffLt n
  | .width .le n => BitStream.falseIffLe n
  | .width .gt n => BitStream.falseIffGt n
  | .width .ge n => BitStream.falseIffGe n
  | lor p q => Predicate.evalLor (p.eval vars) (q.eval vars)
  | land p q => Predicate.evalLand (p.eval vars) (q.eval vars)
  | binary .eq t₁ t₂ => Predicate.evalEq (t₁.eval vars) (t₂.eval vars)
   
  | binary .neq t1 t2 => Predicate.evalNeq (t1.eval vars) (t2.eval vars)
  | binary .ult t₁ t₂ => Predicate.evalUlt (t₁.eval vars) (t₂.eval vars)
  | binary .ule t₁ t₂ =>
     Predicate.evalLor
       (Predicate.evalEq (t₁.eval vars) (t₂.eval vars))
       (Predicate.evalUlt (t₁.eval vars) (t₂.eval vars))
  | binary .slt t₁ t₂ => Predicate.evalSlt (t₁.eval vars) (t₂.eval vars)
  | binary .sle t₁ t₂ => Predicate.evalLor
       (Predicate.evalEq (t₁.eval vars) (t₂.eval vars))
       (Predicate.evalSlt (t₁.eval vars) (t₂.eval vars))

section Predicate

end Predicate
</local_ctx>

<target_theorem>
theorem Predicate.evalUlt_denote_true_iff {w : Nat} (a b : Term) (vars : List (BitVec w)) :
    evalUlt (a.eval (List.map .ofBitVecSext vars)) (b.eval (List.map .ofBitVecSext vars)) w = true ↔
      (Term.denote w b vars) ≤ (Term.denote w a vars) :=
</target_theorem>

