Direct binary counter resource certificates

The successor, predecessor and zero test certificates here are weakenings of the streaming transducer certificates computableInTimeAndSpace_succ, computableInTimeAndSpace_pred and computableInTimeAndSpace_isZero.

Main results

• ComputableInO.natSucc, ComputableInO.natPred: binary counters within the quadratic clock and linear charged workspace used by their clients.
• ComputableInO.natIsZero: linear zero testing.

theorem Turing.MultiTapeTM.ComputableInO.natSucc : ComputableInO (fun (x : ℕ) => x + 1) encNat encNat (fun (n : ℕ) => ((encNat n).length + 1) ^ 2) fun (n : ℕ) => (encNat n).length + 1

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.

theorem Turing.MultiTapeTM.ComputableInO.natPred : ComputableInO (fun (x : ℕ) => x - 1) encNat encNat (fun (n : ℕ) => ((encNat n).length + 1) ^ 2) fun (n : ℕ) => (encNat n).length + 1

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 Turing.MultiTapeTM.ComputableInO.natIsZero : ComputableInO (fun (n : ℕ) => decide (n = 0)) encNat encBool (fun (n : ℕ) => (encNat n).length) fun (n : ℕ) => (encNat n).length

Zero testing is linear in both resources, weakened from the transducer certificate computableInTimeAndSpace_isZero; the output charge remains explicit.