Binary natural encoding and carry increment

This module defines the little-endian binary encoding Turing.MultiTapeTM.encNat of natural numbers (Nat.bits) and the carry-propagation step Turing.MultiTapeTM.NatSucc.incr for binary successor, independent of machine resource certificates.

Main definitions

• Turing.MultiTapeTM.encNat: natural numbers encoded by their binary digits, least significant first.
• Turing.MultiTapeTM.NatSucc.incr: adds an incoming carry bit to a little-endian binary word.

Main statements

• Turing.MultiTapeTM.encNat_apply: unfolding encNat n to n.bits.
• Turing.MultiTapeTM.NatSucc.bits_succ: (n + 1).bits = incr true n.bits.

def Turing.MultiTapeTM.encNat : ℕ ↪ List Bool

Natural numbers encoded by their binary digits, least significant first.

@[simp]

theorem Turing.MultiTapeTM.encNat_apply (n : ℕ) : encNat n = n.bits

encNat n is the little-endian binary digit list n.bits.

def Turing.MultiTapeTM.NatSucc.incr : Bool → List Bool → List Bool

Adds the carry c to the binary digits l, least significant first.

theorem Turing.MultiTapeTM.NatSucc.bits_succ (n : ℕ) : (n + 1).bits = incr true n.bits

The binary digits of n + 1 are obtained by incrementing n.bits with carry true.