Direct certificates for total decoder leaves

These witnesses apply to every input word, with the original independent degree-one cost and output bounds. The type-indexed Decoder field can reuse them without a higher tidy calculus.

theorem Turing.MultiTapeTM.Internal.DecoderWords.bits_degree : ComputableInDegree id encBits encBits 1 1

A runtime word decodes to itself.

theorem Turing.MultiTapeTM.Internal.DecoderWords.unary_degree : ComputableInDegree List.length encBits encUnary 1 1

The unary decoder counts every symbol, including malformed false symbols.

theorem Turing.MultiTapeTM.Internal.DecoderWords.bool_degree : ComputableInDegree (fun (w : List Bool) => w.headD false) encBits encBool 1 1

The Boolean decoder returns false on empty input and the first symbol otherwise.

theorem Turing.MultiTapeTM.Internal.DecoderWords.tail_degree : ComputableInDegree List.tail encBits encBits 1 1

The existing bit-list codec machine drops one symbol, including on empty input.

theorem Turing.MultiTapeTM.Internal.DecoderWords.empty_degree : ComputableInDegree List.isEmpty encBits encBool 1 1

The existing bit-list codec machine tests whether the complete input is empty.

theorem Turing.MultiTapeTM.Internal.DecoderWords.unframe_degree : ComputableInDegree unframe encBits encBits 1 1

Read the initial frame on every word, including incomplete frames.

theorem Turing.MultiTapeTM.Internal.DecoderWords.dropFrame_degree : ComputableInDegree dropFrame encBits encBits 1 1

Read what follows the initial frame on every word, including incomplete frames.