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 in Init.Core
Sum.elim in Init.Data.Sum.Basic
Sum.inl in Init.Core
Sum.inr in Init.Core
Nat in Init.Prelude
Repr in Init.Data.Repr
Inhabited in Init.Prelude
Lean.ToExpr in Lean.ToExpr
Nat.max in Init.Data.Nat.Basic
Nat.min in Init.Data.Nat.Basic
BitVec in Init.Prelude
BitVec.ofBool in Init.Data.BitVec.Basic
BitVec.ofNat in Init.Prelude

syntax "min" : 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 composeBinaryAux'
    (p : FSM Bool)
    (qtrue : FSM α)
    (qfalse : FSM α) :
    FSM α :=
  p.compose (α)
    (λ _ => α)
    (λ _ i => i)
    (λ b => match b with
      | true => qtrue
      | false => qfalse)

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 }

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

def latchImmediate (initVal : Bool) : FSM Bool where
  α := Unit
  initCarry := fun _ => initVal
  outputCirc :=
    let xval := Circuit.var true (inr false)
    let control := Circuit.var true (inr true)
    let state := Circuit.var true (inl ())
    Circuit.ite control xval state
  nextStateCirc := fun () =>
    let xval := Circuit.var true (inr false)
    let control := Circuit.var true (inr true)
    let state := Circuit.var true (inl ())
    Circuit.ite control xval state

def ite (cond t f : Circuit α) : Circuit α :=
  (cond &&& t) ||| (~~~ cond &&& f)

structure TermFSM (wcard tcard bcard ncard icard pcard : Nat) (t : Nondep.Term) where
  toFsmZext : FSM (StateSpace wcard tcard bcard ncard icard pcard)
  width : NatFSM wcard tcard bcard ncard icard pcard t.width

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

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

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 Term.width (t : Term) : WidthExpr :=
  match t with

| .ofNat w _n => w
  | .var _v w => w
  | .add w _a _b => w
  | .zext _a wnew => wnew
  | .setWidth _a wnew => wnew
  | .sext _a wnew => wnew
  | .bor w _a _b => w
  | .band w _a _b => w
  | .bxor w _a _b => w
  | .bnot w _a => w
  | .boolVar _v => WidthExpr.const 1 
  | .boolConst _b => WidthExpr.const 1
  | .shiftl w _a _k => w
  | .bvOfBool _b => WidthExpr.const 1
  | binWidthRel _k wa wb => WidthExpr.const 0
  | binRel _k w _a _b => w
  | or _p1 _p2 => WidthExpr.const 0
  | and _p1 _p2 => WidthExpr.const 0
  | pvar _v => WidthExpr.const 0
  | boolBinRel _k _a _b => WidthExpr.const 0

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

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

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

abbrev Term.Ctx (wcard : Nat) (tcard : Nat) : Type :=
  Fin tcard → WidthExpr wcard

def Term.BoolEnv (bcard : Nat) : Type := Fin bcard → Bool

def Term.IntEnv (icard : Nat) : Type := Fin icard → Nat

structure HTermFSMToBitStream {w : WidthExpr wcard}
  {tctx : Term.Ctx wcard tcard}
  {t : Term bcard ncard icard pcard tctx (.bv w)}
  (fsm : TermFSM wcard tcard bcard ncard icard pcard (.ofDepTerm t)) : 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),
      (henv : HTermEnv fsmEnv tenv benv) →
        fsm.toFsmZext.eval fsmEnv =
        BitStream.ofBitVecZext (t.toBV benv nenv ienv penv tenv)

def Predicate.Env (pcard : Nat) : Type :=
  Fin pcard → Prop

inductive TermKind (wcard : Nat) : Type
| bool
| bv (w : WidthExpr wcard)  : TermKind wcard
| prop
| nat
| int

structure HTermEnv {wcard tcard bcard : Nat}
    {wenv : Fin wcard → Nat} {tctx : Term.Ctx wcard tcard}
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream)
    (tenv : tctx.Env wenv)
    (benv : Term.BoolEnv bcard) : Prop
  extends HWidthEnv fsmEnv wenv where
    heq_term : ∀ (v : Fin tcard),
      fsmEnv (StateSpace.termVar v) = BitStream.ofBitVecZext (tenv v)
    heq_bool : ∀ (v : Fin bcard),
      fsmEnv (StateSpace.boolVar v) = BitStream.ofBool (benv v)

noncomputable def BitStream.ofBool (b : Bool) : BitStream := fun _i => b

