Total binary-number decoding

Binary digits are read least significant first. Trailing false symbols are ignored, including on malformed words, and empty input returns zero. The decoder satisfies the encoding round-trip law and has a certificate from direct plain machines.

def Turing.MultiTapeTM.Decoder.nat : Decoder encNat

Binary numbers are decoded from their digits up to the last true.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsToNat : ComputableInPolyTime ofBits encBits encNat

Decode every little-endian bit word, including noncanonical trailing false symbols.