The length of a bit word as universal-machine symbols

A word of bits handed to the universal machine is the framed list of its symbols x.map Turing.MultiTapeTM.Universal.eBit, each written in unary. Every symbol is 0 or 1, so this encoding is at most three times as long as the word. The diagonal arguments of the hierarchy theorems and the time-space speedup bound the universal machine's input this way.

Main results

• Turing.MultiTapeTM.Universal.length_encList_map_eBit_le: the symbol encoding of x is at most 3 * x.length long.

theorem Turing.MultiTapeTM.Universal.length_encList_map_eBit_le (x : List Bool) : ((encList encUnary) (List.map (⇑eBit) x)).length ≤ 3 * x.length

A bit word as symbols is linear: the unary symbols 0 and 1 of x take at most 3 * x.length bits as a framed list.