Linear cuts of raw bit strings

Convert to framed Boolean elements, use the existing streaming unary list cutter, and remove framing. The complete raw word and unary count are charged. Counts beyond the word length and empty words need no additional hypotheses.

Main results

• Turing.MultiTapeTM.ComputableInDegree.bitsTake: take a unary number of raw bits.
• Turing.MultiTapeTM.ComputableInDegree.bitsDrop: drop a unary number of raw bits.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsTake : ComputableInDegree (fun (p : List Bool × ℕ) => List.take p.2 p.1) (encPair encBits encUnary) encBits 1 1

Take a unary number of bits with linear time, workspace and output length.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsDrop : ComputableInDegree (fun (p : List Bool × ℕ) => List.drop p.2 p.1) (encPair encBits encUnary) encBits 1 1

Drop a unary number of bits with linear time, workspace and output length.