The successor in binary, as a streaming fold

The successor on Turing.MultiTapeTM.encNat reads the digits once, least significant first, keeping the carry as its state: it emits each digit plus the carry and, at the end, a final carry digit. As a streaming fold (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.streamFold) it is tidily computable in linear time and constant space.

Main results

• Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ_stream: the successor is tidily computable in linear time and constant space.

theorem Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ_stream : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (x : ℕ) => x + 1) encNat encNat (fun (n : ℕ) => c * ((encNat n).length + 1)) fun (x : ℕ) => c

The successor is tidily computable in linear time and constant space, in the binary encoding encNat.