Streaming machines for total decoder leaves

Both transducers are total on malformed as well as encoded words. They use no work tapes and the standard transducer clock includes every input symbol.

def Turing.MultiTapeTM.Internal.DecoderWords.unaryLengthT : Transducer Bool Unit

Replace each input symbol by one unary symbol.

theorem Turing.MultiTapeTM.Internal.DecoderWords.unaryLengthT_run (w : List Bool) : unaryLengthT.run () w = List.replicate w.length true

The emitted unary word records the length of every input word.

def Turing.MultiTapeTM.Internal.DecoderWords.headDefaultT (default : Bool) : Transducer Bool Bool

Read the first symbol, returning the fixed default on empty input.

theorem Turing.MultiTapeTM.Internal.DecoderWords.headDefaultT_run_true (default : Bool) (w : List Bool) : (headDefaultT default).run true w = []

After seeing the first symbol, this transducer emits nothing further.

theorem Turing.MultiTapeTM.Internal.DecoderWords.headDefaultT_run (default : Bool) (w : List Bool) : (headDefaultT default).run false w = [w.headD default]

The default applies exactly to empty input, with no resampling or partiality.

def Turing.MultiTapeTM.dropFalsesT : Transducer Bool Bool

Drops the falses at the start of a word.

theorem Turing.MultiTapeTM.dropFalsesT_run_true (w : List Bool) : dropFalsesT.run true w = w

theorem Turing.MultiTapeTM.dropFalsesT_run (w : List Bool) : dropFalsesT.run false w = List.dropWhile (fun (x : Bool) => !x) w