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>
BitVec.xor in Init.Data.BitVec.Basic
Bool in Init.Prelude
DecidableEq in Init.Prelude
Repr in Init.Data.Repr
List in Init.Prelude
Finset in Mathlib.Data.Finset.Defs
Sum in Init.Core
Sum.elim in Init.Data.Sum.Basic
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
ZMod in Mathlib.Data.ZMod.Defs
Sum.inl in Init.Core
Sum.inr in Init.Core
HOr in Init.Prelude
HOr.hOr in Init.Prelude
OrOp in Init.Prelude
AndOp in Init.Prelude
HAnd in Init.Prelude
HAnd.hAnd in Init.Prelude

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

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

def select_icmp_ne_pow2_flipped_after := [llvm|
{
^0(%arg9 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.or %arg9, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

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

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

def andn_or_cmp_1_logical_after := [llvm|
{
^0(%arg173 : i37, %arg174 : i37, %arg175 : i37):
  %0 = llvm.mlir.constant(42 : i37) : i37
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "sle" %arg173, %arg174 : i37
  %3 = llvm.icmp "ugt" %arg175, %0 : i37
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def test13_before := [llvm|
{
^0(%arg0 : i1024):
  %0 = llvm.mlir.constant(1016 : i1024) : i1024
  %1 = llvm.mlir.constant(255 : i1024) : i1024
  %2 = llvm.ashr %arg0, %0 : i1024
  %3 = llvm.and %2, %1 : i1024
  "llvm.return"(%3) : (i1024) -> ()
}
]

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

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

def mul_of_bools_before := [llvm|
{
^0(%arg91 : i32, %arg92 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.and %arg91, %0 : i32
  %3 = llvm.and %arg92, %0 : i32
  %4 = llvm.mul %2, %3 : i32
  %5 = llvm.icmp "ult" %4, %1 : i32
  "llvm.return"(%5) : (i1) -> ()
}
]

def add_smin_simplify_after := [llvm|
{
^0(%arg34 : i32):
  %0 = llvm.mlir.constant(-3 : i32) : i32
  %1 = llvm.add %arg34, %0 overflow<nsw> : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def icmp_ne_sext_ne_zero_before := [llvm|
{
^0(%arg24 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "ne" %arg24, %0 : i32
  %2 = llvm.sext %1 : i1 to i32
  %3 = llvm.icmp "ne" %2, %arg24 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def sle_swap_or_not_min_after := [llvm|
{
^0(%arg280 : i8, %arg281 : i8):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def or_xor_tree_0011_before := [llvm|
{
^0(%arg36 : i32, %arg37 : i32, %arg38 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mul %arg36, %0 : i32
  %2 = llvm.mul %arg37, %0 : i32
  %3 = llvm.mul %arg38, %0 : i32
  %4 = llvm.xor %2, %1 : i32
  %5 = llvm.xor %3, %2 : i32
  %6 = llvm.xor %5, %1 : i32
  %7 = llvm.or %4, %6 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

def test_invert_demorgan_or3_after := [llvm|
{
^0(%arg13 : i32, %arg14 : i32):
  %0 = llvm.mlir.constant(178206 : i32) : i32
  %1 = llvm.mlir.constant(-196608 : i32) : i32
  %2 = llvm.mlir.constant(-1506 : i32) : i32
  %3 = llvm.mlir.constant(-917760 : i32) : i32
  %4 = llvm.mlir.constant(-716213 : i32) : i32
  %5 = llvm.mlir.constant(-1114112 : i32) : i32
  %6 = llvm.mlir.constant(-196112 : i32) : i32
  %7 = llvm.icmp "ne" %arg13, %0 : i32
  %8 = llvm.add %arg14, %1 : i32
  %9 = llvm.icmp "ult" %8, %2 : i32
  %10 = llvm.add %arg14, %3 : i32
  %11 = llvm.icmp "ult" %10, %4 : i32
  %12 = llvm.add %arg14, %5 : i32
  %13 = llvm.icmp "ult" %12, %6 : i32
  %14 = llvm.and %7, %9 : i1
  %15 = llvm.and %14, %11 : i1
  %16 = llvm.and %15, %13 : i1
  "llvm.return"(%16) : (i1) -> ()
}
]

def BoolBinaryRelationKind.toSmtLib : BoolBinaryRelationKind → SexprPBV.BoolBinaryRelationKind
| .eq => .eq

def zext_sext_sgt_known_nonneg_before := [llvm|
{
^0(%arg24 : i8, %arg25 : i8):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.udiv %0, %arg24 : i8
  %2 = llvm.zext %1 : i8 to i32
  %3 = llvm.sext %arg25 : i8 to i32
  %4 = llvm.icmp "sgt" %2, %3 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

def udiv_shl_mul_nuw_exact_before := [llvm|
{
^0(%arg142 : i5, %arg143 : i5, %arg144 : i5):
  %0 = llvm.shl %arg142, %arg144 overflow<nuw> : i5
  %1 = llvm.mul %arg142, %arg143 overflow<nuw> : i5
  %2 = llvm.udiv exact %0, %1 : i5
  "llvm.return"(%2) : (i5) -> ()
}
]

def scalar_i8_lshr_and_signbit_eq_before := [llvm|
{
^0(%arg35 : i8, %arg36 : i8):
  %0 = llvm.mlir.constant(-128 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.lshr %arg35, %arg36 : i8
  %3 = llvm.and %2, %0 : i8
  %4 = llvm.icmp "eq" %3, %1 : i8
  "llvm.return"(%4) : (i1) -> ()
}
]

def test_shl_nuw_nsw__nsw_is_safe_before := [llvm|
{
^0(%arg75 : i32):
  %0 = llvm.mlir.constant(-83886080 : i32) : i32
  %1 = llvm.mlir.constant(-83886079 : i32) : i32
  %2 = llvm.mlir.constant(2 : i32) : i32
  %3 = llvm.mlir.constant(-335544316 : i32) : i32
  %4 = llvm.or %arg75, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.shl %4, %2 overflow<nsw,nuw> : i32
  %7 = "llvm.select"(%5, %3, %6) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %8 = llvm.mul %7, %4 : i32
  %9 = llvm.mul %8, %6 : i32
  "llvm.return"(%9) : (i32) -> ()
}
]

def cmpeq_xor_cst3_before := [llvm|
{
^0(%arg22 : i32, %arg23 : i32):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.xor %arg22, %0 : i32
  %2 = llvm.xor %arg23, %0 : i32
  %3 = llvm.icmp "eq" %1, %2 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

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

def OrSextSext : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] where
  lhs := [LV| {
    ^entry (%x: i32, %y: i32):
      %0 = llvm.sext %x : i32 to i64
      %1 = llvm.sext %y : i32 to i64
      %2 = llvm.or %0, %1 : i64
      llvm.return %2 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i32, %y: i32):
      %0 = llvm.or %x, %y : i32
      %1 = llvm.sext %0 : i32 to i64
      llvm.return %1 : i64
  }]

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

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

def urem? {w : Nat} (x y : BitVec w) : IntW w :=
  if y = 0 then
    .poison
  else
    .value <| x % y

@[simp_denote]
def icmp_ule_llvm_32 : Com LLVMPlusRiscV ⟨[.llvm (.bitvec 32), .llvm (.bitvec 32)]⟩
  .pure (.llvm (.bitvec 1)) := [LV| {
  ^entry (%lhs: i32, %rhs: i32):
    %1 = llvm.icmp.ule %lhs, %rhs : i32
    llvm.return %1 : i1
  }]

def product (final? : Prop → Prop → Prop) (M N : NFA' n) : NFA' n where
  σ := _
  M := M.M.product final? N.M

def and_not_or_wrong_b_before := [llvm|
{
^0(%arg428 : i32, %arg429 : i32, %arg430 : i32, %arg431 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg428, %arg429 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.or %2, %arg430 : i32
  %4 = llvm.and %arg428, %arg430 : i32
  %5 = llvm.xor %4, %0 : i32
  %6 = llvm.or %5, %arg431 : i32
  %7 = llvm.and %3, %6 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

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

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

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

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

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 p0_after := [llvm|
{
^0(%arg16 : i8, %arg17 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.lshr %arg16, %arg17 : i8
  %2 = llvm.icmp "eq" %1, %0 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def or_eq_notY_eq_0_before := [llvm|
{
^0(%arg45 : i8, %arg46 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.xor %arg46, %0 : i8
  %2 = llvm.or %arg45, %1 : i8
  %3 = llvm.icmp "eq" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

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

instance : Trans (@ExtEq Op) ExtEq ExtEq := ⟨ExtEq.trans⟩

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

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 test22_logical_before := [llvm|
{
^0(%arg5 : i32, %arg6 : i32):
  %0 = llvm.mlir.constant(100663295 : i32) : i32
  %1 = llvm.mlir.constant(268435456 : i32) : i32
  %2 = llvm.mlir.constant(7 : i32) : i32
  %3 = llvm.mlir.constant(-1 : i32) : i32
  %4 = llvm.mlir.constant(true) : i1
  %5 = llvm.and %arg5, %0 : i32
  %6 = llvm.icmp "ult" %5, %1 : i32
  %7 = llvm.and %arg6, %2 : i32
  %8 = llvm.icmp "sgt" %7, %3 : i32
  %9 = "llvm.select"(%6, %4, %8) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%9) : (i1) -> ()
}
]

def not_or_or_and_no_and_before := [llvm|
{
^0(%arg121 : i32, %arg122 : i32, %arg123 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg122, %arg121 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.xor %arg121, %0 : i32
  %4 = llvm.or %3, %arg122 : i32
  %5 = llvm.or %4, %arg123 : i32
  %6 = llvm.and %5, %2 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def and_logic_and_logic_or_4_before := [llvm|
{
^0(%arg129 : i1, %arg130 : i1, %arg131 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.and %arg130, %arg129 : i1
  %3 = "llvm.select"(%arg131, %arg129, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%2, %1, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

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

def test2_before := [llvm|
{
^0(%arg0 : i999, %arg1 : i999):
  %0 = llvm.mlir.constant(65280 : i999) : i999
  %1 = llvm.and %arg0, %0 : i999
  %2 = llvm.and %arg1, %0 : i999
  %3 = llvm.icmp "ne" %1, %2 : i999
  "llvm.return"(%3) : (i1) -> ()
}
]

def shlMax (a : BitVec v) (b : BitVec w) : BitVec (max v w) :=
   a.signExtend (max v w) <<< b.signExtend (max v w)

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

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

def n5_after := [llvm|
{
^0(%arg9 : i8, %arg10 : i8, %arg11 : i8):
  "llvm.return"(%arg11) : (i8) -> ()
}
]

Lean.FVarId in Lean.Expr

def test67_before := [llvm|
{
^0(%arg113 : i1, %arg114 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(24 : i32) : i32
  %2 = llvm.mlir.constant(-16777216 : i32) : i32
  %3 = llvm.mlir.constant(0 : i8) : i8
  %4 = llvm.zext %arg113 : i1 to i32
  %5 = llvm.xor %4, %0 : i32
  %6 = llvm.and %arg114, %5 : i32
  %7 = llvm.shl %6, %1 overflow<nsw,nuw> : i32
  %8 = llvm.xor %7, %2 : i32
  %9 = llvm.ashr exact %8, %1 : i32
  %10 = llvm.trunc %9 : i32 to i8
  %11 = llvm.icmp "eq" %10, %3 : i8
  "llvm.return"(%11) : (i1) -> ()
}
]

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

def eq_umin1_before := [llvm|
{
^0(%arg60 : i32, %arg61 : i32):
  %0 = llvm.icmp "ult" %arg60, %arg61 : i32
  %1 = "llvm.select"(%0, %arg60, %arg61) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "eq" %1, %arg60 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

decidable_of_iff in Init.PropLemmas

def ult_rem_zero_after := [llvm|
{
^0(%arg174 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.icmp "ult" %arg174, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def or_or_and_complex_after := [llvm|
{
^0(%arg82 : i64):
  %0 = llvm.mlir.constant(8) : i64
  %1 = llvm.mlir.constant(71777214294589695) : i64
  %2 = llvm.mlir.constant(-71777214294589696) : i64
  %3 = llvm.lshr %arg82, %0 : i64
  %4 = llvm.shl %arg82, %0 : i64
  %5 = llvm.and %3, %1 : i64
  %6 = llvm.and %4, %2 : i64
  %7 = llvm.or disjoint %5, %6 : i64
  "llvm.return"(%7) : (i64) -> ()
}
]

def test12_after := [llvm|
{
^0(%arg46 : i32, %arg47 : i32):
  %0 = llvm.mlir.constant(1431655765 : i32) : i32
  %1 = llvm.and %arg46, %0 : i32
  %2 = llvm.sub %arg47, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def test_nuw_nsw_and_unsigned_pred_after := [llvm|
{
^0(%arg55 : i64):
  %0 = llvm.mlir.constant(6) : i64
  %1 = llvm.icmp "ugt" %arg55, %0 : i64
  "llvm.return"(%1) : (i1) -> ()
}
]

def trunc_shl_zext_64_before := [llvm|
{
^0(%arg0 : i64):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.trunc %arg0 : i64 to i8
  %2 = llvm.shl %1, %0 : i8
  %3 = llvm.zext %2 : i8 to i64
  "llvm.return"(%3) : (i64) -> ()
}
]

def rgn {Γ : Ctxt _} (k : Nat) (input : Var Γ .nat) (body : Com [ExTy.nat] ExTy.nat) :
    Expr Γ .nat :=
  Expr.mk
    (op := .runK k)
    (ty_eq := rfl)
    (eff_le := EffectKind.pure_le _)
    (args := .cons input .nil)
    (regArgs := HVector.cons (body.castPureToEff _) HVector.nil)

@[simp_denote]
def add_hi_and_lo_negone_llvm_i64 := [LV| {
    ^entry (%arg: i64):
    %1 = llvm.mlir.constant (-1) : i64
    %0 = llvm.add %arg, %1 overflow<nsw> : i64
    llvm.return %0 : i64
  }]

@[simp]
def EnvFin.get_ofEnv (env : Env w) (n : Nat) (i : Fin n) : (EnvFin.ofEnv env n) i = env.getD i 0#w := rfl

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

def test_sub_nuw__nsw_is_safe_before := [llvm|
{
^0(%arg22 : i32):
  %0 = llvm.mlir.constant(-2147483648 : i32) : i32
  %1 = llvm.mlir.constant(-2147483647 : i32) : i32
  %2 = llvm.mlir.constant(-1 : i32) : i32
  %3 = llvm.or %arg22, %0 : i32
  %4 = llvm.icmp "eq" %3, %1 : i32
  %5 = llvm.sub %0, %3 overflow<nuw> : i32
  %6 = "llvm.select"(%4, %2, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%6) : (i32) -> ()
}
]

IO.FS.Handle.mk in Init.System.IO

def IndexInvariant (f : LoopBody t) : Prop :=
  ∀ (i j : Int) (v : t), f i v = f j v

def positive_samevar_shlnuwnsw_before := [llvm|
{
^0(%arg47 : i8, %arg48 : i8):
  %0 = llvm.ashr %arg47, %arg48 : i8
  %1 = llvm.shl %0, %arg48 overflow<nsw,nuw> : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

class HasUB (m : Type u → Type v) where
   
  throwUB {α : Type u} : m α

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

ToString in Init.Data.ToString.Basic

def test_after := [llvm|
{
^0(%arg0 : i26):
  "llvm.return"(%arg0) : (i26) -> ()
}
]

RV64.srlw in RISCV.Instructions

|
</all_available_defs>

<all_available_lemmas>
Finset.subset_iff in Mathlib.Data.Finset.Defs
List.mem_append in Init.Data.List.Lemmas
List.mem_dedup in Mathlib.Data.List.Dedup
Finset.mem_union in Mathlib.Data.Finset.Lattice.Basic
List.subset_def in Init.Data.List.Sublist
Finset.mem_biUnion in Mathlib.Data.Finset.Union

theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]

@[simp]
theorem Eqn.denoteFin_width_zero  (es : Eqn) (env : EnvFin 0 es.numVars) :
    Eqn.denoteFin es env = 0

theorem test35_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(True ∧ (0#32 - x &&& 240#32).msb = true) →
    0#64 - zeroExtend 64 x &&& 240#64 = zeroExtend 64 (0#32 - x &&& 240#32)

theorem demorgan_nor_proof : demorgan_nor_before ⊑ demorgan_nor_after

theorem e_2085 :
     - 7 *  ~~~(d ||| ( ~~~e &&& f)) - 3 * (f ^^^  ~~~(d ||| (e &&& f))) - 1 * (e ^^^  ~~~(d ||| (e &&& f))) + 1 * (f ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 2 * (d &&&  ~~~e) + 1 * (e ^^^ (d &&&  ~~~f)) + 5 * ((d ||| e) &&& (d ^^^ (e ^^^ f))) - 5 *  ~~~(d ^^^ ( ~~~e ||| f)) + 4 * (e ^^^ (d ||| (e ^^^ f))) - 1 * (d &&& ( ~~~e ||| f)) - 11 *  ~~~(e |||  ~~~f) - 2 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 2 * ((d &&& e) |||  ~~~(e ||| f)) + 1 * (f ^^^  ~~~(d |||  ~~~e)) - 3 * ((d ||| e) &&& (e ^^^ f)) + 2 *  ~~~e + 7 *  ~~~( ~~~d &&& ( ~~~e &&& f)) - 6 * (d ||| e) + 2 *  ~~~(d &&& (e ||| f)) - 6 * ((d &&& e) ||| (e ^^^ f)) + 2 * (e ^^^ (d ||| ( ~~~e ||| f))) - 2 * (f ^^^  ~~~(d &&&  ~~~e)) + 3 * (e ^^^  ~~~(d &&& (e &&& f))) - 3 * (f &&&  ~~~(d ^^^ e)) + 2 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 6 * ((d &&& f) ^^^ (e ||| f)) - 1 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 1 * d - 5 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) - 7 * (d ||| (e &&& f)) - 1 * (f ^^^ (d ||| (e ||| f))) - 1 * (e ^^^ ( ~~~d ||| (e ||| f))) + 3 * (e ||| (d &&&  ~~~f)) - 1 *  ~~~(d ||| (e ||| f)) + 13 *  ~~~(d ||| ( ~~~e ||| f)) + 2 *  ~~~( ~~~d ||| (e ||| f)) + 18 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 14 * ( ~~~d &&& ( ~~~e &&& f)) + 17 * ( ~~~d &&& (e &&& f)) + 31 * (d &&& ( ~~~e &&& f)) + 16 * (d &&& (e &&& f)) =  - 5 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f)))

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

theorem test4_thm (e : IntW 32) :
  sext 64 (LLVM.udiv e (const? 32 3)) ⊑ zext 64 (LLVM.udiv e (const? 32 3)) { «nneg» := true }

theorem t9_c0_c2_thm.extracted_1._1 : ∀ (x : BitVec 8), 42#8 - x - 24#8 = 18#8 - x

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

theorem ashr_lshr_exact_both_proof : ashr_lshr_exact_both_before ⊑ ashr_lshr_exact_both_after

theorem ashrslt_02_14_exact_proof : ashrslt_02_14_exact_before ⊑ ashrslt_02_14_exact_after

theorem e_1702 :
    2 *  ~~~(a &&& (b &&& c)) - 1 * (a &&&  ~~~c) - 7 *  ~~~(a ^^^ (b ^^^ c)) + 11 * (b ^^^ (a ||| c)) - 6 * (a &&& (b ^^^ c)) + 1 *  ~~~(a ^^^ (b &&& c)) + 11 * ((a &&& b) ^^^  ~~~(a ^^^ (b &&& c))) + 7 * (b ^^^  ~~~(a ||| c)) - 2 * ((a ||| b) &&&  ~~~(a ^^^ (b ^^^ c))) - 2 * ((b &&& c) ^^^  ~~~( ~~~a &&& (b ^^^ c))) + 2 * (b ^^^  ~~~(a &&&  ~~~c)) - 5 * a + 11 * (b ^^^  ~~~( ~~~a ||| (b &&& c))) + 7 * (a ||| (b &&& c)) - 1 * (c ^^^  ~~~( ~~~a ||| (b &&& c))) - 1 * (b ||| (a &&&  ~~~c)) + 3 * ( ~~~(a |||  ~~~b) ||| (a ^^^ (b ^^^ c))) - 1 *  ~~~(a &&&  ~~~c) + 5 * ((a &&& c) ^^^ (a ^^^ ( ~~~b &&& c))) + 4 * (c ^^^ (a ||| b)) + 7 * (c |||  ~~~(a ||| b)) - 23 *  ~~~(a ||| (b ||| c)) - 41 *  ~~~(a ||| ( ~~~b ||| c)) - 31 *  ~~~( ~~~a ||| (b ||| c)) - 16 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 42 * ( ~~~a &&& ( ~~~b &&& c)) - 25 * ( ~~~a &&& (b &&& c)) - 27 * (a &&& ( ~~~b &&& c)) - 28 * (a &&& (b &&& c)) = 2 * (b ^^^  ~~~(a &&& (b ^^^ c))) - 5 * ((a |||  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c)))

theorem test5_proof : test5_before ⊑ test5_after

theorem tryFactorization_xor_lshr_ashr_proof : tryFactorization_xor_lshr_ashr_before ⊑ tryFactorization_xor_lshr_ashr_after

theorem and_nosignbit_select_ashr_proof : and_nosignbit_select_ashr_before ⊑ and_nosignbit_select_ashr_after

theorem and_nosignbit_select_shl_proof : and_nosignbit_select_shl_before ⊑ and_nosignbit_select_shl_after

theorem xor_icmp_to_icmp_add_proof : xor_icmp_to_icmp_add_before ⊑ xor_icmp_to_icmp_add_after

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

theorem or_nosignbit_lshr_proof : or_nosignbit_lshr_before ⊑ or_nosignbit_lshr_after

theorem samesign_inverted_proof : samesign_inverted_before ⊑ samesign_inverted_after

theorem ashr_ult_15_proof : ashr_ult_15_before ⊑ ashr_ult_15_after

theorem and_xor_common_op_commute2_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬(x_1 = 0 ∨ x = 0 ∨ x = 0) →
    ¬(x = 0 ∨ x_1 = 0) → (43#32 / x_1 ^^^ 42#32 / x) &&& 42#32 / x = 42#32 / x &&& (43#32 / x_1 ^^^ -1#32)

theorem e_433 :
    1 * y + 2 *  ~~~(x &&& y) - 1 * (x |||  ~~~y) - 7 *  ~~~(x &&&  ~~~y) + 1 *  ~~~(x &&&  ~~~x) + 5 *  ~~~(x ||| y) + 3 *  ~~~(x |||  ~~~y) - 2 * (x &&&  ~~~y) =  - 6 * (x &&& y)

theorem demo3 (x y : BitVec 8) :
    (x ^^^ -1#8 ||| 7#8) ^^^ 12#8 = x &&& BitVec.ofInt 8 (-8) ^^^ BitVec.ofInt 8 (-13)

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

theorem zext_zext_sgt_proof : zext_zext_sgt_before ⊑ zext_zext_sgt_after

theorem not_or_or_and_no_and_commute1_or_thm (e e_1 e_2 : IntW 32) :
  LLVM.and (LLVM.or (LLVM.or e_2 e_1) (LLVM.xor e (const? 32 (-1)))) (LLVM.xor (LLVM.and e_1 e) (const? 32 (-1))) ⊑
    LLVM.or (LLVM.and e_2 (LLVM.xor e_1 (const? 32 (-1)))) (LLVM.xor e (const? 32 (-1)))

lemma neg_eq {M : NFA' n} : M.neg = M.determinize.flipAccept

theorem select_constants_and_icmp_eq0_zero_tval_proof : select_constants_and_icmp_eq0_zero_tval_before ⊑ select_constants_and_icmp_eq0_zero_tval_after

theorem t0_commutative_thm.extracted_1._9 : ∀ (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 → ¬0#1 = 1#1 → ¬x_1 = 1#1 → False

theorem udiv_i8_thm (e e_1 : IntW 8) : trunc 8 (LLVM.udiv (zext 32 e_1) (zext 32 e)) ⊑ LLVM.udiv e_1 e

theorem add_const_add_const_thm.extracted_1._1 : ∀ (x : BitVec 32), x + 8#32 + 2#32 = x + 10#32

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 select_xor_icmp2_thm (e e_1 e_2 : IntW 32) :
  select (icmp IntPred.ne e_2 (const? 32 0)) e_1 (LLVM.xor e_2 e) ⊑
    select (icmp IntPred.eq e_2 (const? 32 0)) e e_1

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

theorem test2_proof : test2_before ⊑ test2_after

theorem lshrult_02_13_proof : lshrult_02_13_before ⊑ lshrult_02_13_after

theorem e_1110 :
     - 7 * (z |||  ~~~t) - 11 *  ~~~(z &&& t) + 1 * z - 1 *  ~~~(z ^^^ t) - 6 * t + 19 *  ~~~(z ||| t) + 17 * (z &&&  ~~~t) + 13 * (z &&& t) =  - 17 *  ~~~(z |||  ~~~t)

theorem test_shl_nuw_nsw__none_are_safe_thm.extracted_1._1 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ofBool (x_1 &&& BitVec.ofInt 32 (-2) == 0#32) = 1#1 →
    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

theorem badimm1_thm (e : IntW 16) :
  select (icmp IntPred.eq (ashr (trunc 8 e) (const? 8 7)) (trunc 8 (lshr e (const? 16 9)))) (trunc 8 e)
      (LLVM.xor (trunc 8 (ashr e (const? 16 15))) (const? 8 127)) ⊑
    select
      (icmp IntPred.eq (ashr (trunc 8 e) (const? 8 7))
        (trunc 8 (lshr e (const? 16 9)) { «nsw» := true, «nuw» := true }))
      (trunc 8 e) (select (icmp IntPred.sgt e (const? 16 (-1))) (const? 8 127) (const? 8 (-128)))

theorem icmp_slt_0_and_icmp_sgt_neg1_i64_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬63#64 ≥ ↑64 → x >>> 63#64 &&& zeroExtend 64 (ofBool (-1#64 <ₛ x)) = 0#64

theorem t4_proof : t4_before ⊑ t4_after

theorem or_comm (x y : BitStream) : x ||

@[simp] theorem Valuation.comap_cons_consMap {Γ Γ_out : Ctxt Ty}
    (V : Γ_out.Valuation) {t} (x : ⟦t⟧) (map : Γ.Hom Γ_out) :
    Valuation.comap (x ::ᵥ V) (Ctxt.Hom.consMap map)
    = (x ::ᵥ (Valuation.comap V map))

theorem no_masks_with_logical_or_thm.extracted_1._6 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (x_2 != 0#32) = 1#1 →
    ¬ofBool (x_2 ||| x != 0#32) = 1#1 → ofBool (x_1 != 63#32) ||

theorem testi32i8_proof : testi32i8_before ⊑ testi32i8_after

theorem t0_thm (e e_1 e_2 e_3 : IntW 8) (e_4 : IntW 1) :
  select (select (LLVM.xor e_4 (const? 1 1)) (const? 1 1) (icmp IntPred.eq e_3 e_2)) e_1 e ⊑
    select (select e_4 (icmp IntPred.ne e_3 e_2) (const? 1 0)) e e_1

theorem trunc_shl_shl_infloop_thm (e : IntW 64) :
  trunc 32 (shl (shl e (const? 64 1)) (const? 64 2)) ⊑ shl (trunc 32 e) (const? 32 3)

theorem slt_and_not_max_commute_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x_1 != 127#8) &&& ofBool (x_1 <ₛ x) = ofBool (x_1 <ₛ x)

theorem and_orn_xor_commute8_thm (e e_1 : IntW 32) :
  LLVM.and (LLVM.xor (mul e_1 e_1) (mul e e)) (LLVM.or (mul e_1 e_1) (LLVM.xor (mul e e) (const? 32 (-1)))) ⊑
    LLVM.and (mul e_1 e_1) (LLVM.xor (mul e e) (const? 32 (-1)))

theorem icmp_ne_mul_nsw_nonequal_proof : icmp_ne_mul_nsw_nonequal_before ⊑ icmp_ne_mul_nsw_nonequal_after

theorem e_313 :
     - 1 * (x |||  ~~~y) + 7 * y + 7 *  ~~~y - 5 *  ~~~(x ||| y) - 6 *  ~~~(x |||  ~~~y) - 5 * (x &&&  ~~~y) - 6 * (x &&& y) = 1 *  ~~~(x &&& y)

theorem e_513 :
     - 1 *  ~~~(x &&& y) - 1 *  ~~~(x &&&  ~~~y) - 11 * (x |||  ~~~y) + 1 * (x ^^^ y) + 1 *  ~~~y - 1 * y + 17 *  ~~~(x ||| y) + 10 * (x &&&  ~~~y) + 13 * (x &&& y) =  - 7 *  ~~~(x |||  ~~~y) + 5 *  ~~~x

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

theorem sext_zext_uge_known_nonneg_op0_wide_thm.extracted_1._2 : ∀ (x : BitVec 8) (x_1 : BitVec 16),
  ¬(True ∧ (x &&& 12#8).msb = true) →
    ofBool (zeroExtend 32 (x &&& 12#8) ≤ᵤ signExtend 32 x_1) = ofBool (zeroExtend 16 (x &&& 12#8) ≤ᵤ x_1)

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

theorem test10_thm.extracted_1._1 : ∀ (x : BitVec 16), truncate 16 (signExtend 32 x) = x

theorem e_330 :
    1 *  ~~~(x ^^^ y) - 3 * y - 5 * (x ^^^ y) - 7 *  ~~~x + 4 *  ~~~(x ||| y) + 13 *  ~~~(x |||  ~~~y) + 3 * (x &&&  ~~~y) - 1 * (x &&& y) = 1 *  ~~~(x &&& y) - 3 *  ~~~(x &&&  ~~~x)

theorem test9_logical_thm (e : IntW 32) :
  select (icmp IntPred.ne (LLVM.and e (const? 32 1073741824)) (const? 32 0))
      (icmp IntPred.sgt e (const? 32 (-1))) (const? 1 0) ⊑
    icmp IntPred.eq (LLVM.and e (const? 32 (-1073741824))) (const? 32 1073741824)

theorem test2_proof : test2_before ⊑ test2_after

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

theorem trunc_unsigned_nsw_sext_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 32),
  ¬(True ∧ signExtend 32 (truncate 16 x_1) ≠ x_1) →
    ofBool (truncate 16 x_1 <ᵤ signExtend 16 x) = ofBool (x_1 <ᵤ signExtend 32 x)

theorem icmp_sle5_proof : icmp_sle5_before ⊑ icmp_sle5_after

theorem test2_thm.extracted_1._1 : ∀ (x : BitVec 49),
  ¬(11#49 ≥ ↑49 ∨ 4096#49 <<< 11#49 = 0) → x % 4096#49 <<< 11#49 = x &&& 8388607#49

theorem n13_proof : n13_before ⊑ n13_after

theorem or_ranges_single_elem_left_proof : or_ranges_single_elem_left_before ⊑ or_ranges_single_elem_left_after

theorem test_nsw_and_signed_pred_proof : test_nsw_and_signed_pred_before ⊑ test_nsw_and_signed_pred_after

theorem e_1951 :
    7 * ((a ||| b) &&&  ~~~(b ^^^ c)) + 4 * (b ^^^ ( ~~~a ||| ( ~~~b ||| c))) - 2 * ( ~~~(a &&& b) &&&  ~~~(b ^^^ c)) + 7 *  ~~~(a &&& (b ||| c)) - 5 * ( ~~~a ||| (b ||| c)) + 5 * ( ~~~(a |||  ~~~b) ||| (b ^^^ c)) + 1 * (b &&&  ~~~(a ^^^ c)) + 1 * (a ^^^ (b ||| c)) + 4 * (a ^^^ b) - 11 * ((a &&& b) ^^^  ~~~(a ^^^ (b &&& c))) - 2 * (c &&&  ~~~(a &&& b)) - 11 * ( ~~~(a |||  ~~~b) |||  ~~~(b ^^^ c)) - 2 * b - 2 *  ~~~(a ^^^ ( ~~~b &&& c)) - 6 * ((a &&& c) ||| (b &&&  ~~~c)) - 11 * ((a ^^^ b) ||| (a ^^^ c)) + 1 * ((b &&&  ~~~c) ^^^ ( ~~~a ||| (b ^^^ c))) + 1 * ( ~~~(a &&&  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) - 1 * ( ~~~c ||| (a ^^^ b)) + 7 * (a ^^^ (b ^^^ c)) + 5 * (b |||  ~~~(a ||| c)) + 2 * (c ^^^  ~~~( ~~~a ||| ( ~~~b &&& c))) - 2 * ((a &&&  ~~~b) |||  ~~~(b ^^^ c)) + 1 * (c ^^^ (a ||| (b ||| c))) + 3 * ( ~~~a ||| (b ^^^ c)) - 7 * ( ~~~a &&& (b ||| c)) - 6 * (c &&&  ~~~(a ^^^ b)) - 1 *  ~~~(a |||  ~~~b) + 2 * ( ~~~(a &&&  ~~~b) &&&  ~~~(b ^^^ c)) + 4 * (b ^^^ (a &&&  ~~~c)) + 2 * (a ||| (b &&& c)) + 5 *  ~~~(a ||| c) + 3 * (a ||| ( ~~~b &&& c)) + 1 * (a ||| (b ||| c)) + 11 * (a &&& b) + 2 * (a &&& (b ||| c)) + 2 * ((a |||  ~~~b) &&& (b ^^^ c)) - 1 * ((a &&& b) |||  ~~~(b |||  ~~~c)) - 2 * (b ^^^  ~~~(a &&& c)) - 1 * (c ^^^ ( ~~~a ||| (b ||| c))) - 1 * ( ~~~a &&& ( ~~~b ||| c)) - 1 * ((b &&&  ~~~c) |||  ~~~(a ||| ( ~~~b &&& c))) - 5 * ((a ^^^ b) &&& (a ^^^ c)) - 1 * (c ^^^ (a &&& (b ||| c))) - 1 * (a ||| b) - 1 *  ~~~(b |||  ~~~c) + 9 *  ~~~(a ||| (b ||| c)) + 14 *  ~~~(a ||| ( ~~~b ||| c)) - 1 *  ~~~( ~~~a ||| (b ||| c)) - 1 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 19 * ( ~~~a &&& ( ~~~b &&& c)) + 8 * ( ~~~a &&& (b &&& c)) + 8 * (a &&& ( ~~~b &&& c)) - 4 * (a &&& (b &&& c)) = 7 * ((b &&&  ~~~c) ^^^ (a ||| (b ^^^ c))) - 2 * (c ^^^  ~~~(a ||| (b &&& c)))

theorem or_or_logic_and_1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1), ¬x_1 ||

theorem or_eq_with_diff_one_logical_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬ofBool (x == 13#8) = 1#1 → ofBool (x == 14#8) = ofBool (x + BitVec.ofInt 8 (-13) <ᵤ 2#8)

theorem select_replace_udiv_non_speculatable_proof : select_replace_udiv_non_speculatable_before ⊑ select_replace_udiv_non_speculatable_after

theorem icmp_select_var_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), ofBool (x_1 == 0#8) = 1#1 → ofBool (x == x) = 1#1

theorem ashr_ult_10_proof : ashr_ult_10_before ⊑ ashr_ult_10_after

theorem lshrult_02_12_exact_proof : lshrult_02_12_exact_before ⊑ lshrult_02_12_exact_after

theorem ashrslt_02_15_proof : ashrslt_02_15_before ⊑ ashrslt_02_15_after

theorem e_686 :
    1 *  ~~~(x ^^^ y) + 5 * y - 7 *  ~~~(x &&&  ~~~y) + 3 * (x ||| y) + 4 * x - 1 *  ~~~x - 11 *  ~~~(x &&& y) + 11 *  ~~~(x |||  ~~~y) + 4 * (x &&&  ~~~y) - 6 * (x &&& y) =  - 18 *  ~~~(x ||| y)

theorem relabel_unsat_iff_of_not_NonEmpty {aigα : AIG α} {r : α → β} {hidx1} {hidx2}
    (hαNonempty : ¬ Nonempty α) :
    (aigα.relabel r).UnsatAt idx invert hidx1 ↔ aigα.UnsatAt idx invert hidx2

theorem shl_add_nuw_proof : shl_add_nuw_before ⊑ shl_add_nuw_after

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

theorem and_ne_with_one_bit_diff_constants3_logical_thm (e : IntW 8) :
  select (icmp IntPred.ne e (const? 8 65)) (icmp IntPred.ne e (const? 8 (-63))) (const? 1 0) ⊑
    icmp IntPred.ne (LLVM.and e (const? 8 127)) (const? 8 65)

theorem main4c_logical_thm.extracted_1._4 : ∀ (x : BitVec 32),
  ¬ofBool (x &&& 7#32 != 7#32) = 1#1 →
    ¬ofBool (x &&& 48#32 != 48#32) = 1#1 → 1#32 = zeroExtend 32 (ofBool (x &&& 55#32 == 55#32))

theorem or_and1_commuted_proof : or_and1_commuted_before ⊑ or_and1_commuted_after

theorem n11_wrong_pred3_thm (e e_1 : IntW 8) :
  icmp IntPred.ne (add e_1 e) e ⊑ icmp IntPred.ne e_1 (const? 8 0)

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

theorem icmp_eq_sext_ne_zero_proof : icmp_eq_sext_ne_zero_before ⊑ icmp_eq_sext_ne_zero_after

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

theorem not_or_or_and_not_and_and_commute2_or_thm (e e_1 e_2 : IntW 32) :
  LLVM.and (LLVM.or (LLVM.or e_2 e_1) (LLVM.xor e (const? 32 (-1))))
      (LLVM.xor (LLVM.and (LLVM.and e_2 e) e_1) (const? 32 (-1))) ⊑
    LLVM.or (LLVM.xor e_2 e_1) (LLVM.xor e (const? 32 (-1)))

theorem gt_unsigned_to_small_unsigned_thm (e : IntW 8) :
  icmp IntPred.ugt (zext 32 e) (const? 32 17) ⊑ icmp IntPred.ugt e (const? 8 17)

theorem select_mul_icmp_bad_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 == 3#32) = 1#1 → x_1 * x = x * 3#32

@[simp]
theorem denote_splitProgramAt [LawfulMonad d.m] {pos : ℕ} {prog : Com d Γ eff t}
    {res : _} (hres : res ∈ splitProgramAt pos prog) :
    res.denote = prog.denote

theorem ne_basic_equal_minus_7_proof : ne_basic_equal_minus_7_before ⊑ ne_basic_equal_minus_7_after

theorem test4_thm.extracted_1._4 : ∀ (x : BitVec 1023),
  ¬ofBool (x <ₛ 0#1023) = 1#1 → ¬1022#1023 ≥ ↑1023 → 0#1023 = x.sshiftRight' 1022#1023

theorem udiv_i32_c_multiuse_proof : udiv_i32_c_multiuse_before ⊑ udiv_i32_c_multiuse_after

theorem foo1_and_proof : foo1_and_before ⊑ foo1_and_after
</all_available_lemmas>

<local_ctx>
import Mathlib.Data.Finset.Card

import Mathlib.Data.List.Pi

import Mathlib.Data.Finset.Union

import Mathlib.Data.Fin.Basic

import Mathlib.Data.Finset.Basic

import Mathlib.Data.Finset.Defs

import Mathlib.Data.Fintype.Basic

open Std Sat AIG

inductive Circuit (α : Type u) : Type u
  | tru : Circuit α
  | fals : Circuit α
   
  | var : (positive: Bool) → α → Circuit α
  | and : Circuit α → Circuit α → Circuit α
  | or : Circuit α → Circuit α → Circuit α
  | xor : Circuit α → Circuit α → Circuit α
deriving Repr, DecidableEq

open Lean in

namespace Circuit

variable {α : Type u} {β : Type v}

def vars [DecidableEq α] : Circuit α → List α
  | tru => []
  | fals => []
  | var _ x => [x]
  | and c₁ c₂ => (vars c₁ ++ vars c₂).dedup
  | or c₁ c₂ => (vars c₁ ++ vars c₂).dedup
  | xor c₁ c₂ => (vars c₁ ++ vars c₂).dedup

def varsFinset [DecidableEq α] (c : Circuit α) : Finset α :=
  ⟨c.vars, nodup_vars c⟩

def simplifyAnd : Circuit α → Circuit α → Circuit α
  | tru, c => c
  | c, tru => c
  | fals, _ => fals
  | _, fals => fals
  | c₁, c₂ => and c₁ c₂

def simplifyOr : Circuit α → Circuit α → Circuit α
  | tru, _ => tru
  | _, tru => tru
  | fals, c => c
  | c, fals => c
  | c₁, c₂ => or c₁ c₂

def simplifyNot : Circuit α → Circuit α
  | tru => fals
  | fals => tru
  | xor a b => xor (simplifyNot a) b
  | and a b => or (simplifyNot a) (simplifyNot b)
  | or a b => and (simplifyNot a) (simplifyNot b)
  | var b a => var (!b) a

@[simp]
def simplifyXor : Circuit α → Circuit α → Circuit α
  | fals, c => c
  | c, fals => c
  | tru, c => ~~~ c
  | c, tru => ~~~ c
  | c₁, c₂ => xor c₁ c₂

def assignVars [DecidableEq α] :
    ∀ (c : Circuit α) (_f : ∀ (a : α) (_ha : a ∈ c.vars), β ⊕ Bool), Circuit β
  | tru, _ => tru
  | fals, _ => fals
  | var b x, f =>
    Sum.elim
      (var b)
      (λ c : Bool => if Bool.xor b c then fals else tru)
      (f x (by admit /- proof elided -/
      ))
  | and c₁ c₂, f => (assignVars c₁ (λ x hx => f x (by admit /- proof elided -/
  ))) &&&
                    (assignVars c₂ (λ x hx => f x (by admit /- proof elided -/
                    )))
  | or c₁ c₂, f =>  (assignVars c₁ (λ x hx => f x (by admit /- proof elided -/
  ))) |||
                    (assignVars c₂ (λ x hx => f x (by admit /- proof elided -/
                    )))
  | xor c₁ c₂, f => (assignVars c₁ (λ x hx => f x (by admit /- proof elided -/
  ))) ^^^
                    (assignVars c₂ (λ x hx => f x (by admit /- proof elided -/
                    )))
</local_ctx>

<target_theorem>
lemma varsFinset_assignVars [DecidableEq α] [DecidableEq β] :
    ∀ (c : Circuit α) (f : ∀ (a : α) (_ha : a ∈ c.vars), β ⊕ Bool),
      (c.assignVars f).varsFinset ⊆ c.varsFinset.biUnion
        (fun a => if ha : a ∈ c.vars
                  then
                    match f a ha with
                    | Sum.inl b => {b}
                    | Sum.inr _ => ∅
                  else ∅) :=
</target_theorem>