abbrev Term.Ctx.Env
  (tctx : Term.Ctx wcard tcard)
  (wenv : WidthExpr.Env wcard) :=
  (v : Fin tcard) → BitVec ((tctx v).toNat wenv)

abbrev ofBitVecZext {w} (x : BitVec w) : BitStream :=
  fun i => x.getLsbD i

def Term.NatEnv (ncard : Nat) : Type := Fin ncard → Nat

def Term.toBV {wenv : WidthExpr.Env wcard}
    {tctx : Term.Ctx wcard tcard}
    (benv : Term.BoolEnv bcard)
    (nenv : Term.NatEnv ncard)
    (ienv : Term.IntEnv icard)
    (penv : Predicate.Env pcard)
    (tenv : tctx.Env wenv)
    (t : Term bcard ncard icard pcard tctx k) : k.denote wenv :=
match t with
| .ofNat w n => BitVec.ofNat (w.toNat wenv) n
| .boolConst b => b
| .var v => tenv.get v.1 v.2
| .add (w := w) a b =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a + b
| .zext a v => (a.toBV benv nenv ienv penv tenv).zeroExtend (v.toNat wenv)
| .setWidth a v => (a.toBV benv nenv ienv penv tenv).zeroExtend (v.toNat wenv)
| .sext a v => (a.toBV benv nenv ienv penv tenv).signExtend (v.toNat wenv)
| .bor a b (w := w) =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a ||| b
| .band (w := w) a b =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a &&& b
| .bxor (w := w) a b =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a ^^^ b
| .bnot (w := w) a =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    ~~~ a
| .boolVar v => benv v
| .shiftl (w := w) a k =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    a <<< k
| .bvOfBool b => BitVec.ofBool (b.toBV benv nenv ienv penv tenv)

| .binWidthRel rel wa wb =>
  match rel with
  | .eq => wa.toNat wenv = wb.toNat wenv
  | .le => wa.toNat wenv ≤ wb.toNat wenv
| .binRel rel _w a b =>
  match rel with
  | .eq => a.toBV benv nenv ienv penv tenv = b.toBV benv nenv ienv penv tenv
  | .ne => a.toBV benv nenv ienv penv tenv ≠ b.toBV benv nenv ienv penv tenv
  | .ult => (a.toBV benv nenv ienv penv tenv).ult (b.toBV benv nenv ienv penv tenv) = true
  | .ule => (a.toBV benv nenv ienv penv tenv).ule (b.toBV benv nenv ienv penv tenv) = true
  | .slt => (a.toBV benv nenv ienv penv tenv).slt (b.toBV benv nenv ienv penv tenv) = true
  | .sle => (a.toBV benv nenv ienv penv tenv).sle (b.toBV benv nenv ienv penv tenv) = true
| .and p1 p2 => p1.toBV benv nenv ienv penv tenv  ∧ p2.toBV benv nenv ienv penv tenv
| .or p1 p2 => p1.toBV benv nenv ienv penv tenv ∨ p2.toBV benv nenv ienv penv tenv
| .boolBinRel rel a b =>
  match rel with
  
  | .eq => (a.toBV benv nenv ienv penv tenv) = (b.toBV benv nenv ienv penv tenv)
| .pvar v => penv v

inductive Term {wcard tcard : Nat} (bcard : Nat) (ncard : Nat) (icard : Nat) (pcard : Nat)
  (tctx : Term.Ctx wcard tcard) : TermKind wcard → Type

| ofNat (w : WidthExpr wcard) (n : Nat) : Term bcard ncard icard pcard tctx (.bv w)
 
| var (v : Fin tcard) : Term bcard ncard icard pcard tctx (.bv (tctx v))
 
