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
Int.xor in Mathlib.Data.Int.Bitwise
Nat.testBit in Init.Data.Nat.Bitwise.Basic
Empty in Init.Prelude
Empty.elim in Init.Core

syntax "min" : MLIR.Pretty.uniform_op

syntax "slt" : 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)

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
| mul (w : WidthExpr) (a b : Term) : Term
| udiv (w : WidthExpr) (a b : Term) : Term
| umod (w : WidthExpr) (a b : Term) : Term
| boolVar (v : Nat) : Term
| boolConst (b : Bool) : Term
| shiftl (w : WidthExpr) (a : Term) (k : Nat) : Term
| junk (s : String)  : Term 
deriving DecidableEq, Inhabited, Repr, Lean.ToExpr

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

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

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)

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

def eval (x : arity → BitStream) : BitStream :=
  fun n => (p.nextBit (p.carry x n) (fun i => x i n)).2

def nextBit : p.State → (arity → Bool) → p.State × Bool :=
  fun carry inputBits =>
    let input := Sum.elim carry inputBits
    let newState : p.State  := fun (a : p.α) => (p.nextStateCirc a).eval input
    let outBit : Bool       := (p.outputCirc).eval input
    (newState, outBit)

abbrev State : Type := p.α → Bool

def carry (x : arity → BitStream) : ℕ → p.State
  | 0 => p.initCarry
  | n+1 => (p.nextBit (carry x n) (fun i => x i n)).1

def Term.eval (t : Term) (vars : List BitStream) : BitStream :=
  match t with
  | var n       => vars.getD n default
  | zero        => BitStream.zero
  | one         => BitStream.one
  | negOne      => BitStream.negOne
  | ofNat n     => BitStream.ofNat n
  | and t₁ t₂   => (t₁.eval vars) &&& (t₂.eval vars)
  | or t₁ t₂    => (t₁.eval vars) ||| (t₂.eval vars)
  | xor t₁ t₂   => (t₁.eval vars) ^^^ (t₂.eval vars)
  | not t       => ~~~(t.eval vars)
  | add t₁ t₂   => (Term.eval t₁ vars) + (Term.eval t₂ vars)
  | sub t₁ t₂   => (Term.eval t₁ vars) - (Term.eval t₂ vars)
  | neg t       => -(Term.eval t vars)

| shiftL t n  => BitStream.shiftLeft (Term.eval t vars) n

def Predicate.eval (p : Predicate) (vars : List BitStream) : BitStream :=
  match p with
  | .width .eq n => BitStream.falseIffEq n
  | .width .neq n => BitStream.falseIffNeq n
  | .width .lt n => BitStream.falseIffLt n
  | .width .le n => BitStream.falseIffLe n
  | .width .gt n => BitStream.falseIffGt n
  | .width .ge n => BitStream.falseIffGe n
  | lor p q => Predicate.evalLor (p.eval vars) (q.eval vars)
  | land p q => Predicate.evalLand (p.eval vars) (q.eval vars)
  | binary .eq t₁ t₂ => Predicate.evalEq (t₁.eval vars) (t₂.eval vars)
   
  | binary .neq t1 t2 => Predicate.evalNeq (t1.eval vars) (t2.eval vars)
  | binary .ult t₁ t₂ => Predicate.evalUlt (t₁.eval vars) (t₂.eval vars)
  | binary .ule t₁ t₂ =>
     Predicate.evalLor
       (Predicate.evalEq (t₁.eval vars) (t₂.eval vars))
       (Predicate.evalUlt (t₁.eval vars) (t₂.eval vars))
  | binary .slt t₁ t₂ => Predicate.evalSlt (t₁.eval vars) (t₂.eval vars)
  | binary .sle t₁ t₂ => Predicate.evalLor
       (Predicate.evalEq (t₁.eval vars) (t₂.eval vars))
       (Predicate.evalSlt (t₁.eval vars) (t₂.eval vars))

