diff --git a/SSA/Experimental/Bits/Defs.lean b/SSA/Experimental/Bits/Defs.lean
index 985923e7c..ff2043e86 100644
--- a/SSA/Experimental/Bits/Defs.lean
+++ b/SSA/Experimental/Bits/Defs.lean
@@ -53,20 +53,20 @@ so eval requires us to give a value for each possible variable.
 -/
 def Term.eval (t : Term) (vars : Nat → BitStream) : BitStream :=
   match t with
-  | var n     => vars n
-  | zero      => BitStream.zero
-  | one       => BitStream.one
-  | negOne    => BitStream.negOne
-  | 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)
-  | ls b t    => (Term.eval t vars).concat b
-  | 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)
-  | incr t    => BitStream.incr (Term.eval t vars)
-  | decr t    => BitStream.decr (Term.eval t vars)
+  | var n       => vars n
+  | zero        => BitStream.zero
+  | one         => BitStream.one
+  | negOne      => BitStream.negOne
+  | 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)
+  | ls b t      => (Term.eval t vars).concat b
+  | 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)
+  | incr t      => BitStream.incr (Term.eval t vars)
+  | decr t      => BitStream.decr (Term.eval t vars)
 
 instance : Add Term := ⟨add⟩
 instance : Sub Term := ⟨sub⟩
@@ -130,6 +130,6 @@ and only require that many bitstream values to be given in `vars`.
       let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
       let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
       x₁ - x₂
-  | neg t  => -(Term.evalFin t vars)
-  | incr t => BitStream.incr (Term.evalFin t vars)
-  | decr t => BitStream.decr (Term.evalFin t vars)
+  | neg t       => -(Term.evalFin t vars)
+  | incr t      => BitStream.incr (Term.evalFin t vars)
+  | decr t      => BitStream.decr (Term.evalFin t vars)
diff --git a/SSA/Experimental/Bits/Fast/BitStream.lean b/SSA/Experimental/Bits/Fast/BitStream.lean
index cd0105afe..4e7d5c11c 100644
--- a/SSA/Experimental/Bits/Fast/BitStream.lean
+++ b/SSA/Experimental/Bits/Fast/BitStream.lean
@@ -98,6 +98,45 @@ section Lemmas
 theorem ext {x y : BitStream} (h : ∀ i, x i = y i) : x = y := by
   funext i; exact h i
 
+/--
+The field projection `.1` distributes over function composition, so we can compute
+the first field of the result of the composition by repeatedly composing the first projection.
+-/
+theorem compose_first {α: Type u₁} (i : Nat) (a : α) 
+    (f : α → α × Bool) : 
+    (f ((Prod.fst ∘ f)^[i] a)).1 = (Prod.fst ∘ f)^[i] (f a).1 :=
+  match i with
+    | 0 => by simp
+    | i + 1 => by simp [compose_first i ((f a).1) f]
+
+/--
+Coinduction principle for `corec`.
+To show that `corec f a = corec g b`,
+we must show that:
+- The relation `R a b` is inhabited ["base case"]
+- Given that `R a b` holds, then `R (f a) (g b)` holds [coinductive case]
+-/
+theorem corec_eq_corec {a : α} {b : β} {f g}
+    (R : α → β → Prop)
+    (thing : R a b)
+    (h : ∀ a b, R a b →
+          let x := f a
+          let y := g b
+          R x.fst y.fst ∧ x.snd = y.snd) :
+    corec f a = corec g b := by
+  ext i
+  have lem : R ((Prod.fst ∘ f)^[i] (f a).1) ((Prod.fst ∘ g)^[i] (g b).1) ∧ corec f a i = corec g b i := by
+    induction' i with i ih
+    <;> simp only [Function.iterate_succ, Function.comp_apply, corec]
+    · apply h
+      exact thing
+    · have m := h ((Prod.fst ∘ f)^[i] (f a).1) ((Prod.fst ∘ g)^[i] (g b).1) (ih.1)
+      cases' m with l r
+      rw [r, ← compose_first, ← @compose_first β]
+      simp [l]
+  cases lem
+  assumption
+
 end Lemmas
 
 end Basic
@@ -276,6 +315,16 @@ instance : Add BitStream := ⟨add⟩
 instance : Neg BitStream := ⟨neg⟩
 instance : Sub BitStream := ⟨sub⟩
 
