Direct unary degree primitives

Streaming machines implement successor and saturating predecessor with linear cost and output growth. No higher tidy computability calculus is used.

theorem Turing.MultiTapeTM.ComputableInDegree.unary_succ : ComputableInDegree (fun (x : ℕ) => x + 1) encUnary encUnary 1 1

Successor on unary natural numbers, including the empty encoding of zero.

theorem Turing.MultiTapeTM.ComputableInDegree.unary_pred : ComputableInDegree (fun (x : ℕ) => x - 1) encUnary encUnary 1 1

Saturating predecessor on unary natural numbers.

theorem Turing.MultiTapeTM.ComputableInDegree.unary_isZero : ComputableInDegree (fun (n : ℕ) => decide (n = 0)) encUnary encBool 1 1

The unary zero test preserves the original linear cost and output-degree contract.