diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean
index c9e1f8bef..0e75971c4 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean
@@ -13,23 +13,30 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Optio
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
 public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
+import Complexity.Foundations.Data.Nat.Bits
 
 /-!
-# The successor in binary
+# The successor, predecessor and zero test in binary
 
 `encNat`, reexported from `Encodings.Nat.Bits`, encodes a natural number by its binary digits,
 least significant first (`Nat.bits`).
-The successor is computed by one streaming transducer whose state is the carry: on each digit `b`
-in carry `c` it emits `c ^^ b` and keeps the carry `c && b`, and at the end it emits a final `1`
-exactly when a carry remains. The machine reads its input once and uses no work tape.
+Each of the three counter operations is computed by one streaming transducer that reads its input
+once and uses no work tape:
+
+* the successor's state is the carry: on each digit `b` in carry `c` it emits `c ^^ b` and keeps
+  the carry `c && b`, and at the end it emits a final `1` exactly when a carry remains;
+* the predecessor turns the borrowed `0`s into `1`s and the first `1` into a `0`, which it holds
+  back until a further digit shows that it is not the leading digit, and then copies the rest;
+* the zero test emits whether the input was empty.
 
 ## Main results
 
-* `Turing.MultiTapeTM.computableInTimeAndSpace_succ`: the successor is computable within
+* `Turing.MultiTapeTM.computableInTimeAndSpace_succ`, `computableInTimeAndSpace_pred`,
+  `computableInTimeAndSpace_isZero`: the operations are computable within
   `2 * (encNat n).length + 3` steps and zero work space.
-* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc`: its linear form.
+* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc`, `.natPred`, `.natIsZero`: their
+  linear forms.
 -/
-
 namespace Turing.MultiTapeTM
 
 /-- The framed binary encoding of triples of natural numbers. -/
@@ -55,6 +62,80 @@ private lemma run_succTransducer (c : Bool) (l : List Bool) :
 
 end NatSucc
 
