Subtraction and comparison in binary

Truncated subtraction b - a iterates the predecessor a times, counting in binary. It takes time linear in the value a and work space linear in the lengths of the binary encodings. The order a < b tests whether b - a is zero.

Main results

• Turing.MultiTapeTM.ComputableTidilyInO.natSub: truncated subtraction in binary.
• Turing.MultiTapeTM.ComputableTidilyInO.natLt: the strict order in binary.

theorem Turing.MultiTapeTM.ComputableTidilyInO.iterate_sub_one (k n : ℕ) : (fun (x : ℕ) => x - 1)^[k] n = n - k

theorem Turing.MultiTapeTM.ComputableTidilyInO.natSub : ComputableTidilyInO (fun (p : ℕ × ℕ) => p.2 - p.1) (encPair encNat encNat) encNat (fun (p : ℕ × ℕ) => (p.1 + 1) * (((encPair encNat encNat) p).length + 1) ^ 2) fun (p : ℕ × ℕ) => ((encPair encNat encNat) p).length + 1

Truncated subtraction in binary, b - a from (a, b).

theorem Turing.MultiTapeTM.ComputableTidilyInO.natLt : ComputableTidilyInO (fun (p : ℕ × ℕ) => decide (p.1 < p.2)) (encPair encNat encNat) encBool (fun (p : ℕ × ℕ) => (p.1 + 1) * (((encPair encNat encNat) p).length + 1) ^ 2) fun (p : ℕ × ℕ) => ((encPair encNat encNat) p).length + 1

The strict order in binary.