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>
Vector in Init.Data.Vector.Basic
Fin in Init.Prelude
String in Init.Prelude
Unit in Init.Prelude
List in Init.Prelude
Field in Mathlib.Algebra.Field.Defs
Bool in Init.Prelude
DecidableEq in Init.Prelude
FinEnum in Mathlib.Data.FinEnum
Hashable in Init.Prelude
Sum.inl in Init.Core
Sum.inr in Init.Core
Nat in Init.Prelude
Repr in Init.Data.Repr
Sum in Init.Core
Sum.elim in Init.Data.Sum.Basic
id in Init.Prelude
Empty in Init.Prelude
Empty.elim in Init.Core
Nat.max in Init.Data.Nat.Basic
Nat.min in Init.Data.Nat.Basic
Decidable in Init.Prelude

syntax "min" : MLIR.Pretty.uniform_op

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 ls (b : Bool) : FSM Unit :=
  { α := Unit,
    initCarry := fun _ => b,
    nextStateCirc := fun () => Circuit.var true (inr ()),
    outputCirc := Circuit.var true (inl ())
  }

structure FSM (arity : Type) : Type 1 where
   
  ( α  : Type )
  [ i : FinEnum α ]
  [ h : Hashable α ]
  [ dec_eq : DecidableEq α ]
   
  ( initCarry : α → Bool )
   
  outputCirc : Circuit (α ⊕ arity)
  nextStateCirc : α → Circuit (α ⊕ arity)

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

def Var (Γ : Context Ty) (ty : Ty) : Type := { v : VarName // Γ.hasType v ty }

inductive StateSpace (wcard tcard bcard ncard icard pcard : Nat)
| widthVar (v : Fin wcard)
| termVar (v : Fin tcard)
| predVar (v : Fin pcard)
| boolVar (v : Fin bcard)
deriving DecidableEq, Repr, Hashable

inductive Term
| ofNat (w : WidthExpr) (n : Nat) : Term
| var (v : Nat) (w : WidthExpr) : Term
| add (w : WidthExpr) (a b : Term) : Term
| zext (a : Term) (wnew : WidthExpr) : Term
| setWidth (a : Term) (wnew : WidthExpr) : Term
| sext (a : Term) (wnew : WidthExpr) : Term
| bor (w : WidthExpr) (a b : Term) : Term
| band (w : WidthExpr) (a b : Term) : Term
| bxor (w : WidthExpr) (a b : Term) : Term
| bnot (w : WidthExpr)  (a : Term) : Term
| boolVar (v : Nat) : Term
| boolConst (b : Bool) : Term
| shiftl (w : WidthExpr) (a : Term) (k : Nat) : Term
| bvOfBool (b : Term) : Term
| binWidthRel (k : WidthBinaryRelationKind) (wa wb : WidthExpr) : Term
| binRel (k : BinaryRelationKind) (w : WidthExpr)
    (a : Term) (b : Term) : Term
| or (p1 p2 : Term) : Term
| and (p1 p2 : Term) : Term
| pvar (v : Nat) : Term
| boolBinRel (k : BoolBinaryRelationKind)
    (a b : Term) : Term
deriving DecidableEq, Inhabited, Repr, Lean.ToExpr

def composeUnaryAux
    (p : FSM Unit)
    (q : FSM arity) :
    FSM arity :=
  p.compose
    arity
    _
    (λ _ => id)
    (λ _ => q)

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 -/

structure NatFSM (wcard tcard bcard ncard icard pcard : Nat) (v : Nondep.WidthExpr) where
  toFsm : FSM (StateSpace wcard tcard bcard ncard icard pcard)

inductive WidthExpr where
| const : Nat → WidthExpr
| var : Nat → WidthExpr
| max : WidthExpr → WidthExpr → WidthExpr
| min : WidthExpr → WidthExpr → WidthExpr
| addK : WidthExpr → Nat → WidthExpr
| kadd : Nat → WidthExpr → WidthExpr
deriving Inhabited, Repr, Hashable, DecidableEq, Lean.ToExpr

def scanAnd  : FSM Unit :=
  {
   α := Unit,
   initCarry := fun () => true,
   outputCirc := Circuit.var true (inl ()) &&& Circuit.var true (inr ()),
   nextStateCirc := fun () => (Circuit.var true (inl ())) &&& (Circuit.var true (inr ()))
  }

def scanOr  : FSM Unit :=
  {
   α := Unit,
   initCarry := fun () => false,
   outputCirc := Circuit.var true (inl ()) ||| Circuit.var true (inr ()),
   nextStateCirc := fun () => Circuit.var true (inl ()) ||| Circuit.var true (inr ())
  }

def composeBinaryAux'
    (p : FSM Bool)
    (qtrue : FSM α)
    (qfalse : FSM α) :
    FSM α :=
  p.compose (α)
    (λ _ => α)
    (λ _ i => i)
    (λ b => match b with
      | true => qtrue
      | false => qfalse)

def and : FSM Bool :=
  { α := Empty,
    initCarry := Empty.elim,
    nextStateCirc := fun a => a.elim,
    outputCirc := Circuit.var true (inr true) &&& Circuit.var true (inr false),
  }

abbrev WidthExpr.Env (wcard : Nat) : Type :=
  Fin wcard → Nat

structure HWidthEnv {wcard tcard : Nat}
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream)
    (wenv : Fin wcard → Nat) : Prop where
    heq_width : ∀ (v : Fin wcard),
      fsmEnv (StateSpace.widthVar v) = BitStream.ofNatUnary (wenv v)

