The framed encoding of pairs

encPair enc₁ enc₂ encodes a pair as its framed first component (Turing.MultiTapeTM.frame) followed by its second component. It has the capabilities of Turing.MultiTapeTM.PairEncoding.

Main definitions

• Turing.MultiTapeTM.encFramed: an encoding with every encoded value framed.
• Turing.MultiTapeTM.encPair: the framed encoding of pairs.

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

enc with every encoded value framed.

def Turing.MultiTapeTM.encPair {α β : Type u} (enc₁ : α ↪ List Bool) (enc₂ : β ↪ List Bool) : α × β ↪ List Bool

Pairs encoded as the framed first component followed by the second component.

@[simp]

theorem Turing.MultiTapeTM.encFramed_apply {α : Type u} (enc : α ↪ List Bool) (a : α) : (encFramed enc) a = frame (enc a)

@[simp]

theorem Turing.MultiTapeTM.encPair_apply {α β : Type u} {enc₁ : α ↪ List Bool} {enc₂ : β ↪ List Bool} (p : α × β) : (encPair enc₁ enc₂) p = frame (enc₁ p.1) ++ enc₂ p.2

theorem Turing.MultiTapeTM.length_encPair {α β : Type u} {enc₁ : α ↪ List Bool} {enc₂ : β ↪ List Bool} (p : α × β) : ((encPair enc₁ enc₂) p).length = 2 * (enc₁ p.1).length + 1 + (enc₂ p.2).length

theorem Turing.MultiTapeTM.length_le_encPair_left {α β : Type u} (enc₁ : α ↪ List Bool) (enc₂ : β ↪ List Bool) (p : α × β) : (enc₁ p.1).length ≤ ((encPair enc₁ enc₂) p).length

theorem Turing.MultiTapeTM.length_le_encPair_right {α β : Type u} (enc₁ : α ↪ List Bool) (enc₂ : β ↪ List Bool) (p : α × β) : (enc₂ p.2).length ≤ ((encPair enc₁ enc₂) p).length

instance Turing.MultiTapeTM.instPairEncodingEncPair {α β : Type u} {enc₁ : α ↪ List Bool} {enc₂ : β ↪ List Bool} : PairEncoding enc₁ enc₂ (encPair enc₁ enc₂)