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>
Inhabited in Init.Prelude
Lean.ToExpr in Lean.ToExpr
Nat in Init.Prelude
Repr in Init.Data.Repr
Bool in Init.Prelude
Int.xor in Mathlib.Data.Int.Bitwise
BitVec in Init.Prelude
BitVec.adcb in Init.Data.BitVec.Bitblast
Prod in Init.Prelude
Fin in Init.Prelude
Fin.last in Init.Data.Fin.Basic
Fin.mk in Init.Prelude
List in Init.Prelude
List.Vector in Mathlib.Data.Vector.Defs
BitVec.ofNat in Init.Prelude
BitVec.zero in Init.Data.BitVec.Basic
Fin.castLE in Init.Data.Fin.Basic
Set in Mathlib.Data.Set.Defs
Fin.cast in Init.Data.Fin.Basic
Fin.castLT in Init.Data.Fin.Basic
Fin.subNat in Init.Data.Fin.Basic
List.Vector.get in Mathlib.Data.Vector.Defs
List.Vector.nil in Mathlib.Data.Vector.Defs

syntax "xor" : MLIR.Pretty.uniform_op

syntax "max" : MLIR.Pretty.uniform_op

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

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

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

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

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

| shiftL : Term → Nat → Term

deriving Repr, Inhabited, Lean.ToExpr

def neg (x : BitStream) : BitStream :=
  fun n => (negAux x n).1

def negAux (x : BitStream) : Nat → Bool × Bool
  | 0 => (x 0, !(x 0))
  | n+1 =>
    let borrow := (negAux x n).2
    let a := x (n + 1)
    (xor (!a) borrow, !a && borrow)

def BitStream : Type := Nat → Bool

def sub (x y : BitStream) : BitStream :=
  fun n => (subAux x y n).1

def subAux (x y : BitStream) : Nat → Bool × Bool
  | 0 => (xor (x 0) (y 0), !(x 0) && y 0)
  | n+1 =>
    let borrow := (subAux x y n).2
    let a := x (n + 1)
    let b := y (n + 1)
    (xor a (xor b borrow), !a && b || ((!(xor a b)) && borrow))

def add (x y : BitStream) : BitStream :=
  fun n => (addAux x y n).1

def addAux (x y : BitStream) (i : Nat) :  Bool × Bool :=
  let carryIn : Bool := match i with
    | 0 => false
    | i + 1 => (addAux x y i).2
  Prod.swap (BitVec.adcb (x i) (y i) carryIn)

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

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

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

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

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

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

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

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

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

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

| shiftL t .. => arity t

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

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 test1_before := [llvm|
{
^0(%arg3 : i33):
  %0 = llvm.mlir.constant(4096 : i33) : i33
  %1 = llvm.urem %arg3, %0 : i33
  "llvm.return"(%1) : (i33) -> ()
}
]

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