+namespace NatPred
+
+/-- The predecessor as a transducer. In the borrow state `none` each `0` becomes `1`; the first
+`1` becomes a pending `0` (state `some false`), emitted only once a further digit shows it is not
+the leading digit; from then on (state `some true`) the digits are copied. -/
+private def predTransducer : Transducer Bool (Option Bool) where
+  q₀ := none
+  step
+    | none, false => (none, [true])
+    | none, true => (some false, [])
+    | some false, b => (some true, [false, b])
+    | some true, b => (some true, [b])
+  final _ := []
+  length_step_le q b := by rcases q with _ | _ | _ <;> cases b <;> simp
+  length_final_le _ := by simp
+
+private lemma run_predTransducer_copy (l : List Bool) : predTransducer.run (some true) l = l := by
+  induction l with
+  | nil => rfl
+  | cons b l ih => exact congrArg (b :: ·) ih
+
+private lemma run_predTransducer_pending (l : List Bool) :
+    predTransducer.run (some false) l = if l = [] then [] else false :: l := by
+  cases l with
+  | nil => rfl
+  | cons b l =>
+    change [false, b] ++ predTransducer.run (some true) l = _
+    rw [run_predTransducer_copy]
+    rfl
+
+private lemma run_predTransducer (n : ℕ) : predTransducer.run none n.bits = (n - 1).bits := by
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    rcases Nat.even_or_odd' n with ⟨m, rfl | rfl⟩
+    · rcases Nat.eq_zero_or_pos m with rfl | hm
+      · rfl
+      · rw [Nat.bit0_bits m (by omega), show 2 * m - 1 = 2 * (m - 1) + 1 by omega,
+          Nat.bit1_bits, ← ih m (by omega)]
+        rfl
+    · rw [Nat.bit1_bits, Nat.add_sub_cancel]
+      change predTransducer.run (some false) m.bits = _
+      rw [run_predTransducer_pending]
+      rcases Nat.eq_zero_or_pos m with rfl | hm
+      · rfl
+      · rw [Nat.bit0_bits m hm.ne']
+        simp [Nat.bits_eq_nil_iff, hm.ne']
+
+/-- The zero test as a transducer: the state records that no digit has been read yet. -/
+private def isZeroTransducer : Transducer Bool Bool where
+  q₀ := true
+  step _ _ := (false, [])
+  final b := [b]
+  length_step_le _ _ := by simp
+  length_final_le _ := by simp
+
+private lemma run_isZeroTransducer (q : Bool) (l : List Bool) :
+    isZeroTransducer.run q l = [q && l.isEmpty] := by
+  induction l generalizing q with
+  | nil => simp [isZeroTransducer]
+  | cons b l ih =>
+    change [] ++ isZeroTransducer.run false l = _
+    simp [ih]
+
+end NatPred
+
+/-- A transducer certificate on `encNat` is linear in time and work space. -/
+private theorem ComputableInTimeAndSpace.linear {β : Type} {encOut : β ↪ List Bool} {f : ℕ → β}
+    (h : ComputableInTimeAndSpace f encNat encOut (fun n => 2 * (encNat n).length + 3)
+      (fun _ => 0)) :
+    ComputableInLinearTimeAndSpace f encNat encOut :=
+  let ⟨k, Q, hQ, tm, h⟩ := h
+  ⟨3, k, Q, hQ, tm, fun n =>
+    ⟨(h n).1, (h n).2.1.mono (by dsimp; omega), (h n).2.2.mono (Nat.zero_le _)⟩⟩
+
 open NatSucc in
 /-- **Binary successor in linear time and zero work space.** One streaming transducer computes
 `n + 1` from `encNat n` within `2 * (encNat n).length + 3` steps without work tapes. -/
@@ -68,8 +149,40 @@ public theorem computableInTimeAndSpace_succ :
 /-- Binary successor in linear time and work space, from `computableInTimeAndSpace_succ`. -/
 public theorem ComputableInLinearTimeAndSpace.natSucc :
     ComputableInLinearTimeAndSpace (· + 1) encNat encNat :=
-  let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_succ
-  ⟨3, k, Q, hQ, tm, fun n =>
-    ⟨(h n).1, (h n).2.1.mono (by dsimp; omega), (h n).2.2.mono (Nat.zero_le _)⟩⟩
+  computableInTimeAndSpace_succ.linear
+
+open NatPred in
+/-- **Binary predecessor in linear time and zero work space.** One streaming transducer computes
+`n - 1` (so `0 ↦ 0`) from `encNat n` within `2 * (encNat n).length + 3` steps without work
+tapes. -/
+public theorem computableInTimeAndSpace_pred :
+    ComputableInTimeAndSpace (· - 1) encNat encNat (fun n => 2 * (encNat n).length + 3)
+      (fun _ => 0) :=
+  ⟨0, _, inferInstance, predTransducer.toTM, fun n => by
+    rw [encNat_apply, encNat_apply, ← run_predTransducer]
+    exact predTransducer.computesInTimeAndSpace_toTM n.bits⟩
+
+/-- Binary predecessor in linear time and work space, from `computableInTimeAndSpace_pred`. -/
+public theorem ComputableInLinearTimeAndSpace.natPred :
+    ComputableInLinearTimeAndSpace (· - 1) encNat encNat :=
+  computableInTimeAndSpace_pred.linear
+
+open NatPred in
+/-- **Binary zero test in linear time and zero work space.** One streaming transducer decides
+`n = 0` from `encNat n` within `2 * (encNat n).length + 3` steps without work tapes. -/
+public theorem computableInTimeAndSpace_isZero :
+    ComputableInTimeAndSpace (fun n => decide (n = 0)) encNat encBool
+      (fun n => 2 * (encNat n).length + 3) (fun _ => 0) :=
+  ⟨0, _, inferInstance, isZeroTransducer.toTM, fun n => by
+    beta_reduce
+    rw [encNat_apply, encBool_apply, show decide (n = 0) = (true && n.bits.isEmpty) by
+      rw [Bool.true_and, Bool.eq_iff_iff, List.isEmpty_iff, Nat.bits_eq_nil_iff,
+        decide_eq_true_iff], ← run_isZeroTransducer]
+    exact isZeroTransducer.computesInTimeAndSpace_toTM n.bits⟩
+
+/-- Binary zero test in linear time and work space, from `computableInTimeAndSpace_isZero`. -/
+public theorem ComputableInLinearTimeAndSpace.natIsZero :
+    ComputableInLinearTimeAndSpace (fun n => decide (n = 0)) encNat encBool :=
+  computableInTimeAndSpace_isZero.linear
 
 end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Bits.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Bits.lean
index f927855f0..225594f2a 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Bits.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Bits.lean
@@ -16,8 +16,8 @@ import Mathlib.Tactic.Ring
 /-!
 # Binary natural encoding and digit algorithms
 
-The encoding and the carry, borrow and normalization word folds are independent of resource
-certificates. Their original definitions and arithmetic correctness proofs are retained here.
+The encoding and the carry word folds are independent of resource certificates. Their
+definitions and arithmetic correctness proofs are retained here.
 -/
 
 public section
@@ -80,102 +80,4 @@ public lemma length_encAcc (p : Bool × List Bool) : (encAcc p).length = p.2.len
 
 end NatSucc
 
-namespace NatPred
-
-/-- Subtracts a borrow from the binary digits `l`, least significant first, keeping a leading
-zero. -/
-@[expose] public def decr : List Bool → List Bool
-  | [] => []
-  | true :: l => false :: l
-  | false :: l => true :: decr l
-
-/-- Drops a leading zero, the last digit. -/
-@[expose] public def norm (l : List Bool) : List Bool :=
-  if l.getLast? = some false then l.dropLast else l
-
-lemma norm_cons {l : List Bool} (hl : l ≠ []) (b : Bool) : norm (b :: l) = b :: norm l := by
-  obtain ⟨x, hx⟩ := Option.isSome_iff_exists.mp (List.getLast?_isSome.mpr hl)
-  simp only [norm, List.getLast?_cons, hx, Option.getD_some, List.dropLast_cons_of_ne_nil hl]
-  split_ifs <;> rfl
-
-lemma bits_ne_nil {m : ℕ} (hm : m ≠ 0) : m.bits ≠ [] := by
-  rcases Nat.even_or_odd' m with ⟨k, rfl | rfl⟩
-  · rw [Nat.bit0_bits k (by omega)]; simp
-  · rw [Nat.bit1_bits]; simp
-
-lemma decr_ne_nil {l : List Bool} (hl : l ≠ []) : decr l ≠ [] := by
-  rcases l with _ | ⟨_ | _, l⟩ <;> simp_all [decr]
-
-lemma norm_bits (n : ℕ) : norm n.bits = n.bits := by
-  induction n using Nat.strong_induction_on with
-  | _ n ih =>
-    rcases Nat.even_or_odd' n with ⟨m, rfl | rfl⟩
-    · rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit0_bits m (by omega), norm_cons (bits_ne_nil (by omega)), ih m (by omega)]
-    · rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit1_bits, norm_cons (bits_ne_nil (by omega)), ih m (by omega)]
-
-public lemma bits_pred (n : ℕ) : (n - 1).bits = norm (decr n.bits) := by
-  induction n using Nat.strong_induction_on with
-  | _ n ih =>
-    rcases Nat.even_or_odd' n with ⟨m, rfl | rfl⟩
-    · rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit0_bits m (by omega), decr, show 2 * m - 1 = 2 * (m - 1) + 1 by omega,
-          Nat.bit1_bits, ih m (by omega), norm_cons (decr_ne_nil (bits_ne_nil (by omega)))]
-    · rw [Nat.bit1_bits, decr, Nat.add_sub_cancel]
-      rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit0_bits m (by omega), norm_cons (bits_ne_nil (by omega)), norm_bits]
-
-/-- One round of the decrement: subtract the borrow from the digit `b`, append the result and keep
-the borrow. -/
-@[expose] public def decrStep (p : Bool × List Bool) (b : Bool) : Bool × List Bool :=
-  (p.1 && !b, p.2 ++ [p.1 ^^ b])
-
-lemma length_decr (l : List Bool) : (decr l).length = l.length := by
-  induction l with
-  | nil => rfl
-  | cons b l ih => cases b <;> simp [decr, ih]
-
-lemma foldl_decrStep (l : List Bool) (c : Bool) (out : List Bool) :
-    (l.foldl decrStep (c, out)).2 = out ++ if c then decr l else l := by
-  induction l generalizing c out with
-  | nil => cases c <;> simp [decr]
-  | cons b l ih => cases c <;> cases b <;> simp [decrStep, ih, decr]
-
-/-- One round of dropping a leading zero: append the pending digit and keep the new one. -/
-@[expose] public def normStep (p : Option Bool × List Bool) (b : Bool) :
-    Option Bool × List Bool :=
-  (some b, p.2 ++ p.1.toList)
-
-/-- Appends the pending digit unless it is a zero. -/
-@[expose] public def normFinish (p : Option Bool × List Bool) : List Bool :=
-  if p.1 = some true then p.2 ++ [true] else p.2
-
-lemma length_foldl_normStep (l : List Bool) (p : Option Bool) (acc : List Bool) :
-    (l.foldl normStep (p, acc)).2.length ≤ acc.length + p.toList.length + l.length := by
-  induction l generalizing p acc with
-  | nil => simp
-  | cons b l ih =>
-    rw [List.foldl_cons, normStep]
-    have := ih (some b) (acc ++ p.toList)
-    simp only [Option.toList_some, List.length_append, List.length_cons, List.length_nil]
-      at this ⊢
-    omega
-
-lemma normFinish_foldl (l : List Bool) (p : Option Bool) (acc : List Bool) :
-    normFinish (l.foldl normStep (p, acc)) = acc ++ norm (p.toList ++ l) := by
-  induction l generalizing p acc with
-  | nil => rcases p with _ | _ | _ <;> simp [normFinish, norm]
-  | cons b l ih =>
-    rw [List.foldl_cons, normStep, ih]
-    rcases p with _ | p
-    · simp
-    · simp [norm_cons]
-
-end NatPred
-
 end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
