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>
Bool in Init.Prelude
Nat in Init.Prelude
BitVec in Init.Prelude
BitVec.adcb in Init.Data.BitVec.Bitblast
Prod in Init.Prelude
Fin in Init.Prelude
BitVec.iunfoldr in Init.Data.BitVec.Folds
FinEnum in Mathlib.Data.FinEnum
FinEnum.card in Mathlib.Data.FinEnum
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
ZMod in Mathlib.Data.ZMod.Defs
BEq in Init.Prelude
DecidableEq in Init.Prelude
Hashable in Init.Prelude
Repr in Init.Data.Repr
Std.HashMap in Std.Data.HashMap.Basic
Std.HashSet in Std.Data.HashSet.Basic
Array in Init.Prelude
List.map in Init.Prelude
Array.foldl in Init.Data.Array.Basic
Std.HashMap.emptyWithCapacity in Std.Data.HashMap.Basic
Array.size in Init.Prelude
List in Init.Prelude
Vector in Init.Data.Vector.Basic
String in Init.Prelude
Unit in Init.Prelude
Field in Mathlib.Algebra.Field.Defs
Int.xor in Mathlib.Data.Int.Bitwise
Inhabited in Init.Prelude
Lean.ToExpr in Lean.ToExpr
Empty in Init.Prelude
Empty.elim in Init.Core
Sum.inr in Init.Core
Sum.inl in Init.Core
Sum in Init.Core
Sum.elim in Init.Data.Sum.Basic
id in Init.Prelude
Fin.castLE in Init.Data.Fin.Basic
cond in Init.Prelude
Nat.testBit in Init.Data.Nat.Bitwise.Basic
Fin.last in Init.Data.Fin.Basic
Array.emptyWithCapacity in Init.Prelude
Prod.mk in Init.Prelude
Array.empty in Init.Prelude
FinEnum.toList in Mathlib.Data.FinEnum
FinEnum.equiv in Mathlib.Data.FinEnum
NFA in Mathlib.Computability.NFA
NFA.accept in Mathlib.Computability.NFA
NFA.start in Mathlib.Computability.NFA
NFA.step in Mathlib.Computability.NFA
List.Vector in Mathlib.Data.Vector.Defs
Set in Mathlib.Data.Set.Defs
NFA.stepSet in Mathlib.Computability.NFA
Subsingleton in Init.Core
reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
BitVec.ofNat in Init.Prelude
BitVec.zero in Init.Data.BitVec.Basic
Language in Mathlib.Computability.Language
BitVec.cons in Init.Data.BitVec.Basic
List.Vector.ofFn in Mathlib.Data.Vector.Defs
List.Vector.replicate in Mathlib.Data.Vector.Defs
List.finRange in Init.Data.List.FinRange
List.reverseRecOn in Mathlib.Data.List.Induction
SetRel in Mathlib.Data.Rel
Array.back? in Init.Data.Array.Basic
Array.isEmpty in Init.Data.Array.Basic
List.next in Mathlib.Data.List.Cycle
L in Archive.Hairer
Fin.mk in Init.Prelude
Fin.cast in Init.Data.Fin.Basic
Fin.castLT in Init.Data.Fin.Basic
Fin.subNat in Init.Data.Fin.Basic
List.Vector.get in Mathlib.Data.Vector.Defs
List.Vector.nil in Mathlib.Data.Vector.Defs
Finset in Mathlib.Data.Finset.Defs
Finset.range in Mathlib.Data.Finset.Range
DFA in Mathlib.Computability.DFA
NFA.toDFA in Mathlib.Computability.NFA
List.range in Init.Data.List.Basic
Vector.ofFn in Init.Data.Vector.Basic

syntax "max" : MLIR.Pretty.uniform_op

syntax "slt" : MLIR.Pretty.uniform_op

