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>
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
ZMod in Mathlib.Data.ZMod.Defs
Function.surjInv in Mathlib.Logic.Function.Basic
Nat in Init.Prelude
Polynomial in Mathlib.Algebra.Polynomial.Basic
Polynomial.degree in Mathlib.Algebra.Polynomial.Degree.Definitions
Ideal in Mathlib.RingTheory.Ideal.Defs
Ideal.Quotient.mk in Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.span in Mathlib.RingTheory.Ideal.Span
Polynomial.monomial in Mathlib.Algebra.Polynomial.Basic
Int in Init.Data.Int.Basic
List in Init.Prelude
Polynomial.coeff in Mathlib.Algebra.Polynomial.Basic
List.range in Init.Data.List.Basic
Polynomial.map in Mathlib.Algebra.Polynomial.Eval.Defs
Fact in Mathlib.Logic.Basic
Polynomial.Monic in Mathlib.Algebra.Polynomial.Degree.Definitions
ZMod.cast in Mathlib.Data.ZMod.Basic
List.map in Init.Prelude
WithBot in Mathlib.Order.TypeTags
List.length in Init.Prelude
Int.cast in Init.Data.Int.Basic
IntCast in Init.Data.Int.Basic
IntCast.intCast in Init.Data.Int.Basic
List.toFinsupp in Mathlib.Data.List.ToFinsupp
Polynomial.ofFinsupp in Mathlib.Algebra.Polynomial.Basic
List.getD in Init.Data.List.BasicAux
DecidableEq in Init.Prelude
Polynomial.toFinsupp in Mathlib.Algebra.Polynomial.Basic
Semiring in Mathlib.Algebra.Ring.Defs

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

noncomputable def R.repLength {q n} (a : R q n) : Nat := match
  Polynomial.degree a.representative with
    | none => 0
    | some d => d + 1

noncomputable def R.representative :
    R q n → (ZMod q)[X] := fun x => R.representative' q n x %ₘ (f q n)

private noncomputable def R.representative' :
    R q n → (ZMod q)[X] := Function.surjInv (R.surjective_fromPoly q n)

noncomputable def f : (ZMod q)[X] := X^(2^n) + 1

noncomputable def R.fromTensor {q n} (coeffs : List Int) : R q n :=
  coeffs.zipIdx.foldl (init := 0) fun res (c, i) =>
    res + R.monomial ↑c i

noncomputable def R.monomial {q n : Nat} (c : ZMod q) (i : Nat): R q n :=
  R.fromPoly (Polynomial.monomial i c)

abbrev R.fromPoly {q n : Nat} : (ZMod q)[X] →+* R q n := Ideal.Quotient.mk (Ideal.span {f q n})

noncomputable def R.toTensor {q n} (a : R q n) : List Int :=
  List.range a.repLength |>.map fun i =>
        a.coeff i |>.toInt

noncomputable def R.coeff {q n} (a : R q n) (i : Nat) : ZMod q :=
  Polynomial.coeff a.representative i

def ZMod.toInt (x : ZMod q) : Int := ZMod.cast x

noncomputable def R.fromTensorFinsupp (q : Nat) (coeffs : List Int) : (ZMod q)[X] :=
  Polynomial.ofFinsupp (List.toFinsupp (coeffs.map Int.cast))

abbrev R := (ZMod q)[X] ⧸ (Ideal.span {f q n})

def PR42691_8_logical_after := [llvm|
{
^0(%arg328 : i32):
  %0 = llvm.mlir.constant(2147483647 : i32) : i32
  %1 = llvm.mlir.constant(-2147483635 : i32) : i32
  %2 = llvm.add %arg328, %0 : i32
  %3 = llvm.icmp "ult" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def irc_constants_C2MinusAPlusC1_0_neg2 : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%a: i64):
      %c1 = llvm.mlir.constant (0) : i64
      %c2 = llvm.mlir.constant (-2) : i64
      %0 = llvm.add %a, %c1 : i64
      %1 = llvm.sub %c2, %0 : i64
      llvm.return %1 : i64
  }]
  rhs := [LV| {
    ^entry (%a: i64):
      %c1 = llvm.mlir.constant (0) : i64
      %c2 = llvm.mlir.constant (-2) : i64
      %0 = llvm.sub %c2, %c1 : i64
      %1 = llvm.sub %0, %a : i64
      llvm.return %1 : i64
  }]

