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
BitVec.sle in Init.Data.BitVec.Basic
BitVec.slt in Init.Data.BitVec.Basic
BitVec.ule in Init.Data.BitVec.Basic
BitVec.adcb in Init.Data.BitVec.Bitblast
Prod in Init.Prelude

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

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

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)

abbrev map (f : Bool → Bool) : BitStream → BitStream :=
  fun x i => f (x i)

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

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 WidthPredicate
| eq
| neq
| lt
| le
| gt
| ge
deriving Repr, Inhabited, Lean.ToExpr

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

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 concat (b : Bool) (x : BitStream) : BitStream
  | 0   => b
  | i+1 => x i

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

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)

@[simp_denote]
def and_llvm_1 := [LV| {
  ^entry (%lhs: i1, %rhs: i1 ):
  %1 = llvm.and %lhs, %rhs : i1
  llvm.return %1 : i1
  }]

def sltu_i32_test : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] where
  lhs := sltu_llvm_i64
  rhs := sltu_riscv_i64

def shl_sub_lshr_reverse_no_nsw_before := [llvm|
{
^0(%arg133 : i32, %arg134 : i32, %arg135 : i32):
  %0 = llvm.shl %arg133, %arg134 overflow<nuw> : i32
  %1 = llvm.sub %arg135, %0 overflow<nuw> : i32
  %2 = llvm.lshr exact %1, %arg134 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

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

def mkWidthFSM (wcard : Nat) (tcard : Nat) (bcard : Nat) (ncard icard : Nat) (pcard : Nat) (w : Nondep.WidthExpr) :
    (NatFSM wcard tcard bcard ncard icard pcard w) :=
  match w with
  | .const nat => {
      toFsm := (FSM.trueUptoExcluding nat).map Fin.elim0
    }
  | .var wnat =>
    if h : wnat < wcard then
      { toFsm :=
        composeUnaryAux FSM.scanAnd (FSM.var' (StateSpace.widthVar ⟨wnat, h⟩))
        
      }
    else
      { toFsm := FSM.zero' } 
  | .min v w =>
      { toFsm :=
        (mkWidthFSM wcard tcard bcard ncard icard pcard v).toFsm &&& (mkWidthFSM wcard tcard bcard ncard icard pcard w).toFsm
      }
  | .max v w =>
        { toFsm :=
        (mkWidthFSM wcard tcard bcard ncard icard pcard v).toFsm ||| (mkWidthFSM wcard tcard bcard ncard icard pcard w).toFsm
      }
  | .addK v k =>
    { toFsm :=
        composeUnaryAux (FSM.repeatN true k)  (mkWidthFSM wcard tcard bcard ncard icard pcard v).toFsm
    }
  | .kadd k v =>
    { toFsm :=
        composeUnaryAux (FSM.repeatN true k)  (mkWidthFSM wcard tcard bcard ncard icard pcard v).toFsm
    }

def Com.outContextHom (com : Com d Γ eff t) : Γ.Hom com.outContext :=
  com.outContextDiff.toHom

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

partial def collectTerm (state : CollectState) (e : Expr) :
     SolverM (MultiWidth.Nondep.Term × CollectState) := do
  match_expr e with
  | BitVec.ofBool bExpr =>
      let (b, state) ← collectBoolTerm state bExpr
      return (.bvOfBool b, state)
  | BitVec.ofNat wExpr nExpr =>
    let (w, state) ← collectWidthExpr state wExpr
    if let some n ← getNatValue? nExpr then
      return (.ofNat w n, state)
    else
      mkAtom
  | HAdd.hAdd _bv _bv _bv _inst a b =>
    match_expr _bv with
    | BitVec w =>
      let (w, state) ← collectWidthExpr state w
      let (ta, state) ← collectTerm state a
      let (tb, state) ← collectTerm state b
      return (.add w ta tb, state)
    | _ => mkAtom
  | BitVec.zeroExtend _w v x =>
      let (v, state) ← collectWidthExpr state v
      let (x, state) ← collectTerm state x
      return (.zext x v, state)
  | BitVec.setWidth _w v x =>
      let (v, state) ← collectWidthExpr state v
      let (x, state) ← collectTerm state x
      return (.setWidth x v, state)
  | BitVec.signExtend _w v x =>
      let (v, state) ← collectWidthExpr state v
      let (x, state) ← collectTerm state x
      return (.sext x v, state)
  | HXor.hXor _bv _bv _bv _inst a b =>
    match_expr _bv with
    | BitVec w =>
      let (w, state) ← collectWidthExpr state w
      let (ta, state) ← collectTerm state a
      let (tb, state) ← collectTerm state b
      return (.bxor w ta tb, state)
    | _ => mkAtom
  | HAnd.hAnd _bv _bv _bv _inst a b =>
    match_expr _bv with
    | BitVec w =>
      let (w, state) ← collectWidthExpr state w
      let (ta, state) ← collectTerm state a
      let (tb, state) ← collectTerm state b
      return (.band w ta tb, state)
    | _ => mkAtom
  | HOr.hOr _bv _bv _bv _inst a b =>
    match_expr _bv with
    | BitVec w =>
      let (w, state) ← collectWidthExpr state w
      let (ta, state) ← collectTerm state a
      let (tb, state) ← collectTerm state b
      return (.bor w ta tb, state)
    | _ => mkAtom
  | Complement.complement bv _inst a =>
    match_expr bv with
    | BitVec w =>
      let (w, state) ← collectWidthExpr state w
      let (ta, state) ← collectTerm state a
      return (.bnot w ta, state)
    | _ => mkAtom
  | HShiftLeft.hShiftLeft _bv _nat _bv _inst a n =>
    match_expr _bv with
    | BitVec w =>
      match_expr _nat with
      | Nat =>
        let (w, state) ← collectWidthExpr state w
        let (ta, state) ← collectTerm state a
        if let some nn ← getNatValue? n then
          return (.shiftl w ta nn, state)
        else
          mkAtom
      | _ => mkAtom
    | _ => mkAtom
  | _ => mkAtom
  where
    mkAtom := do
      let (t, state) ← collectBVAtom state e
      return (t, state)

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

def buggy_ISEL_pattern : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] where
  lhs:= original_sdiv_srem
  rhs:= combined_sdiv_srem
  correct := by admit /- proof elided -/

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

def or? {w : Nat} (x y : BitVec w) : IntW w :=
  .value <| x ||| y

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 scalar_i64_lshr_and_signbit_eq_before := [llvm|
{
^0(%arg29 : i64, %arg30 : i64):
  %0 = llvm.mlir.constant(-9223372036854775808) : i64
  %1 = llvm.mlir.constant(0) : i64
  %2 = llvm.lshr %arg29, %arg30 : i64
  %3 = llvm.and %2, %0 : i64
  %4 = llvm.icmp "eq" %3, %1 : i64
  "llvm.return"(%4) : (i1) -> ()
}
]

def xor_lshr_multiuse_after := [llvm|
{
^0(%arg596 : i8, %arg597 : i8, %arg598 : i8, %arg599 : i8):
  %0 = llvm.lshr %arg596, %arg599 : i8
  %1 = llvm.xor %0, %arg598 : i8
  %2 = llvm.xor %arg596, %arg597 : i8
  %3 = llvm.lshr %2, %arg599 : i8
  %4 = llvm.xor %3, %arg598 : i8
  %5 = llvm.sdiv %1, %4 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

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

def p_constmask_before := [llvm|
{
^0(%arg49 : i32, %arg50 : i32):
  %0 = llvm.mlir.constant(65280 : i32) : i32
  %1 = llvm.mlir.constant(-65281 : i32) : i32
  %2 = llvm.and %arg49, %0 : i32
  %3 = llvm.and %arg50, %1 : i32
  %4 = llvm.add %2, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def test3_before := [llvm|
{
^0(%arg0 : i59, %arg1 : i1):
  %0 = llvm.mlir.constant(70368744177664 : i59) : i59
  %1 = llvm.mlir.constant(4096 : i59) : i59
  %2 = "llvm.select"(%arg1, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i59, i59) -> i59
  %3 = llvm.urem %arg0, %2 : i59
  "llvm.return"(%3) : (i59) -> ()
}
]

def and_signbit_select_lshr_after := [llvm|
{
^0(%arg30 : i32, %arg31 : i1):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(16776960 : i32) : i32
  %2 = llvm.lshr %arg30, %0 : i32
  %3 = llvm.and %2, %1 : i32
  %4 = "llvm.select"(%arg31, %3, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

def a_false_implies_b_true2_after := [llvm|
{
^0(%arg12 : i8, %arg13 : i1, %arg14 : i1):
  %0 = llvm.mlir.constant(10 : i8) : i8
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.icmp "ugt" %arg12, %0 : i8
  %3 = "llvm.select"(%2, %1, %arg13) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

def trunc_signed_nsw_after := [llvm|
{
^0(%arg50 : i16, %arg51 : i16):
  %0 = llvm.icmp "slt" %arg50, %arg51 : i16
  "llvm.return"(%0) : (i1) -> ()
}
]

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

def test9_after := [llvm|
{
^0(%arg111 : i32, %arg112 : i32):
  %0 = llvm.or %arg111, %arg112 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def composeQuinaryAux' (p : FSM (Fin 5)) (q₀ q₁ q₂ q₃ q₄: FSM α) : FSM α :=
  p.compose (α)
    (λ _ => α)
    (λ _ i => i)
    (λ v =>
      v.cases q₀ fun v =>
        v.cases q₁ fun v =>
          v.cases q₂ fun v =>
            v.cases q₃ fun v =>
              v.cases q₄ fun v => v.elim0)

def ne_21_after := [llvm|
{
^0(%arg72 : i32, %arg73 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.lshr %arg72, %0 : i32
  %2 = llvm.trunc %1 : i32 to i16
  %3 = llvm.lshr %arg73, %0 : i32
  %4 = llvm.trunc %3 : i32 to i16
  %5 = llvm.icmp "ne" %2, %4 : i16
  "llvm.return"(%5) : (i1) -> ()
}
]

def p0_before := [llvm|
{
^0(%arg30 : i8, %arg31 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.shl %0, %arg31 : i8
  %2 = llvm.xor %1, %0 : i8
  %3 = llvm.and %2, %arg30 : i8
  %4 = llvm.icmp "ne" %3, %arg30 : i8
  "llvm.return"(%4) : (i1) -> ()
}
]

def masked_or_allones_before := [llvm|
{
^0(%arg127 : i32):
  %0 = llvm.mlir.constant(7 : i32) : i32
  %1 = llvm.mlir.constant(39 : i32) : i32
  %2 = llvm.and %arg127, %0 : i32
  %3 = llvm.icmp "eq" %2, %0 : i32
  %4 = llvm.and %arg127, %1 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.or %3, %5 : i1
  "llvm.return"(%6) : (i1) -> ()
}
]

instance : ToString FVarId where
  toString f := s! "{f.name}"

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

def Term.denote {w : Nat} (t : Term) (xs : Env w) : Int :=
  t.c * t.f.denote xs

def xor_to_xor2_after := [llvm|
{
^0(%arg83 : i32, %arg84 : i32):
  %0 = llvm.xor %arg83, %arg84 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def test6_before := [llvm|
{
^0(%arg27 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(-1073741824) : i64
  %2 = llvm.ashr %arg27, %0 : i32
  %3 = llvm.sext %2 : i32 to i64
  %4 = llvm.add %3, %1 : i64
  "llvm.return"(%4) : (i64) -> ()
}
]

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

def zext_sext_add_icmp_eq_1_after := [llvm|
{
^0(%arg72 : i1, %arg73 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.xor %arg73, %0 : i1
  %2 = llvm.and %arg72, %1 : i1
  "llvm.return"(%2) : (i1) -> ()
}
]

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

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

def scalar_i16_lshr_and_signbit_eq_before := [llvm|
{
^0(%arg33 : i16, %arg34 : i16):
  %0 = llvm.mlir.constant(-32768 : i16) : i16
  %1 = llvm.mlir.constant(0 : i16) : i16
  %2 = llvm.lshr %arg33, %arg34 : i16
  %3 = llvm.and %2, %0 : i16
  %4 = llvm.icmp "eq" %3, %1 : i16
  "llvm.return"(%4) : (i1) -> ()
}
]

def n0_before := [llvm|
{
^0(%arg4 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.and %arg4, %0 : i8
  %2 = llvm.icmp "ult" %1, %arg4 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def ashr_eq_exact_before := [llvm|
{
^0(%arg173 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.mlir.constant(10 : i8) : i8
  %2 = llvm.ashr exact %arg173, %0 : i8
  %3 = llvm.icmp "eq" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def bitwise_and_logical_and_icmps_comm3_before := [llvm|
{
^0(%arg223 : i8, %arg224 : i8, %arg225 : 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" %arg224, %0 : i8
  %5 = llvm.and %arg223, %1 : i8
  %6 = llvm.shl %1, %arg225 : i8
  %7 = llvm.and %arg223, %6 : i8
  %8 = llvm.icmp "ne" %5, %2 : i8
  %9 = llvm.icmp "ne" %7, %2 : i8
  %10 = "llvm.select"(%8, %4, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %11 = llvm.and %9, %10 : i1
  "llvm.return"(%11) : (i1) -> ()
}
]

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

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

def test_sub_nuw_nsw__all_are_safe_after := [llvm|
{
^0(%arg31 : i32):
  %0 = llvm.mlir.constant(255 : i32) : i32
  %1 = llvm.mlir.constant(-254 : i32) : i32
  %2 = llvm.and %arg31, %0 : i32
  %3 = llvm.sub %1, %2 overflow<nsw,nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def lshrugt_02_01_after := [llvm|
{
^0(%arg398 : i4):
  %0 = llvm.mlir.constant(0 : i4) : i4
  %1 = llvm.icmp "slt" %arg398, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

def test15_before := [llvm|
{
^0(%arg172 : i32, %arg173 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg173, %0 : i32
  %2 = llvm.xor %arg172, %0 : i32
  %3 = llvm.and %arg172, %1 : i32
  %4 = llvm.and %2, %arg173 : i32
  %5 = llvm.xor %3, %4 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def ashrslt_01_08_before := [llvm|
{
^0(%arg261 : i4):
  %0 = llvm.mlir.constant(1 : i4) : i4
  %1 = llvm.mlir.constant(-8 : i4) : i4
  %2 = llvm.ashr %arg261, %0 : i4
  %3 = llvm.icmp "slt" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

def add_of_mul_before := [llvm|
{
^0(%arg4 : i8, %arg5 : i8, %arg6 : i8):
  %0 = llvm.mul %arg4, %arg5 overflow<nsw> : i8
  %1 = llvm.mul %arg4, %arg6 overflow<nsw> : i8
  %2 = llvm.add %0, %1 overflow<nsw> : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def sub_ashr_or_i32_before := [llvm|
{
^0(%arg35 : i32, %arg36 : i32):
  %0 = llvm.mlir.constant(31 : i32) : i32
  %1 = llvm.sub %arg36, %arg35 overflow<nsw> : i32
  %2 = llvm.ashr %1, %0 : i32
  %3 = llvm.or %2, %arg35 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

List 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
BitVec.eq_of_getLsbD_eq in Init.Data.BitVec.Bootstrap
Bool.not_eq_false in Init.SimpLemmas
BitVec.eq_of_toInt_eq in Init.Data.BitVec.Lemmas
Bool.false_eq_true in Init.Data.Bool
Bool.not_eq_true in Init.SimpLemmas
Bool.not_false in Init.SimpLemmas
Bool.not_true in Init.SimpLemmas
decide_false in Init.Core
decide_true in Init.Core
true_and in Init.SimpLemmas
BitVec.neg_one_eq_allOnes in Init.Data.BitVec.Lemmas
Bool.true_and in Init.SimpLemmas
BitVec.msb_eq_getLsbD_last in Init.Data.BitVec.Lemmas
BitVec.le_def in Init.Data.BitVec.Lemmas
BitVec.slt_eq_ult in Init.Data.BitVec.Lemmas

@[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 scanOr_true_iff (s : BitStream) (n : Nat)
    : s.scanOr n = true ↔ ∃ (i : Nat), (i ≤ n) ∧ s i = true

theorem scanOr_false_iff (s : BitStream) (n : Nat) : s.scanOr n = false ↔ ∀ (i : Nat), (hi : i ≤ n) → s i = false

@[simp]
theorem scanOr_succ (s : BitStream) : scanOr s (n+1) = ((s.scanOr n) || s (n + 1))

theorem scanAnd_true_iff (s : BitStream) (n : Nat) :
    s.scanAnd n = true ↔ ∀ (i : Nat), (hi : i ≤ n) → s i = true

@[simp] theorem scanAnd_succ (s : BitStream) : scanAnd s (n+1) = ((s.scanAnd n) && s (n + 1))

theorem scanAnd_false_iff (s : BitStream) (n : Nat)
    : s.scanAnd n = false ↔ ∃ (i : Nat), (i ≤ n) ∧ s i = false

@[simp] theorem and_eq : (x &&& y) i = (x i && y i)

@[simp] theorem getLsbD_toBitVec (w : Nat) (x : BitStream) :
    (x.toBitVec w).getLsbD i = ((decide (i < w)) && x i)

@[simp] theorem xor_eq : (x ^^^ y) i = (xor (x i) (y i))

theorem test53_proof : test53_before ⊑ test53_after

theorem sgt_swap_and_not_min_commute_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 != BitVec.ofInt 8 (-128)) &&& ofBool (x <ₛ x_1) = ofBool (x <ₛ x_1)

theorem sub_inc_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), x_1 - (x + 1#8) = x_1 + (x ^^^ -1#8)

theorem t_0_10_proof : t_0_10_before ⊑ t_0_10_after

theorem fold_icmp_shl_nuw_c1_proof : fold_icmp_shl_nuw_c1_before ⊑ fold_icmp_shl_nuw_c1_after

theorem src_x_and_nmask_slt_thm (e e_1 : IntW 8) :
  icmp IntPred.slt (LLVM.and e_1 (shl (const? 8 (-1)) e)) (shl (const? 8 (-1)) e) ⊑
    icmp IntPred.sgt (shl (const? 8 (-1)) e { «nsw» := true, «nuw» := false }) e_1

theorem main5c_like_logical_thm.extracted_1._12 : ∀ (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 0#1

theorem PR42691_1_proof : PR42691_1_before ⊑ PR42691_1_after

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

theorem sle_or_min_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 ≤ₛ x) = 1#1 → 1#1 = ofBool (x_1 ≤ₛ x)

theorem icmp_sgt10_proof : icmp_sgt10_before ⊑ icmp_sgt10_after

theorem trunc_signed_nsw_sext_thm (e : IntW 8) (e_1 : IntW 32) :
  icmp IntPred.slt (trunc 16 e_1 { «nsw» := true, «nuw» := false }) (sext 16 e) ⊑
    icmp IntPred.slt e_1 (sext 32 e)

theorem e_2385 :
    4 * ((d &&&  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) - 1 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f)) - 2 * (f ^^^  ~~~(d &&& (e ||| f))) - 2 * (e |||  ~~~(d ||| f)) - 1 *  ~~~( ~~~d ||| ( ~~~e &&& f)) - 1 * ( ~~~(d |||  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) - 6 * (e ^^^ (d &&& (e ^^^ f))) - 6 * (d ^^^ f) + 2 * (e ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) - 7 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) + 5 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) + 3 * ((d ||| e) &&& (e ^^^ f)) - 11 * ((d &&& f) ^^^ (d ^^^ ( ~~~e &&& f))) - 3 * (f ^^^ (d ||| ( ~~~e &&& f))) - 7 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) + 4 * (f &&& (d ^^^ e)) - 5 * (e ^^^  ~~~(d &&&  ~~~f)) - 2 * ( ~~~(d ^^^ e) ||| (d ^^^ f)) - 3 * (d &&& f) - 5 * ( ~~~d &&& (e ^^^ f)) + 1 * ((e &&&  ~~~f) ^^^ (d ||| (e ^^^ f))) + 7 *  ~~~(d &&&  ~~~d) - 7 * ((d &&& e) ^^^ (e |||  ~~~f)) - 6 * (e ^^^ (d ||| (e ^^^ f))) - 3 *  ~~~( ~~~d &&& (e ^^^ f)) + 7 * (e ^^^  ~~~(d &&& (e &&& f))) + 2 *  ~~~e + 4 *  ~~~(d ||| (e &&& f)) + 5 * (e ^^^ ( ~~~d ||| (e &&& f))) - 7 * ((e &&& f) ^^^  ~~~( ~~~d &&& (e ^^^ f))) + 2 * ( ~~~d &&& ( ~~~e ||| f)) - 3 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) + 1 * ((d ||| e) &&&  ~~~(e ^^^ f)) + 1 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) + 3 * (e ^^^  ~~~( ~~~d ||| (e &&& f))) - 2 * (d ||| (e &&& f)) - 2 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 11 * (e &&&  ~~~f) + 7 * (e ^^^ f) - 2 * (d ||| e) - 1 * (f ^^^ (d &&&  ~~~e)) + 3 * (e ^^^ ( ~~~d &&& (e ||| f))) - 11 * ((d &&& e) ^^^  ~~~(d ^^^ ( ~~~e ||| f))) + 4 * (f ^^^ (d ||| (e &&& f))) + 1 * (e ^^^ (d ||| (e ||| f))) + 5 * (e ^^^  ~~~(d |||  ~~~f)) + 1 * (e ||| (d &&&  ~~~f)) + 3 *  ~~~(e ||| f) - 2 * ( ~~~d ||| (e ^^^ f)) + 1 * ( ~~~(d &&& e) &&&  ~~~(e ^^^ f)) + 1 * (d ||| (e ||| f)) - 6 * (d &&& (e ^^^ f)) + 11 *  ~~~(e &&&  ~~~f) + 11 * (e ^^^ ( ~~~d &&& (e ^^^ f))) + 11 * (e &&& (d ||| f)) + 3 *  ~~~(d ^^^ (e ^^^ f)) + 5 *  ~~~(d &&& (e ||| f)) - 5 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) - 2 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 1 * (e ^^^ (d &&& ( ~~~e ||| f))) + 2 * ((d ^^^ e) |||  ~~~(d ^^^ f)) - 1 * (e ^^^ (d ||| (e &&& f))) - 11 *  ~~~(d ||| (e ||| f)) + 34 *  ~~~(d ||| ( ~~~e ||| f)) + 15 *  ~~~( ~~~d ||| (e ||| f)) + 19 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 26 * ( ~~~d &&& ( ~~~e &&& f)) - 24 * ( ~~~d &&& (e &&& f)) + 21 * (d &&& ( ~~~e &&& f)) - 33 * (d &&& (e &&& f)) = 1 * (e ^^^  ~~~(d &&& ( ~~~e ||| f)))

theorem ult_to_sgt_thm (e e_1 : IntW 8) :
  icmp IntPred.ult (LLVM.xor e_1 (const? 8 127)) (LLVM.xor e (const? 8 127)) ⊑ icmp IntPred.sgt e_1 e

theorem bitwise_or_bitwise_or_icmps_comm3_proof : bitwise_or_bitwise_or_icmps_comm3_before ⊑ bitwise_or_bitwise_or_icmps_comm3_after

theorem a_false_implies_b_false_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 8),
  ¬ofBool (10#8 <ᵤ x_1) = 1#1 → ofBool (20#8 <ᵤ x_1) = 1#1 → False

theorem src_is_mask_shl_lshr_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬(x ≥ ↑8 ∨ x ≥ ↑8) →
    ¬x ≥ ↑8 →
      ofBool (0#8 != (x_1 ^^^ 123#8) &&& ((-1#8) <<< x >>> x ^^^ -1#8)) = ofBool ((-1#8) >>> x <ᵤ x_1 ^^^ 122#8)

theorem positive_trunc_base_logical_thm (e : IntW 32) :
  select (icmp IntPred.sgt (trunc 16 e) (const? 16 (-1)))
      (icmp IntPred.ult (add (trunc 16 e) (const? 16 128)) (const? 16 256)) (const? 1 0) ⊑
    icmp IntPred.eq (LLVM.and e (const? 32 65408)) (const? 32 0)

theorem lt_signed_to_small_negative_proof : lt_signed_to_small_negative_before ⊑ lt_signed_to_small_negative_after

theorem scalar_i32_lshr_and_negC_eq_X_is_constant1_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬x ≥ ↑32 → ofBool (12345#32 >>> x &&& BitVec.ofInt 32 (-8) == 0#32) = ofBool (12345#32 >>> x <ᵤ 8#32)

theorem t9_ashr_exact_flag_preservation_proof : t9_ashr_exact_flag_preservation_before ⊑ t9_ashr_exact_flag_preservation_after

theorem shl_nsw_nuw_add_proof : shl_nsw_nuw_add_before ⊑ shl_nsw_nuw_add_after

theorem factorize4_thm (e e_1 : IntW 32) : sub (mul (shl e_1 (const? 32 1)) e) (mul e e_1) ⊑ mul e_1 e

theorem ult_1_impliesF_eq_1_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (x <ᵤ 1#8) = 1#1 → ofBool (x != 0#8) = 1#1 → False

theorem tryFactorization_add_nuw_mul_nuw_proof : tryFactorization_add_nuw_mul_nuw_before ⊑ tryFactorization_add_nuw_mul_nuw_after

theorem test_and4_logical_proof : test_and4_logical_before ⊑ test_and4_logical_after

theorem eq1 : ∀ (w : Nat) (a : BitVec w), a = a

theorem signExtend_eq (x : BitVec w) : x.signExtend w = x  := sorry

theorem positive_biggerashr_thm (e : IntW 8) :
  shl (ashr e (const? 8 6)) (const? 8 3) ⊑ LLVM.and (ashr e (const? 8 3)) (const? 8 (-8))

theorem land_bor_left1_thm (e e_1 : IntW 1) : LLVM.or (select e_1 e (const? 1 0)) e_1 ⊑ e_1

theorem ashr_lshr2_proof : ashr_lshr2_before ⊑ ashr_lshr2_after

theorem scalar0_thm (e e_1 : IntW 4) :
  LLVM.xor (LLVM.and (LLVM.xor e_1 e) (const? 4 1)) e ⊑
    LLVM.or (LLVM.and e_1 (const? 4 1)) (LLVM.and e (const? 4 (-2))) { «disjoint» := true }

theorem list_perm_trick (x y a b c : List α) :
    y ~ b ++ x → x ~ a ++ c → y ~ a ++ b ++ c

theorem logical_and_not_cond_reuse_proof : logical_and_not_cond_reuse_before ⊑ logical_and_not_cond_reuse_after

theorem or_xor_xor_normal_variant2_proof : or_xor_xor_normal_variant2_before ⊑ or_xor_xor_normal_variant2_after

theorem test82_thm.extracted_1._1 : ∀ (x : BitVec 64), ¬(8#32 ≥ ↑32 ∨ 9#32 ≥ ↑32) → 1#32 ≥ ↑32 → False

theorem main5e_like_logical_thm.extracted_1._1 : ∀ (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 → 0#32 = zeroExtend 32 1#1

theorem sle_swap_and_min_commute_thm (e e_1 : IntW 8) :
  LLVM.and (icmp IntPred.eq e_1 (const? 8 (-128))) (icmp IntPred.sge e e_1) ⊑
    icmp IntPred.eq e_1 (const? 8 (-128))

theorem masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_2_thm (e : IntW 32) :
  LLVM.or (icmp IntPred.ne (LLVM.and e (const? 32 7)) (const? 32 0))
      (icmp IntPred.eq (LLVM.and e (const? 32 3)) (const? 32 0)) ⊑
    const? 1 1

theorem decideIfZerosAux_correct {arity : Type _} [DecidableEq arity]
    (p : FSM arity) (c : Circuit p.α)
    (hc : ∀ s, c.eval s = true →
      ∃ m y, (p.changeInitCarry s).eval y m = true)
    (hc₂ : ∀ (x : arity → Bool) (s : p.α → Bool),
      (FSM.nextBit p s x).snd = true → Circuit.eval c s = true) :
    decideIfZerosAux p c = true ↔ ∀ n x, p.eval x n = false

theorem test37_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 → ofBool (truncate 8 (x >>> 31#32 ||| 512#32) == 11#8) = 0#1

theorem test59_proof : test59_before ⊑ test59_after

theorem e_1915 :
     - 2 * ( ~~~(a &&&  ~~~b) &&& (b ^^^ c)) - 2 *  ~~~(a &&& (b ^^^ c)) + 4 * (a ^^^ ( ~~~b ||| c)) + 3 *  ~~~(b &&& c) + 1 * ( ~~~(a |||  ~~~b) |||  ~~~(b ^^^ c)) - 5 * (a ||| (b ||| c)) + 2 * ((a ||| b) &&&  ~~~(a ^^^ (b ^^^ c))) - 1 *  ~~~a - 7 *  ~~~(a ^^^ b) + 4 * (b ^^^ (a ||| ( ~~~b ||| c))) - 6 * (b ^^^ ( ~~~a &&& (b ^^^ c))) - 1 * (a ||| b) - 1 * ( ~~~(a &&& b) &&& (b ^^^ c)) - 3 * (c ^^^ ( ~~~a &&& (b ||| c))) - 1 * ( ~~~(a &&& b) &&& (a ^^^ (b ^^^ c))) - 5 * (c ^^^  ~~~(a &&& ( ~~~b ||| c))) + 4 *  ~~~( ~~~a &&& ( ~~~b ||| c)) - 6 * a - 1 * (c ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) + 5 * (b |||  ~~~c) + 2 * (c ||| (a &&& b)) - 1 *  ~~~(a ^^^ c) - 11 * (a &&& c) - 2 * (c ^^^ ( ~~~a &&& ( ~~~b ||| c))) - 1 * ( ~~~(a &&& b) &&&  ~~~(a ^^^ (b ^^^ c))) - 6 * (b &&& (a |||  ~~~c)) - 3 * ((a ^^^ b) &&&  ~~~(a ^^^ c)) - 7 *  ~~~(a ||| ( ~~~b &&& c)) + 11 *  ~~~(a |||  ~~~c) + 4 * (b &&&  ~~~(a ^^^ c)) + 1 * (c |||  ~~~(a |||  ~~~b)) - 1 *  ~~~( ~~~a &&& (b ^^^ c)) + 1 * (c &&& (a |||  ~~~b)) - 3 * (a |||  ~~~c) - 1 * (c &&&  ~~~(a ^^^ b)) + 11 * ( ~~~(a &&&  ~~~b) &&& (a ^^^ (b ^^^ c))) + 2 * (b ^^^  ~~~(a &&& ( ~~~b &&& c))) - 1 * ( ~~~(a ^^^ b) ||| (a ^^^ c)) + 4 * ( ~~~c &&&  ~~~(a ^^^ b)) + 2 *  ~~~(a &&& (b &&& c)) + 7 * (c ^^^ ( ~~~a ||| (b ||| c))) - 5 * (c ^^^ (a ||| (b &&& c))) - 7 * ((a |||  ~~~b) &&&  ~~~(b ^^^ c)) - 11 * ( ~~~b ||| (a ^^^ c)) + 18 *  ~~~(a ||| (b ||| c)) + 23 *  ~~~( ~~~a ||| (b ||| c)) + 27 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 3 * ( ~~~a &&& ( ~~~b &&& c)) + 8 * ( ~~~a &&& (b &&& c)) + 39 * (a &&& (b &&& c)) =  - 35 * (a &&& ( ~~~b &&& c))

theorem logical_and_implies_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x != 0#32) = 1#1 → ofBool (x != 42#32) = ofBool (x != 0#32) &&& ofBool (x != 42#32)

theorem n4_proof : n4_before ⊑ n4_after

theorem select_and_icmp_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), ofBool (x_1 == -1#32) = 1#1 → x_1 &&& x = x

theorem test8_proof : test8_before ⊑ test8_after

theorem slt_zero_ult_i1_fail2_proof : slt_zero_ult_i1_fail2_before ⊑ slt_zero_ult_i1_fail2_after

theorem e_797 :
     - 6 * (z ||| t) - 1 * t - 7 *  ~~~(z ||| t) + 7 * (z &&&  ~~~t) + 8 * (z &&& t) = 1 * z - 7 *  ~~~z

theorem zext_zext_sgt_proof : zext_zext_sgt_before ⊑ zext_zext_sgt_after

theorem lshrult_03_12_exact_proof : lshrult_03_12_exact_before ⊑ lshrult_03_12_exact_after

theorem a_true_implies_b_true2_proof : a_true_implies_b_true2_before ⊑ a_true_implies_b_true2_after

theorem main13_thm (e : IntW 32) :
  select (LLVM.and (icmp IntPred.slt (trunc 16 e) (const? 16 0)) (icmp IntPred.slt (trunc 8 e) (const? 8 0)))
      (const? 32 2) (const? 32 1) ⊑
    select (icmp IntPred.eq (LLVM.and e (const? 32 32896)) (const? 32 32896)) (const? 32 2) (const? 32 1)

theorem f_var0_commutative_and_thm (e e_1 : IntW 32) :
  select (icmp IntPred.eq (LLVM.and e_1 e) (const? 32 0)) (LLVM.and (lshr e (const? 32 1)) (const? 32 1))
      (const? 32 1) ⊑
    zext 32 (icmp IntPred.ne (LLVM.and e (LLVM.or e_1 (const? 32 2))) (const? 32 0))

theorem PR23309v2_proof : PR23309v2_before ⊑ PR23309v2_after

theorem lshrugt_01_07_exact_proof : lshrugt_01_07_exact_before ⊑ lshrugt_01_07_exact_after

@[simp]
theorem BitVec.intCast_eq_ofInt : ((i : Int) : BitVec w) = BitVec.ofInt w i

@[simp]
lemma formula_predicate_term_match {t : Term} :
    t.denote w vars = t.evalNat (vars[·]!)

theorem canonicalize_logic_first_or0_nsw_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(True ∧ x.saddOverflow 112#32 = true) →
    ¬(True ∧ (x ||| 15#32).saddOverflow 112#32 = true) → x + 112#32 ||

theorem subAux_inductive_lemma (i : Nat) :
    a.subAux b i = ⟨(a.addAux b.neg i).1, subCarries? a b i⟩

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

theorem masked_icmps_mask_notallzeros_bmask_mixed_2_proof : masked_icmps_mask_notallzeros_bmask_mixed_2_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_2_after

theorem test_mul_nuw__nuw_is_safe_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x &&& 268435457#32 == 268435456#32) = 1#1 →
    ¬(True ∧ (x &&& 268435457#32).umulOverflow 9#32 = true) →
      BitVec.ofInt 32 (-1879048192) = (x &&& 268435457#32) * 9#32

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

theorem pr33078_2_proof : pr33078_2_before ⊑ pr33078_2_after

theorem zext_sub_proof : zext_sub_before ⊑ zext_sub_after

theorem logical_or_bitwise_or_icmps_comm1_thm.extracted_1._3 : ∀ (x x_1 x_2 : BitVec 8),
  ¬x_1 ≥ ↑8 → ¬ofBool (x_2 &&& 1#8 <<< x_1 == 0#8) = 1#1 → True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8 → False

theorem AvoidCollision_setWidth_setWidth_of_le (x : BitVec w) (h : k ≤ l) :
    (x.setWidth l).setWidth k = x.setWidth k

theorem test_and_ne_a_b_commuted_proof : test_and_ne_a_b_commuted_before ⊑ test_and_ne_a_b_commuted_after

theorem fold_add_udiv_urem_without_noundef_proof : fold_add_udiv_urem_without_noundef_before ⊑ fold_add_udiv_urem_without_noundef_after

theorem lt_signed_to_large_unsigned_proof : lt_signed_to_large_unsigned_before ⊑ lt_signed_to_large_unsigned_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.eval_eq_denote (w : Nat) (p : Predicate) (vars : List (BitVec w)) :
    (p.eval (vars.map .ofBitVecSext) w = false) ↔ p.denote w vars :=
</target_theorem>

