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
BitVec in Init.Prelude
List in Init.Prelude
List.Vector in Mathlib.Data.Vector.Defs
Set in Mathlib.Data.Set.Defs
Fin in Init.Prelude
BitVec.ofNat in Init.Prelude
BitVec.zero in Init.Data.BitVec.Basic
Fin.castLE in Init.Data.Fin.Basic
Fin.last in Init.Data.Fin.Basic
BitVec.iunfoldr in Init.Data.BitVec.Folds
Vector in Init.Data.Vector.Basic
Vector.ofFn in Init.Data.Vector.Basic
Repr in Init.Data.Repr
impl in Mathlib.Deprecated.MLList.BestFirst
Fintype in Mathlib.Data.Fintype.Defs
FinEnum in Mathlib.Data.FinEnum
FinEnum.card in Mathlib.Data.FinEnum
Inhabited in Init.Prelude
Lean.ToExpr in Lean.ToExpr
atom in Leanwuzla.Sexp.Basic
Fin.isValue in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
List.Vector.nil in Mathlib.Data.Vector.Defs
Set.instMembership in Mathlib.Data.Set.Defs
Set.Mem in Mathlib.Data.Set.Defs
List.Vector.get in Mathlib.Data.Vector.Defs

syntax "max" : MLIR.Pretty.uniform_op

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

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

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

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

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

structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

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

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

| shiftL t .. => arity t

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

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

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

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

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

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

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

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