def test19_before := [llvm|
{
^0(%arg13 : i1, %arg14 : i1):
  %0 = llvm.zext %arg13 : i1 to i32
  %1 = llvm.zext %arg14 : i1 to i32
  %2 = llvm.icmp "eq" %0, %1 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

IO.println in Init.System.IO

def uge_swap_and_max_commute_before := [llvm|
{
^0(%arg226 : i8, %arg227 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.icmp "ule" %arg227, %arg226 : i8
  %2 = llvm.icmp "eq" %arg226, %0 : i8
  %3 = llvm.and %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def xor_of_icmps_after := [llvm|
{
^0(%arg31 : i64):
  %0 = llvm.mlir.constant(1) : i64
  %1 = llvm.icmp "sgt" %arg31, %0 : i64
  "llvm.return"(%1) : (i1) -> ()
}
]

def multiuse3_after := [llvm|
{
^0(%arg9 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(48 : i32) : i32
  %2 = llvm.mlir.constant(6 : i32) : i32
  %3 = llvm.mlir.constant(8064 : i32) : i32
  %4 = llvm.mlir.constant(15 : i32) : i32
  %5 = llvm.lshr %arg9, %0 : i32
  %6 = llvm.and %5, %1 : i32
  %7 = llvm.shl %arg9, %2 : i32
  %8 = llvm.and %7, %3 : i32
  %9 = llvm.lshr %arg9, %0 : i32
  %10 = llvm.and %9, %4 : i32
  %11 = llvm.or disjoint %6, %10 : i32
  %12 = llvm.or disjoint %11, %8 : i32
  "llvm.return"(%12) : (i32) -> ()
}
]

def lshr_32_add_known_32_leading_zeroes_after := [llvm|
{
^0(%arg15 : i64, %arg16 : i64):
  %0 = llvm.mlir.constant(4294967295) : i64
  %1 = llvm.mlir.constant(32) : i64
  %2 = llvm.and %arg15, %0 : i64
  %3 = llvm.and %arg16, %0 : i64
  %4 = llvm.add %2, %3 overflow<nsw,nuw> : i64
  %5 = llvm.lshr %4, %1 : i64
  "llvm.return"(%5) : (i64) -> ()
}
]

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

def not_or_or_not_commute1_after := [llvm|
{
^0(%arg546 : i32, %arg547 : i32, %arg548 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg547, %arg548 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.or %arg546, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def sge_smin1_before := [llvm|
{
^0(%arg79 : i32, %arg80 : i32):
  %0 = llvm.icmp "slt" %arg79, %arg80 : i32
  %1 = "llvm.select"(%0, %arg79, %arg80) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "sge" %1, %arg79 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def p2_scalar_shifted_urem_by_const_before := [llvm|
{
^0(%arg16 : i32, %arg17 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(3 : i32) : i32
  %2 = llvm.mlir.constant(0 : i32) : i32
  %3 = llvm.and %arg16, %0 : i32
  %4 = llvm.shl %3, %arg17 : i32
  %5 = llvm.urem %4, %1 : i32
  %6 = llvm.icmp "eq" %5, %2 : i32
  "llvm.return"(%6) : (i1) -> ()
}
]

def function : Parser :=
  leading_parser argumentList >> arrow >> termParser

@[simp_denote] def if_ {Γ : Ctxt _} {t t': Arith.Ty}
  (cond : Var Γ Arith.Ty.bool) (v : Var Γ t) (then_ else_ : Com ScfArith ⟨[t]⟩ .impure t') :
    Expr ScfArith Γ .impure t' :=
  Expr.mk
    (op := .if t t')
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons cond <| .cons v .nil)
    (regArgs := HVector.cons then_ <| HVector.cons else_ <| HVector.nil)

def and_xor_commute3_before := [llvm|
{
^0(%arg151 : i32, %arg152 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.udiv %0, %arg151 : i32
  %2 = llvm.udiv %0, %arg152 : i32
  %3 = llvm.and %2, %1 : i32
  %4 = llvm.xor %3, %2 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def select_exact_lshr_icmp_const_after := [llvm|
{
^0(%arg146 : i32):
  %0 = llvm.mlir.constant(5 : i32) : i32
  %1 = llvm.lshr %arg146, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def test_after := [llvm|
{
^0(%arg0 : i64):
  %0 = llvm.mlir.constant(16) : i64
  %1 = llvm.shl %arg0, %0 : i64
  %2 = llvm.ashr exact %1, %0 : i64
  "llvm.return"(%2) : (i64) -> ()
}
]

def test_after := [llvm|
{
^0(%arg2 : i64, %arg3 : i1):
  %0 = llvm.mlir.constant(4) : i64
  %1 = llvm.mlir.constant(3) : i64
  %2 = llvm.lshr %arg2, %0 : i64
  %3 = llvm.lshr %arg2, %1 : i64
  %4 = llvm.add %2, %3 overflow<nsw,nuw> : i64
  "llvm.return"(%4) : (i64) -> ()
}
]

def ashr_ashr_before := [llvm|
{
^0(%arg7 : i32):
  %0 = llvm.mlir.constant(5 : i32) : i32
  %1 = llvm.mlir.constant(7 : i32) : i32
  %2 = llvm.ashr %arg7, %0 : i32
  %3 = llvm.ashr %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

instance : Lean.ToExpr RegIndex := inherit

def or_xor_not_after := [llvm|
{
^0(%arg56 : i32, %arg57 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg56, %0 : i32
  %2 = llvm.or %arg57, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def shrink_or_after := [llvm|
{
^0(%arg11 : i6):
  %0 = llvm.mlir.constant(1 : i3) : i3
  %1 = llvm.trunc %arg11 : i6 to i3
  %2 = llvm.or %1, %0 : i3
  "llvm.return"(%2) : (i3) -> ()
}
]

def sendReadyValue (_ : Unit) (_ : Unit) : BitVec 1 := 1

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

def test85_before := [llvm|
{
^0(%arg60 : i32):
  %0 = llvm.mlir.constant(-16777216 : i32) : i32
  %1 = llvm.mlir.constant(23 : i32) : i32
  %2 = llvm.add %arg60, %0 overflow<nuw> : i32
  %3 = llvm.lshr exact %2, %1 : i32
  %4 = llvm.trunc %3 : i32 to i8
  "llvm.return"(%4) : (i8) -> ()
}
]

private def attrVal4Symbol : AttrVal := [mlir_attr_val| @"foo" ]

def main15_after := [llvm|
{
^0(%arg14 : i32):
  %0 = llvm.mlir.constant(32896 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.mlir.constant(2 : i32) : i32
  %3 = llvm.and %arg14, %0 : i32
  %4 = llvm.icmp "eq" %3, %0 : i32
  %5 = "llvm.select"(%4, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

@[simp_denote]
def sub_llvm_i32 := [LV| {
    ^entry (%a: i32, %b: i32):
    %0 = llvm.sub %a, %b : i32
    llvm.return %0 : i32
  }]

def trunc_shl_lshr_infloop_before := [llvm|
{
^0(%arg26 : i64):
  %0 = llvm.mlir.constant(1) : i64
  %1 = llvm.mlir.constant(2) : i64
  %2 = llvm.lshr %arg26, %0 : i64
  %3 = llvm.shl %2, %1 : i64
  %4 = llvm.trunc %3 : i64 to i32
  "llvm.return"(%4) : (i32) -> ()
}
]

let g ← revertBvHyps g

def t2_commutative_before := [llvm|
{
^0(%arg20 : i8, %arg21 : i8):
  %0 = llvm.sub %arg20, %arg21 : i8
  %1 = llvm.icmp "uge" %arg20, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def alive_AddSub_1176_tgt :=
[sllvm| {
^bb0(%a : i64, %b : i64):
  %v1 = llvm.mlir.constant 0 : i64
  %v2 = llvm.sub %v1, %b : i64
  %v3 = llvm.sub %a, %b : i64
  llvm.return %v3 : i64
}]

def negate_add_with_single_negatible_operand_after := [llvm|
{
^0(%arg23 : i8, %arg24 : i8):
  %0 = llvm.mlir.constant(-42 : i8) : i8
  %1 = llvm.sub %0, %arg23 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

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

def not_and_and_or_not_or_or_commute3_after := [llvm|
{
^0(%arg232 : i32, %arg233 : i32, %arg234 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sdiv %0, %arg233 : i32
  %3 = llvm.xor %arg234, %2 : i32
  %4 = llvm.or %3, %arg232 : i32
  %5 = llvm.xor %4, %1 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

abbrev HasBool (d : Dialect) [TyDenote d.Ty] [DialectSignature d] : Type := HasTy d Bool

def test1_after := [llvm|
{
^0(%arg14 : i32, %arg15 : i32):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def select_sub_icmp_bad_2_before := [llvm|
{
^0(%arg68 : i32, %arg69 : i32, %arg70 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.icmp "eq" %arg68, %0 : i32
  %2 = llvm.sub %arg70, %arg68 : i32
  %3 = "llvm.select"(%1, %2, %arg69) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def and_ne_with_one_bit_diff_constants1_before := [llvm|
{
^0(%arg364 : i32):
  %0 = llvm.mlir.constant(51 : i32) : i32
  %1 = llvm.mlir.constant(50 : i32) : i32
  %2 = llvm.icmp "ne" %arg364, %0 : i32
  %3 = llvm.icmp "ne" %arg364, %1 : i32
  %4 = llvm.and %2, %3 : i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

def and_not_or_or_not_or_xor_commute2_after := [llvm|
{
^0(%arg319 : i32, %arg320 : i32, %arg321 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.sdiv %0, %arg319 : i32
  %3 = llvm.or %arg320, %arg321 : i32
  %4 = llvm.xor %arg320, %arg321 : i32
  %5 = llvm.or %4, %2 : i32
  %6 = llvm.and %3, %5 : i32
  %7 = llvm.xor %6, %1 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

def and_ne_with_diff_one_signed_after := [llvm|
{
^0(%arg348 : i64):
  %0 = llvm.mlir.constant(-1) : i64
  %1 = llvm.mlir.constant(-2) : i64
  %2 = llvm.add %arg348, %0 : i64
  %3 = llvm.icmp "ult" %2, %1 : i64
  "llvm.return"(%3) : (i1) -> ()
}
]

def zext_mul_before := [llvm|
{
^0(%arg13 : i8):
  %0 = llvm.mlir.constant(3 : i16) : i16
  %1 = llvm.zext %arg13 : i8 to i16
  %2 = llvm.mul %1, %0 : i16
  %3 = llvm.and %2, %1 : i16
  "llvm.return"(%3) : (i16) -> ()
}
]

@[simp, simp_denote]
instance instRefinement : DialectHRefinement SLLVM SLLVM where
  MonadIsRefinedBy := inferInstanceAs <| HRefinement (EffectM _) (EffectM _)
  IsRefinedBy := { IsRefinedBy := Ty.IsRefinedBy }

match_expr hExpr with
    | Eq w lhsExpr rhsExpr =>

def sext_before := [llvm|
{
^0(%arg9 : i16):
  %0 = llvm.mlir.constant(32768 : i32) : i32
  %1 = llvm.mlir.constant(-32768 : i32) : i32
  %2 = llvm.zext %arg9 : i16 to i32
  %3 = llvm.xor %2, %0 : i32
  %4 = llvm.add %3, %1 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

\n Input expression: {hExpr} has generalization: {pretty}"
                          | GeneralizeContext.Tactic _name =>
                            match cfg.output with
                            | .thmStmt =>
                              let name := Name.mkSimple "foo"
                              pure m! "{H.prettifyAsTheorem name res allVariables widthVals}"
                            | .sexpr =>
                              throwError (H.prettifyAsSexpr res allVariables) widthVals|> format
            | none => throwError m! "Could not generalize {bvLogicalExpr}"
    | _ => throwError m!"The top level constructor is not an equality predicate in {hExpr}"

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

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

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

def llvm_trunc_riscv_32_to_8_nuw_nsw : LLVMPeepholeRewriteRefine 8 [Ty.llvm (.bitvec 32)] :=
  {lhs:= trunc_llvm_32_to_8_nsw_nuw, rhs:= trunc_riscv_32_to_8_nsw_nuw}

def scalar_i32_shl_ult_const_before := [llvm|
{
^0(%arg15 : i32):
  %0 = llvm.mlir.constant(11 : i32) : i32
  %1 = llvm.mlir.constant(131072 : i32) : i32
  %2 = llvm.shl %arg15, %0 : i32
  %3 = llvm.icmp "ult" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def eq_irregular_bit_widths_before := [llvm|
{
^0(%arg114 : i31, %arg115 : i31):
  %0 = llvm.mlir.constant(7 : i31) : i31
  %1 = llvm.mlir.constant(13 : i31) : i31
  %2 = llvm.lshr %arg114, %0 : i31
  %3 = llvm.trunc %2 : i31 to i6
  %4 = llvm.lshr %arg114, %1 : i31
  %5 = llvm.trunc %4 : i31 to i5
  %6 = llvm.lshr %arg115, %0 : i31
  %7 = llvm.trunc %6 : i31 to i6
  %8 = llvm.lshr %arg115, %1 : i31
  %9 = llvm.trunc %8 : i31 to i5
  %10 = llvm.icmp "eq" %3, %7 : i6
  %11 = llvm.icmp "eq" %5, %9 : i5
  %12 = llvm.and %11, %10 : i1
  "llvm.return"(%12) : (i1) -> ()
}
]

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

def test_sge_xor_before := [llvm|
{
^0(%arg38 : i32, %arg39 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg38, %0 : i32
  %2 = llvm.xor %1, %arg39 : i32
  %3 = llvm.icmp "sge" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def bitwise_and_logical_and_masked_icmp_allzeros_before := [llvm|
{
^0(%arg147 : i1, %arg148 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(false) : i1
  %3 = llvm.mlir.constant(7 : i32) : i32
  %4 = llvm.and %arg148, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = "llvm.select"(%5, %arg147, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %7 = llvm.and %arg148, %3 : i32
  %8 = llvm.icmp "eq" %7, %1 : i32
  %9 = llvm.and %6, %8 : i1
  "llvm.return"(%9) : (i1) -> ()
}
]

def idempotent_prop : List (Σ Γ, LLVMPeepholeRewriteRefine 64 Γ) :=
  [⟨_, idempotent_prop_freeze⟩]

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

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

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

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

def narrow_sext_and_before := [llvm|
{
^0(%arg56 : i16, %arg57 : i32):
  %0 = llvm.sext %arg56 : i16 to i32
  %1 = llvm.and %0, %arg57 : i32
  %2 = llvm.trunc %1 : i32 to i16
  "llvm.return"(%2) : (i16) -> ()
}
]

def xor_of_icmps_to_ne_commute_after := [llvm|
{
^0(%arg28 : i64):
  %0 = llvm.mlir.constant(5) : i64
  %1 = llvm.icmp "ne" %arg28, %0 : i64
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def addsub_combine_constants_after := [llvm|
{
^0(%arg14 : i7, %arg15 : i7):
  %0 = llvm.mlir.constant(52 : i7) : i7
  %1 = llvm.sub %arg14, %arg15 : i7
  %2 = llvm.add %1, %0 : i7
  "llvm.return"(%2) : (i7) -> ()
}
]

def Var.tryDelete? [TyDenote Ty] {Γ Γ' : Ctxt Ty} {delv : DeleteRange Γ}
  (DEL : Deleted Γ delv Γ') (vs : HVector Γ.Var β) :
    Option { v' : HVector Γ'.Var β // vs = v'.map DEL.toHom } := do
  match vs with
  | .nil => some ⟨.nil, rfl⟩
  | v ::ₕ vs => do
      let ⟨v, hv⟩ ← tryDeleteOne? DEL v
      let ⟨vs, hvs⟩ ← tryDelete? DEL vs
      return ⟨v ::ₕ vs, by admit /- proof elided -/
      ⟩

def positive_samevar_lshrexact_after := [llvm|
{
^0(%arg42 : i8, %arg43 : i8):
  "llvm.return"(%arg42) : (i8) -> ()
}
]

Holor in Mathlib.Data.Holor
</all_available_defs>

<all_available_lemmas>
List.getD_eq_default in Mathlib.Data.List.GetD
List.getD_eq_getElem in Mathlib.Data.List.GetD
Nat.not_lt in Init.Data.Nat.Basic
Polynomial.coeff_eq_zero_of_degree_lt in Mathlib.Algebra.Polynomial.Degree.Operations
WithBot.bot_lt_coe in Mathlib.Order.WithBot
WithBot.coe_lt_coe in Mathlib.Order.WithBot
ZMod.cast_zero in Mathlib.Data.ZMod.Basic
Fact.elim in Mathlib.Logic.Basic
Nat.cast_add in Mathlib.Data.Nat.Cast.Defs
Nat.cast_one in Mathlib.Data.Nat.Cast.Defs
Nat.succ_eq_add_one in Init.Data.Nat.Basic
ZMod.cast_eq_val in Mathlib.Data.ZMod.Basic
ZMod.natCast_val in Mathlib.Data.ZMod.Basic
ZMod.val_intCast in Mathlib.Data.ZMod.Basic
gt_iff_lt in Init.Core
not_lt_zero' in Mathlib.Algebra.Order.GroupWithZero.Canonical
Polynomial.coeff_inj in Mathlib.Algebra.Polynomial.Basic
Polynomial.degree_eq_bot in Mathlib.Algebra.Polynomial.Degree.Definitions
ZMod.coe_intCast in Mathlib.Data.ZMod.Basic

@[simp]
theorem R.fromPoly_kernel_eq_zero (x : (ZMod q)[X]) : R.fromPoly (n := n) (f q n * x) = 0

theorem R.representative_fromPoly :
    forall a : (ZMod q)[X], (R.fromPoly (n:=n) a).representative = a %ₘ (f q n)

theorem R.fromPoly_rep'_eq_ideal :
    forall a : (ZMod q)[X],
      ∃ i ∈ Ideal.span {f q n}, (R.fromPoly (n:=n) a).representative' = a + i

theorem f_monic : Monic (f q n)

theorem R.coeff_fromTensor (tensor : List Int)
    (htensorlen : tensor.length < 2^n) :
    (R.fromTensor (q := q) (n := n) tensor).coeff i = (tensor.getD i 0)

theorem R.fromTensorFinsupp_coeffs (coeffs : List Int) :
  Polynomial.coeff (fromTensorFinsupp q coeffs) i = ↑(List.getD coeffs i 0)

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

theorem Polynomial.degree_toFinsupp [Semiring M] [DecidableEq M]
  (xs : List M) :
  degree { toFinsupp := List.toFinsupp (l := xs) } ≤ List.length xs

theorem R.fromTensor_eq_fromTensorFinsupp_fromPoly {coeffs : List Int} :
    R.fromTensor (q := q) (n := n) coeffs =
  R.fromPoly (q := q) (n := n) (R.fromTensorFinsupp q coeffs)

theorem R.fromTensorFinsupp_concat_monomial (c : Int) (cs : List Int) :
    (R.fromTensorFinsupp q (cs ++ [c])) =
      (R.fromTensorFinsupp q cs) +
        (Polynomial.monomial cs.length (Int.cast c : (ZMod q)))

@[simp]
theorem R.representative_fromPoly_eq (x : (ZMod q)[X]) (DEGREE: x.degree < (f q n).degree) :
   R.representative q n (R.fromPoly (n:=n) x) = x

theorem f_deg_eq : (f q n).degree = 2^n

@[simp]
theorem R.fromPoly_representative [Fact (q > 1)]:
    forall a : R q n, (R.fromPoly (n:=n) (R.representative q n a)) = a

theorem R.repLength_leq_representative_degree_plus_1 (a : R q n) :
  a.repLength ≤ (R.representative q n a).natDegree + 1

theorem R.toTensor_length {q n} (a : R q n) :
    (R.toTensor a).length = a.repLength

theorem t0_commutative_thm.extracted_1._3 : ∀ (x : BitVec 8) (x_1 : BitVec 1) (x_2 x_3 : BitVec 8),
  ofBool (x_3 == x_2) = 1#1 → ofBool (x_3 != x_2) = 1#1 → x_1 ^^^ 1#1 = 1#1 → False

theorem shl_sub_lshr_thm (e e_1 e_2 : IntW 32) :
  lshr (sub (shl e_2 e_1 { «nsw» := false, «nuw» := true }) e { «nsw» := true, «nuw» := true }) e_1
      { «exact» := true } ⊑
    sub e_2 (lshr e e_1 { «exact» := true }) { «nsw» := true, «nuw» := true }

theorem test3_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), ¬1#32 ≥ ↑32 → (x_1 ||| x <<< 1#32) &&& 1#32 = x_1 &&& 1#32

theorem lshr_xor_or_good_mask_thm (e e_1 : IntW 8) :
  LLVM.or (lshr e_1 (const? 8 4)) (LLVM.xor (lshr e (const? 8 4)) (const? 8 48)) ⊑
    LLVM.or (lshr (LLVM.or e e_1) (const? 8 4)) (const? 8 48) { «disjoint» := true }

theorem test_nuw_nsw_and_signed_pred_proof : test_nuw_nsw_and_signed_pred_before ⊑ test_nuw_nsw_and_signed_pred_after

theorem e_283 :
    3 *  ~~~y + 5 * (x |||  ~~~y) + 2 * (x ||| y) - 9 *  ~~~(x ||| y) - 3 *  ~~~(x |||  ~~~y) - 11 * (x &&&  ~~~y) - 8 * (x &&& y) =  - 1 *  ~~~(x &&&  ~~~x)

theorem ashr_ugt_13_proof : ashr_ugt_13_before ⊑ ashr_ugt_13_after

theorem test15_thm (e : IntW 1) :
  shl (select e (const? 45 3) (const? 45 1)) (const? 45 2) ⊑ select e (const? 45 12) (const? 45 4)

theorem ashrslt_01_05_exact_thm (e : IntW 4) :
  icmp IntPred.slt (ashr e (const? 4 1) { «exact» := true }) (const? 4 5) ⊑ const? 1 1

theorem PR42691_1_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x <ₛ 0#32) ||

theorem and_ne_with_diff_one_signed_logical_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ofBool (x != -1#64) = 1#1 → ofBool (x != 0#64) = ofBool (x + -1#64 <ᵤ BitVec.ofInt 64 (-2))

theorem test_proof : test_before ⊑ test_after

theorem sdiv_eq_smin_thm (e e_1 : IntW 8) :
  icmp IntPred.eq (LLVM.sdiv e_1 e) (const? 8 (-128)) ⊑
    LLVM.and (icmp IntPred.eq e_1 (const? 8 (-128))) (icmp IntPred.eq e (const? 8 1))

theorem lshr_shl_pow2_const_case1_thm.extracted_1._2 : ∀ (x : BitVec 16),
  ¬(x ≥ ↑16 ∨ 2#16 ≥ ↑16) → ¬ofBool (x == 7#16) = 1#1 → 256#16 >>> x <<< 2#16 &&& 8#16 = 0#16

theorem trunc_ashr_trunc_outofrange_proof : trunc_ashr_trunc_outofrange_before ⊑ trunc_ashr_trunc_outofrange_after

theorem t0_ult_slt_65536_thm.extracted_1._15 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (x_2 <ᵤ 65536#32) = 1#1 →
    ¬ofBool (x_2 <ₛ 65536#32) = 1#1 → ¬ofBool (65535#32 <ₛ x_2) = 1#1 → ¬ofBool (x_2 <ₛ 0#32) = 1#1 → x = x_2

theorem main7c_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (x_2 == x_2 &&& x_1) &&& ofBool (x * 42#32 == x * 42#32 &&& x_1) = 1#1 →
    1#32 = zeroExtend 32 (ofBool (x_1 &&& (x_2 ||| x * 42#32) != x_2 ||| x * 42#32))

theorem main4e_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 → ¬0#1 = 1#1 → 1#32 = zeroExtend 32 1#1

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

theorem masked_icmps_mask_notallzeros_bmask_mixed_7b_thm (e : IntW 32) :
  LLVM.and (icmp IntPred.ne (LLVM.and e (const? 32 6)) (const? 32 0))
      (icmp IntPred.eq (LLVM.and e (const? 32 15)) (const? 32 8)) ⊑
    const? 1 0

theorem alive_Select_1087 : forall (w : Nat) (Y X val : Bitvec 1)
, TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec w)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (val) %v0;
  %v2 := op:const (↑true) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:xor 1 %v3;
  %v5 := op:const (X) %v0;
  %v6 := op:const (Y) %v0;
  %v7 := triple:%v4 %v5 %v6;
  %v8 := op:select w %v7
  dsl_ret %v8
  ]  ⊑
  TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec w)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (val) %v0;
  %v2 := op:const (↑true) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:xor 1 %v3;
  %v5 := op:const (Y) %v0;
  %v6 := op:const (X) %v0;
  %v7 := triple:%v1 %v5 %v6;
  %v8 := op:select w %v7
  dsl_ret %v8
  ]

theorem e_2 :
    1 *  ~~~x - 2 * (x ^^^ y) + 1 *  ~~~(x &&& y) = 2 *  ~~~(x ||| y) - 1 * (x &&&  ~~~y)

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

theorem shrink_or_proof : shrink_or_before ⊑ shrink_or_after

theorem drop_nuw_trunc_thm (e e_1 : IntW 16) :
  trunc 8 (LLVM.and (LLVM.and e_1 (const? 16 255)) e) { «nsw» := false, «nuw» := true } ⊑
    trunc 8 (LLVM.and e_1 e)

theorem icmp_slt_sext_ne_otherwise_nofold_thm (e : IntW 32) :
  icmp IntPred.slt (sext 32 (icmp IntPred.ne e (const? 32 2))) e ⊑
    icmp IntPred.sgt e (sext 32 (icmp IntPred.ne e (const? 32 2)))

theorem bitwise_and_logical_and_masked_icmp_allones_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (x &&& 8#32 == 8#32) = 1#1 →
    ¬ofBool (x &&& 15#32 == 15#32) = 1#1 → 0#1 &&& ofBool (x &&& 7#32 == 7#32) = 0#1

theorem PR38021_thm (e : IntW 8) :
  add (lshr e (const? 8 3)) (const? 8 (-63)) ⊑
    add (lshr e (const? 8 3)) (const? 8 (-63)) { «nsw» := true, «nuw» := true }

theorem test17_proof : test17_before ⊑ test17_after

theorem select_ashr_icmp_bad_thm (e e_1 e_2 : IntW 32) :
  select (icmp IntPred.eq e_2 (const? 32 1)) (ashr e_1 e_2) e ⊑
    select (icmp IntPred.eq e_2 (const? 32 1)) (ashr e_1 (const? 32 1)) e

theorem badimm2_proof : badimm2_before ⊑ badimm2_after

theorem fold_icmp_shl_nuw_c2_indivisible_thm (e : IntW 32) :
  icmp IntPred.ult (shl (const? 32 16) e { «nsw» := false, «nuw» := true }) (const? 32 63) ⊑
    icmp IntPred.ult e (const? 32 2)

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

omit [LawfulBEq A] [Fintype S] in
lemma processOneElem_rel {s₁ s₂ : State} :
    s₂ ~[(processOneElem A S final s₁ st (a, sa)).rel] sa' ↔
      (s₂ ~[st.rel] sa' ∨ (s₂ = st.m.stateMax ∧ sa' = sa ∧ st.map[sa']? = none))

theorem lshrult_02_05_exact_proof : lshrult_02_05_exact_before ⊑ lshrult_02_05_exact_after

theorem e_2377 :
     - 1 * (f ^^^  ~~~(d |||  ~~~e)) + 1 * (f ^^^  ~~~(d ||| (e &&& f))) - 1 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) - 7 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) - 1 * (e ^^^  ~~~(d |||  ~~~f)) - 1 *  ~~~( ~~~d &&& (e ||| f)) + 3 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) + 5 * ( ~~~(d &&& e) &&& (d ^^^ (e ^^^ f))) - 3 * (e &&&  ~~~(d &&& f)) - 1 * (e ||| (d &&& f)) - 5 * (d &&&  ~~~e) + 4 * (d |||  ~~~f) + 1 *  ~~~( ~~~d &&& ( ~~~e &&& f)) - 7 * (e ^^^  ~~~(d &&& f)) - 1 *  ~~~(d ^^^ f) + 11 * ( ~~~e |||  ~~~(d ^^^ f)) - 2 * ( ~~~d ||| (e ||| f)) - 1 * (e ^^^ (d ||| (e ||| f))) - 1 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) - 11 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f)) + 5 * (e &&& f) + 1 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) - 2 *  ~~~d + 2 * ((d &&&  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) - 1 * ((d |||  ~~~e) &&& (e ^^^ f)) + 2 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) + 1 * (f ^^^ (d |||  ~~~e)) - 3 * ((e &&& f) ^^^  ~~~( ~~~d &&& (e ^^^ f))) + 5 * ((d ||| e) &&&  ~~~(e ^^^ f)) + 3 *  ~~~(d &&&  ~~~e) + 5 * ( ~~~d &&& (e ^^^ f)) + 4 * (d ^^^ (e &&& f)) + 7 * ((d &&& f) ^^^ (d ^^^ ( ~~~e &&& f))) - 2 * (e |||  ~~~f) + 1 * ((d &&&  ~~~e) ||| (e ^^^ f)) - 1 *  ~~~(e ^^^ f) - 2 * (e ^^^ (d &&& (e ^^^ f))) - 5 * (f &&&  ~~~(d &&&  ~~~e)) - 1 * ((d &&& e) ^^^ (e |||  ~~~f)) + 2 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) + 4 * (e ^^^  ~~~(d &&& ( ~~~e ||| f))) + 5 * (f ^^^ (d ||| ( ~~~e ||| f))) - 6 * ((d &&& f) ^^^  ~~~(d ^^^ ( ~~~e &&& f))) + 7 * ( ~~~(d &&& e) &&&  ~~~(d ^^^ (e ^^^ f))) - 11 * ( ~~~(d |||  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) - 11 * (f ||| (d &&&  ~~~e)) - 3 * (e &&& (d ||| f)) + 2 * (e |||  ~~~(d ^^^ f)) + 11 * ( ~~~(d ^^^ e) |||  ~~~(d ^^^ f)) + 2 * (d &&& ( ~~~e ||| f)) - 1 * (f ||| (d ^^^ e)) + 11 * (f ^^^ (d ||| ( ~~~e &&& f))) - 5 * (e ^^^  ~~~(d &&& (e &&& f))) - 2 * (f ^^^ (d &&& ( ~~~e ||| f))) - 1 * (d &&& (e ||| f)) - 1 * (f &&& (d ||| e)) - 2 *  ~~~(d ^^^ e) + 11 *  ~~~( ~~~d ||| (e &&& f)) + 2 * (f ^^^ ( ~~~d ||| ( ~~~e ||| f))) + 1 *  ~~~( ~~~d ||| ( ~~~e &&& f)) - 11 *  ~~~(d &&& ( ~~~e ||| f)) + 1 * (f |||  ~~~(d |||  ~~~e)) + 29 *  ~~~(d ||| (e ||| f)) + 8 *  ~~~(d ||| ( ~~~e ||| f)) - 35 *  ~~~( ~~~d ||| (e ||| f)) - 29 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 20 * ( ~~~d &&& ( ~~~e &&& f)) + 20 * ( ~~~d &&& (e &&& f)) + 2 * (d &&& ( ~~~e &&& f)) + 21 * (d &&& (e &&& f)) = 11 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f)))

theorem absdiff_thm.extracted_1._1 : ∀ (x x_1 : BitVec 64),
  ofBool (x_1 <ᵤ x) = 1#1 →
    (signExtend 64 (ofBool (x_1 <ᵤ x)) ^^^ x_1 - x) - signExtend 64 (ofBool (x_1 <ᵤ x)) = 0#64 - (x_1 - x)

theorem lowmask_sub_zext_commute_thm.extracted_1._1 : ∀ (x : BitVec 5) (x_1 : BitVec 17),
  x_1 - zeroExtend 17 x &&& 31#17 = zeroExtend 17 (truncate 5 x_1 - x)

theorem e_1172 :
    5 * (z |||  ~~~t) - 5 *  ~~~z - 5 *  ~~~t + 4 *  ~~~(z &&&  ~~~t) + 1 *  ~~~(z ||| t) + 12 *  ~~~(z |||  ~~~t) + 11 * (z &&&  ~~~t) + 2 * (z &&& t) = 11 * (z ||| t)

theorem a_or_b_const_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 == x_1) &&& ofBool (x != x_1) ||

theorem test_and3_logical_thm (e e_1 : IntW 32) :
  select (icmp IntPred.sgt (LLVM.and e_1 (const? 32 2147483647)) e) (icmp IntPred.sge e (const? 32 0))
      (const? 1 0) ⊑
    icmp IntPred.ult e (LLVM.and e_1 (const? 32 2147483647))

theorem both_thm.extracted_1._2 : ∀ (x x_1 : BitVec 8),
  ¬(x_1 ≥ ↑8 ∨ x ≥ ↑8) →
    ¬(True ∧ ((-1#8) <<< x_1).sshiftRight' x_1 ≠ -1#8 ∨
          x_1 ≥ ↑8 ∨ True ∧ ((-1#8) <<< x).sshiftRight' x ≠ -1#8 ∨ x ≥ ↑8) →
      ofBool ((-1#8) <<< x_1 ^^^ -1#8 <ᵤ (-1#8) <<< x ^^^ -1#8) = ofBool ((-1#8) <<< x <ᵤ (-1#8) <<< x_1)

theorem shl_lshr_demand6_thm.extracted_1._2 : ∀ (x : BitVec 16),
  ¬(x ≥ ↑16 ∨ 4#16 ≥ ↑16) →
    ¬x ≥ ↑16 → BitVec.ofInt 16 (-32624) <<< x >>> 4#16 &&& 4094#16 = 2057#16 <<< x &&& 4094#16

theorem a_true_implies_b_true2_comm_thm.extracted_1._4 : ∀ (x : BitVec 1) (x_1 : BitVec 8),
  ¬ofBool (10#8 <ᵤ x_1) = 1#1 → ¬ofBool (20#8 <ᵤ x_1) = 1#1 → x &&& ofBool (20#8 <ᵤ x_1) = 0#1

theorem sge_to_ugt_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (15#8 ≤ₛ x ^^^ BitVec.ofInt 8 (-128)) = ofBool (BitVec.ofInt 8 (-114) <ᵤ x)

theorem lshrult_01_00_exact_proof : lshrult_01_00_exact_before ⊑ lshrult_01_00_exact_after

theorem abs_must_be_positive_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (0#32 ≤ₛ x) = 1#1 → ¬(True ∧ (0#32).ssubOverflow x = true) → ofBool (0#32 ≤ₛ 0#32 - x) = 1#1

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

theorem PR42691_9_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬ofBool (13#32 <ₛ x) = 1#1 → 0#1 = ofBool (x + BitVec.ofInt 32 (-14) <ᵤ 2147483633#32)

theorem t0_thm.extracted_1._10 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1),
  ¬x_2 ^^^ 1#1 = 1#1 → ¬x_2 = 1#1 → ¬0#1 = 1#1 → False

lemma Term.evalFin_eq_eval (t : Term)
   (varsList : List BitStream) (varsFin : Fin t.arity → BitStream)
   (hvars : ∀ (i : Fin t.arity), varsList.getD i default = (varsFin i)) :
    Term.evalFin t varsFin = Term.eval t varsList

theorem ashrsgt_03_08_proof : ashrsgt_03_08_before ⊑ ashrsgt_03_08_after

theorem alive_AndOrXor_2243__B__C__A__B___B__A__C : alive_AndOrXor_2243__B__C__A__B___B__A__C_src ⊑ alive_AndOrXor_2243__B__C__A__B___B__A__C_tgt

theorem or_nontrivial_mask1_proof : or_nontrivial_mask1_before ⊑ or_nontrivial_mask1_after

theorem ashr_known_pos_exact_proof : ashr_known_pos_exact_before ⊑ ashr_known_pos_exact_after

theorem test4_thm (e : IntW 1) (e_1 : IntW 32) :
  urem e_1 (select e (const? 32 1) (const? 32 8)) ⊑ LLVM.and e_1 (select e (const? 32 0) (const? 32 7))

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

theorem src_x_and_nmask_ne_thm.extracted_1._3 : ∀ (x : BitVec 8) (x_1 : BitVec 1) (x_2 : BitVec 8),
  x_1 = 1#1 →
    ¬x ≥ ↑8 →
      ¬(True ∧ ((-1#8) <<< x).sshiftRight' x ≠ -1#8 ∨ x ≥ ↑8) →
        ofBool (x_2 &&& (-1#8) <<< x != (-1#8) <<< x) = ofBool (x_2 <ᵤ (-1#8) <<< x)

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

theorem test_sext_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  x_1 + signExtend 32 (ofBool (x == 0#32)) ^^^ -1#32 = signExtend 32 (ofBool (x != 0#32)) - x_1

theorem xor_and_logic_or2_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 1),
  x = 1#1 → x_1 = 1#1 → x_2 &&& x_1 ^^^ 1#1 = x_2 ^^^ 1#1

theorem test3_proof : test3_before ⊑ test3_after

theorem test12_thm (e : IntW 32) : LLVM.srem (LLVM.and e (const? 32 (-4))) (const? 32 2) ⊑ const? 32 0

theorem mul_add_to_mul_6_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(True ∧ x_1.smulOverflow x = true ∨
        True ∧ x_1.smulOverflow x = true ∨
          True ∧ (x_1 * x).smulOverflow 5#32 = true ∨ True ∧ (x_1 * x).saddOverflow (x_1 * x * 5#32) = true) →
    True ∧ x_1.smulOverflow x = true ∨ True ∧ (x_1 * x).smulOverflow 6#32 = true → False

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

lemma RawCNFA.reverse_spec_procesState {m : RawCNFA A} (hwf : m.WF) s₀ a₀ ss' (hs₀ : s₀ ∈ m.states) :
    let motive m' ss' :=
      (∀ s ∈ ss', s ∈ m.states) →
        m'.WF ∧ m'.stateMax = m.stateMax ∧ m'.initials = m.initials ∧ m'.finals = m.finals ∧
          ∀ s a s', s' ∈ m'.tr s a ↔ (s' ∈ m.tr s a ∨ s' = s₀ ∧ a = a₀ ∧ s ∈ ss')
    motive (RawCNFA.reverse.processState m (s₀, a₀) ss') ss'.toSet

theorem t3_thm.extracted_1._2 : ∀ (x : BitVec 32) (x_1 : BitVec 64),
  ¬(x ≥ ↑32 ∨ zeroExtend 64 (4#32 <<< x) = 0) →
    ¬(True ∧ (x + 2#32).msb = true ∨ zeroExtend 64 (x + 2#32) ≥ ↑64) →
      x_1 / zeroExtend 64 (4#32 <<< x) = x_1 >>> zeroExtend 64 (x + 2#32)

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 exact_lshr_eq_opposite_msb_proof : exact_lshr_eq_opposite_msb_before ⊑ exact_lshr_eq_opposite_msb_after

theorem falseIffLt_eq_false_iff (n i : Nat) :
    falseIffLt n i = false ↔ i < n

theorem PR2844_logical_thm.extracted_1._4 : ∀ (x : BitVec 32),
  ¬ofBool (x == 0#32) = 1#1 →
    ¬ofBool (x <ₛ BitVec.ofInt 32 (-638208501)) = 1#1 →
      1#32 = zeroExtend 32 (ofBool (x != 0#32) &&& ofBool (BitVec.ofInt 32 (-638208502) <ₛ x))

@[grind ., simp] lemma RawCNFA.empty_mem_finals {s : State} : s ∉ empty (A := A).finals

theorem t0_thm (e : IntW 8) :
  ashr (shl e (const? 8 7)) (const? 8 7) ⊑
    sub (const? 8 0) (LLVM.and e (const? 8 1)) { «nsw» := true, «nuw» := false }

theorem sub_const_add_const_proof : sub_const_add_const_before ⊑ sub_const_add_const_after

theorem ashrslt_03_01_thm (e : IntW 4) : icmp IntPred.slt (ashr e (const? 4 3)) (const? 4 1) ⊑ const? 1 1

theorem select_xor_icmp_bad_5_proof : select_xor_icmp_bad_5_before ⊑ select_xor_icmp_bad_5_after

theorem sextinreg_alt_thm.extracted_1._1 : ∀ (x : BitVec 32),
  16#32 ≥ ↑32 ∨ True ∧ x <<< 16#32 >>> 16#32 <<< 16#32 ≠ x <<< 16#32 ∨ 16#32 ≥ ↑32 → False

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

theorem masked_icmps_mask_notallzeros_bmask_mixed_swapped_1b_logical_proof : masked_icmps_mask_notallzeros_bmask_mixed_swapped_1b_logical_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_swapped_1b_logical_after

theorem and_or2_proof : and_or2_before ⊑ and_or2_after
</all_available_lemmas>

<local_ctx>
import SSA.Projects.FullyHomomorphicEncryption.Basic

import Batteries.Data.List.Lemmas

import Mathlib.Data.List.Basic

namespace Poly

open Polynomial in

open Polynomial in

end Poly

namespace Poly
</local_ctx>

<target_theorem>
theorem fromTensor_toTensor [hqgt1 : Fact (q > 1)] (a : R q n)
    (adeg : (R.representative q n a).natDegree + 1 < 2^n) :
  R.fromTensor a.toTensor = a :=
</target_theorem>