index 38a816b7f..9dc18eb0e 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
@@ -10,43 +10,31 @@ module
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat
 import Mathlib.Tactic.Linarith
-import Mathlib.Tactic.Ring
 
 /-!
 # Direct binary counter resource certificates
 
-The original borrow and leading-zero normalization folds compute the predecessor. Its time is
-quadratic and its charged workspace linear in the binary input length. The successor's
-certificate here is a weakening of the streaming transducer `computableInTimeAndSpace_succ`; the
-carry rounds remain as the shared step of binary addition. The zero test uses the existing
-empty-word machine. All round certificates are plain; normalization occurs only when the internal
-machine combinators construct the fold.
+The successor, predecessor and zero test certificates here are weakenings of the streaming
+transducer certificates `computableInTimeAndSpace_succ`, `computableInTimeAndSpace_pred` and
+`computableInTimeAndSpace_isZero`. The carry rounds remain as the shared step of binary addition.
 
 ## Main results
 
 * `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates
   for binary addition.
-* `ComputableInO.natSucc`, `ComputableInO.natPred`: quadratic-time, linear-space binary counters.
+* `ComputableInO.natSucc`, `ComputableInO.natPred`: binary counters within the quadratic clock
+  and linear charged workspace used by their clients.
 * `ComputableInO.natIsZero`: linear zero testing.
 -/
 
 @[expose] public section
 namespace Turing.MultiTapeTM
 
-private theorem linear_tail {α β : Type*} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool}
-    {f : α → β} (h : ∀ a, encOut (f a) = (encIn a).tail) :
-    ComputableInLinearTimeAndSpace f encIn encOut := by
-  obtain ⟨c, k, Q, hfin, tm, htm⟩ := ListEncoding.tail (enc₁ := encBool) (enc := encBits)
-  refine ⟨c, k, Q, hfin, tm, fun a => ?_⟩
-  simpa only [h a, encBits_apply] using htm (encIn a)
-
 namespace ComputableInO
 
-open NatPred
-
-private theorem digitStep {op : Bool → Bool → Bool} (xor : Bool → Bool → Bool) :
-    ComputableInO (fun p : (Bool × List Bool) × Bool =>
-      (op p.1.1 p.2, p.1.2 ++ [xor p.1.1 p.2]))
+/-- One consuming carry round has linear time and charged workspace. -/
+theorem succStep :
+    ComputableInO (fun p : (Bool × List Bool) × Bool => NatSucc.succStep p.1 p.2)
       (encPair (encPair encBool encBits) encBool) (encPair encBool encBits)
       (fun p => (encPair (encPair encBool encBits) encBool p).length)
       (fun p => (encPair (encPair encBool encBits) encBool p).length) := by
@@ -54,61 +42,12 @@ private theorem digitStep {op : Bool → Bool → Bool} (xor : Bool → Bool →
   have hb := snd (encPair encBool encBits) encBool
   have hc := hacc.fst'
   have hflag := (of_linear (.of_finite (encIn := encPair encBool encBool) (encMid := encBool)
-    fun q : Bool × Bool => op q.1 q.2)).comp_linear (hc.prod hb)
+    fun q : Bool × Bool => q.1 && q.2)).comp_linear (hc.prod hb)
   have hdig := (of_linear (.of_finite (encIn := encPair encBool encBool) (encMid := encBool)
-    fun q : Bool × Bool => xor q.1 q.2)).comp_linear (hc.prod hb)
+    fun q : Bool × Bool => q.1 ^^ q.2)).comp_linear (hc.prod hb)
   exact (hflag.prod (hacc.snd'.append hdig (encOut := encBits) fun _ => rfl)).mono 5
     (fun _ => by omega) (fun _ => by omega)
 
-private theorem decrStep_inO :
-    ComputableInO (fun p : (Bool × List Bool) × Bool => decrStep p.1 p.2)
-      (encPair (encPair encBool encBits) encBool) (encPair encBool encBits)
-      (fun p => (encPair (encPair encBool encBits) encBool p).length)
-      (fun p => (encPair (encPair encBool encBits) encBool p).length) :=
-  digitStep (op := fun c b => c && !b) (· ^^ ·)
-
-/-- One consuming carry round has linear time and charged workspace. -/
-theorem succStep :
-    ComputableInO (fun p : (Bool × List Bool) × Bool => NatSucc.succStep p.1 p.2)
-      (encPair (encPair encBool encBits) encBool) (encPair encBool encBits)
-      (fun p => (encPair (encPair encBool encBits) encBool p).length)
-      (fun p => (encPair (encPair encBool encBits) encBool p).length) :=
-  digitStep (op := (· && ·)) (· ^^ ·)
-
-private theorem normStep_inO :
-    ComputableInO (fun p : (Option Bool × List Bool) × Bool => normStep p.1 p.2)
-      (encPair (encPair (encOption encBool) encBits) encBool)
-      (encPair (encOption encBool) encBits)
-      (fun p => (encPair (encPair (encOption encBool) encBits) encBool p).length)
-      (fun p => (encPair (encPair (encOption encBool) encBits) encBool p).length) := by
-  have hacc := fst (encPair (encOption encBool) encBits) encBool
-  have hb := snd (encPair (encOption encBool) encBits) encBool
-  have hpend := (of_linear (linear_tail (encIn := encOption encBool) (encOut := encBits)
-    (f := fun o => o.toList) fun o => by cases o <;> rfl)).comp_linear hacc.fst'
-  have hsome : ComputableInLinearTimeAndSpace some encBool (encOption encBool) := by
-    obtain ⟨c, k, Q, hfin, tm, htm⟩ := OptionEncoding.some
-      (enc₁ := encBool) (enc := encOption encBool)
-    exact ⟨c, k, Q, hfin, tm, fun b => htm b⟩
-  exact (((of_linear hsome).comp_linear hb).prod
-    (hacc.snd'.append hpend (encOut := encBits) fun _ => rfl)).mono 3
-      (fun _ => by omega) (fun _ => by omega)
-
-private theorem normFinish_inO :
-    ComputableInO normFinish (encPair (encOption encBool) encBits) encBits
-      (fun p => (encPair (encOption encBool) encBits p).length)
-      (fun p => (encPair (encOption encBool) encBits p).length) := by
-  have hp := fst (encOption encBool) encBits
-  have hds := snd (encOption encBool) encBits
-  have htest := (of_linear (.of_finite (encIn := encOption encBool) (encMid := encBool)
-    fun o : Option Bool => decide (o = some true))).comp_linear hp
-  have happ := hds.append (of_linear (.const (encMid := encBool) true)) (encOut := encBits)
-    (g := fun p : Option Bool × List Bool => p.2 ++ [true]) fun _ => rfl
-  unfold normFinish
-  simpa only [Function.comp_apply, Bool.decide_iff] using
-    (htest.ite happ hds).mono (T' := fun p => (encPair (encOption encBool) encBits p).length)
-      (S' := fun p => (encPair (encOption encBool) encBits p).length) 3
-      (fun _ => by split_ifs <;> omega) (fun _ => by split_ifs <;> omega)
-
 /-- Appending the final carry has linear time and charged workspace. -/
 theorem succFinish :
     ComputableInO NatSucc.succFinish (encPair encBool encBits) encBits
@@ -124,28 +63,6 @@ theorem succFinish :
       (S' := fun p => (encPair encBool encBits p).length) 3
       (fun _ => by split_ifs <;> omega) (fun _ => by split_ifs <;> omega)
 
-/-- A fold over binary words retains quadratic time and linear charged workspace when its
-reachable encoded prefix states have length at most the original word length plus a constant. -/
-theorem foldl_bits {β : Type} {encB : β ↪ List Bool} {init : β} {step : β → Bool → β}
-    (hstep : ComputableInO (fun p : β × Bool => step p.1 p.2)
-      (encPair encB encBool) encB
-      (fun p => (encPair encB encBool p).length)
-      (fun p => (encPair encB encBool p).length)) (b : ℕ)
-    (hb : ∀ (l : List Bool) i, (encB ((l.take i).foldl step init)).length ≤ l.length + b) :
-    ComputableInO (fun l : List Bool => l.foldl step init) encBits encB
-      (fun l => (l.length + 1) ^ 2) (fun l => l.length + 1) := by
-  refine (foldl (encA := encBool) (encL := encBits) (of_eq fun _ => rfl)
-    (of_linear (.const init)) hstep
-    (R := fun l => 2 * l.length + 2 * b + 4)
-    (Q := fun l => 2 * l.length + 2 * b + 4) (B := fun l => l.length + b)
-    (fun l i _ => by have := hb l i; simp only [length_encPair, encBool_apply]; simp; omega)
-    (fun l i _ => by have := hb l i; simp only [length_encPair, encBool_apply]; simp; omega)
-    (fun l i _ => hb l i)).mono (6 * b + 16) (fun l => ?_) (fun l => ?_)
-  · simp only [encBits_apply]
-    nlinarith [Nat.zero_le (b * l.length)]
-  · simp only [encBits_apply]
-    nlinarith
-
 /-- Binary successor within the quadratic clock and linear charged workspace used by its
 clients, weakened from the linear-time, zero-work-space transducer certificate
 `computableInTimeAndSpace_succ`. -/
@@ -154,48 +71,20 @@ theorem natSucc :
       (fun n => (encNat n).length + 1) :=
   (of_linear .natSucc).mono_le (fun n => by simp only [encNat_apply]; nlinarith) fun _ => by omega
 
-/-- Binary predecessor keeps zero at zero and preserves the original independent resource bounds. -/
+/-- Binary predecessor within the quadratic clock and linear charged workspace used by its
+clients, weakened from the linear-time, zero-work-space transducer certificate
+`computableInTimeAndSpace_pred`. -/
 theorem natPred :
     ComputableInO (· - 1) encNat encNat (fun n => ((encNat n).length + 1) ^ 2)
-      (fun n => (encNat n).length + 1) := by
-  have hlen (l : List Bool) : ((l.foldl decrStep (true, [])).2).length = l.length := by
-    rw [foldl_decrStep]
-    simp only [↓reduceIte, List.nil_append, length_decr]
-  have hdecr := foldl_bits (init := (true, [])) decrStep_inO 3 fun l i => by
-    have := hlen (l.take i)
-    have := List.length_take_le' i l
-    simp only [length_encPair, encBool_apply, List.length_singleton, encBits_apply]
-    omega
-  have hnorm := foldl_bits (init := (none, [])) normStep_inO 5 fun l i => by
-    have h₁ := length_foldl_normStep (l.take i) none []
-    have h₂ := List.length_take_le' i l
-    have h₃ : (encOption encBool ((l.take i).foldl normStep (none, [])).1).length ≤ 2 := by
-      cases ((l.take i).foldl normStep (none, [])).1 <;> simp
-    simp only [length_encPair, encBits_apply] at h₁ ⊢
-    simp only [List.length_nil, Option.toList_none, Nat.zero_add] at h₁
-    omega
-  have hword := (normFinish_inO.comp_linear (hnorm.comp hdecr.snd')).mono
-    (T' := fun l => (l.length + 1) ^ 2) (S' := fun l => l.length + 1) 4
-    (fun l => by simp only [hlen]; nlinarith)
-    (fun l => by simp only [hlen]; omega)
-  refine (hword.of_encIn_eq (encD := encNat) Nat.bits (fun _ => rfl)).of_enc_eq fun n => ?_
-  simp only [encNat_apply, encBits_apply, Function.comp_apply, NatPred.bits_pred,
-    normFinish_foldl, foldl_decrStep, Option.toList_none, List.nil_append,
-    ↓reduceIte]
+      (fun n => (encNat n).length + 1) :=
+  (of_linear .natPred).mono_le (fun n => by simp only [encNat_apply]; nlinarith) fun _ => by omega
 
-/-- Zero testing is linear in both resources; the output charge remains explicit. -/
+/-- Zero testing is linear in both resources, weakened from the transducer certificate
+`computableInTimeAndSpace_isZero`; the output charge remains explicit. -/
 theorem natIsZero :
     ComputableInO (fun n => decide (n = 0)) encNat encBool
-      (fun n => (encNat n).length) (fun n => (encNat n).length) := by
-  have hlinear : ComputableInLinearTimeAndSpace List.isEmpty encBits encBool := by
-    obtain ⟨c, k, Q, hfin, tm, htm⟩ := ListEncoding.isEmpty
-      (enc₁ := encBool) (enc := encBits)
-    exact ⟨c, k, Q, hfin, tm, fun l => htm l⟩
-  refine ((of_linear hlinear).of_encIn_eq (encD := encNat) Nat.bits
-    (fun _ => rfl)).of_enc_eq fun n => ?_
-  rcases Nat.eq_zero_or_pos n with rfl | hn
-  · rfl
-  · simp [bits_ne_nil (Nat.pos_iff_ne_zero.mp hn), hn.ne']
+      (fun n => (encNat n).length) (fun n => (encNat n).length) :=
+  of_linear .natIsZero
 
 end ComputableInO
 end Turing.MultiTapeTM
diff --git a/ComplexityTests/Encodings.lean b/ComplexityTests/Encodings.lean
index 91f45fb43..198aab9ff 100644
--- a/ComplexityTests/Encodings.lean
+++ b/ComplexityTests/Encodings.lean
@@ -37,4 +37,24 @@ example : ComputableInTimeAndSpace (fun n : ℕ => encNat (n + 1)) encNat encBit
 example (n : ℕ) : (encNat (n + 1)).length ≤ 2 * (encNat n).length + 3 :=
   computableInTimeAndSpace_succ.length_le n
 
+-- Binary predecessor and zero test: one transducer each, with the same exact bounds.
+example : ComputableInTimeAndSpace (fun n : ℕ => encNat (n - 1)) encNat encBits
+    (fun n => 2 * (encNat n).length + 3) (fun _ => 0) :=
+  let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_pred
+  ⟨k, Q, hQ, tm, h⟩
+
+example : ComputableInTimeAndSpace (fun n : ℕ => encBool (decide (n = 0))) encNat encBits
+    (fun n => 2 * (encNat n).length + 3) (fun _ => 0) :=
+  let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_isZero
+  ⟨k, Q, hQ, tm, h⟩
+
+-- Concrete instances: the borrow out of `4 = 0b100` drops the leading digit, `0 - 1 = 0`, and the
+-- clock for `4` (three digits) is `9` steps.
+example : encNat (4 - 1) = [true, true] ∧ encNat (0 - 1) = [] ∧
+    encNat (6 - 1) = [true, false, true] ∧ (fun n => 2 * (encNat n).length + 3) 4 = 9 := by
+  decide
+
+example : encBool (decide ((0 : ℕ) = 0)) = [true] ∧ encBool (decide ((4 : ℕ) = 0)) = [false] := by
+  decide
+
 end ComplexityTests.Encodings
diff --git a/ComplexityTests/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean b/ComplexityTests/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
index 06d2f2ead..662793974 100644
--- a/ComplexityTests/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
+++ b/ComplexityTests/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
@@ -22,7 +22,7 @@ run_elab do
 
 namespace ComplexityTests.Internal.BinaryPrimitives
 
--- Unbounded carry/borrow chains are verified for the actual folds, then specialized to long words.
+-- Unbounded carry chains are verified for the actual folds, then specialized to long words.
 theorem carryChain (k : ℕ) :
     NatSucc.succFinish ((List.replicate k true).foldl NatSucc.succStep (true, [])) =
       List.replicate k false ++ [true] := by
@@ -33,16 +33,7 @@ theorem carryChain (k : ℕ) :
     simpa only [List.replicate_succ, NatSucc.incr, List.cons_append] using
       congrArg (List.cons false) ih
 
-theorem borrowChain (k : ℕ) :
-    NatPred.norm (NatPred.decr (List.replicate k false ++ [true])) =
-      List.replicate k true := by
-  induction k with
-  | zero => rfl
-  | succ k ih =>
-    simp only [List.replicate_succ, List.cons_append, NatPred.decr]
-    rw [NatPred.norm_cons (NatPred.decr_ne_nil (by simp)), ih]
-
--- Uniform certificates on all natural numbers, carry/borrow boundary equations, and independent
+-- Uniform certificates on all natural numbers, carry boundary equations, and independent
 -- workspace/output charges.
 example (n : ℕ) {f : ℕ → ℕ} {t s T S : ℕ → ℕ}
     (h : ComputableInTimeAndSpace f encNat encNat t s)
@@ -60,27 +51,21 @@ example (n : ℕ) {f : ℕ → ℕ} {t s T S : ℕ → ℕ}
       ∀ n, (encNat (n - 1)).length ≤ c * ((encNat n).length + 1 + 1)) ∧
     NatSucc.succFinish ([].foldl NatSucc.succStep (true, [])) = [true] ∧
     NatSucc.succFinish ([true].foldl NatSucc.succStep (true, [])) = [false, true] ∧
-    NatPred.norm (NatPred.decr []) = [] ∧
-    NatPred.norm (NatPred.decr [true]) = [] ∧
-    NatPred.norm (NatPred.decr [false, false, true]) = [true, true] ∧
     NatSucc.incr true [true, true, true] = [false, false, false, true] ∧
     NatSucc.succFinish ((List.replicate 128 true).foldl NatSucc.succStep (true, [])) =
       List.replicate 128 false ++ [true] ∧
-    NatPred.norm (NatPred.decr (List.replicate 128 false ++ [true])) =
-      List.replicate 128 true ∧
     (encNat 0).isEmpty = true ∧
     (encNat 1).isEmpty = false ∧
     encNat (n + 1) = NatSucc.succFinish ((encNat n).foldl NatSucc.succStep (true, [])) ∧
-    encNat (n - 1) = NatPred.norm (NatPred.decr (encNat n)) ∧
     encNat 0 = [] ∧
     encNat 1 = [true] ∧
     (¬ ComputableInO (fun w : List Bool => w) encBits encBits
       (fun w => (w.length + 1) ^ 2) (fun _ => 0)) ∧
     ComputableInO f encNat encNat T S := by
   refine ⟨.natSucc, .natPred, .natIsZero, ComputableInO.natPred,
-    rfl, rfl, rfl, rfl, rfl, rfl, carryChain 128, borrowChain 128, rfl, rfl,
+    rfl, rfl, rfl, carryChain 128, rfl, rfl,
     by simp only [encNat_apply, NatSucc.succFinish_foldl, List.nil_append, NatSucc.bits_succ],
-    NatPred.bits_pred n, rfl, rfl, ?_, ?_⟩
+    rfl, rfl, ?_, ?_⟩
   · rintro ⟨c, _, hl'⟩
     have hlen := hl' (List.replicate (c + 1) true)
     simp only [encBits_apply, List.length_replicate, Nat.zero_add, Nat.mul_one] at hlen