Encodings of lists

encList enc encodes a list as the concatenation of its framed elements (Turing.MultiTapeTM.frame), for any encoding enc of the elements. Lists of Booleans also have the plain encoding encBits, the list itself, which is the concatenation of the elements encoded by Turing.MultiTapeTM.encBool. Both have the capabilities of Turing.MultiTapeTM.ListEncoding.

Main definitions

• Turing.MultiTapeTM.encList: the concatenation of the framed elements.
• Turing.MultiTapeTM.encBits: lists of Booleans encoded as themselves.

def Turing.MultiTapeTM.encList {α : Type u} (enc : α ↪ List Bool) : List α ↪ List Bool

Lists encoded as the concatenation of their framed elements.

@[simp]

theorem Turing.MultiTapeTM.encList_nil {α : Type u} {enc : α ↪ List Bool} : (encList enc) [] = []

@[simp]

theorem Turing.MultiTapeTM.encList_cons {α : Type u} {enc : α ↪ List Bool} (a : α) (l : List α) : (encList enc) (a :: l) = frame (enc a) ++ (encList enc) l

instance Turing.MultiTapeTM.instListEncodingEncList {α : Type u} {enc : α ↪ List Bool} : ListEncoding enc (encList enc)

def Turing.MultiTapeTM.encBits : List Bool ↪ List Bool

Lists of Booleans encoded as themselves.

@[simp]

theorem Turing.MultiTapeTM.encBits_apply (l : List Bool) : encBits l = l

instance Turing.MultiTapeTM.instListEncodingBoolEncBoolEncBits : ListEncoding encBool encBits