structure HPredicateEnv {wcard tcard bcard ncard icard pcard : Nat}
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream)
    (penv : Fin pcard → Prop) : Prop where
    heq_width : ∀ (v : Fin pcard),
      fsmEnv (StateSpace.predVar v) = BitStream.ofProp (penv v)

def BitStream : Type := Nat → Bool

abbrev ofNatUnary (n : Nat) : BitStream :=
  fun i => decide (i < n)

structure HNatFSMToBitstream {wcard : Nat} {v : WidthExpr wcard} {tcard : Nat} {bcard : Nat} {pcard : Nat}
   (fsm : NatFSM wcard tcard bcard ncard icard pcard (.ofDep v)) : Prop where
  heq :
    ∀ (wenv : Fin wcard → Nat)
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream),
    (henv : HWidthEnv fsmEnv wenv) →
      fsm.toFsm.eval fsmEnv =
      BitStream.ofNatUnary (v.toNat wenv)

def WidthExpr.toNat (e : WidthExpr wcard) (env : WidthExpr.Env wcard) : Nat :=
  match e with
  | .const n => n
  | .var v => env v
  | .min v w => Nat.min (v.toNat env) (w.toNat env)
  | .max v w => Nat.max (v.toNat env) (w.toNat env)
  | .addK v k => v.toNat env + k
  | .kadd k v => k + v.toNat env

inductive WidthExpr (wcard : Nat) : Type
| const (n : Nat) :  WidthExpr wcard
| var : (v : Fin wcard) → WidthExpr wcard
| min : (v w : WidthExpr wcard) → WidthExpr wcard
| max : (v w : WidthExpr wcard) → WidthExpr wcard
| addK : (v : WidthExpr wcard) → (k : Nat) → WidthExpr wcard
| kadd : (k : Nat) → (v : WidthExpr wcard) → WidthExpr wcard

structure HPredFSMToBitStream {pcard : Nat}
  {tctx : Term.Ctx wcard tcard}
  {p : Term bcard ncard icard pcard tctx .prop}
  (fsm : TermFSM wcard tcard bcard ncard icard pcard
    (.ofDepTerm p)) : Prop where
  heq :
    ∀ {wenv : WidthExpr.Env wcard}
      (benv : Term.BoolEnv bcard)
      (nenv : Term.NatEnv ncard)
      (ienv : Term.IntEnv icard)
      (penv : Predicate.Env pcard) (tenv : tctx.Env wenv)
      (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream),
      (htenv : HTermEnv fsmEnv tenv benv) →
      (hpenv : HPredicateEnv fsmEnv penv) →
        p.toBV benv nenv ienv penv tenv  ↔ (fsm.toFsmZext.eval fsmEnv = .negOne)

def scanOr (s : BitStream) : BitStream := scanl false Bool.or s

abbrev scanl (init : Bool) (f : Bool → Bool → Bool) (s : BitStream) : BitStream :=
  fun n => match n with
    | 0 => f init (s 0)
    | n+1 => f (scanl init f s n) (s (n + 1))

def scanAnd (s : BitStream) : BitStream := scanl true Bool.and s