def PR51351_after := [llvm|
{
^0(%arg0 : i64, %arg1 : i32):
  %0 = llvm.mlir.constant(-33 : i32) : i32
  %1 = llvm.add %arg1, %0 : i32
  %2 = llvm.trunc %arg0 : i64 to i32
  %3 = llvm.shl %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def shl_add_lshr_comm_after := [llvm|
{
^0(%arg151 : i32, %arg152 : i32, %arg153 : i32):
  %0 = llvm.mul %arg153, %arg153 : i32
  %1 = llvm.lshr %0, %arg152 : i32
  %2 = llvm.add %1, %arg151 overflow<nuw> : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

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

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

def xor_of_icmps_to_ne_commute_before := [llvm|
{
^0(%arg28 : i64):
  %0 = llvm.mlir.constant(4) : i64
  %1 = llvm.mlir.constant(6) : i64
  %2 = llvm.icmp "sgt" %arg28, %0 : i64
  %3 = llvm.icmp "slt" %arg28, %1 : i64
  %4 = llvm.xor %3, %2 : i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def shl_and_xor_after := [llvm|
{
^0(%arg158 : i8, %arg159 : i8):
  %0 = llvm.mlir.constant(10 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.and %arg158, %0 : i8
  %3 = llvm.xor %arg159, %2 : i8
  %4 = llvm.shl %3, %1 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

def test_before := [llvm|
{
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.icmp "eq" %0, %1 : i32
  %3 = llvm.zext %2 : i1 to i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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 negation_of_increment_via_or_disjoint_after := [llvm|
{
^0(%arg81 : i8, %arg82 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.xor %arg82, %0 : i8
  %2 = llvm.add %arg81, %1 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

def lshr_lshr_pow2_const_negative_overflow_before := [llvm|
{
^0(%arg61 : i16):
  %0 = llvm.mlir.constant(-32768 : i16) : i16
  %1 = llvm.mlir.constant(15 : i16) : i16
  %2 = llvm.mlir.constant(4 : i16) : i16
  %3 = llvm.lshr %0, %arg61 : i16
  %4 = llvm.lshr %3, %1 : i16
  %5 = llvm.and %4, %2 : i16
  "llvm.return"(%5) : (i16) -> ()
}
]

def runNNFSimpSet (g : MVarId) : MetaM (Option MVarId) := do
  let some ext ← (getSimpExtension? `bv_automata_nnf)
    | throwError m!"[bv_nnf] Error: 'bv_automata_nnf' simp attribute not found!"
  let theorems ← ext.getTheorems
  let some ext ← (Simp.getSimprocExtension? `bv_automata_nnf)
    | throwError m!"[bv_nnf] Error: 'bv_automata_nnf' simp attribute not found!"
  let simprocs ← ext.getSimprocs
  let config : Simp.Config := { Simp.neutralConfig with
    failIfUnchanged   := false,
  }
  let ctx ← Simp.mkContext (config := config)
    (simpTheorems := #[theorems])
    (congrTheorems := ← Meta.getSimpCongrTheorems)
  match ← simpGoal g ctx (simprocs := #[simprocs]) with
  | (none, _) => return none
  | (some (_newHyps, g'), _) => pure g'

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

if (evaluatedPositiveExs.any ( λ val => val > 0 || val == 0)) && evaluatedNegativeExs.all (λ val => val < 0) then
              let mut cand := gteZero bvExpr widthId
              if (evaluatedPositiveExs.all ( λ val => val > 0)) then
                  cand := strictlyGTZero bvExpr widthId

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

def sext_sub_const_after := [llvm|
{
^0(%arg25 : i1):
  %0 = llvm.mlir.constant(43) : i64
  %1 = llvm.mlir.constant(42) : i64
  %2 = "llvm.select"(%arg25, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  "llvm.return"(%2) : (i64) -> ()
}
]

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

def positive_biggershl_shlnuwnsw_before := [llvm|
{
^0(%arg44 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.mlir.constant(6 : i8) : i8
  %2 = llvm.ashr %arg44, %0 : i8
  %3 = llvm.shl %2, %1 overflow<nsw,nuw> : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def positive_with_mask_after := [llvm|
{
^0(%arg60 : i32):
  %0 = llvm.mlir.constant(128 : i32) : i32
  %1 = llvm.icmp "ult" %arg60, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def shrink_select_before := [llvm|
{
^0(%arg52 : i1, %arg53 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = "llvm.select"(%arg52, %arg53, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.trunc %1 : i32 to i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def binop_left_to_zero_srem : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (0) : i64
      %0 = llvm.srem %c, %x : i64
      llvm.return %0 : i64
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant (0) : i64
      llvm.return %c : i64
  }]

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

def alive_AndOrXor_1294_A__B__A__B___A__B_tgt :=
[sllvm| {
^bb0(%A : i64, %B : i64):
  %v1 = llvm.or %A, %B : i64
  %v2 = llvm.mlir.constant -1 : i64
  %v3 = llvm.xor %A, %v2 : i64
  %v4 = llvm.xor %v3, %B : i64
  %v5 = llvm.and %A, %B : i64
  llvm.return %v5 : i64
}]

def test_shr_and_1_ne_0_before := [llvm|
{
^0(%arg11 : i32, %arg12 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.lshr %arg11, %arg12 : i32
  %3 = llvm.and %2, %0 : i32
  %4 = llvm.icmp "ne" %3, %1 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

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

@[simp_denote]
def add_shl_moreOneUse_sh4add_riscv := [LV| {
    ^entry (%a: i64):
    %a0 = "builtin.unrealized_conversion_cast" (%a) : (i64) -> (!i64)
    %0 = ori %a0, 1 : !i64
    %1 = slli %a0, 4 : !i64
    %2 = ori %1, 16 : !i64
    %3 = add %2, %0 : !i64
    %4 = "builtin.unrealized_conversion_cast" (%3) : (!i64) -> (i64)
    llvm.return %4 : i64
  }]

def test6_before := [llvm|
{
^0(%arg204 : i8):
  %0 = llvm.mlir.constant(17 : i8) : i8
  %1 = llvm.xor %arg204, %0 : i8
  %2 = llvm.xor %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

preconditionCandidates := preconditionCandidates.insert cand

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

instance instTransformTy : MLIR.AST.TransformTy DC 0 where
  mkTy := mkTy

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

def or_umin_after := [llvm|
{
^0(%arg4 : i32):
  %0 = llvm.mlir.constant(31 : i32) : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

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

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

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

def sameBothSides (bvLogicalExpr : (BoolExpr GenBVPred)) : Bool :=
    match bvLogicalExpr with
  | .literal (GenBVPred.bin lhs _ rhs) => lhs == rhs
  | _ => false

def src_is_notmask_lshr_shl_after := [llvm|
{
^0(%arg61 : i8, %arg62 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(-124 : i8) : i8
  %2 = llvm.shl %0, %arg62 overflow<nsw> : i8
  %3 = llvm.xor %arg61, %1 : i8
  %4 = llvm.icmp "uge" %3, %2 : i8
  "llvm.return"(%4) : (i1) -> ()
}
]

def test4_logical_after := [llvm|
{
^0(%arg304 : i1):
  "llvm.return"(%arg304) : (i1) -> ()
}
]

def xor_ugt_2_before := [llvm|
{
^0(%arg13 : i8, %arg14 : i8, %arg15 : i8):
  %0 = llvm.mlir.constant(63 : i8) : i8
  %1 = llvm.mlir.constant(64 : i8) : i8
  %2 = llvm.add %arg13, %arg15 : i8
  %3 = llvm.and %arg14, %0 : i8
  %4 = llvm.or %3, %1 : i8
  %5 = llvm.xor %2, %4 : i8
  %6 = llvm.icmp "ugt" %2, %5 : i8
  "llvm.return"(%6) : (i1) -> ()
}
]

def reassoc_add_nuw_before := [llvm|
{
^0(%arg26 : i32):
  %0 = llvm.mlir.constant(4 : i32) : i32
  %1 = llvm.mlir.constant(64 : i32) : i32
  %2 = llvm.add %arg26, %0 overflow<nuw> : i32
  %3 = llvm.add %2, %1 overflow<nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

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

def test46_after := [llvm|
{
^0(%arg141 : i64):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(10752 : i32) : i32
  %2 = llvm.trunc %arg141 : i64 to i32
  %3 = llvm.shl %2, %0 : i32
  %4 = llvm.and %3, %1 : i32
  %5 = llvm.zext nneg %4 : i32 to i64
  "llvm.return"(%5) : (i64) -> ()
}
]

def land_land_left2_before := [llvm|
{
^0(%arg100 : i1, %arg101 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = "llvm.select"(%arg101, %arg100, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %2 = "llvm.select"(%1, %arg100, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%2) : (i1) -> ()
}
]

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

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

def test_before := [llvm|
{
^0(%arg0 : i32):
  %0 = llvm.mlir.constant(12 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.shl %arg0, %0 : i32
  %3 = llvm.lshr %2, %0 : i32
  %4 = llvm.icmp "ne" %3, %1 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

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

def scf.for (n: Nat) (f: Nat → β → β) (seed: β) : β :=
  let i := 0
  scf.for.loop f n (n - i) seed

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 slt_zero_sgt_minus1_after := [llvm|
{
^0(%arg22 : i4, %arg23 : i4):
  %0 = llvm.mlir.constant(-1 : i4) : i4
  %1 = llvm.xor %arg22, %arg23 : i4
  %2 = llvm.icmp "sgt" %1, %0 : i4
  "llvm.return"(%2) : (i1) -> ()
}
]

def ule_or_min_commute_before := [llvm|
{
^0(%arg138 : i8, %arg139 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.icmp "ule" %arg138, %arg139 : i8
  %2 = llvm.icmp "eq" %arg138, %0 : i8
  %3 = llvm.or %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

def or_and3_after := [llvm|
{
^0(%arg104 : i1, %arg105 : i1, %arg106 : i32, %arg107 : i32):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.icmp "ne" %arg106, %arg107 : i32
  %3 = "llvm.select"(%2, %arg105, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%arg104, %1, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

withTraceNode `LeanMLIR.Elab (return m!"{exceptEmoji ·} unwrapping `Com` expression") <| do
     
    let com : Q(ExceptM $d (Σ Γ' eff ty, Com $d Γ' eff ty)) ← whnf com
    match com.app3? ``Except.ok with
    | .some (_εexpr, _αexpr, expr) =>
        let (expr : Q(Σ Γ eff ty, Com $d Γ eff ty)) ← whnf expr
        match expr.app4? ``Sigma.mk with
        | .some (_αexpr, _βexpr, (_Γ : Q(Ctxt ($d).Ty)), expr) =>
          let (expr : Q(Σ eff ty, Com $d $_Γ eff ty)) ← whnf expr
          match expr.app4? ``Sigma.mk with
          | .some (_αexpr, _βexpr, (_eff : Q(EffectKind)), expr) =>
            match expr.app4? ``Sigma.mk with
            | .some (_αexpr, _βexpr, (_ty : Q(List ($d).Ty)), (com : Q(Com $d $_Γ $_eff $_ty))) =>
                 
                withTraceNode `LeanMLIR.Elab (return m!"{exceptEmoji ·} reducing `Com` expression") <|
                  comNf com
            | .none => throwError "Expected (Sigma.mk _ _), found {expr}"
          | .none => throwError "Expected (Sigma.mk _ _), found {expr}"
        | .none => throwError "Expected (Sigma.mk _ _), found {expr}"
    | .none => throwError "Expected `Except.ok`, found {com}"

def Deleted (Γ: Ctxt Ty) (vs : DeleteRange Γ) (Γ' : Ctxt Ty) : Prop :=
  Γ' = Γ.delete vs

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

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

def test_cast_select_before := [llvm|
{
^0(%arg12 : i1):
  %0 = llvm.mlir.constant(3 : i16) : i16
  %1 = llvm.mlir.constant(5 : i16) : i16
  %2 = "llvm.select"(%arg12, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i16, i16) -> i16
  %3 = llvm.zext %2 : i16 to i32
  "llvm.return"(%3) : (i32) -> ()
}
]

@[match_pattern] abbrev binary (w : Nat) (op : MOp.BinaryOp) : LLVM.Op :=
  MOp.binary (.concrete w) op

def not_signbit_zext_after := [llvm|
{
^0(%arg17 : i16):
  %0 = llvm.mlir.constant(-1 : i16) : i16
  %1 = llvm.icmp "sgt" %arg17, %0 : i16
  %2 = llvm.zext %1 : i1 to i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def srl_i32_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] where
  lhs := srl_llvm_i32
  rhs := srl_riscv_i32

def test15b_after := [llvm|
{
^0(%arg26 : i32):
  %0 = llvm.mlir.constant(32 : i32) : i32
  %1 = llvm.and %arg26, %0 : i32
  %2 = llvm.xor %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]
</all_available_defs>

<all_available_lemmas>
Nat.add_comm in Init.Data.Nat.Basic
Fin.add_def in Init.Data.Fin.Lemmas
Fin.castLE_castLE in Init.Data.Fin.Lemmas
Nat.le_of_eq in Init.Data.Nat.Basic
Nat.mod_eq_of_lt in Init.Data.Nat.Div.Basic

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

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

@[ext]
theorem ext {x y : BitStream} (h : ∀ i, x i = y i) : x = y

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

theorem shl_trunc_smaller_shl_thm (e : IntW 32) :
  shl (trunc 8 (shl e (const? 32 2))) (const? 8 4) ⊑ shl (trunc 8 e) (const? 8 6)

theorem ugt_and_min_thm (e e_1 : IntW 8) :
  LLVM.and (icmp IntPred.ugt e_1 e) (icmp IntPred.eq e_1 (const? 8 0)) ⊑ const? 1 0

theorem scalar_i32_shl_and_signbit_eq_proof : scalar_i32_shl_and_signbit_eq_before ⊑ scalar_i32_shl_and_signbit_eq_after

theorem reassoc_x2_mul_nuw_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(True ∧ x_1.umulOverflow 5#32 = true ∨
        True ∧ x.umulOverflow 9#32 = true ∨ True ∧ (x_1 * 5#32).umulOverflow (x * 9#32) = true) →
    True ∧ (x_1 * x).umulOverflow 45#32 = true → False

theorem slt_zero_eq_ne_0_fail2_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬30#32 ≥ ↑32 →
    ofBool (zeroExtend 32 (ofBool (x != 0#32)) == x >>> 30#32) =
      ofBool (x >>> 30#32 == zeroExtend 32 (ofBool (x != 0#32)))

theorem test1_thm.extracted_1._2 : ∀ (x x_1 : BitVec 447),
  ¬(True ∧ (x_1 &&& 70368744177664#447 &&& (x &&& 70368744177663#447) != 0) = true) →
    x_1 &&& 70368744177664#447 ^^^ x &&& 70368744177663#447 = x_1 &&& 70368744177664#447 ||

theorem test12_proof : test12_before ⊑ test12_after

theorem e_1909 :
    11 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) + 3 *  ~~~(a &&& (b &&& c)) + 11 * ((a &&&  ~~~b) ||| (a ^^^ (b ^^^ c))) + 5 * (c ^^^ ( ~~~a ||| (b &&& c))) - 7 * (b |||  ~~~c) + 1 * ((a &&& b) |||  ~~~(b |||  ~~~c)) - 7 *  ~~~(a ^^^ ( ~~~b ||| c)) - 3 * ( ~~~a &&& (b ||| c)) - 7 * (b ||| c) + 1 * (a ^^^ b) - 1 * (b ^^^ (a ||| c)) - 1 * (c ^^^  ~~~( ~~~a &&& (b &&& c))) - 11 * (a ||| b) - 1 * (a ||| ( ~~~b ||| c)) + 4 * (c ^^^  ~~~(a &&& (b &&& c))) + 7 * (b ^^^ (a ||| (b &&& c))) + 11 * (b ^^^ ( ~~~a &&& ( ~~~b ||| c))) + 2 * (b ||| (a ^^^ c)) + 1 * (c &&&  ~~~(a ^^^ b)) + 11 * (c ^^^ (a &&& ( ~~~b ||| c))) + 1 * ( ~~~a ||| (b ||| c)) - 2 * (c ^^^  ~~~(a &&&  ~~~b)) + 1 * (a ||| (b ||| c)) - 2 * (c ^^^ (a ||| ( ~~~b ||| c))) + 3 * ( ~~~b &&&  ~~~(a ^^^ c)) + 4 * (b ^^^ ( ~~~a ||| ( ~~~b ||| c))) + 2 *  ~~~(b |||  ~~~c) - 1 * (a ^^^ c) + 1 *  ~~~(b &&& c) + 3 * (c &&&  ~~~(a &&& b)) - 3 * (b ^^^  ~~~(a &&& ( ~~~b &&& c))) - 1 * (a ^^^ (b &&& c)) - 6 *  ~~~(a ||| c) - 1 * ((a &&& b) ^^^  ~~~(a ^^^ ( ~~~b ||| c))) - 11 * (b ^^^ ( ~~~a &&& (b ||| c))) + 1 * ((a |||  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) - 2 * ((a &&& b) ^^^ (b |||  ~~~c)) - 7 * (a |||  ~~~c) - 3 * (c &&& (a ^^^ b)) + 11 *  ~~~(a &&& c) - 2 * ((a &&& c) ^^^ (a ^^^ (b &&& c))) + 2 * (c |||  ~~~(a |||  ~~~b)) - 13 *  ~~~(a ||| (b ||| c)) - 5 *  ~~~(a ||| ( ~~~b ||| c)) - 9 *  ~~~( ~~~a ||| (b ||| c)) + 27 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 36 * ( ~~~a &&& ( ~~~b &&& c)) + 6 * ( ~~~a &&& (b &&& c)) - 5 * (a &&& ( ~~~b &&& c)) + 8 * (a &&& (b &&& c)) = 2 * (c ^^^ (a &&& (b ||| c))) + 11 * (b ^^^ ( ~~~a ||| (b &&& c)))

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

theorem uge_swap_or_max_commute_thm (e e_1 : IntW 8) :
  LLVM.or (icmp IntPred.eq e_1 (const? 8 (-1))) (icmp IntPred.ule e e_1) ⊑
    icmp IntPred.ule e e_1

theorem e_2492 :
     - 1 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) + 5 * ((d &&& e) |||  ~~~(e ||| f)) + 2 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 11 * (d &&& e) - 1 * (e ^^^ (d ||| (e &&& f))) - 2 * ((d ^^^ e) &&& (d ^^^ f)) - 1 * ( ~~~(d &&&  ~~~e) &&& (d ^^^ (e ^^^ f))) - 3 * (e ^^^  ~~~( ~~~d &&& (e &&& f))) - 3 * (f ^^^  ~~~(d &&& (e ||| f))) + 5 * (f ^^^  ~~~(d &&& (e &&& f))) - 6 * (e ^^^  ~~~(d &&& (e ^^^ f))) + 4 * (e ^^^ (d &&& f)) + 4 *  ~~~( ~~~d &&& (e ||| f)) + 3 * d - 11 * (e ^^^ (d ||| (e ^^^ f))) - 11 * (e ^^^ (d &&&  ~~~f)) + 2 * (d &&&  ~~~f) - 3 * (e ^^^  ~~~( ~~~d ||| (e &&& f))) - 1 * (e ||| (d &&& f)) - 1 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) - 6 * ((d ||| e) &&&  ~~~(e ^^^ f)) + 2 * (d &&& (e ||| f)) + 3 * (d ^^^ ( ~~~e ||| f)) - 7 * ((d &&& e) |||  ~~~(d ^^^ (e ^^^ f))) + 3 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) - 5 * ((d &&& e) ^^^ (e |||  ~~~f)) + 4 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) - 11 * (e &&& f) - 7 * ( ~~~d ||| (e ^^^ f)) - 1 * ((d ^^^ e) ||| (d ^^^ f)) + 11 * (e |||  ~~~(d ||| f)) + 1 *  ~~~(e |||  ~~~f) - 2 * ((e &&& f) ^^^  ~~~(d &&& (e ^^^ f))) - 2 * (e ^^^ ( ~~~d ||| (e &&& f))) - 11 * ( ~~~d ||| ( ~~~e ||| f)) + 2 * ((d &&& f) ||| (e &&&  ~~~f)) - 11 *  ~~~(d ^^^ f) + 1 *  ~~~(d &&& e) + 7 * ( ~~~(d ||| e) |||  ~~~(d ^^^ (e ^^^ f))) - 1 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) - 6 * (e ^^^  ~~~(d &&& (e ||| f))) - 5 * (f &&&  ~~~(d &&&  ~~~e)) + 1 * (f ^^^ ( ~~~d ||| ( ~~~e ||| f))) + 1 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) - 5 * ((d ||| e) &&& (d ^^^ (e ^^^ f))) + 5 * (f ||| (d ^^^ e)) - 2 * (f ^^^ (d ||| ( ~~~e &&& f))) - 2 *  ~~~(d &&& (e ^^^ f)) + 1 *  ~~~(d &&& f) + 5 * (f ^^^ (d &&& e)) - 2 * (e ^^^ ( ~~~d ||| ( ~~~e &&& f))) + 1 * (e ^^^ (d ||| f)) - 3 * (f ||| (d &&& e)) - 1 * ( ~~~(d |||  ~~~e) |||  ~~~(e ^^^ f)) + 2 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) + 2 * ((d &&&  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) - 11 *  ~~~(d |||  ~~~e) - 1 * (e ^^^  ~~~( ~~~d &&& (e ||| f))) + 11 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f)) - 1 * ( ~~~(d &&& e) &&&  ~~~(d ^^^ (e ^^^ f))) + 7 * ( ~~~d &&& (e ^^^ f)) + 1 * (d ||| e) + 7 * ( ~~~e &&&  ~~~(d ^^^ f)) - 5 * (f ^^^ (d ||| (e ||| f))) + 2 *  ~~~(e &&&  ~~~f) + 4 * (e ^^^  ~~~(d ||| (e &&& f))) + 1 * (e ||| f) + 11 * (d ^^^ (e ||| f)) + 1 *  ~~~(d ^^^ (e &&& f)) + 4 * (f ^^^  ~~~(d ||| e)) - 2 *  ~~~(d &&& ( ~~~e ||| f)) + 11 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) - 7 * (d ||| ( ~~~e ||| f)) + 1 * (e ||| (d &&&  ~~~f)) + 7 *  ~~~(d ||| (e ||| f)) + 17 *  ~~~(d ||| ( ~~~e ||| f)) + 44 *  ~~~( ~~~d ||| (e ||| f)) - 41 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 13 * ( ~~~d &&& ( ~~~e &&& f)) + 42 * ( ~~~d &&& (e &&& f)) + 20 * (d &&& ( ~~~e &&& f)) + 29 * (d &&& (e &&& f)) = 5 * (e ^^^ ( ~~~d &&& (e ||| f)))

theorem ashrslt_03_03_proof : ashrslt_03_03_before ⊑ ashrslt_03_03_after

theorem and_ashr_not_commuted_thm (e e_1 e_2 : IntW 8) :
  LLVM.and (LLVM.xor (ashr e_2 e_1) (const? 8 (-1))) (ashr e e_1) ⊑
    ashr (LLVM.and e (LLVM.xor e_2 (const? 8 (-1)))) e_1

theorem trunc_equality_nuw_zext_proof : trunc_equality_nuw_zext_before ⊑ trunc_equality_nuw_zext_after

theorem ashr_mul_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬8#20 ≥ ↑20 → True ∧ (signExtend 16 x_1).smulOverflow (signExtend 16 x) = true ∨ 8#16 ≥ ↑16 → False

theorem t2_proof : t2_before ⊑ t2_after

theorem lshrugt_01_13_proof : lshrugt_01_13_before ⊑ lshrugt_01_13_after

theorem positive_biggerlshr_shlnsw_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬(6#8 ≥ ↑8 ∨ True ∧ (x >>> 6#8 <<< 3#8).sshiftRight' 3#8 ≠ x >>> 6#8 ∨ 3#8 ≥ ↑8) →
    ¬3#8 ≥ ↑8 → x >>> 6#8 <<< 3#8 = x >>> 3#8 &&& 24#8

theorem test4_proof : test4_before ⊑ test4_after

theorem test4_thm (e : IntW 8) :
  icmp IntPred.sle e (const? 8 126) ⊑ icmp IntPred.ne e (const? 8 127)

theorem e_1538 :
    2 *  ~~~(a &&&  ~~~a) + 1 * ( ~~~c &&& (a ^^^ b)) + 5 * ( ~~~(a &&&  ~~~b) &&& (b ^^^ c)) - 2 * (b ^^^  ~~~(a &&& (b ^^^ c))) + 4 * (b ^^^ (a ||| (b &&& c))) - 4 *  ~~~(a ||| (b ||| c)) - 12 *  ~~~(a ||| ( ~~~b ||| c)) - 5 *  ~~~( ~~~a ||| (b ||| c)) - 9 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 9 * ( ~~~a &&& ( ~~~b &&& c)) - 10 * (a &&& ( ~~~b &&& c)) - 6 * (a &&& (b &&& c)) = 2 * ( ~~~a &&& (b &&& c)) - 4 * (b ^^^ ( ~~~a ||| ( ~~~b &&& c)))

theorem test_ult_xor_thm (e e_1 : IntW 32) :
  icmp IntPred.ult (LLVM.xor (LLVM.xor e_1 (const? 32 (-1))) e) (LLVM.xor e_1 (const? 32 (-1))) ⊑
    icmp IntPred.ugt (LLVM.xor e e_1) e_1

theorem zext_sext_sle_known_nonneg_op0_narrow_thm.extracted_1._1 : ∀ (x : BitVec 16) (x_1 : BitVec 8),
  True ∧ (x_1 &&& 12#8).msb = true → False

theorem or_trunc_lshr_proof : or_trunc_lshr_before ⊑ or_trunc_lshr_after

theorem test_add_nsw__nuw_is_safe_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 2147483647#32 == 2147483647#32) = 1#1 → True ∧ (x &&& 2147483647#32).uaddOverflow 1#32 = true → False

theorem min_of_max_thm (e : IntW 32) :
  select
      (icmp IntPred.slt
        (select (icmp IntPred.slt e (const? 32 0)) (LLVM.xor e (const? 32 (-1))) (const? 32 (-1)))
        (const? 32 (-1)))
      (select (icmp IntPred.slt e (const? 32 0)) (LLVM.xor e (const? 32 (-1))) (const? 32 (-1))) (const? 32 (-1)) ⊑
    const? 32 (-1)

theorem t0_thm.extracted_1._2 : ∀ (x : BitVec 8) (x_1 : BitVec 1),
  ¬x_1 = 1#1 → signExtend 8 x_1 + x ^^^ signExtend 8 x_1 = x

theorem sext_sext_ne_proof : sext_sext_ne_before ⊑ sext_sext_ne_after

theorem nonexact_lshr_eq_proof : nonexact_lshr_eq_before ⊑ nonexact_lshr_eq_after

theorem sle_smax4_proof : sle_smax4_before ⊑ sle_smax4_after

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

theorem nomask_rhs_proof : nomask_rhs_before ⊑ nomask_rhs_after

theorem mul_splat_fold_thm (e : IntW 32) :
  lshr (mul e (const? 32 65537) { «nsw» := false, «nuw» := true }) (const? 32 16) ⊑ e

theorem test_shl_nuw_nsw__nuw_is_safe_proof : test_shl_nuw_nsw__nuw_is_safe_before ⊑ test_shl_nuw_nsw__nuw_is_safe_after

theorem one_side_fold_sgt_thm.extracted_1._9 : ∀ (x x_1 x_2 : BitVec 32) (x_3 : BitVec 1),
  x_3 = 1#1 → ¬x_3 ^^^ 1#1 = 1#1 → ofBool (x_2 <ₛ x_2) = 0#1

theorem foo1_and_signbit_lshr_proof : foo1_and_signbit_lshr_before ⊑ foo1_and_signbit_lshr_after

theorem shift_no_xor_multiuse_cmp_with_xor_proof : shift_no_xor_multiuse_cmp_with_xor_before ⊑ shift_no_xor_multiuse_cmp_with_xor_after

theorem xor_with_or_disjoint_ab_proof : xor_with_or_disjoint_ab_before ⊑ xor_with_or_disjoint_ab_after

theorem and_logic_and_logic_or_5_thm.extracted_1._7 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 = 1#1 → ¬0#1 = 1#1 → x_2 &&& x = 0#1

@[aesop 50% unsafe]
theorem Std.HashMap.insert_keys_perm_new [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) (v : V) :
    k ∉ m → (m.insert k v).keys.Perm (k :: m.keys)

theorem lor_land_right2_thm (e e_1 : IntW 1) : select e_1 (select e (const? 1 1) e_1) (const? 1 0) ⊑ e_1

theorem scalar_i32_lshr_and_signbit_ne_proof : scalar_i32_lshr_and_signbit_ne_before ⊑ scalar_i32_lshr_and_signbit_ne_after

theorem a_false_implies_b_true_thm (e e_1 : IntW 1) (e_2 : IntW 8) :
  select (icmp IntPred.ugt e_2 (const? 8 10)) (const? 1 1)
      (select (icmp IntPred.ult e_2 (const? 8 20)) e_1 e) ⊑
    select (icmp IntPred.ugt e_2 (const? 8 10)) (const? 1 1) e_1

theorem test_nuw_and_unsigned_pred_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬(True ∧ (10#64).usubOverflow x = true) → ofBool (10#64 - x <ᵤ 3#64) = ofBool (7#64 <ᵤ x)

theorem icmp_eq_and_pow2_minus1_shl_pow2_proof : icmp_eq_and_pow2_minus1_shl_pow2_before ⊑ icmp_eq_and_pow2_minus1_shl_pow2_after

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

theorem test32_thm.extracted_1._1 : ∀ (x : BitVec 32), ¬2#32 ≥ ↑32 → (x &&& 16#32) >>> 2#32 &&& 1#32 = 0#32

theorem t1_flags_sub_nsw_sub_thm (e e_1 e_2 : IntW 8) :
  sub (sub e_2 e_1 { «nsw» := true, «nuw» := false }) e ⊑ sub e_2 (add e_1 e)

theorem lshrult_03_02_proof : lshrult_03_02_before ⊑ lshrult_03_02_after

theorem select_xor_icmp2_thm.extracted_1._3 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x_1 != 0#32) = 1#1 → ¬ofBool (x_1 == 0#32) = 1#1 → False

@[simp]
theorem Term.toBV_bor {wenv : WidthExpr.Env wcard}
    {tctx : Term.Ctx wcard tcard}
    (benv : Term.BoolEnv bcard)
    (tenv : tctx.Env wenv) (a b : Term bcard ncard icard pcard tctx (.bv w)) :
  Term.toBV benv nenv ienv penv tenv (.bor a b) = a.toBV benv nenv ienv penv tenv ||

theorem ashrslt_03_11_thm (e : IntW 4) : icmp IntPred.slt (ashr e (const? 4 3)) (const? 4 (-5)) ⊑ const? 1 0

theorem ashrslt_03_08_proof : ashrslt_03_08_before ⊑ ashrslt_03_08_after

theorem no_shift_no_xor_multiuse_cmp_or_proof : no_shift_no_xor_multiuse_cmp_or_before ⊑ no_shift_no_xor_multiuse_cmp_or_after

@[simp]
theorem xor_ne_self {a b : Bool} : (a ^^ ((!a) != b)) = !b

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

lemma CNFA.reverse_spec {m : CNFA n} : m.reverse.Sim m.toNFA'.reverse

theorem t4_ugt_slt_65536_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ofBool (65535#32 <ᵤ x_1) = 1#1 → ofBool (x_1 <ₛ 65536#32) = 1#1 → ofBool (65535#32 <ₛ x_1) = 1#1 → False

theorem unmasked_shlop_insufficient_mask_shift_amount_proof : unmasked_shlop_insufficient_mask_shift_amount_before ⊑ unmasked_shlop_insufficient_mask_shift_amount_after

theorem not_or_or_and_not_and_and_commute2_proof : not_or_or_and_not_and_and_commute2_before ⊑ not_or_or_and_not_and_and_commute2_after

theorem sub_not_thm (e e_1 : IntW 8) :
  LLVM.xor (sub e_1 e) (const? 8 (-1)) ⊑ add e (LLVM.xor e_1 (const? 8 (-1)))

theorem t0_thm.extracted_1._21 : ∀ (x x_1 x_2 x_3 : BitVec 8) (x_4 : BitVec 1),
  x_4 ^^^ 1#1 = 1#1 → ¬x_4 = 1#1 → ¬ofBool (x_3 == x_2) = 1#1 → ¬ofBool (x_3 != x_2) = 1#1 → x = x_1

theorem and_signbit_select_ashr_proof : and_signbit_select_ashr_before ⊑ and_signbit_select_ashr_after

theorem exact_lshr_eq_exactdiv_proof : exact_lshr_eq_exactdiv_before ⊑ exact_lshr_eq_exactdiv_after

@[simp] theorem Com.denote_rets {eff : EffectKind} (Γ : Ctxt d.Ty) (vs : HVector Γ.Var ts) :
    (Com.rets (eff := eff) vs).denote = fun V => pure (vs.map V)

theorem lshr_mul_times_3_div_2_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(True ∧ x.smulOverflow 3#32 = true ∨ True ∧ x.umulOverflow 3#32 = true ∨ 1#32 ≥ ↑32) →
    1#32 ≥ ↑32 ∨ True ∧ x.saddOverflow (x >>> 1#32) = true ∨ True ∧ x.uaddOverflow (x >>> 1#32) = true → False

theorem test15_proof : test15_before ⊑ test15_after

theorem scalar_i16_shl_ult_const_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬8#16 ≥ ↑16 → ofBool (x <<< 8#16 <ᵤ 1024#16) = ofBool (x &&& 252#16 == 0#16)

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

theorem t17_nocse_mismatching_x_proof : t17_nocse_mismatching_x_before ⊑ t17_nocse_mismatching_x_after

theorem lshr_and_add_proof : lshr_and_add_before ⊑ lshr_and_add_after

theorem lshr_pow2_slt_thm (e : IntW 8) :
  icmp IntPred.slt (lshr (const? 8 (-128)) e) (const? 8 3) ⊑
    icmp IntPred.slt (lshr (const? 8 (-128)) e { «exact» := true }) (const? 8 3)
</all_available_lemmas>

<local_ctx>
import Batteries.Data.Fin.Basic

import Batteries.Data.Fin.Lemmas

import Blase.SingleWidth.Defs

import Blase.AutoStructs.Constructions

import Blase.AutoStructs.Defs

import Blase.AutoStructs.FiniteStateMachine

import Mathlib.Tactic.Ring

import Mathlib.Data.Nat.Size -- TODO: remove and get rid of shiftLeft_eq_mul_pow use

import Mathlib.Data.BitVec

import Mathlib.Tactic.FinCases

open Fin.NatCast

open Mathlib

section fsm

variable {arity : Type} [FinEnum arity]

open BitStream in

end fsm

section nfas_relations

end nfas_relations

def liftOp n : Fin (n + 1) → Fin (n + 3) :=
  fun k =>
    if k = n then Fin.last (n+2) else k.castLE (by admit /- proof elided -/
    )

@[simp]
def liftOp_unchanged (k : Fin n) : liftOp n k.castSucc = k.castLE (by simp) :=

inductive TermBinop where
| and | or | xor | add | sub

def TermBinop.subst (op : TermBinop) (t₁ t₂ : Term) : Term :=
  match op with
  | .and => .and t₁ t₂
  | .or => .or t₁ t₂
  | .xor => .xor t₁ t₂
  | .add => .add t₁ t₂
  | .sub => .sub t₁ t₂

def TermBinop.openTerm (op : TermBinop) : Term := op.subst (.var 0) (.var 1)

@[simp]
def TermBinop.openTerm_arity (op : TermBinop) : op.openTerm.arity + 1 = 3 :=

def swapLastTwoBlock (x : Fin (n + 3)) : Fin (n + 3) :=
  if x = Fin.last (n+2) then n
  else if x = n+1 then Fin.last (n + 2)
  else if x = n then n + 1
  else x
</local_ctx>

<target_theorem>
lemma TermBinop.alt_lang {t₁ t₂ : Term} (op : TermBinop) :
  (op.subst_arity' ▸ (op.subst t₁ t₂).language) =
    let lop : Set (BitVecs 3) :=
</target_theorem>

