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

syntax "max" : MLIR.Pretty.uniform_op

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

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

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

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

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

| shiftL : Term → Nat → Term

deriving Repr, Inhabited, Lean.ToExpr

@[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

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

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

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

Functor in Init.Prelude
</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

@[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 icmp_slt_0_or_icmp_sgt_0_i64_fail3_proof : icmp_slt_0_or_icmp_sgt_0_i64_fail3_before ⊑ icmp_slt_0_or_icmp_sgt_0_i64_fail3_after

theorem fold_add_udiv_urem_commuted_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(10#32 = 0 ∨ 10#32 = 0 ∨ 4#32 ≥ ↑32) →
    ¬(10#32 = 0 ∨ True ∧ (x / 10#32).umulOverflow 6#32 = true) →
      x % 10#32 + (x / 10#32) <<< 4#32 = x / 10#32 * 6#32 + x

theorem and_consts_thm (e : IntW 32) :
  LLVM.or (icmp IntPred.eq (LLVM.and (const? 32 4) e) (const? 32 0))
      (icmp IntPred.eq (LLVM.and (const? 32 8) e) (const? 32 0)) ⊑
    icmp IntPred.ne (LLVM.and e (const? 32 12)) (const? 32 12)

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

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

theorem not_and_and_or_not_or_or_commute3_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  ¬((x_2 == 0 || 32 != 1 && 42#32 == intMin 32 && x_2 == -1) = true ∨
        (x_2 == 0 || 32 != 1 && 42#32 == intMin 32 && x_2 == -1) = true) →
    (x_2 == 0 || 32 != 1 && 42#32 == intMin 32 && x_2 == -1) = true → False

theorem negation_of_increment_via_or_with_no_common_bits_set_proof : negation_of_increment_via_or_with_no_common_bits_set_before ⊑ negation_of_increment_via_or_with_no_common_bits_set_after

theorem ashr_mul_times_3_div_2_exact_proof : ashr_mul_times_3_div_2_exact_before ⊑ ashr_mul_times_3_div_2_exact_after

theorem test_mul_nsw__none_are_safe_thm (e : IntW 32) :
  select (icmp IntPred.eq e (const? 32 805306368)) (const? 32 (-1342177280))
      (mul e (const? 32 9) { «nsw» := true, «nuw» := false }) ⊑
    mul e (const? 32 9)

theorem and_zext_eq_zero_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬x ≥ ↑32 → zeroExtend 32 (ofBool (x_1 == 0#32)) &&& (x_1 >>> x ^^^ -1#32) = zeroExtend 32 (ofBool (x_1 == 0#32))

theorem zext_sext_add_icmp_slt_1_proof : zext_sext_add_icmp_slt_1_before ⊑ zext_sext_add_icmp_slt_1_after

theorem sge_swap_and_max_commute_logical_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬ofBool (x == 127#8) = 1#1 → 0#1 = ofBool (x == 127#8)

theorem test_or4_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 &&& 2147483647#32 <ₛ x) = 1#1 → 1#1 = ofBool (x_1 &&& 2147483647#32 <ᵤ x)

theorem p0_proof : p0_before ⊑ p0_after

theorem icmp_ne_sext_eq_allones_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (signExtend 32 (ofBool (x == -1#32)) != x) = ofBool (x + -1#32 <ᵤ BitVec.ofInt 32 (-2))

theorem different_size_zext_zext_ugt_thm.extracted_1._1 : ∀ (x : BitVec 4) (x_1 : BitVec 7),
  ofBool (zeroExtend 25 x <ᵤ zeroExtend 25 x_1) = ofBool (zeroExtend 7 x <ᵤ x_1)

theorem uge_swap_or_not_max_commute_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 != -1#8) ||

theorem test_add_nuw__nsw_is_safe_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x ||| BitVec.ofInt 32 (-2147483648) == -1#32) = 1#1 →
    ¬(True ∧ (x ||| BitVec.ofInt 32 (-2147483648)).saddOverflow 1#32 = true) →
      0#32 = (x ||| BitVec.ofInt 32 (-2147483648)) + 1#32

theorem ashrslt_03_03_proof : ashrslt_03_03_before ⊑ ashrslt_03_03_after

theorem slt_zero_eq_ne_0_fail1_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 →
    ofBool (zeroExtend 32 (ofBool (x != 0#32)) == x.sshiftRight' 31#32) =
      ofBool (x.sshiftRight' 31#32 == zeroExtend 32 (ofBool (x != 0#32)))

theorem PR42691_7_proof : PR42691_7_before ⊑ PR42691_7_after

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

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

theorem eq3 (w : Nat) (a b : BitVec w) : a = a ||

@[simp] theorem Lets.getPureExprAux_var_appendInr (lets : Lets d Γ_in eff Γ_out)
    (e : Expr d Γ_out eff ty₁) (v : Var Γ_out ty₂) :
    getPureExprAux (lets.var e) v.appendInr
    = (getPureExprAux lets v).map fun ⟨_, w, e⟩ =>
        ⟨_, w, e.changeVars <| Hom.id.castCodomain (by simp)⟩

@[simp] theorem toCom_nil {com : Com d Γ eff ty} : toCom ⟨.nil, com⟩ = com

theorem t0_thm (e : IntW 64) : sub (const? 64 0) (lshr e (const? 64 63)) ⊑ ashr e (const? 64 63)

theorem ashrsgt_02_07_exact_proof : ashrsgt_02_07_exact_before ⊑ ashrsgt_02_07_exact_after

theorem exact_ashr_ne_noexactdiv_proof : exact_ashr_ne_noexactdiv_before ⊑ exact_ashr_ne_noexactdiv_after

theorem shl_xor_lshr_comm_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 32),
  ¬(True ∧ x_1 <<< x >>> x ≠ x_1 ∨ x ≥ ↑32 ∨ x ≥ ↑32) → ¬x ≥ ↑32 → (x_2 ^^^ x_1 <<< x) >>> x = x_2 >>> x ^^^ x_1

theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat

theorem icmp_slt_0_or_icmp_sgt_0_i64_fail3_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬62#64 ≥ ↑64 → 62#64 ≥ ↑64 ∨ 63#64 ≥ ↑64 → False

theorem test12_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(2#32 == 0 || 32 != 1 && x &&& BitVec.ofInt 32 (-4) == intMin 32 && 2#32 == -1) = true →
    (x &&& BitVec.ofInt 32 (-4)).srem 2#32 = 0#32

theorem sub_dec_proof : sub_dec_before ⊑ sub_dec_after

theorem shl_add_lshr_comm_thm (e e_1 e_2 : IntW 32) :
  lshr (add (mul e_2 e_2) (shl e_1 e { «nsw» := false, «nuw» := true }) { «nsw» := false, «nuw» := true }) e ⊑
    add (lshr (mul e_2 e_2) e) e_1 { «nsw» := false, «nuw» := true }

theorem t0_proof : t0_before ⊑ t0_after

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 t0_commutative_thm.extracted_1._18 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1) (x_3 x_4 : BitVec 8),
  ofBool (x_4 == x_3) = 1#1 → ofBool (x_4 != x_3) = 1#1 → ¬True → x_2 = 1#1 → x_1 = x

theorem masked_bit_set_thm (e e_1 : IntW 32) :
  zext 32 (icmp IntPred.ne (LLVM.and (shl (const? 32 1) e_1) e) (const? 32 0)) ⊑
    LLVM.and (lshr e e_1) (const? 32 1)

theorem lshr_C1_add_A_C2_i32_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(x &&& 65535#32) + 5#32 ≥ ↑32 →
    ¬x &&& 65535#32 ≥ ↑32 → 6#32 <<< ((x &&& 65535#32) + 5#32) = 192#32 <<< (x &&& 65535#32)

theorem land_bor_right2_proof : land_bor_right2_before ⊑ land_bor_right2_after

theorem e_1048 :
    2 * (z ^^^ t) + 1 * z - 2 *  ~~~(z &&& t) - 1 *  ~~~(z &&&  ~~~z) - 4 *  ~~~(z ||| t) + 1 *  ~~~(z |||  ~~~t) - 7 * (z &&&  ~~~t) =  - 7 * (z |||  ~~~t) + 7 * (z &&& t)

theorem test9_thm (e : IntW 16) : trunc 16 (sext 32 e) ⊑ e

theorem test_shl_nsw__nuw_is_safe_thm.extracted_1._3 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬ofBool (x_1 &&& 1073741822#32 == 0#32) = 1#1 →
    ¬(True ∧ ((x_1 &&& 1073741822#32) <<< 2#32).sshiftRight' 2#32 ≠ x_1 &&& 1073741822#32 ∨
          2#32 ≥ ↑32 ∨ zeroExtend 64 ((x_1 &&& 1073741822#32) <<< 2#32) ≥ ↑64) →
      2#32 ≥ ↑32 ∨
          True ∧ (x_1 <<< 2#32 &&& BitVec.ofInt 32 (-8)).msb = true ∨
            zeroExtend 64 (x_1 <<< 2#32 &&& BitVec.ofInt 32 (-8)) ≥ ↑64 →
        False

@[simp] theorem carry_succ (initCarry : Bool) (x y : BitStream) :
    (carry initCarry x y (i + 1)) =
  let out

theorem e_1828 :
    4 * (c &&& (a |||  ~~~b)) + 7 * ( ~~~(a &&& b) &&& (a ^^^ (b ^^^ c))) - 1 * ((a &&& b) |||  ~~~(b ^^^ c)) + 11 *  ~~~(a ^^^ ( ~~~b &&& c)) - 6 * (b &&&  ~~~(a &&&  ~~~c)) - 1 * ((a ||| b) &&&  ~~~(b ^^^ c)) + 4 * (b ^^^  ~~~( ~~~a &&& (b ^^^ c))) + 1 * (b ^^^ (a &&& (b ^^^ c))) + 3 * ((b &&&  ~~~c) |||  ~~~(a ||| ( ~~~b &&& c))) + 1 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) + 2 * ( ~~~(a &&& b) &&&  ~~~(b ^^^ c)) + 2 * ( ~~~a ||| (b ^^^ c)) - 11 * ( ~~~(a |||  ~~~b) ||| (a ^^^ (b ^^^ c))) - 1 * (a ||| ( ~~~b &&& c)) + 2 *  ~~~(b |||  ~~~c) - 1 * (b ^^^  ~~~(a ||| ( ~~~b &&& c))) + 4 * (c ^^^ (a &&& ( ~~~b ||| c))) - 7 * (b ^^^ ( ~~~a ||| (b ||| c))) - 2 * ( ~~~(a ^^^ b) &&& (a ^^^ c)) + 2 * (c ||| (a ^^^ b)) + 7 * (c ||| (a &&& b)) - 1 * ( ~~~a ||| ( ~~~b &&& c)) + 4 * (b ^^^ ( ~~~a ||| (b &&& c))) - 1 * (b ^^^ c) - 2 * (c &&&  ~~~(a &&&  ~~~b)) + 5 * ( ~~~(a ^^^ b) |||  ~~~(a ^^^ c)) + 1 * c - 11 * (a ||| (b ||| c)) + 11 * ((a |||  ~~~b) &&& (b ^^^ c)) + 3 * ((a &&& c) |||  ~~~(b ||| c)) + 2 * (b ^^^ (a &&& (b ||| c))) + 1 * (a ^^^ ( ~~~b &&& c)) - 1 * (a ^^^ (b ||| c)) + 1 * ((a &&& c) ||| (b &&&  ~~~c)) - 2 * (c ^^^ (a ||| (b ||| c))) + 5 * (c ^^^ (a &&& (b ||| c))) - 30 *  ~~~(a ||| (b ||| c)) - 5 *  ~~~(a ||| ( ~~~b ||| c)) - 25 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 24 * ( ~~~a &&& ( ~~~b &&& c)) - 6 * ( ~~~a &&& (b &&& c)) - 40 * (a &&& ( ~~~b &&& c)) + 8 * (a &&& (b &&& c)) =  - 5 * (b ^^^ ( ~~~a ||| ( ~~~b ||| c)))

theorem test2_proof : test2_before ⊑ test2_after

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 sgt_or_not_min_proof : sgt_or_not_min_before ⊑ sgt_or_not_min_after

theorem lshrult_02_02_exact_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬(True ∧ x >>> 2#4 <<< 2#4 ≠ x ∨ 2#4 ≥ ↑4) → ofBool (x >>> 2#4 <ᵤ 2#4) = ofBool (-1#4 <ₛ x)

theorem e_1220 :
     - 11 *  ~~~(z &&&  ~~~z) - 1 * t - 6 *  ~~~(z &&& t) + 11 *  ~~~t - 2 * (z |||  ~~~t) + 11 *  ~~~(z &&&  ~~~t) - 3 *  ~~~(z ||| t) + 1 * (z &&&  ~~~t) - 4 * (z &&& t) =  - 7 * (z ||| t)

theorem p_commutative0_proof : p_commutative0_before ⊑ p_commutative0_after

theorem lshr_sub_nsw_proof : lshr_sub_nsw_before ⊑ lshr_sub_nsw_after

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

theorem e_854 :
    2 * t - 7 *  ~~~(z &&&  ~~~z) + 13 *  ~~~(z ||| t) + 7 *  ~~~(z |||  ~~~t) + 15 * (z &&&  ~~~t) + 7 * (z &&& t) = 2 * (z ||| t) + 6 *  ~~~t

theorem invert_both_cmp_operands_complex_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32) (x_2 : BitVec 1),
  x_2 = 1#1 → ofBool (x_1 + (x ^^^ -1#32) ≤ₛ x_1 ^^^ -1#32) = ofBool (x_1 ≤ₛ x - x_1)

theorem zext_false_val_must_be_zero_proof : zext_false_val_must_be_zero_before ⊑ zext_false_val_must_be_zero_after

theorem lshr_exact_add_nuw_thm (e : IntW 32) :
  lshr (const? 32 4) (add e (const? 32 1) { «nsw» := false, «nuw» := true }) { «exact» := true } ⊑
    lshr (const? 32 2) e { «exact» := true }

theorem slt_smin3_proof : slt_smin3_before ⊑ slt_smin3_after

theorem e_240 :
    1 *  ~~~(x ^^^ y) - 1 *  ~~~(x &&&  ~~~x) + 1 * (x ||| y) + 5 * x + 3 *  ~~~(x ||| y) - 5 * (x &&&  ~~~y) - 6 * (x &&& y) = 3 *  ~~~x - 3 *  ~~~(x |||  ~~~y)

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

theorem slt_zero_eq_ne_0_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 → ofBool (zeroExtend 32 (ofBool (x != 0#32)) == x >>> 31#32) = ofBool (x <ₛ 1#32)

theorem xor_add_thm.extracted_1._1 : ∀ (x : BitVec 32),
  True ∧ (73#32).ssubOverflow (x &&& 31#32) = true ∨ True ∧ (73#32).usubOverflow (x &&& 31#32) = true → False

@[simp] theorem Valuation.nil_append {V : Γ.Valuation} :
    HAppend.hAppend (α := Valuation no_index _) (γ := Valuation no_index _)
      (nil (Ty:=Ty)) V -- nil ++ V
    = V

theorem land_land_left2_proof : land_land_left2_before ⊑ land_land_left2_after

theorem lshr_or_or_no_const_proof : lshr_or_or_no_const_before ⊑ lshr_or_or_no_const_after

theorem mul_x_selectp2_thm.extracted_1._2 : ∀ (x : BitVec 1) (x_1 : BitVec 8),
  x = 1#1 → ¬3#8 ≥ ↑8 → x_1 * x_1 * 8#8 = (x_1 * x_1) <<< 3#8

theorem icmp_and_ashr_multiuse_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬4#32 ≥ ↑32 →
    ¬ofBool (x.sshiftRight' 4#32 &&& 15#32 != 14#32) = 1#1 →
      0#1 = ofBool (x &&& 240#32 != 224#32) &&& ofBool (x &&& 496#32 != 432#32)

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 t0_proof : t0_before ⊑ t0_after

theorem t2_ult_sgt_128_thm.extracted_1._4 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 + 16#32 <ᵤ 144#32) = 1#1 → ofBool (127#32 <ₛ x_1) = 1#1 → False

theorem mul16_low_miss_shift_amount_thm.extracted_1._1 : ∀ (x x_1 : BitVec 16),
  ¬(8#16 ≥ ↑16 ∨ 8#16 ≥ ↑16 ∨ 8#16 ≥ ↑16) →
    8#16 ≥ ↑16 ∨
        True ∧ (x_1 >>> 8#16).smulOverflow (x &&& 127#16) = true ∨
          True ∧ (x_1 >>> 8#16).umulOverflow (x &&& 127#16) = true ∨
            8#16 ≥ ↑16 ∨
              True ∧ (x_1 &&& 127#16).smulOverflow (x >>> 8#16) = true ∨
                True ∧ (x_1 &&& 127#16).umulOverflow (x >>> 8#16) = true ∨
                  True ∧ (x_1 >>> 8#16 * (x &&& 127#16)).uaddOverflow ((x_1 &&& 127#16) * x >>> 8#16) = true ∨
                    8#16 ≥ ↑16 ∨
                      True ∧ (x_1 &&& 127#16).smulOverflow (x &&& 127#16) = true ∨
                        True ∧ (x_1 &&& 127#16).umulOverflow (x &&& 127#16) = true →
      False

theorem icmp_select_var_pred_uge_commuted_proof : icmp_select_var_pred_uge_commuted_before ⊑ icmp_select_var_pred_uge_commuted_after

theorem select_icmp_sgt_not_smin_proof : select_icmp_sgt_not_smin_before ⊑ select_icmp_sgt_not_smin_after

theorem sub_sel_op1_thm.extracted_1._2 : ∀ (x : BitVec 1),
  ¬x = 1#1 → ¬(True ∧ (42#32).ssubOverflow 41#32 = true) → 42#32 - 41#32 = zeroExtend 32 (x ^^^ 1#1)

theorem src3_proof : src3_before ⊑ src3_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

--
</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 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>
lemma formula_language_case_atom :
    let φ :=
</target_theorem>

