Reading arbitrary little-endian natural-number words

The existing word interpretation and normalization identity are independent of machine or complexity certificates. Trailing false symbols are ignored, and the empty word represents zero.

Main definitions

• Turing.MultiTapeTM.ofBits: read little-endian digits as a natural number.

Main results

• Turing.MultiTapeTM.bits_ofBits: normalize a word by removing its trailing false symbols.
• Turing.MultiTapeTM.length_encNat_ofBits_le: a word read as a number has at most as many binary digits as the word.
• Turing.MultiTapeTM.bits_add_two_pow: the binary digits of x + 2 ^ W, for x < 2 ^ W, are the W low-order digits of x (Cslib.BitString.lowBits) followed by a one.

def Turing.MultiTapeTM.ofBits (w : List Bool) : ℕ

Binary digits, least significant first, read as a number.

theorem Turing.MultiTapeTM.bits_ofBits (w : List Bool) : (ofBits w).bits = List.rdropWhile (fun (x : Bool) => !x) w

The binary digits of a word read as a number are the word up to its last true.

theorem Turing.MultiTapeTM.length_encNat_ofBits_le (w : List Bool) : (encNat (ofBits w)).length ≤ w.length

A word read as a number has at most as many binary digits as the word.

theorem Turing.MultiTapeTM.bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : (x + 2 ^ W).bits = Cslib.BitString.lowBits W x ++ [true]

The binary digits of x + 2 ^ W, for x < 2 ^ W, are the W low-order digits of x, followed by a one.

theorem Turing.MultiTapeTM.dropLast_bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : (x + 2 ^ W).bits.dropLast = Cslib.BitString.lowBits W x

The W low-order digits of x < 2 ^ W are (x + 2 ^ W).bits without its last digit.