def bools_multi_uses2_logical_after := [llvm|
{
^0(%arg36 : i1, %arg37 : i1, %arg38 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.xor %arg38, %0 : i1
  %3 = "llvm.select"(%2, %arg36, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %4 = "llvm.select"(%arg38, %arg37, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %5 = "llvm.select"(%arg38, %arg37, %arg36) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %6 = llvm.xor %3, %4 : i1
  %7 = "llvm.select"(%5, %6, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%7) : (i1) -> ()
}
]

def test1_after := [llvm|
{
^0(%arg34 : i32, %arg35 : i32):
  %0 = llvm.icmp "ugt" %arg35, %arg34 : i32
  "llvm.return"(%0) : (i1) -> ()
}
]

def ValueStream := Stream

def liftMax2 (n m : Nat) : Fin m → Fin (max n m) :=
  fun k => k.castLE (by admit /- proof elided -/
  )

def sgt_negative_multip_rem_zero_before := [llvm|
{
^0(%arg169 : i8):
  %0 = llvm.mlir.constant(-7 : i8) : i8
  %1 = llvm.mlir.constant(21 : i8) : i8
  %2 = llvm.mul %arg169, %0 overflow<nsw> : i8
  %3 = llvm.icmp "sgt" %2, %1 : i8
  "llvm.return"(%3) : (i1) -> ()
}
]

def icmp_slt_0_and_icmp_sge_neg1_i64_fail_after := [llvm|
{
^0(%arg59 : i64):
  %0 = llvm.mlir.constant(-2) : i64
  %1 = llvm.mlir.constant(62) : i64
  %2 = llvm.mlir.constant(1) : i64
  %3 = llvm.mlir.constant(0) : i64
  %4 = llvm.icmp "sgt" %arg59, %0 : i64
  %5 = llvm.lshr %arg59, %1 : i64
  %6 = llvm.and %5, %2 : i64
  %7 = "llvm.select"(%4, %6, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i64, i64) -> i64
  "llvm.return"(%7) : (i64) -> ()
}
]

def sge_swap_and_max_commute_logical_after := [llvm|
{
^0(%arg240 : i8, %arg241 : i8):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.icmp "eq" %arg240, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def positive_sameconst_shlnuwnsw_lshrexact_before := [llvm|
{
^0(%arg26 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.lshr exact %arg26, %0 : i8
  %2 = llvm.shl %1, %0 overflow<nsw,nuw> : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

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

instance [ToString w] : ToString (DCOp.ValueStream w) where
  toString s := toString (Stream.toList 10 s)

def eq_smax3_after := [llvm|
{
^0(%arg59 : i32, %arg60 : i32):
  %0 = llvm.mlir.constant(3 : i32) : i32
  %1 = llvm.add %arg59, %0 : i32
  %2 = llvm.icmp "sge" %1, %arg60 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def t1_after := [llvm|
{
^0(%arg12 : i4):
  %0 = llvm.mlir.constant(3 : i4) : i4
  %1 = llvm.mlir.constant(6 : i4) : i4
  %2 = llvm.and %arg12, %0 : i4
  %3 = llvm.xor %2, %1 : i4
  "llvm.return"(%3) : (i4) -> ()
}
]

List.insert in Init.Data.List.Basic

protected instance Expr.decidableEq [DecidableEq d.Op] [DecidableEq d.Ty] :
    {Γ : Ctxt d.Ty} → {ty : List d.Ty} → DecidableEq (Expr d Γ eff ty)
  | Γ, _, .mk op₁ rfl eff_le₁ arg₁ regArgs₁, .mk op₂ eq eff_le₂ arg₂ regArgs₂ =>
    if ho : op₁ = op₂ then by
      subst ho
      letI := HVector.decidableEq arg₁ arg₂
      letI := HVector.decidableEqReg regArgs₁ regArgs₂
      exact decidable_of_iff (arg₁ = arg₂ ∧ regArgs₁ = regArgs₂) (by admit /- proof elided -/
      )
    else isFalse (by admit /- proof elided -/
    )

def icmp_and_ashr_multiuse_logical_after := [llvm|
{
^0(%arg4 : i32):
  %0 = llvm.mlir.constant(240 : i32) : i32
  %1 = llvm.mlir.constant(224 : i32) : i32
  %2 = llvm.mlir.constant(496 : i32) : i32
  %3 = llvm.mlir.constant(432 : i32) : i32
  %4 = llvm.and %arg4, %0 : i32
  %5 = llvm.icmp "ne" %4, %1 : i32
  %6 = llvm.and %arg4, %2 : i32
  %7 = llvm.icmp "ne" %6, %3 : i32
  %8 = llvm.and %5, %7 : i1
  "llvm.return"(%8) : (i1) -> ()
}
]

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

def test9_after := [llvm|
{
^0(%arg111 : i32, %arg112 : i32):
  %0 = llvm.or %arg111, %arg112 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

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

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

def Lets.outContext (lets : UnTyped.Lets Op VarName) (Γ_in : Context Ty) : Context Ty :=
  lets.inner.foldl (fun Γ e => Γ.push e.varName (signature e.op).returnType) Γ_in

def test2_after := [llvm|
{
^0(%arg24 : i32, %arg25 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg24, %arg25 : i32
  %2 = llvm.icmp "sgt" %1, %0 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def udiv_common_dividend_defined_cond_before := [llvm|
{
^0(%arg17 : i1, %arg18 : i5, %arg19 : i5, %arg20 : i5):
  %0 = llvm.udiv %arg18, %arg19 : i5
  %1 = llvm.udiv %arg18, %arg20 : i5
  %2 = "llvm.select"(%arg17, %1, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i5, i5) -> i5
  "llvm.return"(%2) : (i5) -> ()
}
]

def and_xor_or4_after := [llvm|
{
^0(%arg664 : i64, %arg665 : i64, %arg666 : i64):
  %0 = llvm.mlir.constant(42) : i64
  %1 = llvm.udiv %0, %arg665 : i64
  %2 = llvm.udiv %0, %arg666 : i64
  %3 = llvm.or %2, %1 : i64
  "llvm.return"(%3) : (i64) -> ()
}
]

def xvar := @MultiWidth.Term.var (wcard := 1) (bcard := 0) (ncard := 0) (icard := 0) (pcard := 0) (tcard := 2)
  (tctx := tctx) (v := ⟨0, by admit /- proof elided -/
  ⟩)

def eq_3210_before := [llvm|
{
^0(%arg126 : i32, %arg127 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(16 : i32) : i32
  %2 = llvm.mlir.constant(24 : i32) : i32
  %3 = llvm.trunc %arg126 : i32 to i8
  %4 = llvm.lshr %arg126, %0 : i32
  %5 = llvm.trunc %4 : i32 to i8
  %6 = llvm.lshr %arg126, %1 : i32
  %7 = llvm.trunc %6 : i32 to i8
  %8 = llvm.lshr %arg126, %2 : i32
  %9 = llvm.trunc %8 : i32 to i8
  %10 = llvm.trunc %arg127 : i32 to i8
  %11 = llvm.lshr %arg127, %0 : i32
  %12 = llvm.trunc %11 : i32 to i8
  %13 = llvm.lshr %arg127, %1 : i32
  %14 = llvm.trunc %13 : i32 to i8
  %15 = llvm.lshr %arg127, %2 : i32
  %16 = llvm.trunc %15 : i32 to i8
  %17 = llvm.icmp "eq" %3, %10 : i8
  %18 = llvm.icmp "eq" %5, %12 : i8
  %19 = llvm.icmp "eq" %7, %14 : i8
  %20 = llvm.icmp "eq" %9, %16 : i8
  %21 = llvm.and %17, %18 : i1
  %22 = llvm.and %19, %21 : i1
  %23 = llvm.and %20, %22 : i1
  "llvm.return"(%23) : (i1) -> ()
}
]

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

def only_one_masked_after := [llvm|
{
^0(%arg0 : i64):
  %0 = llvm.mlir.constant(-9223372036854775808) : i64
  %1 = llvm.icmp "eq" %arg0, %0 : i64
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def test_implied_true_before := [llvm|
{
^0(%arg9 : i8):
  %0 = llvm.mlir.constant(10 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.mlir.constant(5 : i8) : i8
  %3 = llvm.mlir.constant(20 : i8) : i8
  %4 = llvm.icmp "slt" %arg9, %0 : i8
  %5 = llvm.icmp "slt" %arg9, %1 : i8
  %6 = "llvm.select"(%4, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %7 = "llvm.select"(%5, %6, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%7) : (i8) -> ()
}
]

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

def masked_icmps_mask_notallzeros_bmask_mixed_negated_7_logical_before := [llvm|
{
^0(%arg55 : 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.mlir.constant(true) : i1
  %5 = llvm.and %arg55, %0 : i32
  %6 = llvm.icmp "eq" %5, %1 : i32
  %7 = llvm.and %arg55, %2 : i32
  %8 = llvm.icmp "ne" %7, %3 : i32
  %9 = "llvm.select"(%6, %4, %8) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%9) : (i1) -> ()
}
]

def main4f_like_logical_after := [llvm|
{
^0(%arg115 : i32, %arg116 : i32, %arg117 : i32):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.and %arg115, %arg116 : i32
  %2 = llvm.icmp "eq" %1, %arg116 : i32
  %3 = llvm.and %arg115, %arg117 : i32
  %4 = llvm.icmp "eq" %3, %arg117 : i32
  %5 = "llvm.select"(%2, %4, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %6 = llvm.zext %5 : i1 to i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def udiv_shl_shl_nuw_nsw2_before := [llvm|
{
^0(%arg55 : i8, %arg56 : i8, %arg57 : i8):
  %0 = llvm.shl %arg55, %arg57 overflow<nsw,nuw> : i8
  %1 = llvm.shl %arg56, %arg57 overflow<nsw> : i8
  %2 = llvm.udiv %0, %1 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def not_after := [llvm|
{
^0(%arg7 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.udiv %arg7, %0 : i8
  %3 = llvm.xor %arg7, %1 : i8
  %4 = llvm.mul %2, %3 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

def llvm_const_lower_riscv_li44 : LLVMPeepholeRewriteRefine 64 [] :=
  {lhs := constLLVM44, rhs:= liRiscv44,
   correct := by admit /- proof elided -/

def liRiscv_38 := [LV| {
  ^entry ():
    %0 = "li"() {imm = -38 : !i64} : (!i64) -> (!i64)
    %1 = "builtin.unrealized_conversion_cast"(%0) : (!i64) -> (i64)
    llvm.return %1 : i64
  }]

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

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

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

def and_nosignbit_select_shl_before := [llvm|
{
^0(%arg44 : i32, %arg45 : i1):
  %0 = llvm.mlir.constant(2147418112 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.and %arg44, %0 : i32
  %3 = "llvm.select"(%arg45, %2, %arg44) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %4 = llvm.shl %3, %1 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def src_is_mask_p2_m1_after := [llvm|
{
^0(%arg90 : i8, %arg91 : i8):
  %0 = llvm.mlir.constant(2 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.mlir.constant(123 : i8) : i8
  %3 = llvm.shl %0, %arg91 : i8
  %4 = llvm.add %3, %1 : i8
  %5 = llvm.xor %arg90, %2 : i8
  %6 = llvm.icmp "ugt" %5, %4 : i8
  "llvm.return"(%6) : (i1) -> ()
}
]

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

RV64.rorw in RISCV.Instructions

def Vector.ofList {α : Type u} (l : List α) : List.Vector α l.length :=
⟨l, rfl⟩

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

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

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

def or_and_or_pat2_after := [llvm|
{
^0(%arg34 : i8, %arg35 : i8, %arg36 : i8, %arg37 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.udiv %0, %arg36 : i8
  %2 = llvm.or %arg37, %arg35 : i8
  %3 = llvm.and %2, %arg34 : i8
  %4 = llvm.or %1, %3 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

instance : DialectPrint Handshake where
  printOpName := reprStr
  printTy := reprStr
  printAttributes _ := ""
  dialectName := "handshake"
  printReturn _ := "return"

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

def shl_and_and_fail_after := [llvm|
{
^0(%arg170 : i8, %arg171 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.mlir.constant(5 : i8) : i8
  %2 = llvm.mlir.constant(64 : i8) : i8
  %3 = llvm.shl %arg170, %0 : i8
  %4 = llvm.shl %arg171, %1 : i8
  %5 = llvm.and %4, %2 : i8
  %6 = llvm.and %3, %5 : i8
  "llvm.return"(%6) : (i8) -> ()
}
]

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

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

noncomputable def TV_sub_lhs_add_const : PeepholeRewrite (ModArith q) [.modLike] .modLike :=
{
  lhs := test_sub_lhs_add_const_LHS,
  rhs := test_sub_lhs_add_const_RHS,
  correct := by admit /- proof elided -/

def fold_icmp_shl_nuw_c2_precondition3_before := [llvm|
{
^0(%arg0 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.shl %0, %arg0 overflow<nuw> : i32
  %2 = llvm.icmp "ult" %1, %0 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

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

def fold_add_sdiv_srem_before := [llvm|
{
^0(%arg9 : i32):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.mlir.constant(4 : i32) : i32
  %2 = llvm.sdiv %arg9, %0 : i32
  %3 = llvm.shl %2, %1 : i32
  %4 = llvm.srem %arg9, %0 : i32
  %5 = llvm.add %3, %4 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

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

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

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

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

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

def select_constants_and_icmp_eq0_zero_tval_after := [llvm|
{
^0(%arg34 : i1, %arg35 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = "llvm.select"(%arg34, %0, %arg35) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%1) : (i1) -> ()
}
]

def src_x_and_nmask_slt_after := [llvm|
{
^0(%arg19 : i8, %arg20 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.shl %0, %arg20 overflow<nsw> : i8
  %2 = llvm.icmp "sgt" %1, %arg19 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def xor_lshr_multiuse_before := [llvm|
{
^0(%arg596 : i8, %arg597 : i8, %arg598 : i8, %arg599 : i8):
  %0 = llvm.lshr %arg596, %arg599 : i8
  %1 = llvm.lshr %arg597, %arg599 : i8
  %2 = llvm.xor %0, %arg598 : i8
  %3 = llvm.xor %2, %1 : i8
  %4 = llvm.sdiv %2, %3 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

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

BitVec.xor in Init.Data.BitVec.Basic

def add_or_sub_comb_i32_commuted1_nuw_after := [llvm|
{
^0(%arg16 : i32):
  "llvm.return"(%arg16) : (i32) -> ()
}
]
</all_available_defs>

<all_available_lemmas>
decide_eq_true_iff in Init.PropLemmas
iff_true in Init.SimpLemmas
inf_of_le_left in Mathlib.Order.Lattice
le_refl in Mathlib.Order.Defs.PartialOrder
left_eq_inf in Mathlib.Order.Lattice
not_iff in Mathlib.Logic.Basic
not_le in Mathlib.Order.Defs.LinearOrder
not_lt in Mathlib.Order.Defs.LinearOrder
decide_eq_decide in Init.PropLemmas

theorem scanOr_eq_decide (s : BitStream) (n : Nat) :
    s.scanOr n = decide (∃ (i : Nat), i ≤ n ∧ s i = true)

theorem scanOr_true_iff (s : BitStream) (n : Nat)
    : s.scanOr n = true ↔ ∃ (i : Nat), (i ≤ n) ∧ s i = true

theorem scanOr_false_iff (s : BitStream) (n : Nat) : s.scanOr n = false ↔ ∀ (i : Nat), (hi : i ≤ n) → s i = false

@[simp]
theorem scanOr_succ (s : BitStream) : scanOr s (n+1) = ((s.scanOr n) || s (n + 1))

theorem scanAnd_eq_decide (s : BitStream) (n : Nat) :
    s.scanAnd n = decide (∀ (i : Nat), i ≤ n → s i = true)

theorem scanAnd_true_iff (s : BitStream) (n : Nat) :
    s.scanAnd n = true ↔ ∀ (i : Nat), (hi : i ≤ n) → s i = true

@[simp] theorem scanAnd_succ (s : BitStream) : scanAnd s (n+1) = ((s.scanAnd n) && s (n + 1))

theorem e_1128 :
    7 * (z ^^^ t) + 1 *  ~~~(z ^^^ t) - 7 *  ~~~z - 3 *  ~~~(z &&& t) + 11 * t + 9 *  ~~~(z ||| t) - 8 *  ~~~(z |||  ~~~t) - 4 * (z &&&  ~~~t) = 12 * (z &&& t)

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

@[simp] theorem pure_le (e : EffectKind) : pure ≤ e

theorem zext_nneg_sext_ule_op0_wide_thm (e : IntW 8) (e_1 : IntW 9) :
  icmp IntPred.ule (zext 32 e_1 { «nneg» := true }) (sext 32 e) ⊑ icmp IntPred.ule e_1 (sext 9 e)

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

theorem lshrult_02_13_exact_proof : lshrult_02_13_exact_before ⊑ lshrult_02_13_exact_after

theorem main14_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (0#16 ≤ₛ truncate 16 x) &&& ofBool (0#8 ≤ₛ truncate 8 x) = 1#1 →
    ¬ofBool (x &&& 32896#32 == 0#32) = 1#1 → 2#32 = 1#32

theorem t0_sub_of_trueval_thm (e e_1 : IntW 8) (e_2 : IntW 1) :
  sub (select e_2 e_1 e) e_1 ⊑ select e_2 (const? 8 0) (sub e e_1)

theorem slt_swap_and_max_logical_proof : slt_swap_and_max_logical_before ⊑ slt_swap_and_max_logical_after

theorem test4_thm.extracted_1._1 : ∀ (x : BitVec 49), (x &&& BitVec.ofInt 49 (-2)) + 1#49 = x ||

theorem ashrsgt_02_04_exact_thm (e : IntW 4) :
  icmp IntPred.sgt (ashr e (const? 4 2) { «exact» := true }) (const? 4 4) ⊑ const? 1 0

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

theorem srem_common_dividend_defined_cond_proof : srem_common_dividend_defined_cond_before ⊑ srem_common_dividend_defined_cond_after

theorem trunc_shl_nsw_31_i32_i64_thm (e : IntW 64) :
  trunc 32 (shl e (const? 64 31) { «nsw» := true, «nuw» := false }) ⊑ shl (trunc 32 e) (const? 32 31)

theorem foo1_or_commuted_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 32),
  ¬(x_1 ≥ ↑32 ∨ x ≥ ↑32) →
    ¬(True ∧ 1#32 <<< x_1 >>> x_1 ≠ 1#32 ∨
          x_1 ≥ ↑32 ∨
            True ∧ 1#32 <<< x >>> x ≠ 1#32 ∨
              x ≥ ↑32 ∨ True ∧ 1#32 <<< x_1 >>> x_1 ≠ 1#32 ∨ x_1 ≥ ↑32 ∨ True ∧ 1#32 <<< x >>> x ≠ 1#32 ∨ x ≥ ↑32) →
      ofBool (x_2 * x_2 &&& 1#32 <<< x_1 != 0#32) &&& ofBool (1#32 <<< x &&& x_2 * x_2 != 0#32) =
        ofBool (x_2 * x_2 &&& (1#32 <<< x_1 ||| 1#32 <<< x) == 1#32 <<< x_1 ||| 1#32 <<< x)

@[simp] theorem bv_isRefinedBy_iff (x y : BitVec w) : x ⊑ y ↔ x = y

theorem zext_sext_ugt_known_nonneg_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (signExtend 32 x <ᵤ zeroExtend 32 (x_1 &&& 127#8)) = ofBool (x <ᵤ x_1 &&& 127#8)

theorem trunc_shl_ashr_infloop_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬(3#64 ≥ ↑64 ∨ 2#64 ≥ ↑64) →
    ¬1#64 ≥ ↑64 → truncate 32 (x.sshiftRight' 3#64 <<< 2#64) = truncate 32 (x >>> 1#64) &&& BitVec.ofInt 32 (-4)

theorem udiv_lshr_mul_nuw_proof : udiv_lshr_mul_nuw_before ⊑ udiv_lshr_mul_nuw_after

theorem ult_rem_zero_nsw_thm (e : IntW 8) :
  icmp IntPred.ult (mul e (const? 8 7) { «nsw» := true, «nuw» := true }) (const? 8 21) ⊑
    icmp IntPred.ult e (const? 8 3)

theorem icmp_sgt6_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ (x <<< 1#8).sshiftRight' 1#8 ≠ x ∨ 1#8 ≥ ↑8) → ofBool (16#8 <ₛ x <<< 1#8) = ofBool (8#8 <ₛ x)

theorem ripple_nsw3_thm (e e_1 : IntW 16) :
  add (LLVM.and e_1 (const? 16 (-21845))) (LLVM.and e (const? 16 21843)) ⊑
    add (LLVM.and e_1 (const? 16 (-21845))) (LLVM.and e (const? 16 21843)) { «nsw» := true, «nuw» := true }

theorem neg_thm (e : IntW 8) :
  LLVM.xor (sub (const? 8 0) e) (LLVM.udiv e (const? 8 42)) ⊑
    LLVM.xor (LLVM.udiv e (const? 8 42)) (sub (const? 8 0) e)

theorem select_ashr_thm.extracted_1._3 : ∀ (x x_1 : BitVec 128) (x_2 : BitVec 1), ¬x_2 = 1#1 → 0#128 ≥ ↑128 → False

theorem n2_thm (e : IntW 8) :
  LLVM.sdiv e (const? 8 (-128)) ⊑ zext 8 (icmp IntPred.eq e (const? 8 (-128)))

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

theorem p0_proof : p0_before ⊑ p0_after

theorem or_and1_commuted_thm.extracted_1._6 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 &&& (x_1 ^^^ 1#1) = 1#1 → x_1 = 1#1 → x_1 = 1#1

theorem test10_proof : test10_before ⊑ test10_after

theorem test_add_nsw__all_are_safe_proof : test_add_nsw__all_are_safe_before ⊑ test_add_nsw__all_are_safe_after

theorem test_lshr__exact_is_unsafe_thm.extracted_1._2 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ofBool (x_1 &&& 63#32 == 0#32) = 1#1 →
    ¬(2#32 ≥ ↑32 ∨ True ∧ (x_1 >>> 2#32 &&& 15#32).msb = true ∨ zeroExtend 64 (x_1 >>> 2#32 &&& 15#32) ≥ ↑64) →
      x = x.sshiftRight' (zeroExtend 64 (x_1 >>> 2#32 &&& 15#32))

theorem fold_mask_cmps_to_false_logical_proof : fold_mask_cmps_to_false_logical_before ⊑ fold_mask_cmps_to_false_logical_after

theorem or_xor_tree_1111_thm (e e_1 e_2 : IntW 32) :
  LLVM.or (LLVM.xor (mul e_2 (const? 32 42)) (LLVM.xor (mul e_1 (const? 32 42)) (mul e (const? 32 42))))
      (LLVM.xor (mul e (const? 32 42)) (mul e_2 (const? 32 42))) ⊑
    LLVM.or (LLVM.xor (mul e (const? 32 42)) (mul e_2 (const? 32 42))) (mul e_1 (const? 32 42))

theorem lshrult_03_06_proof : lshrult_03_06_before ⊑ lshrult_03_06_after

theorem rem_euclid_i128_thm (e : IntW 128) :
  select (icmp IntPred.slt (LLVM.srem e (const? 128 8)) (const? 128 0))
      (add (LLVM.srem e (const? 128 8)) (const? 128 8)) (LLVM.srem e (const? 128 8)) ⊑
    LLVM.and e (const? 128 7)

theorem not_and_and_or_not_or_or_commute4_proof : not_and_and_or_not_or_or_commute4_before ⊑ not_and_and_or_not_or_or_commute4_after

theorem n7_wrong_pred2_thm (e e_1 : IntW 8) :
  icmp IntPred.eq (sub e_1 e) e_1 ⊑ icmp IntPred.eq e (const? 8 0)

theorem foo_proof : foo_before ⊑ foo_after

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

theorem bitwise_and_logical_and_icmps_comm3_thm.extracted_1._5 : ∀ (x x_1 x_2 : BitVec 8),
  ¬x_1 ≥ ↑8 →
    ofBool (x_2 &&& 1#8 != 0#8) = 1#1 →
      ¬(True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8 ∨ True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8) →
        ¬ofBool (x_2 &&& (1#8 <<< x_1 ||| 1#8) == 1#8 <<< x_1 ||| 1#8) = 1#1 →
          ofBool (x_2 &&& 1#8 <<< x_1 != 0#8) &&& ofBool (x == 42#8) = 0#1

theorem test_add__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 positive_biggerlshr_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬(6#8 ≥ ↑8 ∨ 3#8 ≥ ↑8) → ¬3#8 ≥ ↑8 → x >>> 6#8 <<< 3#8 = x >>> 3#8 &&& 24#8

theorem ult_rem_zero_thm (e : IntW 8) :
  icmp IntPred.ult (mul e (const? 8 7) { «nsw» := false, «nuw» := true }) (const? 8 21) ⊑
    icmp IntPred.ult e (const? 8 3)

theorem test_sub_4_Y_ne_4_proof : test_sub_4_Y_ne_4_before ⊑ test_sub_4_Y_ne_4_after

theorem addsub_combine_constants_proof : addsub_combine_constants_before ⊑ addsub_combine_constants_after

theorem trunc_lshr_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬2#8 ≥ ↑8 → ¬2#6 ≥ ↑6 → truncate 6 (x >>> 2#8) &&& 14#6 = truncate 6 x >>> 2#6 &&& 14#6

theorem c0_proof : c0_before ⊑ c0_after

theorem shl_add_proof : shl_add_before ⊑ shl_add_after

theorem e_606 :
     - 2 * x + 2 * (x |||  ~~~y) - 1 *  ~~~(x &&& y) - 6 *  ~~~(x &&&  ~~~y) + 5 * (x ||| y) - 2 *  ~~~y - 1 *  ~~~(x &&&  ~~~x) + 3 * (x ^^^ y) + 8 *  ~~~(x ||| y) - 4 * (x &&&  ~~~y) =  - 2 * (x &&& y)

theorem sub_from_constant_commute_proof : sub_from_constant_commute_before ⊑ sub_from_constant_commute_after

theorem lowmask_or_zext_commute_proof : lowmask_or_zext_commute_before ⊑ lowmask_or_zext_commute_after

theorem test4_proof : test4_before ⊑ test4_after

@[bv_automata_preprocess] theorem BitVec.mul_nat_eq_ofNat_mul (x : BitVec w) (n : Nat) :
  x * n = BitVec.ofNat w n * x

theorem sdiv_icmp6_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬(True ∧ x.smod (BitVec.ofInt 64 (-5)) ≠ 0 ∨
        (BitVec.ofInt 64 (-5) == 0 || 64 != 1 && x == intMin 64 && BitVec.ofInt 64 (-5) == -1) = true) →
    ofBool (x.sdiv (BitVec.ofInt 64 (-5)) == -1#64) = ofBool (x == 5#64)

theorem main5f_like_logical_thm.extracted_1._9 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (x_2 &&& x_1 != x_2) = 1#1 →
    ofBool (x_2 &&& x_1 == x_2) = 1#1 →
      ofBool (x_2 &&& x != x_2) = 1#1 → 0#32 = zeroExtend 32 (ofBool (x_2 &&& x == x_2))

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

theorem and_xor_common_op_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(x_1 = 0 ∨ x_1 = 0 ∨ x = 0) → x_1 = 0 ∨ x = 0 → False

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

theorem logical_or_logical_or_icmps_comm1_thm.extracted_1._5 : ∀ (x x_1 x_2 : BitVec 8),
  ¬x_1 ≥ ↑8 →
    ¬(ofBool (x_2 &&& 1#8 <<< x_1 == 0#8) = 1#1 ∨ ofBool (x == 42#8) = 1#1) →
      ¬(True ∧ 1#8 <<< x_1 >>> x_1 ≠ 1#8 ∨ x_1 ≥ ↑8) →
        ofBool (x_2 &&& 1#8 <<< x_1 == 0#8) = 1#1 → True → ofBool (x_2 &&& 1#8 == 0#8) = 1#1

theorem test6_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬32#128 ≥ ↑128 →
    ¬(32#64 ≥ ↑64 ∨ True ∧ zeroExtend 64 (truncate 32 (x >>> 32#64)) ≠ x >>> 32#64) →
      truncate 32 (zeroExtend 128 x >>> 32#128) = truncate 32 (x >>> 32#64)

theorem zext_proof : zext_before ⊑ zext_after

theorem scalar_i32_shl_and_signbit_ne_proof : scalar_i32_shl_and_signbit_ne_before ⊑ scalar_i32_shl_and_signbit_ne_after

theorem t6_no_extrause_thm (e e_1 : IntW 8) :
  icmp IntPred.uge (add e_1 e) e ⊑ icmp IntPred.ule e_1 (LLVM.xor e (const? 8 (-1)))

theorem ashrslt_01_07_exact_proof : ashrslt_01_07_exact_before ⊑ ashrslt_01_07_exact_after

theorem sge_swap_or_not_max_commute_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬ofBool (x_1 != 127#8) = 1#1 → ofBool (x ≤ₛ x_1) = 1#1

theorem uge_umin1_proof : uge_umin1_before ⊑ uge_umin1_after

theorem modulo32_proof : modulo32_before ⊑ modulo32_after

theorem bool2 (x y : Bool) (h : x = y) : y = x

theorem masked_and_notA_logical_proof : masked_and_notA_logical_before ⊑ masked_and_notA_logical_after

theorem main8_proof : main8_before ⊑ main8_after

theorem and_logic_and_logic_or_3_proof : and_logic_and_logic_or_3_before ⊑ and_logic_and_logic_or_3_after

theorem mul_setnzV_unkV_nuw_eq_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬(True ∧ (x_1 ||| 2#8).umulOverflow x = true) → ofBool ((x_1 ||| 2#8) * x == 0#8) = ofBool (x == 0#8)

theorem nomask_rhs_logical_proof : nomask_rhs_logical_before ⊑ nomask_rhs_logical_after

theorem scalar_i32_shl_and_negC_slt_proof : scalar_i32_shl_and_negC_slt_before ⊑ scalar_i32_shl_and_negC_slt_after

theorem PR2844_logical_proof : PR2844_logical_before ⊑ PR2844_logical_after

theorem e_1485 :
     - 2 *  ~~~(z &&&  ~~~t) + 2 *  ~~~(z &&& t) + 5 * z + 1 * (z |||  ~~~t) - 2 *  ~~~z + 3 *  ~~~(z ^^^ t) + 1 * (z ^^^ t) - 3 *  ~~~(z &&&  ~~~z) + 1 *  ~~~(z ||| t) + 12 *  ~~~(z |||  ~~~t) + 4 * (z &&& t) = 2 * t + 6 * (z ||| t)

theorem foo4_proof : foo4_before ⊑ foo4_after

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

theorem icmp_ne_and1_lshr_pow2_proof : icmp_ne_and1_lshr_pow2_before ⊑ icmp_ne_and1_lshr_pow2_after

theorem add_five (x : BitVec w) : (x + x) + (x + x) + x = x + x + x + x + x

theorem eq_21_comm_eq2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(16#32 ≥ ↑32 ∨ 16#32 ≥ ↑32 ∨ 8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32) → 8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32 → False
</all_available_lemmas>

<local_ctx>
import Blase.Fast.FiniteStateMachine

import Blase.Vars

import Blase.MultiWidth.Defs

import Blase.KInduction.KInduction

import Lean

namespace MultiWidth

def NatFSM.fsmUnaryIndexUle (a : NatFSM wcard tcard bcard ncard icard pcard v) :
    FSM (StateSpace wcard tcard bcard ncard icard pcard) :=
  composeUnaryAux (FSM.ls true) a.toFsm

def fsmUnaryUle (a : NatFSM wcard tcard bcard ncard icard pcard (.ofDep v))
    (b : NatFSM wcard tcard bcard ncard icard pcard (.ofDep w)) : FSM (StateSpace wcard tcard bcard ncard icard pcard) :=
 composeUnaryAux FSM.scanAnd (b.fsmUnaryIndexUle ||| ~~~ a.fsmUnaryIndexUle)

def fsmUnaryNeqUpto (a : NatFSM wcard tcard bcard ncard icard pcard (.ofDep v))
    (b : NatFSM wcard tcard bcard ncard icard pcard (.ofDep w)) : FSM (StateSpace wcard tcard bcard ncard icard pcard) :=
  composeUnaryAux FSM.scanOr (a.fsmUnaryIndexUle ^^^ b.fsmUnaryIndexUle)

def fsmUltUnary
    (a : NatFSM wcard tcard bcard ncard icard pcard (.ofDep v))
    (b : NatFSM wcard tcard bcard ncard icard pcard (.ofDep w)) : FSM (StateSpace wcard tcard bcard ncard icard pcard) :=
  composeBinaryAux' FSM.and (fsmUnaryUle a b) (fsmUnaryNeqUpto a b)
</local_ctx>

<target_theorem>
theorem eval_fsmUltUnary_eq_decide
    (a : NatFSM wcard tcard bcard ncard icard pcard (.ofDep v))
    (b : NatFSM wcard tcard bcard ncard icard pcard (.ofDep w))
    {wenv : WidthExpr.Env wcard}
    {fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream}
    (henv : HWidthEnv fsmEnv wenv)
    (ha : HNatFSMToBitstream a) (hb : HNatFSMToBitstream b) :
    ((fsmUltUnary a b).eval fsmEnv) i =
   (decide (min i (v.toNat wenv) < min i (w.toNat wenv))) :=
</target_theorem>