def Predicate.evalUlt (t₁ t₂ : BitStream) : BitStream := (~~~ (t₁.borrow t₂)).concat true

def borrow (x y : BitStream) : BitStream :=
  fun n => (subAux x y n).2

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

def Predicate.evalSlt (t₁ t₂ : BitStream) : BitStream :=
    (((Predicate.evalUlt t₁ t₂)) ^^^ (Predicate.evalMsbEq t₁ t₂))

def Predicate.evalMsbEq (t₁ t₂ : BitStream) : BitStream :=
  (t₁ ^^^ t₂).concat false

def Predicate.evalLand (t₁ t₂ : BitStream) : BitStream := (t₁ ||| t₂)

def Predicate.evalNeq (t₁ t₂ : BitStream) : BitStream := (t₁.nxor t₂).concat true |>.scanAnd

def nxor (a b : BitStream) : BitStream := fun i => a i == b i

def scanAnd (s : BitStream) : BitStream := scanl true Bool.and 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 Predicate.evalLor (t₁ t₂ : BitStream) : BitStream := (t₁ &&& t₂)

def Predicate.evalEq (t₁ t₂ : BitStream) : BitStream := (t₁ ^^^ t₂).concat false |>.scanOr

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

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

abbrev falseIffLt (n : Nat) : BitStream := fun i => decide (i ≥ n)

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

abbrev falseIffEq (n : Nat) : BitStream := fun i => decide (i != n)

abbrev falseIffGt (n : Nat) : BitStream := fun i => decide (i ≤ n)

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

abbrev negOne : BitStream := fun _ => true

def shiftLeft (x : BitStream) (k : Nat) : BitStream :=
  fun i => if i < k then false else x (i - k)

def ofNat (x : Nat) : BitStream :=
  Nat.testBit x

abbrev one    : BitStream := (· == 0)

abbrev zero   : BitStream := fun _ => false

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

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