syntax "xor" : 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 carry (initCarry : Bool) (x y : BitStream) : BitStream :=
  fun n => (addAux' initCarry x y n).2

def BitStream : Type := Nat → Bool

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

def BitVec.ofFn {w : Nat} (f : Fin w → Bool) : BitVec w :=
  BitVec.iunfoldr (fun i _ => ((), f i)) () |>.2

noncomputable def f : (ZMod q)[X] := X^(2^n) + 1

def worklistRun (final : S → Bool) (inits : Array S)
    (hinits : inits.toList.Nodup) (f : S → Array (BitVec n × S)) : CNFA n :=
  ⟨worklistRun' _ S final inits hinits f, worklistRun'_wf (BitVec n) S⟩

def worklistRun' (final : S → Bool) (inits : Array S) (hinits : inits.toList.Nodup) (f : S → Array (A × S)) : RawCNFA A :=
  let st0 := worklist.initState _ _ inits hinits final
  go st0
where go (st0 : worklist.St A S) : RawCNFA A :=
  if hemp : st0.worklist.isEmpty then st0.m else
  let sa? := st0.worklist.back?
  match heq : sa? with
  | some sa =>
    let wl := st0.worklist.pop
    let st1 := { st0 with worklist := wl,
                          worklist_nodup := by admit /- proof elided -/

structure worklist.St where
  m : RawCNFA A
  map : Std.HashMap S State := ∅
  worklist : Array S := ∅
  worklist_nodup : worklist.toList.Nodup
  worklist_incl : ∀ sa ∈ worklist, sa ∈ map

def worklist.initState (inits : Array S) (hinits : inits.toList.Nodup) (final? : S → Bool) : worklist.St A S :=
  let m := RawCNFA.empty (A := A)
  let mapm := inits.foldl (init := (Std.HashMap.emptyWithCapacity, m)) fun (map, m) sa =>
    let (s, m) := m.newState
    let m := m.addInitial s
    let m := if final? sa then m.addFinal s else m
    (map.insert sa s, m)
  let map := mapm.1
  let m := mapm.2
  let worklist_incl : ∀ sa ∈ inits, sa ∈ map :=

instance RawCNFA.statesFinset (m : RawCNFA A) : Fintype m.states := (Finset.range m.stateMax).fintypeCoeSort

abbrev State := Nat

def RawCNFA.empty : RawCNFA A := {
  stateMax := 0
  initials := ∅
  finals := ∅
  trans := ∅
}

def processOneElem (final : S → Bool) (s : State) (st : worklist.St A S) : A × S → worklist.St A S :=
  fun (a', sa') =>
    let (s', st') := st.addOrCreateState _ _ (final sa') sa'
    let m := st'.m.addTrans a' s s'
    { st' with m }

def worklist.St.addOrCreateState (st : worklist.St A S) (final? : Bool) (sa : S) : State × worklist.St A S :=
  match heq : st.map[sa]? with
  | some s => (s, st)
  | none =>
    let (s, m) := st.m.newState
    let m := if final? then m.addFinal s else m
    let map := st.map.insert sa s
    let worklist := st.worklist.push sa
    have worklist_nodup : worklist.toList.Nodup := by admit /- proof elided -/

structure CNFA (n : Nat) where
  m : RawCNFA (BitVec n)
  wf : m.WF

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 sub (x y : BitStream) : BitStream :=
  fun n => (subAux x y n).1

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

abbrev ofTerm (t : Term) : FSM (Fin t.arity) := termEvalEqFSM t |>.toFSM

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

| shiftL : Term → Nat → Term

deriving Repr, Inhabited, Lean.ToExpr

def termEvalEqFSM : ∀ (t : Term), FSMTermSolution t
  | ofNat n =>
    { toFSM := FSM.ofNat n,
      good := by admit /- proof elided -/

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

def shiftLeft (n : Nat) : FSM Unit :=
  match n with
  | 0 => FSM.id
  | n + 1 => composeUnaryAux (FSM.ls false) (shiftLeft n)

def id : FSM Unit := {
 α := Empty,
 initCarry := Empty.elim,
 outputCirc := Circuit.var true (inr ()),
 nextStateCirc := Empty.elim
}

def ls (b : Bool) : FSM Unit :=
  { α := Unit,
    initCarry := fun _ => b,
    nextStateCirc := fun () => Circuit.var true (inr ()),
    outputCirc := Circuit.var true (inl ())
  }

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

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

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 xor : FSM Bool :=
  { α := Empty,
    initCarry := Empty.elim,
    outputCirc := Circuit.var true (inr true) ^^^ Circuit.var true (inr false),
    nextStateCirc := Empty.elim
  }

def neg : FSM Unit :=
  { α := Unit,
    i := by admit /- proof elided -/

def composeBinary
    (p : FSM Bool)
    {t₁ t₂ : Term}
    (q₁ : FSMTermSolution t₁)
    (q₂ : FSMTermSolution t₂) :
    FSM (Fin (max t₁.arity t₂.arity)) := composeBinaryAux p q₁.toFSM q₂.toFSM

def composeBinaryAux
    (p : FSM Bool)
    (q₁ : FSM (Fin a₁))
    (q₂ : FSM (Fin a₂)) :
    FSM (Fin (max a₁ a₂)) :=
  p.compose (Fin (max a₁ a₂))
    (λ b => Fin (cond b a₁ a₂))
    (λ b i => Fin.castLE (by admit /- proof elided -/
    ) i)
    (λ b => match b with
      | true => q₁
      | false => q₂)

structure FSMTermSolution (t : Term) extends FSM (Fin t.arity) where
  ( good : t.evalFin = toFSM.eval )

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

@[simp] def Predicate.evalFin (p : Predicate) (vars : Fin (arity p) → 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
| .binary .eq t₁ t₂ =>
    let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    Predicate.evalEq x₁ x₂
| .binary .neq t₁ t₂  =>
    let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
    ) i))
    Predicate.evalNeq x₁ x₂
| .land p q =>
  
  
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLand x₁ x₂
| .lor p q =>
  
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLor x₁ x₂
| .binary .slt p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalSlt x₁ x₂
| .binary .sle p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLor (Predicate.evalSlt x₁ x₂) (Predicate.evalEq x₁ x₂)
| .binary .ult p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  (Predicate.evalUlt x₁ x₂)
| .binary .ule p q =>
  let x₁ := p.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  let x₂ := q.evalFin (fun i => vars (Fin.castLE (by admit /- proof elided -/
  ) i))
  Predicate.evalLor (Predicate.evalUlt x₁ x₂) (Predicate.evalEq x₁ x₂)

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 Predicate.evalLor (t₁ t₂ : BitStream) : BitStream := (t₁ &&& t₂)

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.evalEq (t₁ t₂ : BitStream) : BitStream := (t₁ ^^^ t₂).concat false |>.scanOr

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

inductive Predicate : Type where
 
| width (wp : WidthPredicate) (n : Nat) : Predicate
| binary (p : BinaryPredicate) (t₁ t₂ : Term)
| land  (p q : Predicate) : Predicate
| lor (p q : Predicate) : Predicate
deriving Repr, Inhabited, Lean.ToExpr

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

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

abbrev falseIffLe (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)

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

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

| shiftL t .. => arity t

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 ofNat (n : Nat)  : FSM (Fin 0) :=
  match hn : n with
  | 0 => FSM.zero

| n' + 1 =>
    let bit := n.testBit 0
    let m := n / 2
    have h : m < n := by admit /- proof elided -/

def zero : FSM (Fin 0) :=
  { α := Empty,
    initCarry := Empty.elim,
    nextStateCirc := Empty.elim,
    outputCirc := Circuit.fals
  }

def composeUnary
    (p : FSM Unit)
    {t : Term}
    (q : FSMTermSolution t) :
    FSM (Fin t.arity) := composeUnaryAux p q.toFSM

def one : FSM (Fin 0) :=
  { α := Unit,
    i := by admit /- proof elided -/

def var (n : ℕ) : FSM (Fin (n+1)) :=
  { α := Empty,
    i := by admit /- proof elided -/

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

def negOne : FSM (Fin 0) :=
  { α := Empty,
    i := by admit /- proof elided -/

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

def not : FSM Unit :=
  { α := Empty,
    initCarry := Empty.elim,
    nextStateCirc := Empty.elim,
    outputCirc := Circuit.var false (inr ())
  }

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

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

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

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

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

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

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

def CNFA.inter (m1 m2 : CNFA n) : CNFA n := product (fun b1 b2 => b1 && b2) m1 m2

def product (final? : Bool → Bool → Bool) (m₁ m₂ : CNFA n) : CNFA n :=
  worklistRun (m₁.m.states × m₂.m.states) final (product.inits m₁ m₂)
    (by admit /- proof elided -/
    ) f
where final (ss : m₁.m.states × m₂.m.states) := final? (ss.1 ∈ m₁.m.finals) (ss.2 ∈ m₂.m.finals)
      f (ss : m₁.m.states × m₂.m.states) :=
        let (s1, s2) := ss
        (FinEnum.toList (α := BitVec n)).foldl (init := Array.empty) fun as a =>
          product.prodArray' (λ s₁ s₂ ↦ (a, (s₁, s₂)))
            (fun s' => m₁.wf.trans_tgt_lt (s := s1) (a := a)) (fun s' => m₂.wf.trans_tgt_lt (s := s2) (a := a)) as

@[inline]
def product.prodArray' (a : Array γ) :=
  m₁.attachWith _ hm₁ |>.fold (init := a) fun is s1 =>
    m₂.attachWith _ hm₂ |>.fold (init := is) fun is s2 =>
      is.push (f s1 s2)

def product.inits_nodup : inits m₁ m₂ |>.toList.Nodup :=

def product.inits (m₁ m₂ : CNFA n) :=
  product.prodArray Prod.mk @m₁.wf.initials_lt @m₂.wf.initials_lt

@[inline]
def product.prodArray := prodArray' f hm₁ hm₂ (Array.emptyWithCapacity <| m₁.size * m₂.size)

def CNFA.inter_bv_language (m₁ m₂ : CNFA n) :
    m₁.bv_recognizes L₁ →
    m₂.bv_recognizes L₂ →
    (m₁.inter m₂).bv_recognizes (L₁ ∩ L₂) :=

def HashSet.inter [BEq A] [Hashable A] (m1 m2 : Std.HashSet A) : Std.HashSet A :=
  m1.fold (init := ∅) fun mi x => if m2.contains x then mi.insert x else mi

structure NFA' (n : Nat) where
  σ : Type
  M : NFA (BitVec n) σ

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

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 carryBV (x : ar → BitVec w) : p.State :=
  p.carry (fun ar => .ofBitVecSext (x ar)) w

def evalBV {w} (x : ar → BitVec w) : BitVec w :=
  BitVec.ofFn fun k => p.eval (fun ar => .ofBitVecSext (x ar)) k

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

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

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

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

def enc (bvs : BitVecs n) : BitVecs' n :=
  (List.finRange bvs.w).map (fun i =>
    BitVec.ofFn (fun (k : Fin n) => (bvs.bvs.get k)[i]))

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

def accepts (M : NFA' n) : Set (BitVecs n) := dec '' M.accepts'

def accepts' (M : NFA' n) : Set (BitVecs' n) := M.M.accepts

def worklistRun_spec : (worklistRun S final inits hinits f |>.Sim $ nfa' inits final f) :=
  worklistRun'_spec inits final f

def nfa' : NFA' n :=
  { σ := _, M := nfa inits final f }

def nfa : NFA A S where
  start := { sa | sa ∈ inits }
  accept := { sa | final sa }
  step sa a := { sa' | (a, sa') ∈ f sa }

def worklistRun'_spec :
    (worklistRun' A S final inits hinits f |>.Sim $ nfa inits final f) :=

structure StInv (m : RawCNFA A) (map : Std.HashMap S State) where
  wf : m.WF
  map_states : ∀ (sa : S) s, map[sa]? = some s → s ∈ m.states
  map_surj : ∀ s : m.states, ∃ (sa : S), map[sa]? = some s.val
  map_inj : ∀ {s} {sa sa' : S}, map[sa]? = some s → map[sa']? = some s → sa = sa'

def worklist.St.D (st : worklist.St A S) : Set S := st.visited

def worklist.St.visited (st : worklist.St A S) : Set S := { s : S | s ∈ st.map ∧ s ∉ st.worklist }

def worklistGo_spec {st : worklist.St A S} (inv : StInv A S st.m st.map) :
    st.sim inits final f ∅ →
    (worklistRun'.go A S final f st |>.Sim $ nfa inits final f) :=

def worklist.St.rel (st : worklist.St A S) : SetRel State S := {(s, sa) | st.map[sa]? = some s }

def processOneElem_mot (s : State) (sa : S) (n : ℕ) (st : worklist.St A S) : Prop :=
  st.map[sa]? = some s ∧
  sa ∈ st.visited ∧
  StInv A S st.m st.map ∧
  st.sim inits final f  {(sa1, a, sa') | sa1 = sa ∧ ∃ k ≥ n, (f sa)[k]? = some (a, sa') }

abbrev worklist.St.sim {st : worklist.St A S} (T : Set (S × A × S)) :=
  st.m.Simul (nfa inits final f) st.rel st.D T

def RawCNFA.Sim (m : RawCNFA A) (A : NFA A S) := ∃ R, RawCNFA.Simul m A R ⊤ ∅

structure RawCNFA.Simul (m : RawCNFA A) (M : NFA A Q) (R : SetRel State Q) (D : Set Q) (T : Set (Q × A × Q)) where
  accept {s q} : s ~[R] q → (s ∈ m.finals ↔ q ∈ M.accept)
  initial₁ {s} : s ∈ m.initials → ∃ q ∈ M.start, s ~[R] q
  initial₂ {q} : q ∈ M.start → ∃ s ∈ m.initials, s ~[R] q
  trans_match₁ {s s' a q} : s ~[R] q → s' ∈ m.tr s a → ∃ q', q' ∈ M.step q a ∧ s' ~[R] q'
  trans_match₂ {s a q q'} : s ~[R] q → q' ∈ M.step q a → q ∈ D → (q, a, q') ∉ T → ∃ s', s' ∈ m.tr s a ∧ s' ~[R] q'

structure RawCNFA.SimulFun (m : RawCNFA A) (M : NFA A Q) (f : m.states ≃ Q)  where
  accept {q} : ((f.invFun q).val ∈ m.finals ↔ q ∈ M.accept)
  initial {q} : q ∈ M.start ↔ (f.invFun q).val ∈ m.initials
  trans_match {a q q'} : q' ∈ M.step q a ↔ (f.invFun q').val ∈ m.tr (f.invFun q) a

@[inline]
def RawCNFA.tr (m : RawCNFA A) s a := m.trans.getD (s, a) ∅

abbrev R := (ZMod q)[X] ⧸ (Ideal.span {f q n})

def CNFA.Sim (m : CNFA n) (M : NFA' n) :=
  m.m.Sim M.M

def CNFA.bv_recognizes (m : CNFA n) (L : Set (BitVecs n)) :=
  ∃ L', m.recognizes L' ∧ L = dec '' L'

def RawCNFA.recognizes (m : RawCNFA A) (L : Language A) :=
  ∃ (σ : Type) (M : NFA A σ), m.Sim M ∧ M.accepts = L

def CNFA.recognizes (m : CNFA n) (L : Language (BitVec n)) :=
  ∃ (M : NFA' n), m.Sim M ∧ M.M.accepts = L

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

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

def CNFA.minimize (m : CNFA n) : CNFA n :=
  let mᵣ := m.reverse.determinize
  mᵣ.reverse.determinize

def CNFA.determinize (m : CNFA n) : CNFA n :=
  worklistRun (BitVec m.m.stateMax)
    (fun ss => ss.any fun n b => b == true && n ∈ m.m.finals)
    (determinize.inits m)
    (by admit /- proof elided -/
    )
    f
where
  f := fun (ss : BitVec m.m.stateMax) =>
        (FinEnum.toList (BitVec n)).foldl (init := Array.empty) fun ts a =>
          let ss' := m.m.transSetBV ss a
          ts.push (a, ss')

def CNFA.determinize.inits (m : CNFA n) : Array (BitVec m.m.stateMax) :=
  #[BitVec.ofFn (fun n => n ∈ m.m.initials)]

def CNFA.reverse (m : CNFA n) : CNFA n :=
  ⟨m.m.reverse, RawCNFA.reverse_spec m.wf |>.1⟩

def RawCNFA.reverse (m : RawCNFA A) : RawCNFA A :=
  let m' := { stateMax := m.stateMax, trans := Std.HashMap.emptyWithCapacity m.trans.size, initials := m.finals, finals := m.initials}
  m.trans.fold (init := m') processState
where
  processState := fun m' (s, a) ss' =>
    ss'.fold (init := m') fun m' s' => m'.addTrans a s' s

def CNFA.toNFA' (m : CNFA n) : NFA' n := ⟨_, m.toNFA⟩

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 RawCNFA.states (m : RawCNFA A) : Finset State := Finset.range m.stateMax

def reverse (M : NFA' n) : NFA' n where
  σ := _
  M := M.M.reverse

def CNFA.determinize_spec (m : CNFA n)
  {M : NFA' n} (hsim : m.Sim M) :
    m.determinize.Sim M.determinize :=

private def bv_to_set (bv : BitVec w) : Set State :=
  { s | bv.getLsbD s }

structure _root_.SetRel.set_eq (R : SetRel α β) (A : Set α) (B : Set β) where
  fwd : a ∈ A → ∃ b ∈ B, a ~[R] b
  bwd : b ∈ B → ∃ a ∈ A, a ~[R] b

@[inline]
def RawCNFA.lift (m₁: RawCNFA (BitVec n1)) (f : Fin n1 → Fin n2) : RawCNFA (BitVec n2) :=
  let trans := (List.range m₁.stateMax).foldl (init := ∅) fun m2 s => processState m2 s
  { m₁ with trans }
where

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

def BitVecs.transport (f : Fin n → Fin m) (bvs : BitVecs m) : BitVecs n :=
  { w := bvs.w, bvs := bvs.bvs.transport f }

def BitVec.transport (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2 :=
  BitVec.ofFn fun i => bv.getLsbD (f i)

def List.Vector.transport (v : Vector α m) (f : Fin n → Fin m) : Vector α n :=
  Vector.ofFn fun i => v.get (f i)

def BitVecs'.transport (f : Fin n → Fin m) (bvs' : BitVecs' m): BitVecs' n :=
  bvs'.map fun bv => bv.transport f

@[inline]
def RawCNFA.proj (m1: RawCNFA (BitVec n1)) (f : Fin n2 → Fin n1) : RawCNFA (BitVec n2) :=
  let trans := m1.trans.keysArray.foldl (init := Std.HashMap.emptyWithCapacity) process
  { m1 with trans }
where

def CNFA.proj_spec (m : CNFA n2) (f : Fin n1 → Fin n2) {M : NFA' n2} :
    m.Sim M → (m.proj f |>.Sim (M.proj f)) :=

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

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

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 simplify_neg_minmax : RISCVPeepholeRewrite [Ty.riscv (.bv) ] where
  lhs := [LV| {
    ^entry (%x: !riscv.reg):
      %0 = neg %x : !riscv.reg
      %1 = min %x, %0 : !riscv.reg
      %2 = neg %1 : !riscv.reg
      ret %2 : !riscv.reg
  }]
  rhs := [LV| {
    ^entry (%x: !riscv.reg):
      %0 = neg %x : !riscv.reg
      %1 = max %x, %0 : !riscv.reg
      ret %1 : !riscv.reg
  }]

def constLLVM_22 : Com LLVMPlusRiscV ⟨[]⟩ .pure (.llvm (.bitvec 64)) := [LV| {
  ^entry ():
    %1 = llvm.mlir.constant (-22) : i64
    llvm.return %1 : i64
  }]

def t9_after := [llvm|
{
^0(%arg176 : i8, %arg177 : i8):
  %0 = llvm.sub %arg176, %arg177 : i8
  "llvm.return"(%0) : (i8) -> ()
}
]

def hoist_logic_op_with_same_opcode_hands_32 : List (Σ Γ, LLVMPeepholeRewriteRefine 32 Γ) :=
  [⟨_, AndTruncTrunc⟩,
  ⟨_, OrTruncTrunc⟩,
  ⟨_, XorTruncTrunc⟩]

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

def llvm_zext_lower_riscv_1_to_16 : LLVMPeepholeRewriteRefine 16 [Ty.llvm (.bitvec 1)] :=
  {lhs:= zext_llvm_1_to_16, rhs:= zext_riscv_1_to_16}

def muxVal (x y c : ValueStream (BitVec 1)): ValueStream (BitVec 1) :=
  Stream.corec (β := ValueStream (BitVec 1) × ValueStream (BitVec 1) × ValueStream (BitVec 1)) (x, y, c)
  fun ⟨x, y, c⟩ =>
    match (c 0) with
    | none => (none, x, y, c.tail) 
    | some 1#1 =>
      match (x 0) with
      | none => (none, x.tail, y, c) 
      | some e => (some e, x.tail, y, c.tail) 
    | some 0#1 =>
      match (y 0) with
      | none => (none, x, y.tail, c) 
      | some e => (some e, x, y.tail, c.tail)

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

def ashr_overshift_before := [llvm|
{
^0(%arg6 : i32):
  %0 = llvm.mlir.constant(15 : i32) : i32
  %1 = llvm.mlir.constant(17 : i32) : i32
  %2 = llvm.ashr %arg6, %0 : i32
  %3 = llvm.ashr %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

|
</all_available_defs>

<all_available_lemmas>
List.nodup_singleton in Mathlib.Data.List.Nodup
NFA.eval_append_singleton in Mathlib.Computability.NFA
NFA.eval_nil in Mathlib.Computability.NFA
Set.mem_setOf_eq in Mathlib.Data.Set.Operations
Nat.add_comm in Init.Data.Nat.Basic
Fin.add_def in Init.Data.Fin.Lemmas
Fin.castLE_castLE in Init.Data.Fin.Lemmas
Nat.le_of_eq in Init.Data.Nat.Basic
Nat.mod_eq_of_lt in Init.Data.Nat.Div.Basic

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

lemma bisim_comp (m : RawCNFA A) :
    m.Sim M₁ → M₁.Bisim M₂ → m.Sim M₂

lemma bisimul_comp {m : RawCNFA A} :
    m.Simul M₁ R₁ ⊤ ∅ → M₁.Bisimul R₂ M₂ →
    m.Simul M₂ (R₁.comp R₂) ⊤ ∅

lemma CNFA.bv_recognizes_equiv {m : CNFA n} :
    m.bv_recognizes L ↔ ∃ (M : NFA' n), m.Sim M ∧ M.accepts = L

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

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

lemma CNFA.minimize_bv_language {m : CNFA n} :
    m.bv_recognizes L → m.minimize.bv_recognizes L

lemma CNFA.minimize_language {m : CNFA n} :
    m.recognizes L → m.minimize.recognizes L

lemma CNFA.reverse_language {m : CNFA n} (hl : m.recognizes L) : m.reverse.recognizes L.reverse

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

lemma RawCNFA.reverse_spec {m : RawCNFA A} (hwf : m.WF) :
    let m'

lemma RawCNFA.reverse_spec_procesState {m : RawCNFA A} (hwf : m.WF) s₀ a₀ ss' (hs₀ : s₀ ∈ m.states) :
    let motive m' ss'

lemma CNFA.determinize_language {m : CNFA n} :
    m.recognizes L → m.determinize.recognizes L

@[simp]
lemma CNFA.lift_bv_language {m : CNFA n1} {f : Fin n1 → Fin n2} :
    m.bv_recognizes L → (m.lift f |>.bv_recognizes (BitVecs.transport f ⁻¹' L))

lemma CNFA.lift_spec (m : CNFA n1) (f : Fin n1 → Fin n2) {M : NFA' n1} :
    m.Sim M → (m.lift f |>.Sim (M.lift f))

lemma CNFA.proj_bv_language {m : CNFA n2} {f : Fin n1 → Fin n2} :
    m.bv_recognizes L → (m.proj f |>.bv_recognizes (BitVecs.transport f '' L))

theorem e_1090 :
    1 *  ~~~(z ^^^ t) + 3 * z + 2 *  ~~~(z &&&  ~~~t) - 5 *  ~~~t - 2 *  ~~~z + 5 *  ~~~(z ||| t) + 3 * (z &&&  ~~~t) - 5 * (z &&& t) = 1 * (z |||  ~~~t)

theorem ashr_bitwidth_mask_proof : ashr_bitwidth_mask_before ⊑ ashr_bitwidth_mask_after

theorem append_valid {Γ₁ Γ₂ Γ₃  : Ctxt Ty} {d₁ d₂ : Nat} :
  Diff.Valid Γ₁ Γ₂ d₁ →  Diff.Valid Γ₂ Γ₃ d₂ → Diff.Valid Γ₁ Γ₃ (d₁ + d₂)

theorem lshrugt_01_00_exact_thm (e : IntW 4) :
  icmp IntPred.ugt (lshr e (const? 4 1) { «exact» := true }) (const? 4 0) ⊑
    icmp IntPred.ne e (const? 4 0)

@[simp, simp_denote]
theorem liftEffect_rfl [Pure m] (hle : eff ≤ eff) :
    liftEffect hle (α := α) (m := m) = id

theorem ashrslt_03_10_exact_proof : ashrslt_03_10_exact_before ⊑ ashrslt_03_10_exact_after

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

theorem e_2343 :
     - 1 * (f ||| (d &&&  ~~~e)) + 11 * (e |||  ~~~(d |||  ~~~f)) + 2 * (e ^^^ (d ||| f)) + 1 *  ~~~( ~~~d ||| (e ^^^ f)) + 7 * ( ~~~(d &&& e) &&&  ~~~(e ^^^ f)) - 1 *  ~~~(d &&& ( ~~~e &&& f)) - 7 * (f ^^^ (d ||| (e &&& f))) - 7 * (e ^^^  ~~~(d &&&  ~~~f)) + 3 * (f ^^^ (d &&& (e ||| f))) - 1 * (e &&& (d |||  ~~~f)) - 6 * (d ^^^ e) + 2 *  ~~~( ~~~d &&& (e &&& f)) + 5 * (e ^^^  ~~~( ~~~d &&& (e ^^^ f))) + 11 *  ~~~(d &&& e) + 4 * (e |||  ~~~(d ||| f)) + 4 * (f ^^^  ~~~( ~~~d &&& ( ~~~e &&& f))) + 2 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) + 1 *  ~~~( ~~~d &&& (e ||| f)) - 1 *  ~~~(d &&& (e ||| f)) + 3 * (e ^^^  ~~~(d &&& ( ~~~e &&& f))) - 5 * ((d &&& f) ^^^  ~~~(e &&&  ~~~f)) - 3 * ((d &&& e) ^^^  ~~~(d ^^^ (e &&& f))) + 1 *  ~~~( ~~~d ||| (e &&& f)) - 5 * (e ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 1 * ( ~~~(d &&& e) &&& (d ^^^ (e ^^^ f))) - 11 * ((d |||  ~~~e) &&& (d ^^^ (e ^^^ f))) + 4 * (e &&&  ~~~(d &&& f)) - 7 *  ~~~(d ||| (e ^^^ f)) + 1 * (d &&& (e ^^^ f)) - 1 * ((e &&& f) ||| ( ~~~d &&& (e ||| f))) - 1 * ( ~~~(d |||  ~~~e) |||  ~~~(e ^^^ f)) - 1 * ( ~~~(d &&& e) &&& (e ^^^ f)) + 1 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) - 2 *  ~~~(d |||  ~~~f) + 2 * (f ^^^  ~~~(d |||  ~~~e)) - 7 *  ~~~e - 2 * (d ||| (e ^^^ f)) + 7 * (e ^^^ (d ||| ( ~~~e &&& f))) - 2 * ((d ^^^ e) ||| (d ^^^ f)) + 1 * (e ^^^  ~~~(d &&& ( ~~~e ||| f))) + 7 * (f ^^^  ~~~(d &&& (e &&& f))) + 5 *  ~~~(d ^^^ (e ^^^ f)) + 11 * ( ~~~d &&& ( ~~~e ||| f)) + 2 * (e &&& (d ^^^ f)) + 1 * (f ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) + 1 * ( ~~~d &&& (e ||| f)) + 1 * (f |||  ~~~(d |||  ~~~e)) + 1 * (d &&& e) - 5 * (d ^^^ (e &&& f)) + 1 * (e ^^^ f) - 1 *  ~~~(e |||  ~~~f) - 6 * ((d |||  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) + 1 * (e ^^^ (d &&& (e ^^^ f))) - 1 * (e ^^^  ~~~(d &&& (e &&& f))) - 5 * ((d &&& f) ^^^ (e ||| f)) + 1 * (e ||| (d &&&  ~~~f)) + 1 *  ~~~(d &&& (e ^^^ f)) - 3 * (f ^^^ (d &&&  ~~~e)) - 5 * (e ^^^ ( ~~~d ||| (e &&& f))) + 2 * ( ~~~d ||| ( ~~~e ||| f)) - 20 *  ~~~(d ||| (e ||| f)) - 39 *  ~~~(d ||| ( ~~~e ||| f)) + 1 * ( ~~~d &&& ( ~~~e &&& f)) - 29 * ( ~~~d &&& (e &&& f)) - 7 * (d &&& ( ~~~e &&& f)) - 16 * (d &&& (e &&& f)) = 5 *  ~~~( ~~~d ||| ( ~~~e ||| f))

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

theorem e_298 :
    1 * y - 7 * (x ^^^ y) + 1 *  ~~~(x &&& y) + 11 *  ~~~y - 12 *  ~~~(x ||| y) - 5 * (x &&&  ~~~y) - 1 * (x &&& y) =  - 5 *  ~~~(x |||  ~~~y)

theorem bools_logical_commute1_and2_proof : bools_logical_commute1_and2_before ⊑ bools_logical_commute1_and2_after

theorem ashrslt_01_03_exact_proof : ashrslt_01_03_exact_before ⊑ ashrslt_01_03_exact_after

theorem test4_logical_proof : test4_logical_before ⊑ test4_logical_after

theorem slt_positive_multip_rem_zero_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ x.smulOverflow 7#8 = true) → ofBool (x * 7#8 <ₛ 21#8) = ofBool (x <ₛ 3#8)

theorem ne_umin1_proof : ne_umin1_before ⊑ ne_umin1_after
</all_available_lemmas>

<local_ctx>
import Batteries.Data.Fin.Basic

import Batteries.Data.Fin.Lemmas

import Blase.SingleWidth.Defs

import Blase.AutoStructs.Constructions

import Blase.AutoStructs.Defs

import Blase.AutoStructs.FiniteStateMachine

import Mathlib.Tactic.Ring

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

import Mathlib.Data.BitVec

import Mathlib.Tactic.FinCases

open Fin.NatCast

open Mathlib

def NFA.sa (_ : NFA α σ) := σ → Language α

structure NFA.correct (M : NFA α σ) (ζ : M.sa) (L : Language α) where
  cond1 : ∀ w, (w ∈ L ↔ ∃ q ∈ M.accept, w ∈ ζ q)
  cond2 : ∀ w q, q ∈ M.eval w ↔ w ∈ ζ q

abbrev BVNRel n := ∀ ⦃w⦄, List.Vector (BitVec w) n → Prop

def NFA'.sa (M : NFA' n) := M.σ → BVNRel n

def langRel (R : BVNRel n) : Set (BitVecs n) :=
  { bvs | R bvs.bvs }

structure NFA'.correct (M : NFA' n) (ζ : M.sa) (L : BVNRel n) where
  cond1 : ∀ ⦃w⦄ (bvn : List.Vector (BitVec w) n), (L bvn ↔ ∃ q ∈ M.M.accept, ζ q bvn)
  cond2 q : q ∈ M.M.start ↔ ζ q (List.Vector.replicate n .nil)
  cond3 q a {w} (bvn : List.Vector (BitVec w) n) : q ∈ M.M.stepSet { q | ζ q bvn } a ↔
              ζ q (List.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) (bvn.get k))

structure NFA'.correct2 (M : NFA' 2) (ζ : M.sa2) (L : BVRel) where
  cond1 : ∀ (bv1 bv2 : BitVec w), (L bv1 bv2 ↔ ∃ q ∈ M.M.accept, ζ q bv1 bv2)
  cond2 q : q ∈ M.M.start ↔ ζ q .nil .nil
  cond3 q a w (bv1 bv2 : BitVec w) : q ∈ M.M.stepSet { q | ζ q bv1 bv2 } a ↔
              ζ q (BitVec.cons (a.getLsbD 0) bv1) (BitVec.cons (a.getLsbD 1) bv2)

section fsm

abbrev Alphabet (arity: Type) [FinEnum arity] := BitVec (FinEnum.card arity + 1)

variable {arity : Type} [FinEnum arity]

def finFunToBitVec [fe : FinEnum carry] (c : carry → Bool) : BitVec (FinEnum.card carry) :=
  BitVec.ofFn fun i => c (fe.equiv.invFun i)

def bitVecToFinFun [FinEnum ar] (bv : BitVec $ FinEnum.card ar) : ar → Bool :=
  fun c => bv[FinEnum.equiv.toFun c]

def NFA.ofFSM (p : FSM arity) : NFA (Alphabet arity) (p.α → Bool) where
  start := { q | q = p.initCarry }
  accept := ⊤
  step s a := {s' |
    let (s'', b) := p.nextBit s (bitVecToFinFun (a.truncate $ FinEnum.card arity))
    s' = s'' ∧ a.msb = b }

@[simp]
abbrev inFSMRel (p : FSM arity) {w} (bvn : List.Vector (BitVec w) _) :=
  bvn.get (Fin.last (FinEnum.card arity)) = p.evalBV (fun ar => bvn.get (FinEnum.equiv.toFun ar))

def NFA'.ofFSM_sa (p : FSM arity) : (NFA'.ofFSM' p).sa := fun q _ bvn =>
    inFSMRel p bvn ∧ q = p.carryBV (fun ar => bvn.get (FinEnum.equiv.toFun ar))

def NFA'.ofFSM_correct (p : FSM arity) :
    (NFA'.ofFSM' p).correct (ofFSM_sa p) (fun _ bvn => inFSMRel p bvn) :=

open BitStream in

def CNFA.ofFSM (p : FSM arity) : CNFA (FinEnum.card arity + 1) :=
  worklistRun (BitVec (FinEnum.card p.α))
    (fun _ => true)
    #[finFunToBitVec p.initCarry]
    (by admit /- proof elided -/
    )
    f
  where

end fsm

section nfas_relations

inductive NFA.msbState : Type where
| i | f
deriving DecidableEq, Fintype

end nfas_relations

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

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

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

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

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

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

def TermBinop.termGadget (t : TermBinop) : CNFA 3 :=
  match t with
  | .and => FSM.ofTerm (.and (.var 0) (.var 1)) |> CNFA.ofFSM
  | .or => FSM.ofTerm (.or (.var 0) (.var 1)) |> CNFA.ofFSM
  | .xor => FSM.ofTerm (.xor (.var 0) (.var 1)) |> CNFA.ofFSM
  | .add => FSM.ofTerm (.add (.var 0) (.var 1)) |> CNFA.ofFSM
  | .sub => FSM.ofTerm (.sub (.var 0) (.var 1)) |> CNFA.ofFSM

def autOfTermBinop (op : TermBinop) (m₁ : CNFA (n + 1)) (m₂ : CNFA (m + 1)) : CNFA ((n ⊔ m) + 1 ) :=
  let mop : CNFA 3 := op.termGadget
  let f₁ := liftMaxSuccSucc1 n m
  let m1' := m₁.lift f₁
  let f₂ := liftMaxSuccSucc2 n m
  let m2' := m₂.lift f₂
  let mop := mop.lift $ liftLast3 (max (FinEnum.card (Fin n)) (FinEnum.card (Fin m)))
  let m := CNFA.inter m1' m2' |> CNFA.inter mop
  let mfinal := m.proj (liftOp _)
  mfinal.minimize

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

inductive TermUnop where
| neg | not | shiftL (k : Nat)

def TermUnop.openTerm (op : TermUnop) : Term :=
  match op with
  | .neg => .neg (.var 0)
  | .not => .not (.var 0)
  | .shiftL k => .shiftL (.var 0) k

def TermUnop.openTerm_arity (op : TermUnop) : op.openTerm.arity = 1 :=

def TermUnop.subst (op : TermUnop) (t : Term) : Term :=
  match op with
  | .neg => .neg t
  | .not => .not t
  | .shiftL k => .shiftL t k
</local_ctx>

<target_theorem>
lemma autOfTermBinop_bv_language op {t₁ t₂ : Term} (m₁ : CNFA (t₁.arity + 1)) (m₂ : CNFA (t₂.arity + 1)) :
    m₁.bv_recognizes t₁.language →
    m₂.bv_recognizes t₂.language →
    (autOfTermBinop op m₁ m₂ |>.bv_recognizes (op.subst_arity' ▸ (op.subst t₁ t₂).language)) :=
</target_theorem>

