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>
Option in Init.Prelude
Stream' in Mathlib.Data.Stream.Defs
Stream'.const in Mathlib.Data.Stream.Defs
Stream'.head in Mathlib.Data.Stream.Defs
Nat in Init.Prelude
Nat.strongRecOn in Init.WF
Stream'.drop in Mathlib.Data.Stream.Defs
Stream'.get in Mathlib.Data.Stream.Defs
Stream'.tail in Mathlib.Data.Stream.Defs
Stream'.corec in Mathlib.Data.Stream.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) )

def Stream (β : Type) := Stream' (Option β)

def head : Stream α → Option α := Stream'.head

def tail : Stream α → Stream α := Stream'.tail

def corec {α} {β} (s0 : β) (f : β → (Option α × β)) : Stream α :=
  Stream'.corec (f · |>.fst) (f · |>.snd) s0

def supp {Γ : Ctxt _} (a : Var Γ (.stream r)) (b : Var Γ (.stream (.bitvec 1))) : Expr (Handshake) Γ .pure (.stream r)  :=
  Expr.mk
    (op := .supp r)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons a <| .cons b <| .nil)
    (regArgs := .nil)

def one_inst_concrete_macro_proof :
    one_inst_concrete_macro ⊑ one_inst_concrete_macro :=

BitVec.reduceOfNat in Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec

def test9_before := [llvm|
{
^0(%arg111 : i32, %arg112 : i32):
  %0 = llvm.and %arg111, %arg112 : i32
  %1 = llvm.xor %arg111, %arg112 : i32
  %2 = llvm.xor %0, %1 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

@[inline]
def CNFA.proj (m: CNFA n2) (f : Fin n1 → Fin n2) : CNFA n1 :=
  ⟨m.m.proj f, m.m.proj_wf m.wf⟩

def ne_10_after := [llvm|
{
^0(%arg78 : i32, %arg79 : i32):
  %0 = llvm.trunc %arg78 : i32 to i16
  %1 = llvm.trunc %arg79 : i32 to i16
  %2 = llvm.icmp "ne" %0, %1 : i16
  "llvm.return"(%2) : (i1) -> ()
}
]

structure Item where
 name : String
 tac : Syntax

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

def select_icmp_and_2147483648_eq_0_xor_2147483648_after := [llvm|
{
^0(%arg169 : i32):
  %0 = llvm.mlir.constant(-2147483648 : i32) : i32
  %1 = llvm.or %arg169, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

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

@[simp_sllvm]
def srem (x y : LLVM.IntW w) : EffectM (LLVM.IntW w) := do
  if y.canBe 0#w then
    throwUB
  else
    pure <| LLVM.srem x y

def test59_after := [llvm|
{
^0(%arg122 : i8, %arg123 : i8):
  %0 = llvm.mlir.constant(4 : i32) : i32
  %1 = llvm.mlir.constant(48 : i32) : i32
  %2 = llvm.mlir.constant(4 : i8) : i8
  %3 = llvm.zext %arg122 : i8 to i32
  %4 = llvm.shl %3, %0 overflow<nsw,nuw> : i32
  %5 = llvm.and %4, %1 : i32
  %6 = llvm.lshr %arg123, %2 : i8
  %7 = llvm.zext nneg %6 : i8 to i32
  %8 = llvm.or disjoint %5, %7 : i32
  %9 = llvm.zext nneg %8 : i32 to i64
  "llvm.return"(%9) : (i64) -> ()
}
]

def fold_sext_to_and_wrong7_before := [llvm|
{
^0(%arg3 : i8):
  %0 = llvm.mlir.constant(-2147483647 : i32) : i32
  %1 = llvm.mlir.constant(128 : i32) : i32
  %2 = llvm.sext %arg3 : i8 to i32
  %3 = llvm.and %2, %0 : i32
  %4 = llvm.icmp "ne" %3, %1 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

@[simp_denote]
def udiv_llvm_no_exact_32 : Com  LLVMPlusRiscV ⟨[.llvm (.bitvec 32), .llvm (.bitvec 32)]⟩
  .pure (.llvm (.bitvec 32)) := [LV| {
  ^entry (%x: i32, %y: i32 ):
    %1 = llvm.udiv    %x, %y : i32
    llvm.return %1 : i32
  }]

def llvm_const_lower_riscv_li_36 : LLVMPeepholeRewriteRefine 64 [] :=
  {lhs := constLLVM_36, rhs:= liRiscv_36,
   correct := by admit /- proof elided -/

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

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

def ashr_ult_13_after := [llvm|
{
^0(%arg83 : i4):
  %0 = llvm.mlir.constant(-6 : i4) : i4
  %1 = llvm.icmp "ult" %arg83, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def slt_swap_and_not_max_logical_before := [llvm|
{
^0(%arg116 : i8, %arg117 : i8):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "sgt" %arg117, %arg116 : i8
  %3 = llvm.icmp "ne" %arg116, %0 : i8
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

GetElem? in Init.GetElem

def test1_after := [llvm|
{
^0(%arg209 : i32):
  "llvm.return"(%arg209) : (i32) -> ()
}
]

def slt_zero_sgt_minus1_before := [llvm|
{
^0(%arg22 : i4, %arg23 : i4):
  %0 = llvm.mlir.constant(0 : i4) : i4
  %1 = llvm.mlir.constant(-1 : i4) : i4
  %2 = llvm.icmp "slt" %arg22, %0 : i4
  %3 = llvm.icmp "sgt" %arg23, %1 : i4
  %4 = llvm.xor %2, %3 : i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

@[simp_denote]
def select_riscv_64 := [LV| {
  ^entry (%cond : i1, %arg0: i64, %arg1: i64):
    %0 = "builtin.unrealized_conversion_cast" (%arg0) : (i64) -> (!i64)
    %1 = "builtin.unrealized_conversion_cast" (%arg1) : (i64) -> (!i64)
    %2 = "builtin.unrealized_conversion_cast" (%cond) : (i1) -> (!i64)
    %3 = snez %2 : !i64
    %4 = sub %0, %1 : !i64
    %5 = mul %4, %3 : !i64
    %6 = add %5, %1 : !i64
    %7 = "builtin.unrealized_conversion_cast" (%6) : (!i64) -> (i64)
    llvm.return %7 : i64
  }]

def udiv {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW w := do
  let x' ← x
  let y' ← y
  if flag.exact ∧ x'.umod y' ≠ 0 then
    .poison
  else
    udiv? x' y'

def sge_swap_or_max_logical_after := [llvm|
{
^0(%arg180 : i8, %arg181 : i8):
  %0 = llvm.icmp "sle" %arg181, %arg180 : i8
  "llvm.return"(%0) : (i1) -> ()
}
]

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

def State.consOldExpr2Cache [DecidableEq d.Ty] [DecidableEq d.Op]
    {Γ : Ctxt d.Ty} {α}
    {lets : Lets d Γstart .pure Γ}
    (s : State d lets) (enew : Expr d Γ .pure α) (eold : Expr d Γ .pure α) (henew :
        ∀ (V : Γstart.Valuation), enew.denote (lets.denote V) = eold.denote (lets.denote V))
    (vold : HVector Γ.Var α)
    (hv : ∀ (V : Γstart.Valuation), eold.denoteOp (lets.denote V) =
      vold.map (lets.denote V)) :
    State d (Lets.var lets enew) where
  var2var := fun v => by admit /- proof elided -/
    | .none => .none
    | .some ⟨e', he'⟩ => .some ⟨e'.map fun _ v => v.appendInr, by admit /- proof elided -/
      ⟩

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

def mulh_to_lshr_256 : RISCVPeepholeRewrite [Ty.riscv (.bv)] where
  lhs := [LV| {
    ^entry (%x: !riscv.reg):
      %c = li (256) : !riscv.reg
      %0 = mulh %c, %x : !riscv.reg
      ret %0 : !riscv.reg
  }]
  rhs := [LV| {
    ^entry (%x: !riscv.reg):
      %c = li (56) : !riscv.reg
      %0 = sra %x, %c : !riscv.reg
      ret %0 : !riscv.reg
  }]

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 t_0_1_after := [llvm|
{
^0(%arg15 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.and %arg15, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

@[simp_denote]
def llvm_shl_lower_riscv_32: LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] where
  lhs := shl_llvm_32
  rhs := shl_riscv_32

def or_basic_before := [llvm|
{
^0(%arg15 : i16):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.mlir.constant(-256 : i16) : i16
  %2 = llvm.mlir.constant(17664 : i16) : i16
  %3 = llvm.trunc %arg15 : i16 to i8
  %4 = llvm.icmp "ne" %3, %0 : i8
  %5 = llvm.and %arg15, %1 : i16
  %6 = llvm.icmp "ne" %5, %2 : i16
  %7 = llvm.or %4, %6 : i1
  "llvm.return"(%7) : (i1) -> ()
}
]

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

def PR42691_1_before := [llvm|
{
^0(%arg343 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(2147483647 : i32) : i32
  %2 = llvm.icmp "slt" %arg343, %0 : i32
  %3 = llvm.icmp "eq" %arg343, %1 : i32
  %4 = llvm.or %2, %3 : i1
  "llvm.return"(%4) : (i1) -> ()
}
]

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

def compose [FinEnum arity] [DecidableEq arity] [Hashable arity]
    (new_arity : Type)        
    (q_arity : arity → Type)  
    (vars : ∀ (a : arity), q_arity a → new_arity)
    
    
    (q : ∀ (a : arity), FSM (q_arity a)) : 
    FSM new_arity :=
  { α := p.α ⊕ (Σ a, (q a).α),
    i := by admit /- proof elided -/

def p_commutative2_after := [llvm|
{
^0(%arg27 : i32, %arg28 : i32, %arg29 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg27, %arg29 : i32
  %2 = llvm.xor %arg29, %0 : i32
  %3 = llvm.and %arg28, %2 : i32
  %4 = llvm.or disjoint %3, %1 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

BitVec.sshiftRight' in Init.Data.BitVec.Basic

partial def reflectPredicateAux (exprToIx : ReflectMap) (e : Expr) (wExpected : Expr) : MetaM (ReflectResult Predicate) := do
  match_expr e with
  | Eq α a b =>
    match_expr α with
    | Nat =>
       
      
      if wExpected != a then
        throwError m!"Only Nat expressions allowed are '{wExpected} ≠ <concrete value>'. Found {indentD e}."
      let some natVal ← Lean.Meta.getNatValue? b
        | throwError m!"Expected '{wExpected} ≠ <concrete width>', found symbolic width {indentD b}."
      let out := Predicate.width .eq natVal
      return { exprToIx := exprToIx, e := out }

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

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

def test3_before := [llvm|
{
^0(%arg11 : i23):
  %0 = llvm.mlir.constant(127 : i23) : i23
  %1 = llvm.mlir.constant(128 : i23) : i23
  %2 = llvm.and %arg11, %0 : i23
  %3 = llvm.and %2, %1 : i23
  "llvm.return"(%3) : (i23) -> ()
}
]

def Region.WellTyped : UnTyped.Region Op VarName → RegionType Ty → Prop
  | ⟨entry, _⟩ => BasicBlock.WellTyped entry

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

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

def Expr.mkToFSM (self : Expr) : MetaM Expr :=
  mkAppM ``FSMPredicateSolution.toFSM #[self]

def icmp_eq_x_invertable_y_todo_after := [llvm|
{
^0(%arg10 : i8, %arg11 : i1):
  %0 = llvm.mlir.constant(-8 : i8) : i8
  %1 = llvm.mlir.constant(-25 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = "llvm.select"(%arg11, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %4 = llvm.and %arg10, %3 : i8
  %5 = llvm.icmp "eq" %4, %2 : i8
  "llvm.return"(%5) : (i1) -> ()
}
]

propext in Init.Core

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

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

def shl_or_with_or_disjoint_instead_of_add_before := [llvm|
{
^0(%arg1 : i8):
  %0 = llvm.mlir.constant(16 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.mlir.constant(3 : i8) : i8
  %3 = llvm.shl %0, %arg1 : i8
  %4 = llvm.or disjoint %arg1, %1 : i8
  %5 = llvm.shl %2, %4 : i8
  %6 = llvm.or %3, %5 : i8
  "llvm.return"(%6) : (i8) -> ()
}
]

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

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

def logical_and_implies_folds_before := [llvm|
{
^0(%arg248 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(false) : i1
  %3 = llvm.icmp "ugt" %arg248, %0 : i32
  %4 = llvm.icmp "ne" %arg248, %1 : i32
  %5 = "llvm.select"(%3, %4, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%5) : (i1) -> ()
}
]

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

RV64.sh2adduw in RISCV.Instructions

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

|

Membership in Init.Prelude
</all_available_defs>

<all_available_lemmas>
Nat.not_lt_zero in Init.Prelude
Nat.zero_add in Init.Data.Nat.Basic
false_implies in Init.SimpLemmas
implies_true in Init.SimpLemmas
ne_eq in Init.SimpLemmas
true_and in Init.SimpLemmas

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

theorem test_nuw_dropped_proof : test_nuw_dropped_before ⊑ test_nuw_dropped_after

@[simp]
theorem eval_latchDelayed_zero_eq (initVal : Bool)
    (x : Bool → BitStream) :
    (latchDelayed initVal).eval x 0 = initVal

theorem select_icmp_ne_0_and_4096_xor_32_thm.extracted_1._3 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (0#32 != x_1 &&& 4096#32) = 1#1 → 7#32 ≥ ↑32 → False

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

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

theorem t0_proof : t0_before ⊑ t0_after

theorem logic_and_logic_or_3_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1), x_1 = 1#1 → x = 1#1 → 1#1 = x

theorem test11_thm (e : IntW 32) :
  icmp IntPred.ult (LLVM.udiv (const? 32 4) e) (const? 32 1) ⊑ icmp IntPred.ugt e (const? 32 4)

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

theorem test5_thm (e : IntW 32) :
  sext 64 (urem e (const? 32 30000)) ⊑ zext 64 (urem e (const? 32 30000)) { «nneg» := true }

theorem lshrult_02_15_proof : lshrult_02_15_before ⊑ lshrult_02_15_after

theorem slt_swap_or_not_max_commute_proof : slt_swap_or_not_max_commute_before ⊑ slt_swap_or_not_max_commute_after

theorem ashr_and_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬(x ≥ ↑8 ∨ x + 1#8 ≥ ↑8) →
    ¬x ≥ ↑8 →
      (BitVec.ofInt 8 (-64)).sshiftRight' x &&& (BitVec.ofInt 8 (-128)).sshiftRight' (x + 1#8) =
        (BitVec.ofInt 8 (-64)).sshiftRight' x

@[simp]
theorem ofBitVec_getLsbD (n : Nat) (h : n < w) : ofBitVecSext x n = x.getLsbD n

theorem ashrsgt_03_06_thm (e : IntW 4) : icmp IntPred.sgt (ashr e (const? 4 3)) (const? 4 6) ⊑ const? 1 0

theorem e_1218 :
    1 * t - 2 * (z |||  ~~~t) + 11 *  ~~~z + 1 *  ~~~(z &&&  ~~~t) - 1 *  ~~~t - 2 * z - 9 *  ~~~(z ||| t) - 17 *  ~~~(z |||  ~~~t) + 1 * (z &&&  ~~~t) =  - 2 * (z &&& t) - 4 * (z ^^^ t)

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

@[simp]
lemma BitVec.cons_sgt_iff {w} {bv1 bv2 : BitVec w} :
    ((BitVec.cons b2 bv2).slt (BitVec.cons b1 bv1)) ↔
      (if b1 = b2 then bv2.ult bv1 else b2)

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

theorem e_2288 :
    1 *  ~~~(e &&& f) - 1 * f - 6 * (e &&&  ~~~(d &&& f)) + 2 * ((d &&&  ~~~e) ||| (e ^^^ f)) + 4 * (d &&& e) - 11 * d + 3 * (d ||| f) + 7 *  ~~~(e ^^^ f) - 1 *  ~~~(d ||| e) - 6 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 1 * ( ~~~e |||  ~~~(d ^^^ f)) - 1 *  ~~~(d ^^^ ( ~~~e ||| f)) + 2 * ((e &&&  ~~~f) |||  ~~~( ~~~d ||| ( ~~~e &&& f))) + 5 *  ~~~(d |||  ~~~e) - 7 * (e ^^^  ~~~(d &&& (e ||| f))) - 1 *  ~~~(d ^^^ (e ||| f)) - 5 * ( ~~~(d &&& e) &&&  ~~~(d ^^^ (e ^^^ f))) - 6 * (f |||  ~~~(d ||| e)) + 2 * (e |||  ~~~(d |||  ~~~f)) + 7 * ( ~~~(d ||| e) |||  ~~~(e ^^^ f)) - 1 *  ~~~( ~~~d &&& ( ~~~e ||| f)) + 1 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) - 1 * (d ||| e) + 3 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) + 1 * (e ||| (d &&& f)) - 11 * (f &&& (d ||| e)) - 11 * (f |||  ~~~(d |||  ~~~e)) + 1 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) - 11 * (f ^^^ (d &&&  ~~~e)) + 5 * (e &&&  ~~~f) - 3 *  ~~~e + 1 * (e ^^^  ~~~(d ||| (e &&& f))) - 1 * (f ^^^  ~~~(d &&& (e ||| f))) - 2 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) - 1 * (d ^^^ e) + 1 * (f ^^^  ~~~(d ||| e)) - 6 *  ~~~(d ^^^ (e &&& f)) - 1 * (f &&& (d |||  ~~~e)) + 4 * ( ~~~d &&& (e ^^^ f)) - 3 *  ~~~(d &&& (e ||| f)) + 3 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) + 5 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) - 2 * ((d &&& e) ^^^ (d ^^^ (e &&& f))) + 11 * ( ~~~f &&& (d ^^^ e)) + 11 * ((d ^^^ e) ||| (d ^^^ f)) - 11 * ((d ||| e) &&& (d ^^^ (e ^^^ f))) - 2 * (f ^^^  ~~~(d &&& e)) + 7 * (e ^^^ f) - 5 * (e ^^^ (d &&& (e ||| f))) + 2 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) - 3 * (f ^^^  ~~~(d |||  ~~~e)) - 2 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) + 11 * (d |||  ~~~f) + 11 *  ~~~(d ||| (e ||| f)) - 12 *  ~~~(d ||| ( ~~~e ||| f)) - 12 *  ~~~( ~~~d ||| (e ||| f)) - 30 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 4 * ( ~~~d &&& ( ~~~e &&& f)) + 17 * ( ~~~d &&& (e &&& f)) + 22 * (d &&& ( ~~~e &&& f)) + 47 * (d &&& (e &&& f)) =  - 2 * (d ^^^ (e &&& f)) - 1 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f)))

theorem test_shl_nuw_nsw__none_are_safe_proof : test_shl_nuw_nsw__none_are_safe_before ⊑ test_shl_nuw_nsw__none_are_safe_after

theorem e_2043 :
     - 2 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) + 5 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) + 5 * ( ~~~f |||  ~~~(d ^^^ e)) + 1 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) + 1 * (e ^^^  ~~~( ~~~d &&& (e &&& f))) + 1 * ((d ||| e) &&&  ~~~(e ^^^ f)) - 1 * ( ~~~d ||| (e ^^^ f)) - 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 3 * ((d &&& e) ^^^ (d ^^^ (e &&& f))) - 1 * (e ^^^  ~~~(d |||  ~~~f)) - 2 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) + 1 * (e ||| (d &&& f)) - 2 *  ~~~(d ^^^ f) + 2 * (f |||  ~~~(d ^^^ e)) - 7 * (e ||| (d &&&  ~~~f)) - 2 * (e ^^^ (d |||  ~~~f)) - 5 * (e |||  ~~~(d ||| f)) + 2 *  ~~~(d &&& (e ^^^ f)) - 2 * (e ||| f) + 11 * ( ~~~f &&&  ~~~(d ^^^ e)) + 3 *  ~~~(d &&& (e ||| f)) - 1 * (e ^^^ (d ||| (e ^^^ f))) + 5 * (d ||| e) - 2 * ( ~~~(d &&& e) &&& (e ^^^ f)) + 1 * (f ||| (d ^^^ e)) - 1 * d + 2 * (e ^^^ ( ~~~d ||| ( ~~~e ||| f))) - 11 * (e ^^^  ~~~(d ||| ( ~~~e &&& f))) + 11 * ( ~~~e &&& (d ^^^ f)) - 10 *  ~~~(d ||| (e ||| f)) + 1 *  ~~~(d ||| ( ~~~e ||| f)) - 13 *  ~~~( ~~~d ||| (e ||| f)) - 1 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 9 * ( ~~~d &&& (e &&& f)) + 2 * (d &&& ( ~~~e &&& f)) + 17 * (d &&& (e &&& f)) = 23 * ( ~~~d &&& ( ~~~e &&& f))

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

theorem com_Γ : com.1 = (Γn 1)

theorem fold_add_udiv_urem_commuted_proof : fold_add_udiv_urem_commuted_before ⊑ fold_add_udiv_urem_commuted_after

theorem sel_zext_constants_thm (e : IntW 1) :
  zext 16 (select e (const? 8 (-1)) (const? 8 42)) ⊑ select e (const? 16 255) (const? 16 42)

theorem e_436 :
    1 *  ~~~(x &&& y) + 11 * (x ||| y) + 1 *  ~~~y + 2 *  ~~~(x &&&  ~~~y) - 4 *  ~~~(x ||| y) - 11 *  ~~~(x |||  ~~~y) - 13 * (x &&&  ~~~y) - 10 * (x &&& y) = 3 * y

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

theorem land_bor_left1_proof : land_bor_left1_before ⊑ land_bor_left1_after

theorem e_2483 :
    1 * (d &&& ( ~~~e ||| f)) + 2 * (f ^^^  ~~~(d &&& ( ~~~e &&& f))) + 5 * ( ~~~(d ||| e) ||| (d ^^^ (e ^^^ f))) - 6 * ((d ^^^ e) &&&  ~~~(d ^^^ f)) - 2 * ((d |||  ~~~e) &&&  ~~~(e ^^^ f)) + 3 * (e ^^^ ( ~~~d ||| (e ||| f))) - 1 * (e ^^^  ~~~( ~~~d &&& (e ^^^ f))) - 2 * (d |||  ~~~e) - 5 * (e ||| (d &&& f)) + 1 * (e ^^^ ( ~~~d &&& (e ^^^ f))) - 1 * (e ^^^ (d ||| f)) + 3 * (d ||| (e ^^^ f)) + 4 * (e ^^^  ~~~(d &&& (e &&& f))) - 6 * (e ^^^ ( ~~~d &&& ( ~~~e ||| f))) + 1 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 2 * (f ^^^ (d ||| ( ~~~e &&& f))) - 11 * (e ^^^  ~~~( ~~~d ||| (e &&& f))) + 1 * ( ~~~f &&&  ~~~(d ^^^ e)) - 5 * (e ^^^ ( ~~~d ||| (e ^^^ f))) - 1 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 1 * (f ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 7 * (f ^^^ ( ~~~d ||| (e ||| f))) - 1 * (e &&& (d ^^^ f)) + 3 * (e ||| (d ^^^ f)) + 1 * (d ||| ( ~~~e ||| f)) + 2 *  ~~~d - 1 * ((d &&& f) ^^^ (e ||| f)) - 2 * (e ^^^ (d ||| (e ||| f))) - 1 * (f ^^^  ~~~(d &&& e)) - 7 *  ~~~(d ||| f) - 2 *  ~~~(d &&&  ~~~d) + 1 * ((e &&&  ~~~f) ^^^ (d ||| (e ^^^ f))) + 2 * (f ||| (d ^^^ e)) + 7 * (e ^^^ (d &&& (e ^^^ f))) + 11 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) + 3 *  ~~~(d ||| ( ~~~e &&& f)) + 7 * ((e &&&  ~~~f) |||  ~~~( ~~~d ||| ( ~~~e &&& f))) + 1 * ((d &&& f) ||| (e &&&  ~~~f)) - 3 * (f |||  ~~~(d |||  ~~~e)) - 2 * (d ^^^ (e ^^^ f)) - 6 *  ~~~(d ||| (e &&& f)) - 1 * (e ^^^ (d &&& ( ~~~e ||| f))) - 2 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) + 2 * (d &&& e) - 1 * (f ^^^ (d &&&  ~~~e)) + 5 * (f ^^^ (d ||| (e &&& f))) - 11 * ( ~~~(d ||| e) ||| (e ^^^ f)) - 11 *  ~~~( ~~~d &&& ( ~~~e &&& f)) - 2 * (d ^^^ f) - 1 * (f ||| (d &&& e)) - 1 * (e ^^^ (d ||| (e &&& f))) + 1 *  ~~~(d ^^^ (e ^^^ f)) + 2 *  ~~~( ~~~d ||| (e &&& f)) - 7 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) + 4 * ((d &&& f) ^^^  ~~~(d ^^^ ( ~~~e &&& f))) - 11 * (f ||| (d &&&  ~~~e)) + 5 * (e ^^^  ~~~(d &&&  ~~~f)) - 6 * (e ^^^ (d ||| (e ^^^ f))) + 5 * (f &&& (d ^^^ e)) + 4 * (f ^^^  ~~~(d &&&  ~~~e)) + 1 *  ~~~(d ||| (e ^^^ f)) + 11 * (e ||| f) - 1 * (e ^^^  ~~~(d ||| ( ~~~e &&& f))) + 4 * (e &&&  ~~~(d ^^^ f)) + 1 * (f ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) + 1 * ( ~~~e &&&  ~~~(d ^^^ f)) - 1 *  ~~~(d &&&  ~~~e) + 1 * (f &&& (d ||| e)) + 3 * ((d ||| e) &&& (d ^^^ (e ^^^ f))) + 3 * ((e &&& f) ||| (d &&& (e ||| f))) - 1 * (e &&&  ~~~f) + 11 * (e ^^^ ( ~~~d &&& (e ||| f))) + 7 * (f ^^^  ~~~(d ||| e)) + 9 *  ~~~(d ||| (e ||| f)) + 7 *  ~~~(d ||| ( ~~~e ||| f)) + 11 *  ~~~( ~~~d ||| (e ||| f)) - 13 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 3 * ( ~~~d &&& ( ~~~e &&& f)) + 9 * ( ~~~d &&& (e &&& f)) - 8 * (d &&& ( ~~~e &&& f)) - 32 * (d &&& (e &&& f)) =  - 11 *  ~~~(d ^^^ f) - 1 * (d |||  ~~~f)

theorem src_is_mask_xor_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool ((x_1 ^^^ 123#8) &&& (x ^^^ x + -1#8) != x_1 ^^^ 123#8) = ofBool (x ^^^ x + -1#8 <ᵤ x_1 ^^^ 123#8)

@[simp] theorem isPoison_value : isPoison (value a) = false

theorem band_lor_right2_thm (e e_1 : IntW 1) : select e_1 (const? 1 1) (LLVM.and e e_1) ⊑ e_1

theorem set_bits_thm.extracted_1._3 : ∀ (x : BitVec 8) (x_1 : BitVec 1),
  ¬x_1 = 1#1 → True ∧ (x &&& BitVec.ofInt 8 (-6) &&& 0#8 != 0) = true → False

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

theorem udiv_i32_c_proof : udiv_i32_c_before ⊑ udiv_i32_c_after

theorem e_687 :
    2 * (x ^^^ y) - 2 *  ~~~(x ^^^ y) + 5 *  ~~~y - 6 *  ~~~(x &&&  ~~~y) - 7 *  ~~~(x &&&  ~~~x) - 1 * (x |||  ~~~y) - 2 *  ~~~(x &&& y) + 13 *  ~~~(x ||| y) + 15 *  ~~~(x |||  ~~~y) + 3 * (x &&&  ~~~y) =  - 18 * (x &&& y) + 2 * y

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

theorem e_1907 :
     - 2 * (a &&& ( ~~~b ||| c)) + 7 * ((a &&& c) |||  ~~~(b ||| c)) - 6 * ( ~~~a ||| (b ||| c)) + 11 * (b ^^^ (a ||| (b ||| c))) - 7 * (a &&& (b ^^^ c)) - 11 * ( ~~~(a |||  ~~~b) ||| (b ^^^ c)) + 2 * (c ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) - 2 * (b ^^^ (a ||| (b &&& c))) + 1 * ( ~~~(a &&&  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) - 5 * ((b &&& c) ||| ( ~~~a &&& (b ||| c))) + 2 * (c ^^^  ~~~(a ||| ( ~~~b &&& c))) + 1 * (c &&& (a ||| b)) - 11 * ( ~~~(a &&&  ~~~b) &&& (b ^^^ c)) + 1 *  ~~~(a &&& (b ||| c)) + 11 * ((a &&& c) ||| (b &&&  ~~~c)) - 1 *  ~~~(a ^^^ ( ~~~b ||| c)) - 7 *  ~~~(b ^^^ c) - 5 * ((a &&& c) ^^^  ~~~(b &&&  ~~~c)) + 2 * (c ^^^ (a ||| ( ~~~b ||| c))) + 2 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) - 6 *  ~~~( ~~~a &&& ( ~~~b ||| c)) - 2 * (b ^^^ (a &&&  ~~~c)) - 2 * (b ^^^  ~~~(a |||  ~~~c)) + 3 *  ~~~c - 6 *  ~~~(b &&&  ~~~c) - 7 * (c ^^^  ~~~( ~~~a &&& (b ||| c))) + 1 *  ~~~( ~~~a &&& ( ~~~b &&& c)) - 3 *  ~~~(a &&&  ~~~a) + 11 * (b &&&  ~~~c) + 4 *  ~~~( ~~~a ||| (b &&& c)) - 5 * (b &&& c) - 6 * ((a &&&  ~~~b) |||  ~~~(a ^^^ (b ^^^ c))) - 1 * ((a ||| b) &&&  ~~~(a ^^^ (b ^^^ c))) + 5 * (b ^^^  ~~~( ~~~a &&& ( ~~~b ||| c))) - 7 * (c ^^^  ~~~(a ||| b)) - 2 * (c ^^^  ~~~(a &&& b)) + 3 * (c ^^^ ( ~~~a ||| (b ||| c))) + 4 * (c ^^^  ~~~(a &&& (b &&& c))) + 5 * (a |||  ~~~c) - 2 * ((a &&& b) ||| (a ^^^ (b ^^^ c))) - 2 * ((b &&& c) ||| (a &&& (b ||| c))) + 2 *  ~~~(a ||| (b &&& c)) - 1 * ((a &&&  ~~~b) ||| (b ^^^ c)) + 14 *  ~~~(a ||| (b ||| c)) + 9 *  ~~~(a ||| ( ~~~b ||| c)) + 7 *  ~~~( ~~~a ||| (b ||| c)) + 18 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 39 * ( ~~~a &&& ( ~~~b &&& c)) + 64 * ( ~~~a &&& (b &&& c)) + 25 * (a &&& (b &&& c)) =  - 14 * (a &&& ( ~~~b &&& c))

theorem lshr_shl_pow2_const_case2_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬(x ≥ ↑16 ∨ 4#16 ≥ ↑16) → ofBool (x == 12#16) = 1#1 → 8192#16 >>> x <<< 4#16 &&& 32#16 = 32#16

private theorem BitVec.signExtend_slt_signExtend_of_slt {x y : BitVec w}
    {N : Nat} (hN : w ≤ N)
    (h : x.slt y) : (x.signExtend N).slt (y.signExtend N)

@[simp]
theorem Std.HashSet.mem_attachWith_mem [BEq α] [Hashable α] [LawfulBEq α] (m : HashSet α) {P H} (x : α) h :
    ⟨x, h⟩ ∈ m.attachWith P H ↔ x ∈ m

theorem not_false_not_thm.extracted_1._1 : ∀ (x : BitVec 1), x ^^^ 1#1 = 1#1 → x = 1#1 → False

theorem test2_proof : test2_before ⊑ test2_after

theorem e_1679 :
    1 * (a ||| (b ||| c)) + 11 * (b &&&  ~~~(a ^^^ c)) - 11 * (a &&&  ~~~b) + 5 * ( ~~~(a &&& b) &&& (b ^^^ c)) + 7 * ( ~~~c &&& (a ^^^ b)) - 1 * (c ^^^  ~~~(a &&&  ~~~b)) - 1 * (a ^^^ (b ^^^ c)) + 1 * (c ^^^  ~~~(a &&& ( ~~~b ||| c))) + 11 * ((b &&&  ~~~c) ^^^ ( ~~~a ||| (b ^^^ c))) + 4 * ((a &&& b) ||| (b ^^^ c)) - 1 * (b ^^^  ~~~( ~~~a &&& (b ^^^ c))) + 2 * (b ^^^ (a ||| (b ||| c))) - 11 * ( ~~~(a ||| b) ||| (a ^^^ (b ^^^ c))) + 7 * (b ^^^ ( ~~~a ||| (b ^^^ c))) + 2 * (b ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) + 11 * ((a &&& b) ^^^ (b ||| c)) - 1 * (c |||  ~~~(a |||  ~~~b)) + 1 * (c ^^^ ( ~~~a ||| (b ||| c))) + 1 * (b ^^^  ~~~(a &&& ( ~~~b &&& c))) - 11 *  ~~~(a ||| (b ||| c)) - 26 *  ~~~(a ||| ( ~~~b ||| c)) + 10 *  ~~~( ~~~a ||| (b ||| c)) - 29 * ( ~~~a &&& ( ~~~b &&& c)) - 23 * ( ~~~a &&& (b &&& c)) - 31 * (a &&& ( ~~~b &&& c)) - 11 * (a &&& (b &&& c)) =  - 1 * ((a &&&  ~~~b) |||  ~~~(a ^^^ (b ^^^ c))) + 7 *  ~~~( ~~~a ||| ( ~~~b ||| c))

theorem ashrslt_02_06_exact_proof : ashrslt_02_06_exact_before ⊑ ashrslt_02_06_exact_after

theorem bools_logical_commute0_and2_thm (e e_1 e_2 : IntW 1) :
  select (select (LLVM.xor e_2 (const? 1 1)) e_1 (const? 1 0)) (const? 1 1) (LLVM.and e_2 e) ⊑ select e_2 e e_1

theorem slt1 (w : Nat) (a b : BitVec w) : (a.slt b) ∨ (b.sle a)

theorem nonexact_ashr_ne_noexactdiv_proof : nonexact_ashr_ne_noexactdiv_before ⊑ nonexact_ashr_ne_noexactdiv_after

theorem PR42691_1_thm (e : IntW 32) :
  LLVM.or (icmp IntPred.slt e (const? 32 0)) (icmp IntPred.eq e (const? 32 2147483647)) ⊑
    icmp IntPred.ugt e (const? 32 2147483646)

theorem test24_thm (e : IntW 32) :
  LLVM.and (icmp IntPred.sgt e (const? 32 1)) (icmp IntPred.ne e (const? 32 2)) ⊑
    icmp IntPred.sgt e (const? 32 2)

theorem icmp_eq_and_pow2_minus1_shl1_negative2_thm (e : IntW 32) :
  zext 32 (icmp IntPred.eq (LLVM.and (shl (const? 32 32) e) (const? 32 15)) (const? 32 0)) ⊑ const? 32 1

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

theorem sgt_swap_and_min_commute_logical_proof : sgt_swap_and_min_commute_logical_before ⊑ sgt_swap_and_min_commute_logical_after

theorem ne_smax1_proof : ne_smax1_before ⊑ ne_smax1_after

theorem lshrult_03_13_proof : lshrult_03_13_before ⊑ lshrult_03_13_after

theorem e_995 :
    1 *  ~~~t + 11 *  ~~~z - 1 * z - 6 *  ~~~(z ||| t) - 6 *  ~~~(z |||  ~~~t) + 6 * (z &&&  ~~~t) + 7 * (z &&& t) = 1 * (z |||  ~~~t) + 5 *  ~~~(z &&&  ~~~z)

theorem sle_smax3_proof : sle_smax3_before ⊑ sle_smax3_after

theorem ashr_2_add_zext_basic_thm.extracted_1._1 : ∀ (x x_1 : BitVec 1),
  ¬1#2 ≥ ↑2 → True ∧ (zeroExtend 2 x_1).uaddOverflow (zeroExtend 2 x) = true ∨ 1#2 ≥ ↑2 → False

theorem or_and_shifts1_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(3#32 ≥ ↑32 ∨ 5#32 ≥ ↑32) →
    ¬(3#32 ≥ ↑32 ∨ 5#32 ≥ ↑32 ∨ True ∧ (x <<< 3#32 &&& 8#32 &&& (x <<< 5#32 &&& 32#32) != 0) = true) →
      x <<< 3#32 &&& 15#32 ||

theorem n2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), ¬x_1 ≥ ↑8 → True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8 → False

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

theorem andn_or_cmp_4_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 == x) = 1#1 → ofBool (x_1 != x) = 1#1 → True → False

theorem shl_add_proof : shl_add_before ⊑ shl_add_after
</all_available_lemmas>

<local_ctx>
import SSA.Projects.CIRCT.Stream.Stream

import Mathlib.Logic.Function.Iterate

import Mathlib.Data.Stream.Init

namespace CIRCTStream

namespace Stream

namespace Bisim

scoped infix:50 " ~ " => Bisim

end Bisim

open Bisim

def stuck (α : Type) : Stream α := Stream'.const none

noncomputable def nonesUntilSome (x : Stream α) (not_stuck : x ≠ stuck α) : Nat :=
  prop.choose
where
  prop : ∃ i, (x.drop i).head.isSome ∧ ∀ j < i, x.get j = none := by admit /- proof elided -/

noncomputable def dropLeadingNones (x : Stream α) (not_stuck : x ≠ stuck α) : Stream α:=
  x.drop (nonesUntilSome x not_stuck)

open Classical in

noncomputable def removeNone (x : Stream α) : Stream α :=
  Stream.corec x fun x =>
    if h : x ≠ stuck α then
      let x := x.dropLeadingNones h
      (x.head, x.tail)
    else
      (none, x)

open Classical in

open Classical in

open Classical in
</local_ctx>

<target_theorem>
theorem removeNone_equiv (x : Stream α) :
    x.removeNone ~ x :=
</target_theorem>