| add (a : Term bcard ncard icard pcard tctx (.bv w))
  (b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| shiftl (a : Term bcard ncard icard pcard tctx (.bv w)) (k : Nat) : Term bcard ncard icard pcard tctx (.bv w)
 
| bor (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| band (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| bxor (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| bnot (a : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| zext (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| setWidth (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| sext (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| bvOfBool (b : Term bcard ncard icard pcard tctx .bool) : Term bcard ncard icard pcard tctx (.bv (.const 1))

| boolConst (b : Bool) : Term bcard ncard icard pcard tctx .bool
| boolVar (v : Fin bcard) : Term bcard ncard icard pcard tctx .bool
| binWidthRel (k : WidthBinaryRelationKind) (wa wb : WidthExpr wcard) :
    Term bcard ncard icard pcard tctx .prop
| binRel
    (k : BinaryRelationKind)
    (w : WidthExpr wcard)
    (a : Term bcard ncard icard pcard tctx (.bv w))
    (b : Term bcard ncard icard pcard tctx (.bv w)) :
    Term bcard ncard icard pcard tctx .prop
| and (p1 p2 : Term bcard ncard icard pcard tctx (.prop)) : Term bcard ncard icard pcard tctx (.prop)
| or (p1 p2 : Term bcard ncard icard pcard tctx (.prop)) : Term bcard ncard icard pcard tctx (.prop)
| pvar (v : Fin pcard) : Term bcard ncard icard pcard tctx (.prop)

| boolBinRel
  (k : BoolBinaryRelationKind)
  (a b : Term bcard ncard icard pcard tctx .bool) :
  Term bcard ncard icard pcard tctx (.prop)

def Term.Ctx.Env.get {tcard : Nat}
  {wcard : Nat} {wenv : Fin wcard → Nat}
  {tctx : Term.Ctx wcard tcard}
  (tenv : tctx.Env wenv) (i : Nat) (hi : i < tcard) :
  BitVec ((tctx ⟨i, hi⟩).toNat wenv) :=
  tenv ⟨i, hi⟩

inductive BinaryRelationKind
| eq
| ne
| ule
| slt
| sle
| ult 
deriving DecidableEq, Repr, Inhabited, Lean.ToExpr

inductive WidthBinaryRelationKind
| eq
| le

deriving DecidableEq, Repr, Inhabited, Lean.ToExpr

abbrev ofBitVecSext {w} (x : BitVec w) : BitStream :=
  fun i => if i < w then x.getLsbD i else x.msb

inductive Term {wcard tcard : Nat} (bcard : Nat) (ncard : Nat) (icard : Nat) (pcard : Nat)
  (tctx : Term.Ctx wcard tcard) : TermKind wcard → Type

| ofNat (w : WidthExpr wcard) (n : Nat) : Term bcard ncard icard pcard tctx (.bv w)
 
| var (v : Fin tcard) : Term bcard ncard icard pcard tctx (.bv (tctx v))
 
| add (a : Term bcard ncard icard pcard tctx (.bv w))
  (b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| shiftl (a : Term bcard ncard icard pcard tctx (.bv w)) (k : Nat) : Term bcard ncard icard pcard tctx (.bv w)
 
| bor (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| band (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| bxor (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| bnot (a : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| zext (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| setWidth (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| sext (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| bvOfBool (b : Term bcard ncard icard pcard tctx .bool) : Term bcard ncard icard pcard tctx (.bv (.const 1))

| boolConst (b : Bool) : Term bcard ncard icard pcard tctx .bool
| boolVar (v : Fin bcard) : Term bcard ncard icard pcard tctx .bool
| binWidthRel (k : WidthBinaryRelationKind) (wa wb : WidthExpr wcard) :
    Term bcard ncard icard pcard tctx .prop
| binRel
    (k : BinaryRelationKind)
    (w : WidthExpr wcard)
    (a : Term bcard ncard icard pcard tctx (.bv w))
    (b : Term bcard ncard icard pcard tctx (.bv w)) :
    Term bcard ncard icard pcard tctx .prop
| and (p1 p2 : Term bcard ncard icard pcard tctx (.prop)) : Term bcard ncard icard pcard tctx (.prop)
| or (p1 p2 : Term bcard ncard icard pcard tctx (.prop)) : Term bcard ncard icard pcard tctx (.prop)
| pvar (v : Fin pcard) : Term bcard ncard icard pcard tctx (.prop)

| boolBinRel
  (k : BoolBinaryRelationKind)
  (a b : Term bcard ncard icard pcard tctx .bool) :
  Term bcard ncard icard pcard tctx (.prop)

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

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

def masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_6_logical_after := [llvm|
{
^0(%arg13 : i32):
  %0 = llvm.mlir.constant(15 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.and %arg13, %0 : i32
  %3 = llvm.icmp "ne" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def test3_before := [llvm|
{
^0(%arg2 : i32, %arg3 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(31 : i32) : i32
  %2 = llvm.sub %arg2, %arg3 overflow<nsw> : i32
  %3 = llvm.icmp "eq" %2, %0 : i32
  %4 = llvm.icmp "eq" %2, %1 : i32
  %5 = llvm.or %3, %4 : i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def llvm_zext_lower_riscv_1_to_64 : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 1)] :=
  {lhs:= zext_llvm_1_to_64, rhs:= zext_riscv_1_to_64}

def xor_or2_before := [llvm|
{
^0(%arg158 : i8):
  %0 = llvm.mlir.constant(33 : i8) : i8
  %1 = llvm.mlir.constant(7 : i8) : i8
  %2 = llvm.xor %arg158, %0 : i8
  %3 = llvm.or %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

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

def Tensor2d.transpose (t: Tensor2d α) : Tensor2d α where
  size0 := t.size1
  size1 := t.size0
  val := fun ix0 => fun ix1 => t.val ix1 ix0

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

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

def ashr_icmp2_after := [llvm|
{
^0(%arg26 : i64):
  %0 = llvm.mlir.constant(16) : i64
  %1 = llvm.icmp "slt" %arg26, %0 : i64
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def test11_before := [llvm|
{
^0(%arg197 : i8):
  %0 = llvm.mlir.constant(12 : i8) : i8
  %1 = llvm.mlir.constant(4 : i8) : i8
  %2 = llvm.or %arg197, %0 : i8
  %3 = llvm.xor %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

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

def trunc_shl_nsw_31_i32_i64_after := [llvm|
{
^0(%arg57 : i64):
  %0 = llvm.mlir.constant(31 : i32) : i32
  %1 = llvm.trunc %arg57 : i64 to i32
  %2 = llvm.shl %1, %0 : i32
  "llvm.return"(%2) : (i32) -> ()
}
]

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

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

def select_icmp_ne_0_and_4096_and_not_32_before := [llvm|
{
^0(%arg205 : i32, %arg206 : i32):
  %0 = llvm.mlir.constant(4096 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(-33 : i32) : i32
  %3 = llvm.and %arg205, %0 : i32
  %4 = llvm.icmp "ne" %1, %3 : i32
  %5 = llvm.and %arg206, %2 : i32
  %6 = "llvm.select"(%4, %arg206, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%6) : (i32) -> ()
}
]

example (op : Comb.Op) : DialectSignature.effectKind (d := DCxComb) (.comb op) = .pure := rfl

def changeFpExprWidth (bvExpr: FpExpr w) (target: Nat) : FpExpr target :=
  if h : w = target then
    (h ▸ bvExpr)
  else
    match bvExpr with
    | .var idx => (FpExpr.var idx : FpExpr target)
    | .bin lhs op rhs =>
      FpExpr.bin
        (changeFpExprWidth lhs target)
        op
        (changeFpExprWidth rhs target)
    | .const val =>
      
      
      
      FpExpr.const (val.setWidth _)

def p_constmask_before := [llvm|
{
^0(%arg49 : i32, %arg50 : i32):
  %0 = llvm.mlir.constant(65280 : i32) : i32
  %1 = llvm.mlir.constant(-65281 : i32) : i32
  %2 = llvm.and %arg49, %0 : i32
  %3 = llvm.and %arg50, %1 : i32
  %4 = llvm.add %2, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

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

unsafe def main : IO Unit := do
  initSearchPath (← findSysroot)
  Lean.withImportModules #[{ module := `Lean.Elab.Tactic.BVDecide}, {module := `Std.Tactic.BVDecide}]
      (opts := {}) (trustLevel := 0) fun env => do
    let ctxCore : Core.Context := { fileName := "SynthCadicalFile", fileMap := FileMap.ofString "" }
    let sCore : Core.State :=  { env }
    let ctxMeta : Meta.Context := {}
    let sMeta : Meta.State := {}
    let ctxTerm : Term.Context :=  { declName? := .some (Name.mkSimple s!"problem")}
    let sTerm : Term.State := {}
    let mut pix := 0
    for p in Bits.testPredicates do
      pix := pix + 1
      IO.println s!"testing predicate '{pix}'"
      let nIters : Nat := 2
      for i in [0:nIters] do
        IO.println s!"Iteration #{i + 1}/{nIters}"
        let fsm := predicateEvalEqFSM p
        
        let ((out, circuitStats), tElapsedCadical) ← timeElapsedMs do
          let ((out, circuitStats), _coreState, _metaState, _termState) ←
            fsm.toFSM.decideIfZerosVerified 5 |>.toIO ctxCore sCore ctxMeta sMeta ctxTerm sTerm
          return (out, circuitStats)
        let b := out.isSuccess
        
        IO.println s!" (cadical)  is all zeroes: '{b}' | stats: '{repr circuitStats}' | time: '{tElapsedCadical}' ms"
        IO.println "
  return ()

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

List.Mem in Init.Data.List.Basic

def logical_and_logical_and_icmps_after := [llvm|
{
^0(%arg208 : i8, %arg209 : i8, %arg210 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.icmp "eq" %arg209, %0 : i8
  %5 = llvm.and %arg208, %1 : i8
  %6 = llvm.shl %1, %arg210 overflow<nuw> : i8
  %7 = llvm.and %arg208, %6 : i8
  %8 = llvm.icmp "ne" %5, %2 : i8
  %9 = llvm.icmp "ne" %7, %2 : i8
  %10 = "llvm.select"(%4, %8, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %11 = "llvm.select"(%10, %9, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%11) : (i1) -> ()
}
]

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

def lshrugt_01_04_after := [llvm|
{
^0(%arg411 : i4):
  %0 = llvm.mlir.constant(-7 : i4) : i4
  %1 = llvm.icmp "ugt" %arg411, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def HVector.replicateToList {α : Type} {f : α → Type} {a : α} :
    {n : Nat} → HVector f (List.replicate n a) → List (f a)
  | 0, _ => []
  | n + 1, HVector.cons x xs => x :: replicateToList xs

def or_and_or_pat4_after := [llvm|
{
^0(%arg26 : i8, %arg27 : i8, %arg28 : i8, %arg29 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.udiv %0, %arg28 : i8
  %2 = llvm.or %arg29, %arg26 : i8
  %3 = llvm.and %2, %arg27 : i8
  %4 = llvm.or %1, %3 : i8
  "llvm.return"(%4) : (i8) -> ()
}
]

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

def mul_constant_eq_before := [llvm|
{
^0(%arg140 : i32, %arg141 : i32):
  %0 = llvm.mlir.constant(5 : i32) : i32
  %1 = llvm.mul %arg140, %0 : i32
  %2 = llvm.mul %arg141, %0 : i32
  %3 = llvm.icmp "eq" %1, %2 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def const_sub_const_sub_before := [llvm|
{
^0(%arg20 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.sub %0, %arg20 : i32
  %3 = llvm.sub %1, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def select_mul_icmp_before := [llvm|
{
^0(%arg284 : i32, %arg285 : i32, %arg286 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.icmp "eq" %arg284, %0 : i32
  %2 = llvm.mul %arg284, %arg286 : i32
  %3 = "llvm.select"(%1, %2, %arg285) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def CNFA.toNFA (m : CNFA n) : NFA (BitVec n) m.m.states where
  start := { s | s.val ∈ m.m.initials }
  accept := { s | s.val ∈ m.m.finals }
  step s₁ a := { s₂ | s₂.val ∈ m.m.tr s₁.val a }

def positive_sameconst_ashrexact_before := [llvm|
{
^0(%arg41 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.ashr exact %arg41, %0 : i8
  %2 = llvm.shl %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

def t0_before := [llvm|
{
^0(%arg12 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.shl %arg12, %0 : i8
  %2 = llvm.ashr %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

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

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

def commute_int_constant_to_rhs: List (Σ Γ, RISCVPeepholeRewrite  Γ) :=
  [⟨_, commute_int_constant_to_rhs_add⟩,
  ⟨_, commute_int_constant_to_rhs_mul⟩,
  ⟨_, commute_int_constant_to_rhs_and⟩,
  ⟨_, commute_int_constant_to_rhs_or⟩,
  ⟨_, commute_int_constant_to_rhs_xor⟩,
  ⟨_, commute_int_constant_to_rhs_mulhu⟩]

def shift_xor_multiuse_cmp_and_after := [llvm|
{
^0(%arg28 : i32, %arg29 : i32, %arg30 : i32, %arg31 : i32):
  %0 = llvm.mlir.constant(4096 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(2048 : i32) : i32
  %3 = llvm.and %arg28, %0 : i32
  %4 = llvm.icmp "eq" %3, %1 : i32
  %5 = llvm.and %arg29, %2 : i32
  %6 = "llvm.select"(%4, %5, %arg29) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %7 = "llvm.select"(%4, %arg31, %arg30) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %8 = llvm.mul %6, %7 : i32
  %9 = llvm.mul %8, %5 : i32
  "llvm.return"(%9) : (i32) -> ()
}
]

def canonicalize_icmp_ne_neg1 : LLVMPeepholeRewriteRefine 1 [Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant -1 : i64
      %1 = llvm.icmp.ne %c, %x : i64
      llvm.return %1 : i1
  }]
  rhs := [LV| {
    ^entry (%x: i64):
      %c = llvm.mlir.constant -1 : i64
      %1 = llvm.icmp.ne %x, %c : i64
      llvm.return %1 : i1
  }]

def narrow_zext_ashr_keep_trunc2_after := [llvm|
{
^0(%arg6 : i9, %arg7 : i9):
  %0 = llvm.mlir.constant(1 : i16) : i16
  %1 = llvm.zext %arg6 : i9 to i16
  %2 = llvm.zext %arg7 : i9 to i16
  %3 = llvm.add %1, %2 overflow<nsw,nuw> : i16
  %4 = llvm.lshr %3, %0 : i16
  %5 = llvm.trunc %4 : i16 to i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def visitSUB_AANegB : LLVMPeepholeRewriteRefine 64 [Ty.llvm (.bitvec 64), Ty.llvm (.bitvec 64)] where
  lhs := [LV| {
    ^entry (%a: i64, %b: i64):
      %0 = llvm.sub %a, %b : i64
      %1 = llvm.sub %a, %0 : i64
      llvm.return %1 : i64
  }]
  rhs := [LV| {
    ^entry (%a: i64, %b: i64):
      llvm.return %b : i64
  }]

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

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

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

Lean.mkApp6 in Lean.Expr
</all_available_defs>

<all_available_lemmas>
BitVec.msb_eq_getLsbD_last in Init.Data.BitVec.Lemmas

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

theorem positive_with_aggressive_icmp_logical_proof : positive_with_aggressive_icmp_logical_before ⊑ positive_with_aggressive_icmp_logical_after

theorem uge_umin1_proof : uge_umin1_before ⊑ uge_umin1_after

theorem bools2_logical_commute1_thm.extracted_1._4 : ∀ (x x_1 : BitVec 1),
  x_1 = 1#1 → ¬x ^^^ 1#1 = 1#1 → ¬x = 1#1 → False

theorem masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_0_logical_proof : masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_0_logical_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_0_logical_after

theorem n2_thm.extracted_1._6 : ∀ (x x_1 : BitVec 32) (x_2 : BitVec 1),
  x_2 = 1#1 → ¬x_2 ^^^ 1#1 = 1#1 → 1#1 ^^^ 1#1 = 0#1

private theorem falseAfterExcluding_false_iff (n i : Nat) {env : Fin 0 → BitStream} :
  (falseAfterExcluding n).eval env i = false ↔ i > n

theorem ashr_ult_14_proof : ashr_ult_14_before ⊑ ashr_ult_14_after

theorem select_constants_and_icmp_ne0_zero_tval_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1),
  x_1 = 1#1 → ¬x = 1#1 → ofBool (0#8 &&& 12#8 != 0#8) = 1#1 ^^^ 1#1

theorem not_or_neg_proof : not_or_neg_before ⊑ not_or_neg_after

theorem ult_toNat (x y : BitVec n) :
    (BitVec.ult (n := n) x y) = decide (x.toNat < y.toNat)

theorem lshr_pow2_sgt_proof : lshr_pow2_sgt_before ⊑ lshr_pow2_sgt_after

theorem ugt_umax1_proof : ugt_umax1_before ⊑ ugt_umax1_after

theorem or_and_not_not_proof : or_and_not_not_before ⊑ or_and_not_not_after

theorem trunc_equality_nsw_zext_thm (e : IntW 8) (e_1 : IntW 32) :
  icmp IntPred.ne (trunc 16 e_1 { «nsw» := true, «nuw» := false }) (zext 16 e) ⊑
    icmp IntPred.ne e_1 (zext 32 e)

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

theorem fold_select_trunc_nsw_false_proof : fold_select_trunc_nsw_false_before ⊑ fold_select_trunc_nsw_false_after

theorem eq_umax3_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬ofBool (x <ᵤ x_1 + 3#32) = 1#1 → ofBool (x_1 + 3#32 == x) = ofBool (x ≤ᵤ x_1 + 3#32)

theorem ashrsgt_01_15_exact_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬(True ∧ x >>> 1#4 <<< 1#4 ≠ x ∨ 1#4 ≥ ↑4) → ofBool (-1#4 <ₛ x.sshiftRight' 1#4) = ofBool (-1#4 <ₛ x)

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

theorem add_select_zext_proof : add_select_zext_before ⊑ add_select_zext_after

theorem test24_thm.extracted_1._1 : ∀ (x : BitVec 1), x = 1#1 → ofBool (14#32 != 0#32) = 1#1

theorem scalar_i64_lshr_and_negC_eq_proof : scalar_i64_lshr_and_negC_eq_before ⊑ scalar_i64_lshr_and_negC_eq_after

theorem positive_biggershl_shlnuwnsw_proof : positive_biggershl_shlnuwnsw_before ⊑ positive_biggershl_shlnuwnsw_after

theorem and_nosignbit_select_lshr_proof : and_nosignbit_select_lshr_before ⊑ and_nosignbit_select_lshr_after

theorem test9_thm (e : IntW 32) : trunc 8 (LLVM.and e (const? 32 42)) ⊑ LLVM.and (trunc 8 e) (const? 8 42)

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

theorem sgt_3_impliesF_eq_2_thm (e e_1 : IntW 8) :
  icmp IntPred.eq (select (icmp IntPred.sgt e_1 (const? 8 3)) (const? 8 2) e) e_1 ⊑
    select (icmp IntPred.slt e_1 (const? 8 4)) (icmp IntPred.eq e e_1) (const? 1 0)

theorem negative4_proof : negative4_before ⊑ negative4_after

theorem ashrslt_03_01_exact_proof : ashrslt_03_01_exact_before ⊑ ashrslt_03_01_exact_after

theorem bv_AndOrXor_1294_A__B__A__B___A__B :
    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.or e e_1) (LLVM.xor (LLVM.xor e (LLVM.const? w (-1))) e_1) ⊑ LLVM.and e e_1

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

theorem shrink_select_proof : shrink_select_before ⊑ shrink_select_after

theorem test5_thm.extracted_1._1 : ∀ (x : BitVec 32), x &&& x = x

theorem test31_proof : test31_before ⊑ test31_after

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

theorem add_umin_simplify_proof : add_umin_simplify_before ⊑ add_umin_simplify_after

theorem corec₂_eq_corec_of_corec₂ (streamInt: DCOp.ValueStream Int) :
    (corec₂ streamInt fun x => (x 0, x 0, x.tail)).1 ≈
    corec
      ((corec₂ streamInt fun (x : DCOp.ValueStream Int) =>
            (match x 0 with
              | some val => (x 0, some (), x.tail)
              | none => (none, none, x.tail))).1,
        (corec₂
            (corec₂ streamInt fun x =>
                (match x 0 with
                  | some val => (x 0, some (), x.tail)
                  | none => (none, none, x.tail))).2
            fun x => Id.run (x 0, x 0, tail x)).1)
      fun x =>
      match x.1 0, x.2 0 with

theorem commutativity_constant_14_vary_thm (e : IntW 4) :
  LLVM.xor e (LLVM.and (LLVM.xor e (const? 4 (-2))) (const? 4 1)) ⊑ LLVM.and e (const? 4 (-2))

theorem sextbool_add_commute_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 32),
  ¬42#32 = 0 → 42#32 = 0 ∨ True ∧ (x_1 % 42#32).saddOverflow (signExtend 32 x) = true → False

theorem slt_smin2_thm (e e_1 : IntW 32) :
  icmp IntPred.slt (select (icmp IntPred.slt e_1 e) e_1 e) e ⊑ icmp IntPred.slt e_1 e

theorem xor_of_icmps_to_ne_commute_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ofBool (x <ₛ 6#64) ^^^ ofBool (4#64 <ₛ x) = ofBool (x != 5#64)

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

theorem test14_thm.extracted_1._1 : ∀ (x x_1 : BitVec 1), ofBool (x_1 == x) = x_1 ^^^ x ^^^ 1#1

theorem add_nosignbit_select_shl_proof : add_nosignbit_select_shl_before ⊑ add_nosignbit_select_shl_after

theorem alive_Select_699 : forall (w : Nat) (A B : Bitvec 1)
, TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec 1)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (A) %v0;
  %v2 := op:const (B) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:icmp uge  w %v3;
  %v5 := triple:%v4 %v1 %v2;
  %v6 := op:select 1 %v5;
  %v7 := pair:%v6 %v2;
  %v8 := op:icmp uge  w %v7;
  %v9 := triple:%v8 %v6 %v2;
  %v10 := op:select 1 %v9
  dsl_ret %v10
  ]  ⊑
  TSSA.eval
  (Op := Op) (e := e)
  (i := TSSAIndex.STMT (UserType.base (BaseType.bitvec 1)))
  [dsl_bb|
  ^bb
  %v0 := unit: ;
  %v1 := op:const (A) %v0;
  %v2 := op:const (B) %v0;
  %v3 := pair:%v1 %v2;
  %v4 := op:icmp uge  1 %v3;
  %v5 := triple:%v4 %v1 %v2;
  %v6 := op:select 1 %v5;
  %v7 := pair:%v6 %v2;
  %v8 := op:icmp uge  1 %v7;
  %v9 := triple:%v4 %v1 %v2;
  %v10 := op:select 1 %v9
  dsl_ret %v10
  ]

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

theorem shl_shl_proof : shl_shl_before ⊑ shl_shl_after

theorem select_icmp_sgt_not_smin_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (-1#8 <ₛ x) = 1#1 → ofBool (x <ₛ 0#8) = 1#1 → x = x ^^^ BitVec.ofInt 8 (-127)

theorem fold_inverted_icmp_preds_reverse_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 <ₛ x) = 1#1 → ofBool (x ≤ₛ x_1) = 1#1 → False

theorem eq_umin1_proof : eq_umin1_before ⊑ eq_umin1_after

theorem shl_sub_i64_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬63#64 - x ≥ ↑64 →
    ¬(True ∧ BitVec.ofInt 64 (-9223372036854775808) >>> x <<< x ≠ BitVec.ofInt 64 (-9223372036854775808) ∨ x ≥ ↑64) →
      1#64 <<< (63#64 - x) = BitVec.ofInt 64 (-9223372036854775808) >>> x

theorem narrow_zext_ashr_keep_trunc2_thm.extracted_1._2 : ∀ (x x_1 : BitVec 9),
  ¬(True ∧ (signExtend 64 x_1).saddOverflow (signExtend 64 x) = true ∨ 1#64 ≥ ↑64) →
    ¬(True ∧ (zeroExtend 16 x_1).saddOverflow (zeroExtend 16 x) = true ∨
          True ∧ (zeroExtend 16 x_1).uaddOverflow (zeroExtend 16 x) = true ∨ 1#16 ≥ ↑16) →
      truncate 8 ((signExtend 64 x_1 + signExtend 64 x).sshiftRight' 1#64) =
        truncate 8 ((zeroExtend 16 x_1 + zeroExtend 16 x) >>> 1#16)

theorem select_icmp_x_and_8_eq_0_y_xor_8_proof : select_icmp_x_and_8_eq_0_y_xor_8_before ⊑ select_icmp_x_and_8_eq_0_y_xor_8_after

theorem ashr_sgt_overflow_thm (e : IntW 8) : icmp IntPred.sgt (ashr e (const? 8 1)) (const? 8 63) ⊑ const? 1 0

theorem test13_proof : test13_before ⊑ test13_after

theorem select_add_icmp_bad_thm.extracted_1._2 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 == 1#32) = 1#1 → x_2 + x_1 = x_1 + 1#32

theorem scalar_i8_shl_ult_const_3_proof : scalar_i8_shl_ult_const_3_before ⊑ scalar_i8_shl_ult_const_3_after

theorem slt_smin2_proof : slt_smin2_before ⊑ slt_smin2_after

theorem lshr_C1_add_A_C2_i32_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(x &&& 65535#32) + 5#32 ≥ ↑32 →
    ¬x &&& 65535#32 ≥ ↑32 → 6#32 <<< ((x &&& 65535#32) + 5#32) = 192#32 <<< (x &&& 65535#32)

theorem positive_with_mask_proof : positive_with_mask_before ⊑ positive_with_mask_after
</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 fsmMsb (x w : FSM α) : FSM α :=
  composeBinaryAux'
    (FSM.latchImmediate false)
    (qfalse := x)
    (qtrue := w)
</local_ctx>

<target_theorem>
theorem eval_fsmMsb_eq_BitStream_ofBitVecSext {wenv : WidthExpr.Env wcard}
    {fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream}
    {tctx : Term.Ctx wcard tcard}
    (tenv : Term.Ctx.Env tctx wenv)
    (benv : Term.BoolEnv bcard)
    (nenv : Term.NatEnv ncard)
    (ienv : Term.IntEnv icard)
    (w : WidthExpr wcard)
    (x : Term bcard ncard icard pcard tctx (.bv w))
    (xfsm : TermFSM wcard tcard bcard ncard icard pcard (.ofDepTerm x))
    (hxfsm : HTermFSMToBitStream xfsm)
    (wfsm : NatFSM wcard tcard bcard ncard icard pcard (.ofDep w))
    (hwfsm : HNatFSMToBitstream wfsm)
    (htenv : HTermEnv fsmEnv tenv benv) :
    (fsmMsb xfsm.toFsmZext wfsm.toFsm).eval fsmEnv =
      BitStream.ofBitVecSext (x.toBV benv nenv ienv penv tenv) :=
</target_theorem>