+/-- `repeatBit xs` will repeat the first bit of `xs` which is `true`.
+That is, it will be all-zeros iff `xs` is all-zeroes,
+otherwise, there's some number `k` so that after dropping the `k` least
+significant bits, `repeatBit xs` is all-ones. -/
+def repeatBit (xs : BitStream) : BitStream :=
+  corec (b := (false, xs)) fun (carry, xs) =>
+    let carry := carry || xs 0
+    let xs := xs.tail
+    ((carry, xs), carry)
+
 /-!
 TODO: We should define addition and `carry` in terms of `mapAccum`.
 For example:
diff --git a/SSA/Experimental/Bits/Fast/Decide.lean b/SSA/Experimental/Bits/Fast/Decide.lean
index 3227f6df2..1fa084970 100644
--- a/SSA/Experimental/Bits/Fast/Decide.lean
+++ b/SSA/Experimental/Bits/Fast/Decide.lean
@@ -1,5 +1,5 @@
 import SSA.Experimental.Bits.Fast.FiniteStateMachine
-import SSA.Experimental.Bits.Lemmas
+import SSA.Experimental.Bits.Fast.Lemmas
 
 instance (t₁ t₂ : Term) : Decidable (t₁.eval = t₂.eval) :=
   decidable_of_iff
@@ -33,96 +33,110 @@ example : ((and x y) + (or x y)).eval = (x + y).eval := by
 example : ((or x y) - (xor x y)).eval = (and x y).eval := by
   native_decide
 
+
+/-
+Note that we use `#eval!` instead of `#eval`, since our
+proof of `decide` currently contains a `sorry`. We should elminate the `sorry`,
+and then switch to `#eval`.
+-/
+
+/--
+info: 'Decidable.decide' does not depend on any axioms
+---
+info: 'decide' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
+-/
+#guard_msgs in #print axioms decide
+
 /-- info: true -/
-#guard_msgs in #eval decide (x + -x) 0
+#guard_msgs in #eval! decide (x + -x) 0
 
 /-- info: true -/
-#guard_msgs in #eval decide (incr x) (x + 1)
+#guard_msgs in #eval! decide (incr x) (x + 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (decr x) (x - 1)
+#guard_msgs in #eval! decide (decr x) (x - 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + -y) (x - y)
+#guard_msgs in #eval! decide (x + -y) (x - y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + 0) (var 0)
+#guard_msgs in #eval! decide (x + 0) (var 0)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) (y + x)
+#guard_msgs in #eval! decide (x + y) (y + x)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + (y + z)) (x + y + z)
+#guard_msgs in #eval! decide (x + (y + z)) (x + y + z)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - x) 0
+#guard_msgs in #eval! decide (x - x) 0
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + 0) x
+#guard_msgs in #eval! decide (x + 0) x
 
 /-- info: true -/
-#guard_msgs in #eval decide (0 + x) x
+#guard_msgs in #eval! decide (0 + x) x
 
 /-- info: true -/
-#guard_msgs in #eval decide (-x) (not x).incr
+#guard_msgs in #eval! decide (-x) (not x).incr
 
 /-- info: true -/
-#guard_msgs in #eval decide (-x) (not x.decr)
+#guard_msgs in #eval! decide (-x) (not x.decr)
 
 /-- info: true -/
-#guard_msgs in #eval decide (not x) (-x).decr
+#guard_msgs in #eval! decide (not x) (-x).decr
 
 /-- info: true -/
