Encoded sizes when selecting from lists and options

The optional head of a framed list and a value selected from an option have size bounds that include the option tag and a possible default. These facts do not require a computation certificate.

Main results

• Turing.MultiTapeTM.length_encOption_head?_le: bound the encoded optional head by the encoded list.
• Turing.MultiTapeTM.length_enc_getD_le: bound an encoded selected value by the option and its default.

theorem Turing.MultiTapeTM.length_encOption_head?_le {β : Type} {encB : β ↪ List Bool} (l : List β) : ((encOption encB) l.head?).length ≤ ((encList encB) l).length + 1

The encoded optional head is bounded by the encoded list plus its option tag.

theorem Turing.MultiTapeTM.length_enc_getD_le {γ : Type} {encC : γ ↪ List Bool} [Inhabited γ] (o : Option γ) : (encC (o.getD default)).length ≤ ((encOption encC) o).length + (encC default).length

Selecting an option value or its default charges the option and the encoded default.