def eq_shift_in_zeros_after := [llvm|
{
^0(%arg84 : i32, %arg85 : i32):
  %0 = llvm.mlir.constant(256 : i32) : i32
  %1 = llvm.xor %arg84, %arg85 : i32
  %2 = llvm.icmp "ult" %1, %0 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

abbrev AttrVal (φ := 0) := AttrValue φ

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

def matchMulO: List (Σ Γ, LLVMPeepholeRewriteRefine 64 Γ) :=
  [⟨_, mulo_by_2_unsigned_signed⟩,
  ⟨_, mulo_by_2_unsigned⟩,
  ⟨_, mulo_by_2_signed⟩]

def trunc_lshr_sext_narrow_input_after := [llvm|
{
^0(%arg24 : i8):
  %0 = llvm.mlir.constant(6 : i8) : i8
  %1 = llvm.ashr %arg24, %0 : i8
  %2 = llvm.sext %1 : i8 to i16
  "llvm.return"(%2) : (i16) -> ()
}
]

def andn_or_cmp_2_after := [llvm|
{
^0(%arg170 : i16, %arg171 : i16, %arg172 : i16):
  %0 = llvm.mlir.constant(42 : i16) : i16
  %1 = llvm.icmp "slt" %arg170, %arg171 : i16
  %2 = llvm.icmp "ugt" %arg172, %0 : i16
  %3 = llvm.and %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

def OrZextOr_after := [llvm|
{
^0(%arg4 : i3):
  %0 = llvm.mlir.constant(11 : i5) : i5
  %1 = llvm.zext %arg4 : i3 to i5
  %2 = llvm.or %1, %0 : i5
  "llvm.return"(%2) : (i5) -> ()
}
]

Std.Tactic.BVDecide.BVBinOp.xor in Std.Tactic.BVDecide.Bitblast.BVExpr.Basic

let mut preconditions := none
        if !negativeExamples.isEmpty then
          preconditions ← withTraceNode `Generalize (fun _ => return m! "Attempted to generate weak precondition for {expr}") do
                      generatePreconditions expr positiveExamples negativeExamples numConjunctions

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

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

partial def existsForAll
    [H : HydrableExistsForall parsedExpr genPred genExpr]
    (origExpr : BoolExpr genPred) (existsVars: List Nat) (forAllVars: List Nat)  (numExamples: Nat := 1) :
    GeneralizerStateM parsedExpr genPred (List (Std.HashMap Nat BVExpr.PackedBitVec)) := do

def shift_xor_multiuse_cmp_before := [llvm|
{
^0(%arg84 : i32, %arg85 : i32, %arg86 : i32, %arg87 : 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 %arg84, %0 : i32
  %4 = llvm.icmp "ne" %1, %3 : i32
  %5 = llvm.or %arg85, %2 : i32
  %6 = "llvm.select"(%4, %arg85, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %7 = "llvm.select"(%4, %arg86, %arg87) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %8 = llvm.mul %6, %7 : i32
  "llvm.return"(%8) : (i32) -> ()
}
]

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

OrOp in Init.Prelude

def alive_AddSub_1202_tgt  (w : Nat)  :=
[llvm( w )| {
^bb0(%x : _, %C : _):
  %v1 = llvm.mlir.constant -1
  %v2 = llvm.xor %x, %v1
  %v3 = llvm.mlir.constant 1
  %v4 = llvm.sub %C, %v3
  %v5 = llvm.sub %v4, %x
  llvm.return %v5
}]

def test7_before := [llvm|
{
^0(%arg7 : i47):
  %0 = llvm.mlir.constant(39 : i47) : i47
  %1 = llvm.mlir.constant(255 : i47) : i47
  %2 = llvm.ashr %arg7, %0 : i47
  %3 = llvm.and %2, %1 : i47
  "llvm.return"(%3) : (i47) -> ()
}
]

def ashr_not_after := [llvm|
{
^0(%arg78 : i8):
  %0 = llvm.mlir.constant(5 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.ashr %arg78, %0 : i8
  %3 = llvm.xor %2, %1 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def trunc_ashr_before := [llvm|
{
^0(%arg98 : i32):
  %0 = llvm.mlir.constant(-2147483648 : i36) : i36
  %1 = llvm.mlir.constant(8 : i36) : i36
  %2 = llvm.zext %arg98 : i32 to i36
  %3 = llvm.or %2, %0 : i36
  %4 = llvm.ashr %3, %1 : i36
  %5 = llvm.trunc %4 : i36 to i32
  "llvm.return"(%5) : (i32) -> ()
}
]

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

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

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

def icmp_ne_and_z_and_onefail_after := [llvm|
{
^0(%arg18 : i8):
  %0 = llvm.mlir.constant(2 : i8) : i8
  %1 = llvm.icmp "ugt" %arg18, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

abbrev EnumerativeSearchCache :=  Std.HashMap BVExprWrapper BVExpr.PackedBitVec

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

Except in Init.Prelude

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

def ashr_bitwidth_mask_before := [llvm|
{
^0(%arg127 : i8, %arg128 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.ashr %arg127, %0 : i8
  %2 = llvm.and %1, %arg128 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def Var.tryDelete? [TyDenote Ty] {Γ Γ' : Ctxt Ty} {delv : DeleteRange Γ}
  (DEL : Deleted Γ delv Γ') (vs : HVector Γ.Var β) :
    Option { v' : HVector Γ'.Var β // vs = v'.map DEL.toHom } := do
  match vs with
  | .nil => some ⟨.nil, rfl⟩
  | v ::ₕ vs => do
      let ⟨v, hv⟩ ← tryDeleteOne? DEL v
      let ⟨vs, hvs⟩ ← tryDelete? DEL vs
      return ⟨v ::ₕ vs, by admit /- proof elided -/
      ⟩

Lean.Parser.Term.matchAltExpr in Lean.Parser.Term

def p_constmask_after := [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.or disjoint %2, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

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

def elabDefSignatureFor (dialect : Term) (alts : TSyntax ``matchAltsSig) : CommandElabM Unit := do
  let msg := (return m!"{exceptEmoji ·} Defining operation signature for {dialect} dialect")
  withTraceNode `LeanMLIR.Elab msg (collapsed := false) <| do
    let alts := getMatchAlts alts
    let alts ← do
      alts.mapM fun view => do
        trace[LeanMLIR.Elab] m!"Parsing match alternative with\n\
          \tpatterns: {view.patterns}\n\
          \tsignature: {view.rhs}"
        let rhs ← parseSignature view.rhs
        return { view with rhs }

def or_ranges_adjacent_before := [llvm|
{
^0(%arg260 : i8):
  %0 = llvm.mlir.constant(5 : i8) : i8
  %1 = llvm.mlir.constant(10 : i8) : i8
  %2 = llvm.mlir.constant(11 : i8) : i8
  %3 = llvm.mlir.constant(20 : i8) : i8
  %4 = llvm.icmp "uge" %arg260, %0 : i8
  %5 = llvm.icmp "ule" %arg260, %1 : i8
  %6 = llvm.and %4, %5 : i1
  %7 = llvm.icmp "uge" %arg260, %2 : i8
  %8 = llvm.icmp "ule" %arg260, %3 : i8
  %9 = llvm.and %7, %8 : i1
  %10 = llvm.or %6, %9 : i1
  "llvm.return"(%10) : (i1) -> ()
}
]

def fsmCarry'' (initialCarryVal : Bool): FSM Bool :=
  let outputCirc :=
    let carry := Circuit.var true (Sum.inl ())
    let a := Circuit.var true (Sum.inr true)
    let b := Circuit.var true (Sum.inr false)
    
    ((a &&& b) ||| (a &&& carry) ||| (b &&& carry))
  { α := Unit,
    
    
    initCarry := fun () => initialCarryVal, 
    outputCirc := Circuit.var true (Sum.inl ()) ,
    nextStateCirc := fun () => outputCirc
  }

def test23_before := [llvm|
{
^0(%arg185 : i32, %arg186 : i32):
  %0 = llvm.xor %arg186, %arg185 : i32
  %1 = llvm.icmp "eq" %0, %arg185 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def add : FSM Bool :=
  { α := Unit,
    initCarry := λ _ => false,
    nextStateCirc := fun () =>
      Circuit.var true (inr true) &&& Circuit.var true (inr false) |||
      Circuit.var true (inr true) &&& Circuit.var true (inl ()) |||
      Circuit.var true (inr false) &&& Circuit.var true (inl ()),
    outputCirc := Circuit.var true (inr true) ^^^
                  Circuit.var true (inr false) ^^^
                  Circuit.var true (inl ()),
  }

class DialectPrint (d : Dialect) where
   
  printOpName : d.Op → String
   
  printAttributes : d.Op → String

|
</all_available_defs>

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

@[simp] theorem and_eq : (x &&& y) i = (x i && y i)

@[simp]
theorem FSM.eval_and' (a b : FSM arity) : (a &&& b).eval env = a.eval env &&& b.eval env

theorem FSM.and_eq (a b : FSM arity) : (a &&& b) = composeBinaryAux' FSM.and a b

theorem mul_add_to_mul_8_proof : mul_add_to_mul_8_before ⊑ mul_add_to_mul_8_after

theorem wide_source_matching_signbits_proof : wide_source_matching_signbits_before ⊑ wide_source_matching_signbits_after

theorem set_bits_proof : set_bits_before ⊑ set_bits_after

theorem eq_10_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32) →
    ofBool (truncate 8 x_1 == truncate 8 x) &&& ofBool (truncate 8 (x_1 >>> 8#32) == truncate 8 (x >>> 8#32)) =
      ofBool (truncate 16 x_1 == truncate 16 x)

@[simp] theorem map'_cons : map' f g (cons x xs) = cons (g _ x) (map' f g xs)

theorem badimm4_thm.extracted_1._5 : ∀ (x : BitVec 16),
  ¬(7#8 ≥ ↑8 ∨ 8#16 ≥ ↑16) →
    ¬ofBool ((truncate 8 x).sshiftRight' 7#8 == truncate 8 (x >>> 8#16)) = 1#1 →
      ¬15#16 ≥ ↑16 →
        ¬ofBool (127#16 <ₛ x) = 1#1 →
          ¬ofBool (x <ₛ BitVec.ofInt 16 (-128)) = 1#1 → truncate 8 (x.sshiftRight' 15#16) ^^^ 126#8 = truncate 8 x

theorem t0_proof : t0_before ⊑ t0_after

lemma CNFA.ofFSM_spec (p : FSM arity) :
    (CNFA.ofFSM p).Sim (NFA'.ofFSM p)

theorem scalar_i32_lshr_and_negC_slt_thm (e e_1 : IntW 32) :
  icmp IntPred.slt (LLVM.and (lshr e_1 e) (const? 32 (-8))) (const? 32 0) ⊑
    icmp IntPred.slt (lshr e_1 e) (const? 32 0)

theorem ashr_ult_1_proof : ashr_ult_1_before ⊑ ashr_ult_1_after

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

theorem xor_i8_to_i64_shl_save_and_ne_thm (e : IntW 64) (e_1 : IntW 8) :
  select (icmp IntPred.ne (LLVM.and e_1 (const? 8 1)) (const? 8 0)) (LLVM.xor e (const? 64 (-9223372036854775808)))
      e ⊑
    LLVM.xor e (shl (zext 64 e_1) (const? 64 63))

theorem shift_xor_multiuse_cmp_and_thm.extracted_1._3 : ∀ (x x_1 x_2 x_3 : BitVec 32),
  ofBool (0#32 != x_3 &&& 4096#32) = 1#1 →
    ofBool (x_3 &&& 4096#32 == 0#32) = 1#1 →
      x_2 * x_1 * (x_2 &&& 2048#32) = (x_2 &&& 2048#32) * x * (x_2 &&& 2048#32)

theorem test_const_shr_and_1_ne_0_i1_negative_thm (e : IntW 1) :
  icmp IntPred.ne (LLVM.and (lshr (const? 1 1) e) (const? 1 1)) (const? 1 0) ⊑ const? 1 1

theorem icmp_select_var_select_thm.extracted_1._9 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1),
  x_2 = 1#1 → ¬(ofBool (x_1 == 0#8) = 1#1 ∧ x_2 = 1#1) → ofBool (x_1 == 0#8) = 1#1 → True → ofBool (x_1 == x) = 1#1

theorem select_icmp_slt_zero_smin_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬ofBool (x <ₛ 0#8) = 1#1 → x ^^^ BitVec.ofInt 8 (-128) = x ||

theorem test12_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬zeroExtend 128 x &&& 31#128 ≥ ↑128 →
    ¬(True ∧ (x &&& 31#32).msb = true ∨ zeroExtend 64 (x &&& 31#32) ≥ ↑64) →
      truncate 64 (zeroExtend 128 x_1 >>> (zeroExtend 128 x &&& 31#128)) =
        zeroExtend 64 x_1 >>> zeroExtend 64 (x &&& 31#32)

theorem positive_samevar_shlnuwnsw_lshrexact_proof : positive_samevar_shlnuwnsw_lshrexact_before ⊑ positive_samevar_shlnuwnsw_lshrexact_after

theorem not_mul_of_pow2_proof : not_mul_of_pow2_before ⊑ not_mul_of_pow2_after

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

@[simp] theorem Hom.castDomain_rfl {h : Δ = Δ} {f : Γ.Hom Δ} :
    (f.castCodomain h) = f

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

theorem select_icmp_eq_0_and_1_xor_1_thm.extracted_1._1 : ∀ (x : BitVec 32) (x_1 : BitVec 64),
  ofBool (x_1 &&& 1#64 == 0#64) = 1#1 → x = x ^^^ truncate 32 x_1 &&& 1#32

theorem t20_thm.extracted_1._1 : ∀ (x : BitVec 16) (x_1 : BitVec 8),
  ¬x ≥ ↑16 → x_1 - truncate 8 (BitVec.ofInt 16 (-42) <<< x) = x_1 + truncate 8 (42#16 <<< x)

theorem lshr_lshr_pow2_const_negative_nopow2_1_thm (e : IntW 16) :
  LLVM.and (lshr (lshr (const? 16 2047) e) (const? 16 6)) (const? 16 4) ⊑
    LLVM.and (lshr (const? 16 31) e) (const? 16 4)

theorem test_shl_nuw_nsw__all_are_safe_thm (e : IntW 64) (e_1 : IntW 32) :
  select (icmp IntPred.eq (LLVM.and e_1 (const? 32 15)) (const? 32 0)) e
      (ashr e (zext 64 (shl (LLVM.and e_1 (const? 32 15)) (const? 32 2) { «nsw» := true, «nuw» := true }))) ⊑
    ashr e (zext 64 (LLVM.and (shl e_1 (const? 32 2)) (const? 32 60)) { «nneg» := true })

theorem e_1098 :
    7 *  ~~~t + 5 *  ~~~(z &&& t) - 3 *  ~~~z + 11 * z - 3 *  ~~~(z ||| t) + 4 *  ~~~(z |||  ~~~t) - 23 * (z &&&  ~~~t) - 5 * (z &&& t) = 6 *  ~~~(z &&&  ~~~t)

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

theorem dialect_mul_f_eq_zero (a : R q n) : a * (f q n) = 0

theorem positive_with_extra_and_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬(ofBool (x + 128#32 <ᵤ 256#32) = 1#1 ∧ ofBool (-1#32 <ₛ x) = 1#1) → ofBool (x <ᵤ 128#32) = 1#1 → False

theorem or_xor_tree_0001_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 32),
  x_2 * 42#32 ^^^ x_1 * 42#32 ||

theorem unsigned_sign_bit_extract_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 → ofBool (x >>> 31#32 != 0#32) = ofBool (x <ₛ 0#32)

@[simp]
theorem FSM.eval_ite_eq_decide {α : Type}
    (cond t e : FSM α)
    (env : α → BitStream) (i : Nat) :
    (FSM.ite cond t e).eval env i =
    if (cond.eval env i) then t.eval env i else e.eval env i

theorem e_2368 :
    3 * (d ||| e) - 7 * (e &&&  ~~~(d &&&  ~~~f)) - 1 * ( ~~~(d &&& e) &&& (d ^^^ (e ^^^ f))) - 6 * ( ~~~d &&& (e ||| f)) + 11 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) + 2 * ((d &&& e) ^^^ (d ^^^ (e &&& f))) - 1 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) + 11 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 1 * (e ^^^  ~~~(d &&& ( ~~~e ||| f))) - 3 * (d &&& (e ^^^ f)) + 11 *  ~~~(d &&& ( ~~~e ||| f)) - 11 * (f |||  ~~~(d |||  ~~~e)) - 1 * ((e &&& f) ||| (d &&& (e ||| f))) - 7 * (f &&&  ~~~(d &&& e)) + 1 *  ~~~(d ^^^ (e &&& f)) + 4 * ((e &&&  ~~~f) ^^^ ( ~~~d ||| (e ^^^ f))) - 1 * (d ||| (e ^^^ f)) - 1 * ((d &&& e) |||  ~~~(e ^^^ f)) + 2 * ( ~~~d ||| (e ^^^ f)) + 11 * (e ^^^ ( ~~~d &&& (e ||| f))) - 7 * (f ^^^  ~~~(d &&& ( ~~~e ||| f))) - 7 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) + 2 * (f &&&  ~~~(d ^^^ e)) + 2 * (d &&& f) - 11 * (e ^^^ (d &&& ( ~~~e ||| f))) + 2 * (e &&&  ~~~(d &&& f)) + 3 * ((d &&& e) |||  ~~~(e ||| f)) - 5 *  ~~~(d &&& ( ~~~e &&& f)) + 1 * ((d &&& f) ^^^  ~~~(d ^^^ ( ~~~e &&& f))) - 3 * ((d &&&  ~~~e) ||| (e ^^^ f)) + 2 *  ~~~( ~~~d &&& ( ~~~e ||| f)) - 5 *  ~~~(e &&& f) + 5 *  ~~~( ~~~d ||| (e &&& f)) + 4 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) + 1 * (e ||| (d &&&  ~~~f)) - 11 * (f ^^^  ~~~(d ||| e)) - 2 * ((d &&& f) |||  ~~~(e ||| f)) - 1 * ( ~~~f |||  ~~~(d ^^^ e)) - 1 * (e &&& (d ||| f)) + 7 *  ~~~(d ||| ( ~~~e &&& f)) + 1 *  ~~~(d ||| (e &&& f)) - 5 * (d ^^^ (e ||| f)) + 5 * ( ~~~(d ^^^ e) &&&  ~~~(d ^^^ f)) - 1 * (e ^^^ (d |||  ~~~f)) - 5 * ( ~~~e ||| (d ^^^ f)) + 11 * (e ^^^ (d ||| ( ~~~e &&& f))) + 3 *  ~~~(d ^^^ (e ^^^ f)) - 2 *  ~~~( ~~~d ||| (e ^^^ f)) - 2 * (e ||| (d ^^^ f)) + 3 *  ~~~d - 6 * (d ^^^ e) + 7 * (e &&& f) + 2 * (e ^^^  ~~~(d &&& f)) + 5 *  ~~~(d ^^^ e) - 2 * (f ^^^  ~~~(d &&&  ~~~e)) + 5 * ((e &&&  ~~~f) |||  ~~~(d ||| ( ~~~e &&& f))) - 3 * (e |||  ~~~(d |||  ~~~f)) + 2 * (f &&& (d ^^^ e)) + 1 *  ~~~( ~~~d &&& (e ^^^ f)) - 2 * ( ~~~e &&& (d ^^^ f)) + 1 * (e ^^^ ( ~~~d ||| (e ^^^ f))) - 27 *  ~~~(d ||| (e ||| f)) + 17 *  ~~~(d ||| ( ~~~e ||| f)) + 28 *  ~~~( ~~~d ||| (e ||| f)) + 7 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 11 * ( ~~~d &&& ( ~~~e &&& f)) + 11 * ( ~~~d &&& (e &&& f)) + 37 * (d &&& ( ~~~e &&& f)) - 13 * (d &&& (e &&& f)) = 2 * (d |||  ~~~f)

theorem icmp_slt_0_and_icmp_sge_neg2_i64_proof : icmp_slt_0_and_icmp_sge_neg2_i64_before ⊑ icmp_slt_0_and_icmp_sge_neg2_i64_after

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

theorem t3_ult_sgt_neg1_thm.extracted_1._7 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 + 16#32 <ᵤ 144#32) = 1#1 →
    ¬ofBool (127#32 <ₛ x_1) = 1#1 → ofBool (x_1 <ₛ BitVec.ofInt 32 (-16)) = 1#1 → x_1 = x

theorem trunc_shl_15_i16_i64_thm.extracted_1._2 : ∀ (x : BitVec 64),
  ¬15#64 ≥ ↑64 → ¬15#16 ≥ ↑16 → truncate 16 (x <<< 15#64) = truncate 16 x <<< 15#16

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

theorem or_test1_proof : or_test1_before ⊑ or_test1_after

theorem substitute_constant_or_ne_uge_commute_logical_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ofBool (x ≤ᵤ x_1) = 1#1 → 1#1 = ofBool (x_1 != 42#8) ||

theorem expand_thm (e : IntW 32) :
  LLVM.and (LLVM.or (LLVM.and e (const? 32 1)) (const? 32 2)) (const? 32 1) ⊑ LLVM.and e (const? 32 1)

theorem PR42691_8_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x <ₛ 14#32) = 1#1 →
    ofBool (x != BitVec.ofInt 32 (-2147483648)) = ofBool (x + 2147483647#32 <ᵤ BitVec.ofInt 32 (-2147483635))

theorem test17_thm.extracted_1._1 : ∀ (x : BitVec 32), ¬x = 0 → 1#32 % x = zeroExtend 32 (ofBool (x != 1#32))

theorem icmp_equality_test_commute_select2_proof : icmp_equality_test_commute_select2_before ⊑ icmp_equality_test_commute_select2_after

theorem test19_commutative2_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(x ≥ ↑32 ∨ x_1 ≥ ↑32 ∨ x ≥ ↑32 ∨ 1#32 <<< x + (1#32 <<< x_1 &&& 1#32 <<< x) = 0) →
    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 →
      False

theorem t1_sub_of_falseval_proof : t1_sub_of_falseval_before ⊑ t1_sub_of_falseval_after

theorem t4_ugt_slt_65536_proof : t4_ugt_slt_65536_before ⊑ t4_ugt_slt_65536_after

theorem test56_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬5#32 ≥ ↑32 → 5#32 ≥ ↑32 ∨ True ∧ (signExtend 32 x >>> 5#32).msb = true → False

theorem test5_thm.extracted_1._1 : ∀ (x x_1 : BitVec 399),
  x_1 + (x &&& 18446742974197923840#399) &&& (274877906943#399 ^^^ -1#399) ||

theorem mul_of_pow2_commute_thm (e e_1 : IntW 32) :
  icmp IntPred.ugt (mul (LLVM.and e_1 (const? 32 255)) (LLVM.and e (const? 32 4))) (const? 32 1020) ⊑
    const? 1 0

theorem cmpeq_xor_cst1_commuted_proof : cmpeq_xor_cst1_commuted_before ⊑ cmpeq_xor_cst1_commuted_after

theorem lshrult_01_14_proof : lshrult_01_14_before ⊑ lshrult_01_14_after

theorem only_one_masked_proof : only_one_masked_before ⊑ only_one_masked_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)

def fsmSext (x wold wnew : FSM α) : FSM α :=
  (fsmMsb x wold) &&& wnew
</local_ctx>

<target_theorem>
theorem fsmSext_eval_eq
    (woldFsm : NatFSM wcard tcard bcard ncard icard pcard (.ofDep wold))
    (wnewFsm : NatFSM wcard tcard bcard ncard icard pcard (.ofDep wnew))
    {wenv : WidthExpr.Env wcard}
    {fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream}
    (hwnew : HNatFSMToBitstream wnewFsm)
    (hwold : HNatFSMToBitstream woldFsm)
    {tctx : Term.Ctx wcard tcard}
    (tenv : Term.Ctx.Env tctx wenv)
    (benv : Term.BoolEnv bcard)
    (nenv : Term.NatEnv ncard)
    (ienv : Term.IntEnv icard)
    (t : Term bcard ncard icard pcard tctx (.bv wold))
    (tFsm : TermFSM wcard tcard bcard ncard icard pcard (.ofDepTerm t))
    (htfsm : HTermFSMToBitStream tFsm)
    (htenv : HTermEnv fsmEnv tenv benv) :
    (fsmSext tFsm.toFsmZext woldFsm.toFsm  wnewFsm.toFsm).eval fsmEnv = fun i =>
      ((BitStream.ofBitVecZext ((Term.sext t wnew).toBV benv nenv ienv penv tenv))) i :=
</target_theorem>