-#guard_msgs in #eval decide (-not x) (x + 1)
+#guard_msgs in #eval! decide (-not x) (x + 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) (x - not y - 1)
+#guard_msgs in #eval! decide (x + y) (x - not y - 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) ((xor x y) + (and x y).ls false)
+#guard_msgs in #eval! decide (x + y) ((xor x y) + (and x y).ls false)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) (or x y + and x y)
+#guard_msgs in #eval! decide (x + y) (or x y + and x y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) ((or x y).ls false - (xor x y))
+#guard_msgs in #eval! decide (x + y) ((or x y).ls false - (xor x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) (x + not y).incr
+#guard_msgs in #eval! decide (x - y) (x + not y).incr
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) (xor x y - (and (not x) y).ls false)
+#guard_msgs in #eval! decide (x - y) (xor x y - (and (not x) y).ls false)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) (and x (not y) - (and (not x) y))
+#guard_msgs in #eval! decide (x - y) (and x (not y) - (and (not x) y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) ((and x (not y)).ls false - (xor x y))
+#guard_msgs in #eval! decide (x - y) ((and x (not y)).ls false - (xor x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (xor x y) ((or x y) - (and x y))
+#guard_msgs in #eval! decide (xor x y) ((or x y) - (and x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (and x (not y)) (or x y - y)
+#guard_msgs in #eval! decide (and x (not y)) (or x y - y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (and x (not y)) (x - and x y)
+#guard_msgs in #eval! decide (and x (not y)) (x - and x y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (x - y)) (y - x).decr
+#guard_msgs in #eval! decide (not (x - y)) (y - x).decr
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (x - y)) (not x + y)
+#guard_msgs in #eval! decide (not (x - y)) (not x + y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (xor x y)) (and x y - (or x y)).decr
+#guard_msgs in #eval! decide (not (xor x y)) (and x y - (or x y)).decr
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (xor x y)) (and x y + not (or x y))
+#guard_msgs in #eval! decide (not (xor x y)) (and x y + not (or x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (or x y) (and x (not y) + y)
+#guard_msgs in #eval! decide (or x y) (and x (not y) + y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (and x y) (or (not x) y - not x)
+#guard_msgs in #eval! decide (and x y) (or (not x) y - not x)
 end testDecide
