Lengths of encoded lists

The framed encoding of a list (Turing.MultiTapeTM.encList) spends 2 * |enc a| + 1 symbols on each element a. In particular the sum of the lengths of its encoded elements is no longer than the encoding, as is the list itself (Turing.MultiTapeTM.length_le_length_encList). Such bounds are what a reduction needs to bound the size of its output, or a verifier the length of a certificate, in terms of the input.

Main results

• Turing.MultiTapeTM.length_encList: the exact length.
• Turing.MultiTapeTM.sum_length_le_length_encList: the encoded elements are no longer, in total, than the encoded list.

theorem Turing.MultiTapeTM.length_encList {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : ((encList enc) l).length = (List.map (fun (a : α) => 2 * (enc a).length + 1) l).sum

@[simp]

theorem Turing.MultiTapeTM.length_encList_reverse {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : ((encList enc) l.reverse).length = ((encList enc) l).length

Reversing a list preserves the full encoded size, including each element's framing.

theorem Turing.MultiTapeTM.sum_length_le_length_encList {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : (List.map (fun (a : α) => (enc a).length) l).sum ≤ ((encList enc) l).length

The encoded elements of a list are no longer, in total, than the encoded list.