def demorgan_nand_before := [llvm|
{
^0(%arg38 : i8, %arg39 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.xor %arg38, %0 : i8
  %2 = llvm.and %1, %arg39 : i8
  %3 = llvm.xor %2, %0 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def and1_shl1_is_cmp_eq_0_multiuse_before := [llvm|
{
^0(%arg14 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.shl %0, %arg14 : i8
  %2 = llvm.and %1, %0 : i8
  %3 = llvm.add %1, %2 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def in_constant_varx_6_invmask_after := [llvm|
{
^0(%arg39 : i4, %arg40 : i4):
  %0 = llvm.mlir.constant(6 : i4) : i4
  %1 = llvm.xor %arg39, %0 : i4
  %2 = llvm.and %1, %arg40 : i4
  %3 = llvm.xor %2, %arg39 : i4
  "llvm.return"(%3) : (i4) -> ()
}
]

def test15_after := [llvm|
{
^0(%arg44 : i8, %arg45 : i8):
  %0 = llvm.mlir.constant(33 : i8) : i8
  %1 = llvm.xor %arg45, %arg44 : i8
  %2 = llvm.xor %arg44, %arg45 : i8
  %3 = llvm.xor %2, %0 : i8
  %4 = llvm.and %1, %3 : i8
  %5 = llvm.mul %4, %3 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def test19_after := [llvm|
{
^0(%arg7 : i10):
  %0 = llvm.mlir.constant(1 : i3) : i3
  %1 = llvm.mlir.constant(0 : i3) : i3
  %2 = llvm.trunc %arg7 : i10 to i3
  %3 = llvm.and %2, %0 : i3
  %4 = llvm.sub %1, %3 overflow<nsw> : i3
  %5 = llvm.sext %4 : i3 to i10
  "llvm.return"(%5) : (i10) -> ()
}
]

def uadd_sat_flipped_wrong_bounds4_before := [llvm|
{
^0(%arg93 : i32):
  %0 = llvm.mlir.constant(-8 : i32) : i32
  %1 = llvm.mlir.constant(9 : i32) : i32
  %2 = llvm.mlir.constant(-1 : i32) : i32
  %3 = llvm.icmp "uge" %arg93, %0 : i32
  %4 = llvm.add %arg93, %1 : i32
  %5 = "llvm.select"(%3, %2, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

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

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) -> ()
}
]

HPow.hPow in Init.Prelude

def n11_wrong_pred3_before := [llvm|
{
^0(%arg8 : i8, %arg9 : i8):
  %0 = llvm.add %arg8, %arg9 : i8
  %1 = llvm.icmp "ne" %0, %arg9 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def smear_sign_and_widen_after := [llvm|
{
^0(%arg169 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.ashr %arg169, %0 : i8
  %2 = llvm.zext %1 : i8 to i32
  "llvm.return"(%2) : (i32) -> ()
}
]

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

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

def alive_AndOrXor_2627_tgt  (w : Nat)  :=
[llvm( w )| {
^bb0(%a : _, %c : _, %b : _):
  %v1 = llvm.mlir.constant -1
  %v2 = llvm.xor %a, %v1
  %v3 = llvm.and %v2, %b
  %v4 = llvm.xor %a, %c
  %v5 = llvm.or %a, %b
  %v6 = llvm.xor %v3, %c
  llvm.return %v6
}]

def alive_Select_859'_src :=
[sllvm| {
^bb0(%a : i1, %b : i1):
  %v1 = llvm.mlir.constant -1 :  i1
  %v2 = llvm.xor %a, %v1 : i1
  %v3 = llvm.select %a,%b, %v2 : i1
  llvm.return %v3 : i1
}]

def BuilderM.isOk {α : Type} (x : BuilderM d α) : Bool :=
  match x.run [] with
  | Except.ok _ => true
  | Except.error _ => false

def negate_lowbitmask_before := [llvm|
{
^0(%arg48 : i8, %arg49 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.and %arg48, %0 : i8
  %3 = llvm.sub %1, %2 : i8
  %4 = llvm.and %3, %arg49 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

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

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

def sgt_and_min_before := [llvm|
{
^0(%arg352 : i9, %arg353 : i9):
  %0 = llvm.mlir.constant(-256 : i9) : i9
  %1 = llvm.icmp "sgt" %arg352, %arg353 : i9
  %2 = llvm.icmp "eq" %arg352, %0 : i9
  %3 = llvm.and %1, %2 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def RegionSignature.map (f : Ty → Ty') : RegionSignature Ty → RegionSignature Ty' :=
  List.map fun ⟨Γ, ty⟩ => (Γ.map f, ty.map f)

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

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

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

def zero_sign_bit2_before := [llvm|
{
^0(%arg29 : i16, %arg30 : i16):
  %0 = llvm.mlir.constant(32767 : i16) : i16
  %1 = llvm.and %arg29, %0 : i16
  %2 = llvm.and %arg30, %0 : i16
  %3 = llvm.add %1, %2 : i16
  "llvm.return"(%3) : (i16) -> ()
}
]

def inputSource : DCOp.TokenStream := ofList [some (), none, some (), some (), none]

def ashr_overshift_before := [llvm|
{
^0(%arg6 : i32):
  %0 = llvm.mlir.constant(15 : i32) : i32
  %1 = llvm.mlir.constant(17 : i32) : i32
  %2 = llvm.ashr %arg6, %0 : i32
  %3 = llvm.ashr %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def lshrult_01_04_before := [llvm|
{
^0(%arg363 : i4):
  %0 = llvm.mlir.constant(1 : i4) : i4
  %1 = llvm.mlir.constant(4 : i4) : i4
  %2 = llvm.lshr %arg363, %0 : i4
  %3 = llvm.icmp "ult" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def bad_shl2_sub_i32_before := [llvm|
{
^0(%arg9 : i32):
  %0 = llvm.mlir.constant(31 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.sub %arg9, %0 : i32
  %3 = llvm.shl %1, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def test2_after := [llvm|
{
^0(%arg6 : i32, %arg7 : i32, %arg8 : i32):
  %0 = llvm.xor %arg7, %arg6 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

abbrev Width.mvar : Fin φ → Width φ := ConcreteOrMVar.mvar

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

def or_i32_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] where
  lhs := or_llvm_i32
  rhs := or_riscv_i32

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

def test2_before := [llvm|
{
^0(%arg18 : i8):
  %0 = llvm.mlir.constant(7 : i32) : i32
  %1 = llvm.mlir.constant(3 : i32) : i32
  %2 = llvm.zext %arg18 : i8 to i32
  %3 = llvm.add %2, %0 : i32
  %4 = llvm.ashr %3, %1 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

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

def negate_select_of_op_vs_negated_op_nsw_commuted_after := [llvm|
{
^0(%arg18 : i8, %arg19 : i8, %arg20 : i1):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %0, %arg18 : i8
  %2 = "llvm.select"(%arg20, %1, %arg18) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %3 = llvm.add %2, %arg19 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def sra  {Γ : Ctxt _} (e₁ e₂: Ctxt.Var Γ .bv) : Expr RV64 Γ .pure [.bv]  :=
  Expr.mk
    (op := Op.sll)
    (eff_le := by admit /- proof elided -/
    )
    (ty_eq := by admit /- proof elided -/
    )
    (args := .cons e₁ <| .cons e₂ .nil)
    (regArgs := HVector.nil)

def test16_after := [llvm|
{
^0(%arg38 : i32, %arg39 : i32):
  %0 = llvm.mlir.constant(1431655766 : i32) : i32
  %1 = llvm.or %arg38, %0 : i32
  %2 = llvm.sub %arg39, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def handshakeAdd := [HSxComb_com| {
  ^entry(%a: !Stream_BitVec_32, %b: !Stream_BitVec_32):
    %add1 = "HSxComb.add" (%a, %a) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream_BitVec_32)
    %syncAdd = "HSxComb.sync" (%add1, %b) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream2_BitVec_32)
    %syncAdd1 = "HSxComb.snd" (%syncAdd) : (!Stream2_BitVec_32) -> !Stream_BitVec_32
    %add2 = "HSxComb.add" (%syncAdd1, %a) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream_BitVec_32)
    "return" (%add2) : (!Stream_BitVec_32) -> ()
  }]

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

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

let specialConstants : Std.HashMap (GenBVExpr bitwidth) BVExpr.PackedBitVec := Std.HashMap.ofList [
      ((one bitwidth), {bv := BitVec.ofNat bitwidth 1}),
      ((minusOne bitwidth), {bv := BitVec.ofInt bitwidth (-1)}),
      (GenBVExpr.var widthId, {bv := BitVec.ofNat bitwidth bitwidth})]

def canonicalize_icmp_sge_2 : LLVMPeepholeRewriteRefine 1 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant 2 : i64
      %1 = llvm.icmp.sge %c, %x : i64
      llvm.return %1 : i1
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant 2 : i64
      %1 = llvm.icmp.sle %x, %c : i64
      llvm.return %1 : i1
  }]

def lshr_sub_after := [llvm|
{
^0(%arg77 : i8, %arg78 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(3 : i8) : i8
  %2 = llvm.srem %arg77, %0 : i8
  %3 = llvm.lshr %arg78, %1 : i8
  %4 = llvm.sub %2, %3 overflow<nsw> : i8
  %5 = llvm.shl %4, %1 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def scalar_i64_signbit_lshr_and_eq_after := [llvm|
{
^0(%arg29 : i64, %arg30 : i64):
  %0 = llvm.mlir.constant(-9223372036854775808) : i64
  %1 = llvm.mlir.constant(0) : i64
  %2 = llvm.lshr exact %0, %arg30 : i64
  %3 = llvm.and %2, %arg29 : i64
  %4 = llvm.icmp "eq" %3, %1 : i64
  "llvm.return"(%4) : (i1) -> ()
}
]

instance : DecidableEq VarName :=

def differentconsts_after := [llvm|
{
^0(%arg29 : i32, %arg30 : i16, %arg31 : i16):
  %0 = llvm.mlir.constant(-16 : i32) : i32
  %1 = llvm.mlir.constant(127 : i32) : i32
  %2 = llvm.mlir.constant(256 : i16) : i16
  %3 = llvm.mlir.constant(-1 : i16) : i16
  %4 = llvm.icmp "slt" %arg29, %0 : i32
  %5 = llvm.icmp "sgt" %arg29, %1 : i32
  %6 = llvm.trunc %arg29 : i32 to i16
  %7 = "llvm.select"(%4, %2, %6) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i16, i16) -> i16
  %8 = "llvm.select"(%5, %3, %7) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i16, i16) -> i16
  "llvm.return"(%8) : (i16) -> ()
}
]

def mullo_variant3_before := [llvm|
{
^0(%arg4 : i64, %arg5 : i64):
  %0 = llvm.mlir.constant(4294967295) : i64
  %1 = llvm.mlir.constant(32) : i64
  %2 = llvm.and %arg4, %0 : i64
  %3 = llvm.lshr %arg4, %1 : i64
  %4 = llvm.and %arg5, %0 : i64
  %5 = llvm.lshr %arg5, %1 : i64
  %6 = llvm.mul %4, %2 overflow<nuw> : i64
  %7 = llvm.mul %4, %3 overflow<nuw> : i64
  %8 = llvm.mul %5, %2 overflow<nuw> : i64
  %9 = llvm.add %8, %7 : i64
  %10 = llvm.shl %9, %1 : i64
  %11 = llvm.add %10, %6 : i64
  "llvm.return"(%11) : (i64) -> ()
}
]

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

if preconditionCandidates.size > origCandidatesSize then
            validCandidates ← filterCandidatePredicates bvLogicalExpr preconditionCandidates visited
            match validCandidates with
            | [] => visited := preconditionCandidates
            | _ => return validCandidates

def test12commuted_after := [llvm|
{
^0(%arg87 : i32, %arg88 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg87, %arg88 : i32
  %2 = llvm.xor %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def args : BasicBlock Op T → List VarName
  | ⟨_, args, _⟩ => args

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

def and_two_ranges_to_mask_and_range_no_add_on_one_range_before := [llvm|
{
^0(%arg249 : i16):
  %0 = llvm.mlir.constant(12 : i16) : i16
  %1 = llvm.mlir.constant(16 : i16) : i16
  %2 = llvm.mlir.constant(28 : i16) : i16
  %3 = llvm.icmp "uge" %arg249, %0 : i16
  %4 = llvm.icmp "ult" %arg249, %1 : i16
  %5 = llvm.icmp "uge" %arg249, %2 : i16
  %6 = llvm.or %4, %5 : i1
  %7 = llvm.and %3, %6 : i1
  "llvm.return"(%7) : (i1) -> ()
}
]

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

def or_xor_common_op_commute5_after := [llvm|
{
^0(%arg120 : i8, %arg121 : i8, %arg122 : i8):
  %0 = llvm.or %arg121, %arg120 : i8
  %1 = llvm.or %0, %arg122 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def trunc_equality_nsw_zext_after := [llvm|
{
^0(%arg16 : i32, %arg17 : i8):
  %0 = llvm.zext %arg17 : i8 to i32
  %1 = llvm.icmp "ne" %arg16, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def badimm4_before := [llvm|
{
^0(%arg25 : i16):
  %0 = llvm.mlir.constant(8 : i16) : i16
  %1 = llvm.mlir.constant(7 : i8) : i8
  %2 = llvm.mlir.constant(15 : i16) : i16
  %3 = llvm.mlir.constant(126 : i8) : i8
  %4 = llvm.lshr %arg25, %0 : i16
  %5 = llvm.trunc %4 : i16 to i8
  %6 = llvm.trunc %arg25 : i16 to i8
  %7 = llvm.ashr %6, %1 : i8
  %8 = llvm.icmp "eq" %7, %5 : i8
  %9 = llvm.ashr %arg25, %2 : i16
  %10 = llvm.trunc %9 : i16 to i8
  %11 = llvm.xor %10, %3 : i8
  %12 = "llvm.select"(%8, %6, %11) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%12) : (i8) -> ()
}
]

checkTimeout
</all_available_defs>

<all_available_lemmas>
Nat.add_comm in Init.Data.Nat.Basic
Fin.val_last in Init.Data.Fin.Lemmas
Nat.mod_eq_of_lt in Init.Data.Nat.Div.Basic
Set.mem_setOf_eq in Mathlib.Data.Set.Operations
le_add_iff_nonneg_right in Mathlib.Algebra.Order.Monoid.Unbundled.Basic
zero_le in Mathlib.Algebra.Order.Monoid.Canonical.Defs
Set.compl_def in Mathlib.Order.BooleanAlgebra.Set
Set.mem_image in Mathlib.Data.Set.Operations
Set.mem_inter_iff in Mathlib.Data.Set.Basic
Set.preimage_setOf_eq in Mathlib.Data.Set.Image

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

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

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

theorem e_247 :
    1 *  ~~~y + 1 *  ~~~(x &&&  ~~~y) + 3 *  ~~~x - 11 * x - 12 *  ~~~(x ||| y) - 4 *  ~~~(x |||  ~~~y) + 3 * (x &&& y) =  - 7 *  ~~~(x ^^^ y) - 10 * (x &&&  ~~~y)

theorem add_shl_same_amount_partial_nsw1_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 6),
  ¬(True ∧ (x_2 <<< x_1).sshiftRight' x_1 ≠ x_2 ∨ x_1 ≥ ↑6 ∨ True ∧ (x <<< x_1).sshiftRight' x_1 ≠ x ∨ x_1 ≥ ↑6) →
    ¬x_1 ≥ ↑6 → x_2 <<< x_1 + x <<< x_1 = (x_2 + x) <<< x_1

theorem sel_false_val_is_a_masked_shl_of_true_val1_thm.extracted_1._4 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬ofBool (x_1 &&& 15#32 == 0#32) = 1#1 →
    ¬(True ∧ ((x_1 &&& 15#32) <<< 2#32).sshiftRight' 2#32 ≠ x_1 &&& 15#32 ∨
          True ∧ (x_1 &&& 15#32) <<< 2#32 >>> 2#32 ≠ x_1 &&& 15#32 ∨
            2#32 ≥ ↑32 ∨ zeroExtend 64 ((x_1 &&& 15#32) <<< 2#32) ≥ ↑64) →
      ¬(2#32 ≥ ↑32 ∨ True ∧ (x_1 <<< 2#32 &&& 60#32).msb = true ∨ zeroExtend 64 (x_1 <<< 2#32 &&& 60#32) ≥ ↑64) →
        x.sshiftRight' (zeroExtend 64 ((x_1 &&& 15#32) <<< 2#32)) =
          x.sshiftRight' (zeroExtend 64 (x_1 <<< 2#32 &&& 60#32))

theorem icmp_eq_mul_nsw_nonequal_proof : icmp_eq_mul_nsw_nonequal_before ⊑ icmp_eq_mul_nsw_nonequal_after

theorem test11_proof : test11_before ⊑ test11_after

theorem e_1087 :
    2 * z - 1 *  ~~~(z &&&  ~~~t) + 2 *  ~~~(z &&& t) + 5 * (z |||  ~~~t) + 4 *  ~~~z - 4 *  ~~~(z ||| t) - 5 *  ~~~(z |||  ~~~t) - 9 * (z &&&  ~~~t) = 6 *  ~~~(z ^^^ t)

theorem sext_zext_apint1_thm.extracted_1._1 : ∀ (x : BitVec 77),
  signExtend 1024 (zeroExtend 533 x) = zeroExtend 1024 x

theorem ashrslt_01_07_thm.extracted_1._1 : ∀ (x : BitVec 4), ¬1#4 ≥ ↑4 → ofBool (x.sshiftRight' 1#4 <ₛ 7#4) = 1#1

theorem test31_proof : test31_before ⊑ test31_after

theorem bitwise_and_logical_and_masked_icmp_allzeros_poison1_thm.extracted_1._3 : ∀ (x : BitVec 1)
  (x_1 x_2 : BitVec 32),
  ofBool (x_2 &&& x_1 == 0#32) = 1#1 →
    ofBool (x_2 &&& (x_1 ||| 7#32) == 0#32) = 1#1 → x &&& ofBool (x_2 &&& 7#32 == 0#32) = x

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

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

theorem or_and_shift_shift_and_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(3#32 ≥ ↑32 ∨ 2#32 ≥ ↑32) →
    (x &&& 7#32) <<< 3#32 ||

theorem lshr_shl_pow2_const_case2_proof : lshr_shl_pow2_const_case2_before ⊑ lshr_shl_pow2_const_case2_after

theorem test44_proof : test44_before ⊑ test44_after

theorem e_206 :
     - 1 *  ~~~y + 3 *  ~~~x - 2 * (x ||| y) - 4 *  ~~~(x ||| y) - 3 *  ~~~(x |||  ~~~y) + 3 * (x &&&  ~~~y) =  - 2 *  ~~~(x &&&  ~~~y)

theorem zext_ult_zext_proof : zext_ult_zext_before ⊑ zext_ult_zext_after

theorem test_sub_nsw__nsw_is_safe_thm (e : IntW 32) :
  select (icmp IntPred.eq (LLVM.or e (const? 32 (-2147483648))) (const? 32 (-2147483647))) (const? 32 (-1))
      (sub (const? 32 (-2147483648)) (LLVM.or e (const? 32 (-2147483648))) { «nsw» := true, «nuw» := false }) ⊑
    sub (const? 32 (-2147483648)) (LLVM.or e (const? 32 (-2147483648))) { «nsw» := true, «nuw» := false }

theorem reassoc_x2_sub_nuw_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(True ∧ x_1.usubOverflow 4#32 = true ∨
        True ∧ x.usubOverflow 8#32 = true ∨ True ∧ (x_1 - 4#32).usubOverflow (x - 8#32) = true) →
    x_1 - 4#32 - (x - 8#32) = x_1 - x + 4#32

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

theorem src_is_notmask_sext_proof : src_is_notmask_sext_before ⊑ src_is_notmask_sext_after

theorem lt_signed_to_small_negative_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (signExtend 32 x <ₛ BitVec.ofInt 32 (-17)) = ofBool (x <ₛ BitVec.ofInt 8 (-17))

theorem or_not_and_wrong_b_proof : or_not_and_wrong_b_before ⊑ or_not_and_wrong_b_after

theorem select_lshr_icmp_bad_proof : select_lshr_icmp_bad_before ⊑ select_lshr_icmp_bad_after

theorem test25_thm (e : IntW 32) :
  LLVM.and (icmp IntPred.sge e (const? 32 50)) (icmp IntPred.slt e (const? 32 100)) ⊑
    icmp IntPred.ult (add e (const? 32 (-50))) (const? 32 50)

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

theorem zext_sext_add_icmp_ugt_1_proof : zext_sext_add_icmp_ugt_1_before ⊑ zext_sext_add_icmp_ugt_1_after

theorem e_754 :
    5 *  ~~~(z ^^^ t) - 2 * (z ^^^ t) + 2 * (z &&&  ~~~t) = 5 *  ~~~(z &&&  ~~~t) - 7 *  ~~~(z |||  ~~~t)

theorem ashrsgt_02_15_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬2#4 ≥ ↑4 → ofBool (-1#4 <ₛ x.sshiftRight' 2#4) = ofBool (-1#4 <ₛ x)

theorem ashr_16_to_64_add_zext_basic_proof : ashr_16_to_64_add_zext_basic_before ⊑ ashr_16_to_64_add_zext_basic_after

theorem test16_proof : test16_before ⊑ test16_after

theorem select_icmp_ne_0_and_4096_or_32_proof : select_icmp_ne_0_and_4096_or_32_before ⊑ select_icmp_ne_0_and_4096_or_32_after

theorem lshr_add_exact_proof : lshr_add_exact_before ⊑ lshr_add_exact_after

theorem test_or3_logical_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x_1 &&& 2147483647#32 ≤ₛ x) = 1#1 → ofBool (x <ₛ 0#32) = ofBool (x_1 &&& 2147483647#32 ≤ᵤ x)

theorem eq_smax4_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 + 3#32 <ₛ x) = 1#1 → ofBool (x_1 + 3#32 == x) = ofBool (x ≤ₛ x_1 + 3#32)

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

theorem shl_shl_thm (e : IntW 32) : shl (shl e (const? 32 6)) (const? 32 28) ⊑ const? 32 0

theorem test4_proof : test4_before ⊑ test4_after

theorem t2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), ¬x ≥ ↑8 → x_1 - BitVec.ofInt 8 (-42) <<< x = 42#8 <<< x + x_1

theorem udiv_common_divisor_defined_cond_proof : udiv_common_divisor_defined_cond_before ⊑ udiv_common_divisor_defined_cond_after

theorem ashr_ugt_0_proof : ashr_ugt_0_before ⊑ ashr_ugt_0_after

theorem e_1258 :
     - 1 *  ~~~(z &&& t) + 7 * z + 2 * (z |||  ~~~t) - 1 *  ~~~(z &&&  ~~~t) + 2 *  ~~~t + 3 *  ~~~(z ||| t) + 2 *  ~~~(z |||  ~~~t) - 10 * (z &&&  ~~~t) - 3 * (z &&& t) = 5 *  ~~~(z ^^^ t)

theorem fold_sext_to_and_wrong3_proof : fold_sext_to_and_wrong3_before ⊑ fold_sext_to_and_wrong3_after

theorem main7f_thm.extracted_1._1 : ∀ (x x_1 x_2 x_3 x_4 : BitVec 32),
  ofBool (x_4 &&& x_3 == x_2 &&& (x_4 &&& x_3)) &&& ofBool (x_1 &&& x == x_2 &&& (x_1 &&& x)) = 1#1 →
    0#32 = zeroExtend 32 (ofBool (x_2 &&& (x_4 &&& x_3 ||| x_1 &&& x) != x_4 &&& x_3 ||| x_1 &&& x))

theorem R.fromTensorFinsupp_degree (q : Nat) (coeffs : List Int):
  (R.fromTensorFinsupp q coeffs).degree ≤ coeffs.length

theorem bitvec_AddSub_1309 :
  [llvm(w)| {
    ^bb0(%X : _, %Y : _):
      %v1 = llvm.and %X, %Y
      %v2 = llvm.or %X, %Y
      %v3 = llvm.add %v1, %v2
      llvm.return %v3
  }] ⊑ [llvm(w)| {
    ^bb0(%X : _, %Y : _):
      %v3 = llvm.add %X, %Y
      llvm.return %v3
  }]

theorem low_mask_nsw_nuw_proof : low_mask_nsw_nuw_before ⊑ low_mask_nsw_nuw_after

theorem Holor.pointwise_mul_index [Mul α] (h₁ h₂ : Holor α ds) :
  (h₁ * h₂) i = h₁ i * h₂ i

theorem select_icmp_x_and_8_ne_0_y_xor_8_thm.extracted_1._4 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬ofBool (x_1 &&& 8#32 == 0#32) = 1#1 →
    ¬(True ∧ (x_1 &&& 8#32 ^^^ 8#32).msb = true) → x = x ^^^ zeroExtend 64 (x_1 &&& 8#32 ^^^ 8#32)

theorem lshrult_02_00_exact_thm (e : IntW 4) :
  icmp IntPred.ult (lshr e (const? 4 2) { «exact» := true }) (const? 4 0) ⊑ const? 1 0

theorem e_1366 :
    5 *  ~~~t - 2 *  ~~~(z &&&  ~~~z) + 5 *  ~~~(z ^^^ t) + 11 * z + 4 * (z ^^^ t) - 7 *  ~~~(z &&& t) + 10 *  ~~~(z ||| t) + 16 *  ~~~(z |||  ~~~t) - 11 * (z &&&  ~~~t) - 14 * (z &&& t) = 11 *  ~~~z

theorem e_331 :
     - 6 *  ~~~x + 2 * (x |||  ~~~y) - 3 * x + 2 * (x ||| y) - 10 *  ~~~(x ||| y) - 10 *  ~~~(x |||  ~~~y) - 4 * (x &&&  ~~~y) - 15 * (x &&& y) =  - 3 *  ~~~(x &&&  ~~~x) - 11 *  ~~~(x &&&  ~~~y)

theorem test35_with_trunc_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ofBool (0#32 ≤ₛ truncate 32 x) = 1#1 → ¬ofBool (x &&& 2147483648#64 == 0#64) = 1#1 → 60#32 = 100#32

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

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

theorem uge_umin4_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x <ᵤ x_1 + 3#32) = 1#1 → ofBool (x_1 + 3#32 ≤ᵤ x_1 + 3#32) = ofBool (x_1 + 3#32 ≤ᵤ x)

theorem test_and_ne_a_b_commuted_proof : test_and_ne_a_b_commuted_before ⊑ test_and_ne_a_b_commuted_after

theorem masked_and_notA_slightly_optimized_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (8#32 ≤ᵤ x) = 1#1 → 0#1 = ofBool (x &&& BitVec.ofInt 32 (-40) != 0#32)

theorem shl_mask_wrong_shl_const_proof : shl_mask_wrong_shl_const_before ⊑ shl_mask_wrong_shl_const_after

theorem test_zext1_proof : test_zext1_before ⊑ test_zext1_after

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

theorem lshr_add_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬(5#8 ≥ ↑8 ∨ (42#8 == 0 || 8 != 1 && x == intMin 8 && 42#8 == -1) = true ∨ 5#8 ≥ ↑8) →
    (42#8 == 0 || 8 != 1 && x == intMin 8 && 42#8 == -1) = true ∨ 5#8 ≥ ↑8 → False

theorem sub_dec_proof : sub_dec_before ⊑ sub_dec_after

theorem test13_proof : test13_before ⊑ test13_after

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

theorem bv_AndOrXor_1683_2 :
    ∀ (e e_1 : LLVM.IntW w), LLVM.or (LLVM.icmp LLVM.IntPred.uge e e_1) (LLVM.icmp LLVM.IntPred.ne e e_1) ⊑ LLVM.const? 1 1

theorem positive_biggerlshr_lshrexact_proof : positive_biggerlshr_lshrexact_before ⊑ positive_biggerlshr_lshrexact_after

theorem sgt_smin1_thm (e e_1 : IntW 32) :
  icmp IntPred.sgt (select (icmp IntPred.slt e_1 e) e_1 e) e_1 ⊑ const? 1 0

theorem icmp_power2_and_icmp_shifted_mask_1073741824_1073741823_proof : icmp_power2_and_icmp_shifted_mask_1073741824_1073741823_before ⊑ icmp_power2_and_icmp_shifted_mask_1073741824_1073741823_after

theorem add_or_sub_comb_i8_negative_y_add_thm (e e_1 : IntW 8) :
  add (LLVM.or (sub (const? 8 0) e_1) e_1) e ⊑ add (LLVM.or e_1 (sub (const? 8 0) e_1)) e

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

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

theorem demorgan_nor_use2bc_proof : demorgan_nor_use2bc_before ⊑ demorgan_nor_use2bc_after

theorem e_1753 :
     - 7 * ((a &&& b) ^^^  ~~~(a ^^^ ( ~~~b ||| c))) - 1 * ( ~~~(a |||  ~~~b) ||| (b ^^^ c)) - 6 * ( ~~~c ||| (a ^^^ b)) - 1 * (b ^^^  ~~~(a &&&  ~~~c)) + 2 * (b ^^^  ~~~(a &&& c)) + 11 * (b ^^^ c) - 1 * ((a &&&  ~~~b) |||  ~~~(b ^^^ c)) + 7 * (c ^^^  ~~~(a &&& (b &&& c))) - 11 * ( ~~~(a &&&  ~~~b) &&&  ~~~(b ^^^ c)) + 3 * (a ^^^ c) - 7 * ( ~~~(a |||  ~~~b) ||| (a ^^^ (b ^^^ c))) - 6 * ((a &&& b) ^^^ (b |||  ~~~c)) + 1 *  ~~~(a &&& ( ~~~b ||| c)) + 1 * (c &&& (a ||| b)) - 5 * ((a |||  ~~~b) &&& (b ^^^ c)) - 2 * ( ~~~c |||  ~~~(a ^^^ b)) - 3 *  ~~~(b |||  ~~~c) + 7 * (a &&& b) + 1 * ( ~~~b |||  ~~~(a ^^^ c)) - 2 * (c ^^^  ~~~(a &&& ( ~~~b &&& c))) - 6 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) - 2 * ( ~~~a ||| ( ~~~b ||| c)) + 1 * a - 2 * (a ^^^ (b ^^^ c)) + 1 * ((a &&& c) ^^^  ~~~(b &&&  ~~~c)) - 7 * ((a &&& b) |||  ~~~(b |||  ~~~c)) + 7 * ( ~~~a &&& ( ~~~b ||| c)) + 18 *  ~~~(a ||| (b ||| c)) + 15 *  ~~~(a ||| ( ~~~b ||| c)) + 20 *  ~~~( ~~~a ||| (b ||| c)) + 10 * ( ~~~a &&& ( ~~~b &&& c)) + 21 * ( ~~~a &&& (b &&& c)) + 21 * (a &&& ( ~~~b &&& c)) + 19 * (a &&& (b &&& c)) =  - 1 *  ~~~( ~~~a ||| ( ~~~b ||| c))

theorem add_or_sub_comb_i8_negative_y_add_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  (0#8 - x_1 ||| x_1) + x = (x_1 ||| 0#8 - x_1) + x

theorem test1_thm.extracted_1._2 : ∀ (x : BitVec 333),
  ¬70368744177664#333 = 0 → ¬46#333 ≥ ↑333 → x / 70368744177664#333 = x >>> 46#333

theorem test_sgt_xor_thm (e e_1 : IntW 32) :
  icmp IntPred.sgt (LLVM.xor (LLVM.xor e_1 (const? 32 (-1))) e) (LLVM.xor e_1 (const? 32 (-1))) ⊑
    icmp IntPred.slt (LLVM.xor e e_1) e_1

theorem pr40493_neg1_thm (e : IntW 32) :
  icmp IntPred.eq (LLVM.and (mul e (const? 32 11)) (const? 32 4)) (const? 32 0) ⊑
    icmp IntPred.eq (LLVM.and (mul e (const? 32 3)) (const? 32 4)) (const? 32 0)

theorem test2_proof : test2_before ⊑ test2_after
</all_available_lemmas>

<local_ctx>
import Blase.AutoStructs.ForMathlib

import Blase.SingleWidth.Defs

open Fin.NatCast

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

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

def liftLast2 n : Fin 2 → Fin (n + 2)
| 0 => n
| 1 => Fin.last (n + 1)

def liftExcept2 n : Fin n → Fin (n + 2) :=
  fun k => Fin.castLE (by admit /- proof elided -/
  ) k

def liftMax1 (n m : Nat) : Fin n → Fin (max n m) :=
  fun k => k.castLE (by admit /- proof elided -/
  )

def liftMax2 (n m : Nat) : Fin m → Fin (max n m) :=
  fun k => k.castLE (by admit /- proof elided -/
  )

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

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

inductive RelationOrdering
| lt | le | gt | ge
deriving Repr, Fintype

inductive Relation
| eq
| signed (ord : RelationOrdering)
| unsigned (ord : RelationOrdering)
deriving Repr

def evalRelation (rel : Relation) {w} (bv1 bv2 : BitVec w) : Prop :=
  match rel with
  | .eq => bv1 = bv2
  | .signed .lt => bv1.slt bv2
  | .signed .le => bv1.sle  bv2
  | .signed .gt => bv2.slt bv1
  | .signed .ge => bv2.sle bv1
  | .unsigned .lt => bv1.ult bv2
  | .unsigned .le => bv1.ule bv2
  | .unsigned .gt => bv2.ult bv1
  | .unsigned .ge => bv2.ule bv1

@[simp]
def Relation.language (rel : Relation) : Set (BitVecs 2) :=
  { bvs | evalRelation rel (bvs.bvs.get 0) (bvs.bvs.get 1) }

inductive Binop
| and | or | impl | equiv
deriving Repr

def evalBinop (op : Binop) (b1 b2 : Prop) : Prop :=
  match op with
  | .and => b1 ∧ b2
  | .or => b1 ∨ b2
  | .impl => b1 → b2
  | .equiv => b1 ↔ b2

def langBinop (op : Binop) (l1 l2 : Set (BitVecs n)) : Set (BitVecs n) :=
  match op with
  | .and => l1 ∩ l2
  | .or => l1 ∪ l2
  | .impl => l1ᶜ ∪ l2
  | .equiv => (l1ᶜ ∪ l2) ∩ (l2ᶜ ∪ l1)

inductive Unop
| neg
deriving Repr

inductive Formula : Type
| width : WidthPredicate → Nat → Formula
| atom : Relation → Term → Term → Formula
| msbSet : Term → Formula
| unop : Unop → Formula → Formula
| binop : Binop → Formula → Formula → Formula
deriving Repr

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

@[simp]
def WidthPredicate.sat (wp : WidthPredicate) (w n : Nat) : Bool :=
  match wp with
  | .eq => w = n
  | .neq => w ≠ n
  | .lt => w < n
  | .le => w ≤ n
  | .gt => w > n
  | .ge => w ≥ n

@[simp]
def Formula.sat {w : Nat} (φ : Formula) (ρ : Fin φ.arity → BitVec w) : Prop :=
  match φ with
  | .width wp n => wp.sat w n
  | .atom rel t1 t2 =>
    let bv1 := t1.evalFinBV (fun n => ρ $ Fin.castLE (by admit /- proof elided -/
    ) n)
    let bv2 := t2.evalFinBV (fun n => ρ $ Fin.castLE (by admit /- proof elided -/
    ) n)
    evalRelation rel bv1 bv2
  | .unop .neg φ => ¬ φ.sat ρ
  | .binop op φ1 φ2 =>
    let b1 := φ1.sat (fun n => ρ $ Fin.castLE (by admit /- proof elided -/
    ) n)
    let b2 := φ2.sat (fun n => ρ $ Fin.castLE (by admit /- proof elided -/
    ) n)
    evalBinop op b1 b2
  | .msbSet t => (t.evalFinBV ρ).msb

@[simp]
def _root_.Set.lift (f : Fin n → Fin m) (bvs : Set (BitVecs n)) : Set (BitVecs m) :=
  BitVecs.transport f ⁻¹' bvs

@[simp]
def _root_.Set.proj (f : Fin n → Fin m) (bvs : Set (BitVecs m)) : Set (BitVecs n) :=
  BitVecs.transport f '' bvs

@[simp]
def langMsb : Set (BitVecs 1) := { bvs | bvs.bvs.get 0 |>.msb }

@[simp]
def Formula.language (φ : Formula) : Set (BitVecs φ.arity) :=
  match φ with
  | .width wp n => { bvs | wp.sat bvs.w n }
  | .atom rel t1 t2 =>
    let l1 := t1.language.lift (liftMaxSucc1 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity))
    let l2 := t2.language.lift (liftMaxSucc2 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity))
    let lrel := rel.language.lift $ liftLast2 (max (FinEnum.card (Fin t1.arity)) (FinEnum.card (Fin t2.arity)))
    let l := lrel ∩ l1 ∩ l2
    l.proj (liftExcept2 _)
  | .unop .neg φ => φ.languageᶜ
  | .binop op φ1 φ2 =>
    let l1 := φ1.language.lift $ liftMax1 φ1.arity φ2.arity
    let l2 := φ2.language.lift $ liftMax2 φ1.arity φ2.arity
    langBinop op l1 l2
  | .msbSet t =>
    let lmsb := langMsb.lift $ fun _ => Fin.last t.arity
    let l' := t.language ∩ lmsb
    l'.proj fun n => n.castLE (by admit /- proof elided -/
    )
</local_ctx>

<target_theorem>
theorem formula_language (φ : Formula) :
    φ.language = { (bvs : BitVecs φ.arity) | φ.sat (fun k => bvs.bvs.get k) } :=
</target_theorem>