diff --git a/SSA/Experimental/Bits/Fast/Defs.lean b/SSA/Experimental/Bits/Fast/Defs.lean
new file mode 100644
index 000000000..f3ba2dfa6
--- /dev/null
+++ b/SSA/Experimental/Bits/Fast/Defs.lean
@@ -0,0 +1,145 @@
+/-
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import Mathlib.Data.Bool.Basic
+import Mathlib.Data.Fin.Basic
+import SSA.Experimental.Bits.Fast.BitStream
+
+/-!
+# Term Language
+This file defines the term language the decision procedure operates on,
+and the denotation of these terms into operations on bitstreams -/
+
+/-- A `Term` is an expression in the language our decision procedure operates on,
+it represent an infinite bitstream (with free variables) -/
+inductive Term : Type
+| var : Nat → Term
+/-- The constant `0` -/
+| zero : Term
+/-- The constant `-1` -/
+| negOne : Term
+/-- The constant `1` -/
+| one : Term
+/-- Bitwise and -/
+| and : Term → Term → Term
+/-- Bitwise or -/
+| or : Term → Term → Term
+/-- Bitwise xor -/
+| xor : Term → Term → Term
+/-- Bitwise complement -/
+| not : Term → Term
+/-- Append a single bit the start (i.e., least-significant end) of the bitstream -/
+| ls (b : Bool) : Term → Term
+/-- Addition -/
+| add : Term → Term → Term
+/-- Subtraction -/
+| sub : Term → Term → Term
+/-- Negation -/
+| neg : Term → Term
+/-- Increment (i.e., add one) -/
+| incr : Term → Term
+/-- Decrement (i.e., subtract one) -/
+| decr : Term → Term
+/-- `repeatBit` is an operation that will repeat the infinitely repeat the
+least significant `true` bit of the input.
+
+That is `repeatBit t` is all-zeroes iff `t` is all-zeroes.
+Otherwise, there is some number `k` s.t. `repeatBit t` is all-ones after
+dropping the least significant `k` bits  -/
+| repeatBit : Term → Term
+
+open Term
+
+open BitStream in
+/--
+Evaluate a term `t` to the BitStream it represents,
+given a value for the free variables in `t`.
+
+Note that we don't keep track of how many free variable occur in `t`,
+so eval requires us to give a value for each possible variable.
+-/
+def Term.eval (t : Term) (vars : Nat → BitStream) : BitStream :=
+  match t with
+  | var n       => vars n
+  | zero        => BitStream.zero
+  | one         => BitStream.one
+  | negOne      => BitStream.negOne
+  | 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)
+  | ls b t      => (Term.eval t vars).concat b
+  | 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)
+  | incr t      => BitStream.incr (Term.eval t vars)
+  | decr t      => BitStream.decr (Term.eval t vars)
+  | repeatBit t => BitStream.repeatBit (Term.eval t vars)
+
+instance : Add Term := ⟨add⟩
+instance : Sub Term := ⟨sub⟩
+instance : One Term := ⟨one⟩
+instance : Zero Term := ⟨zero⟩
+instance : Neg Term := ⟨neg⟩
+
+/-- `t.arity` is the max free variable id that occurs in the given term `t`,
+and thus is an upper bound on the number of free variables that occur in `t`.
+
+Note that the upper bound is not perfect:
+a term like `var 10` only has a single free variable, but its arity will be `11` -/
+@[simp] def Term.arity : Term → Nat
+| (var n) => n+1
+| zero => 0
+| one => 0
+| negOne => 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
+| ls _ t => arity t
+| add t₁ t₂ => max (arity t₁) (arity t₂)
+| sub t₁ t₂ => max (arity t₁) (arity t₂)
+| neg t => arity t
+| incr t => arity t
+| decr t => arity t
+| repeatBit t => arity t
+
+/--
+Evaluate a term `t` to the BitStream it represents.
+
+This differs from `Term.eval` in that `Term.evalFin` uses `Term.arity` to
+determine the number of free variables that occur in the given term,
+and only require that many bitstream values to be given in `vars`.
+-/
+@[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
+  | and t₁ t₂ =>
+      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      x₁ &&& x₂
+  | or t₁ t₂ =>
+      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      x₁ ||| x₂
+  | xor t₁ t₂ =>
+      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      x₁ ^^^ x₂
+  | not t     => ~~~(t.evalFin vars)
+  | ls b t    => (t.evalFin vars).concat b
+  | add t₁ t₂ =>
+      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      x₁ + x₂
+  | sub t₁ t₂ =>
+      let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
+      x₁ - x₂
+  | neg t       => -(Term.evalFin t vars)
+  | incr t      => BitStream.incr (Term.evalFin t vars)
+  | decr t      => BitStream.decr (Term.evalFin t vars)
+  | repeatBit t => BitStream.repeatBit (Term.evalFin t vars)
diff --git a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean
index 0a6cc1bfc..7dcd1d97c 100644
--- a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean
+++ b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean
@@ -5,11 +5,12 @@ import Mathlib.Data.Fintype.Pi
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Tactic.Zify
 import Mathlib.Tactic.Ring
-import SSA.Experimental.Bits.Defs
+import SSA.Experimental.Bits.Fast.Defs
 import SSA.Experimental.Bits.Fast.Circuit
 
 open Sum
 
+section FSM
 variable {α β α' β' : Type} {γ : β → Type}
 
 /-- `FSM n` represents a function `BitStream → ⋯ → BitStream → BitStream`,
@@ -103,6 +104,15 @@ theorem eval_eq_carry (x : arity → BitStream) (n : ℕ) :
     p.eval x n = (p.nextBit (p.carry x n) (fun i => x i n)).2 :=
   rfl
 
+theorem eval_eq_eval' :
+    p.eval x = p.eval' x := by
+  funext i
+  simp only [eval, eval']
+  induction i generalizing p x
+  case zero => rfl
+  case succ i ih =>
+    sorry
+
 /-- `p.changeVars f` changes the arity of an `FSM`.
 The function `f` determines how the new input bits map to the input expected by `p` -/
 def changeVars {arity2 : Type} (changeVars : arity → arity2) : FSM arity2 :=
@@ -475,6 +485,23 @@ theorem eval_eq_zero_of_set {arity : Type _} (p : FSM arity)
   rw [eval]
   exact (evalAux_eq_zero_of_set p R hR hi hr1 x n).1
 
+def repeatBit : FSM Unit where
+  α := Unit
+  initCarry := fun () => false
+  nextBitCirc := fun _ =>
+    .or (.var true <| .inl ()) (.var true <| .inr ())
+
+@[simp] theorem eval_repeatBit :
+    repeatBit.eval x = BitStream.repeatBit (x ()) := by
+  unfold BitStream.repeatBit
+  rw [eval_eq_eval', eval']
+  apply BitStream.corec_eq_corec
+    (R := fun a b => a.1 () = b.2 ∧ (a.2 ()) = b.1)
+  · simp [repeatBit]
+  · intro ⟨y, a⟩ ⟨b, x⟩ h
+    simp at h
+    simp [h, nextBit, BitStream.head]
+
 end FSM
 
 structure FSMSolution (t : Term) extends FSM (Fin t.arity) :=
@@ -504,6 +531,19 @@ def composeBinary
       | true => q₁.toFSM
       | false => q₂.toFSM)
 
+def composeBinary'
+    (p : FSM Bool)
+    {n m : Nat}
+    (q₁ : FSM (Fin n))
+    (q₂ : FSM (Fin m)) :
+    FSM (Fin (max n m)) :=
+  p.compose (Fin (max n m))
+    (λ b => Fin (cond b n m))
+    (λ b i => Fin.castLE (by cases b <;> simp) i)
+    (λ b => match b with
+      | true => q₁
+      | false => q₂)
+
 @[simp] lemma composeUnary_eval
     (p : FSM Unit)
     {t : Term}
@@ -589,6 +629,69 @@ def termEvalEqFSM : ∀ (t : Term), FSMSolution t
     let q := termEvalEqFSM t
     { toFSM := by dsimp [arity]; exact composeUnary FSM.decr q,
       good := by ext; simp }
+  | repeatBit t =>
+    let p := termEvalEqFSM t
+    { toFSM := by dsimp [arity]; exact composeUnary FSM.repeatBit p,
+      good := by ext; simp }
+
+/-!
+FSM that implement bitwise-and. Since we use `0` as the good state,
+we keep the invariant that if both inputs are good and our state is `0`, then we produce a `0`.
+If not, we produce an infinite sequence of `1`.
+-/
+def and : FSM Bool :=
+  { α := Unit,
+    initCarry := fun _ => false,
+    nextBitCirc := fun a =>
+      match a with
+      | some () =>
+             -- Only if both are `0` we produce a `0`.
+             (Circuit.var true (inr false)  |||
+             ((Circuit.var false (inr true) |||
+              -- But if we have failed and have value `1`, then we produce a `1` from our state.
+              (Circuit.var true (inl ())))))
+      | none => -- must succeed in both arguments, so we are `0` if both are `0`.
+                Circuit.var true (inr true) |||
+                Circuit.var true (inr false)
+                }
+
+/-!
+FSM that implement bitwise-or. Since we use `0` as the good state,
+we keep the invariant that if either inputs is `0` then our state is `0`.
+If not, we produce a `1`.
+-/
+def or : FSM Bool :=
+  { α := Unit,
+    initCarry := fun _ => false,
+    nextBitCirc := fun a =>
+      match a with
+      | some () =>
+             -- If either succeeds, then the full thing succeeds
+             ((Circuit.var true (inr false)  &&&
+             ((Circuit.var false (inr true)) |||
+             -- On the other hand, if we have failed, then propagate failure.
+              (Circuit.var true (inl ())))))
+      | none => -- can succeed in either argument, so we are `0` if either is `0`.
+                Circuit.var true (inr true) &&&
+                Circuit.var true (inr false)
+                }
+
+/-!
+FSM that implement logical not.
+we keep the invariant that if the input ever fails and becomes a `1`, then we produce a `0`.
+IF not, we produce an infinite sequence of `1`.
+
+EDIT: Aha, this doesn't work!
+We need NFA to DFA here (as the presburger book does),
+where we must produce an infinite sequence of`0` iff the input can *ever* become a `1`.
+But here, since we phrase things directly in terms of producing sequences, it's a bit less clear
+what we should do :)
+
+- Alternatively, we need to be able to decide `eventually always zero`.
+- Alternatively, we push negations inside, and decide `⬝ ≠ ⬝` and `⬝ ≰ ⬝`.
+-/
+-- def lnot : FSM Unit := sorry
+
 
 inductive Result : Type
   | falseAfter (n : ℕ) : Result
