Linear conversion between raw and framed Boolean lists

The values are unchanged: only the existing encodings differ. Framing followed by a finite-state transducer inserts a delimiter after each bit; a second transducer removes those delimiters. Both directions have linear time, workspace and output length, without a fold over growing words.

Main results

• Turing.MultiTapeTM.ComputableInDegree.bitsToList: raw bits to framed Boolean elements.
• Turing.MultiTapeTM.ComputableInDegree.listToBits: framed Boolean elements to raw bits.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsToList : ComputableInDegree (fun (word : List Bool) => word) encBits (encList encBool) 1 1

Convert raw bits to the existing framed Boolean-list encoding in linear time and space.

theorem Turing.MultiTapeTM.ComputableInDegree.listToBits : ComputableInDegree (fun (word : List Bool) => word) (encList encBool) encBits 1 1

Remove Boolean-element framing in linear time and space, leaving the list unchanged.