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.

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.