@@ -679,3 +782,47 @@ theorem decideIfZeros_correct {arity : Type _} [DecidableEq arity]
     intro x s h
     use x
     exact h
+
+end FSM
+
+/--
+The fragment of predicate logic that we support in `bv_automata`.
+Currently, we support equality, conjunction, disjunction, and negation.
+This can be expanded to also support arithmetic constraints such as unsigned-less-than.
+-/
+inductive Predicate : Nat → Type _ where
+| eq (t1 t2 : Term) : Predicate ((max t1.arity t2.arity))
+| and  (p : Predicate n) (q : Predicate m) : Predicate (max n m)
+| or  (p : Predicate n) (q : Predicate m) : Predicate (max n m)
+-- For now, we can't prove `not`, because it needs NFA → DFA conversion
+-- the way Sid knows how to build it, or negation normal form,
+-- both of which is machinery we lack.
+-- | not (p : Predicate n) : Predicate n
+
+
+
+/--
+denote a reflected `predicate` into a `prop.
+-/
+def Predicate.denote : Predicate α → Prop
+| eq t1 t2 => t1.eval = t2.eval
+| and p q => p.denote ∧  q.denote
+| or p q => p.denote ∨  q.denote
+-- | not p => ¬ p.denote
+
+/--
+Convert a predicate into a proposition
+-/
+def Predicate.toFSM : Predicate k → FSM (Fin k)
+| .eq t1 t2 => (termEvalEqFSM (Term.repeatBit <| Term.xor t1 t2)).toFSM
+| .and p q =>
+    let p := toFSM p
+    let q := toFSM q
+    composeBinary' FSM.and p q
+| .or p q =>
+    let p := toFSM p
+    let q := toFSM q
+    composeBinary' FSM.or p q
+
+theorem Predicate.toFsm_correct {k : Nat} (p : Predicate k) :
+  decideIfZeros p.toFSM = true ↔ p.denote := by sorry
diff --git a/SSA/Experimental/Bits/Fast/Lemmas.lean b/SSA/Experimental/Bits/Fast/Lemmas.lean
new file mode 100644
index 000000000..12bb39e93
--- /dev/null
+++ b/SSA/Experimental/Bits/Fast/Lemmas.lean
@@ -0,0 +1,38 @@
+/-
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import Mathlib.Data.Fintype.Card
+import Mathlib.Data.Fintype.Sum
+import Mathlib.Data.Fintype.Sigma
+import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Tactic.Zify
+import Mathlib.Tactic.Ring
+import SSA.Experimental.Bits.Fast.Defs
+import SSA.Experimental.Bits.Fast.BitStream
+
+open Term
+
+lemma evalFin_eq_eval (t : Term) (vars : Nat → BitStream) :
+    Term.evalFin t (fun i => vars i) = Term.eval t vars := by
+  induction t <;>
+  dsimp [Term.evalFin, Term.eval, arity] at * <;> simp [*]
+
+lemma eq_iff_xor_eq_zero (seq₁ seq₂ : BitStream) :
+    (∀ i, seq₁ i = seq₂ i) ↔ (∀ i, (seq₁ ^^^ seq₂) i = BitStream.zero i) := by
+  simp [Function.funext_iff]
+
+lemma eval_eq_iff_xor_eq_zero (t₁ t₂ : Term) :
+    t₁.eval = t₂.eval ↔ (t₁.xor t₂).evalFin = fun _ => BitStream.zero := by
+  simp only [Function.funext_iff, Term.eval, Term.evalFin,
+    ← eq_iff_xor_eq_zero, ← evalFin_eq_eval]
+  constructor
+  · intro h seq
+    ext j
+    simp only [arity.eq_7, BitStream.xor_eq, BitStream.zero_eq, bne_eq_false_iff_eq]
+    apply congr_fun
+    simpa using h (fun j => if hj : j < (arity (t₁.xor t₂)) then seq ⟨j, hj⟩ else fun _ => false)
+  · intro h seq
+    ext j
+    have := h (seq ·)
+    apply_fun (· j) at this
+    simpa
diff --git a/SSA/Experimental/Bits/Fast/Tactic.lean b/SSA/Experimental/Bits/Fast/Tactic.lean
index d58941717..af85a5c80 100644
--- a/SSA/Experimental/Bits/Fast/Tactic.lean
+++ b/SSA/Experimental/Bits/Fast/Tactic.lean
@@ -1,7 +1,7 @@
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import SSA.Experimental.Bits.Fast.BitStream
 import SSA.Experimental.Bits.Fast.Decide
-import SSA.Experimental.Bits.Lemmas
+import SSA.Experimental.Bits.Fast.Lemmas
 import Qq.Macro
 
 open Lean Elab Tactic
@@ -332,143 +332,185 @@ macro "bv_automata" : tactic =>
 def alive_1 {w : ℕ} (x x_1 x_2 : BitVec w) : (x_2 &&& x_1 ^^^ x_1) + 1#w + x = x - (x_2 ||| ~~~x_1) := by
   bv_automata
 
-/-- info: 'alive_1' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'alive_1' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms alive_1
 
 def test_OfNat_ofNat (x : BitVec 1) : 1 + x = x + 1 := by
   bv_automata
 
-/-- info: 'test_OfNat_ofNat' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test_OfNat_ofNat' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test_OfNat_ofNat
 
 def test_BitVec_ofNat (x : BitVec 1) : 1 + x = x + 1#1 := by
   bv_automata
 
 /--
-info: 'test_BitVec_ofNat' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]
+info: 'test_BitVec_ofNat' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
 -/
 #guard_msgs in #print axioms test_BitVec_ofNat
 
 def test0 {w : Nat} (x y : BitVec (w + 1)) : x + 0 = x := by
   bv_automata
 
-/-- info: 'test0' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test0' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test0
 
 def test_simple2 {w : Nat} (x y : BitVec (w + 1)) : x = x := by
   bv_automata
 
 /--
-info: 'test_simple2' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]
+info: 'test_simple2' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
 -/
 #guard_msgs in #print axioms test_simple2
 
 def test1 {w : Nat} (x y : BitVec (w + 1)) : (x ||| y) - (x ^^^ y) = x &&& y := by
   bv_automata
 
-/-- info: 'test1' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test1' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test1
 
 def test2 (x y : BitVec 300) : (x &&& y) + (x ||| y) = x + y := by
   bv_automata
 
-/-- info: 'test2' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test2' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test2
 
 def test3 (x y : BitVec 300) : ((x ||| y) - (x ^^^ y)) = (x &&& y) := by
   bv_automata
 
-/-- info: 'test3' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test3' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test3
 
 def test4 (x y : BitVec 2) : (x + -y) = (x - y) := by
   bv_automata
 
-/-- info: 'test4' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test4' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test4
 
 def test5 (x y z : BitVec 2) : (x + y + z) = (z + y + x) := by
   bv_automata
 
-/-- info: 'test5' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test5' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test5
 
 def test6 (x y z : BitVec 2) : (x + (y + z)) = (x + y + z) := by
   bv_automata
 
-/-- info: 'test6' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test6' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test6
 
 def test11 (x y : BitVec 2) : (x + y) = ((x |||  y) +  (x &&&  y)) := by
   bv_automata
 
-/-- info: 'test11' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test11' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test11
 
 def test15 (x y : BitVec 2) : (x - y) = (( x &&& (~~~ y)) - ((~~~ x) &&&  y)) := by
   bv_automata
 
-/-- info: 'test15' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test15' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test15
 
 def test17 (x y : BitVec 2) : (x ^^^ y) = ((x ||| y) - (x &&& y)) := by
   bv_automata
 
-/-- info: 'test17' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test17' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test17
 
 def test18 (x y : BitVec 2) : (x &&&  (~~~ y)) = ((x ||| y) - y) := by
   bv_automata
 
-/-- info: 'test18' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test18' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test18
 
 def test19 (x y : BitVec 2) : (x &&&  (~~~ y)) = (x -  (x &&& y)) := by
   bv_automata
 
-/-- info: 'test19' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test19' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test19
 
 def test21 (x y : BitVec 2) : (~~~(x - y)) = (~~~x + y) := by
   bv_automata
 
-/-- info: 'test21' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test21' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test21
 
 def test23 (x y : BitVec 2) : (~~~(x ^^^ y)) = ((x &&& y) + ~~~(x ||| y)) := by
   bv_automata
 
-/-- info: 'test23' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test23' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test23
 
 def test24 (x y : BitVec 2) : (x ||| y) = (( x &&& (~~~y)) + y) := by
   bv_automata
 
-/-- info: 'test24' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test24' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test24
 
 def test25 (x y : BitVec 2) : (x &&& y) = (((~~~x) ||| y) - ~~~x) := by
   bv_automata
 
-/-- info: 'test25' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test25' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test25
 
 def test26 {w : Nat} (x y : BitVec (w + 1)) : 1 + x + 0 = 1  + x := by
   bv_automata
 
-/-- info: 'test26' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test26' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test26
 
 def test27 (x y : BitVec 5) : 2 + x  = 1  + x + 1 := by
   bv_automata
 
-/-- info: 'test27' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test27' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test27
 
 def test28 {w : Nat} (x y : BitVec (w + 1)) : x &&& x &&& x &&& x &&& x &&& x = x := by
   bv_automata
 
-/-- info: 'test28' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
+/--
+info: 'test28' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
 #guard_msgs in #print axioms test28
 
 -- This test is commented out because it takes over a minute to run