Tagged sum encodings

A Boolean tag selects the payload encoding: false for the left summand and true for the right summand. This permits differently encoded, possibly empty summands without padding.

Main definitions

• Turing.MultiTapeTM.encSum: a tagged sum of two supplied encodings.

def Turing.MultiTapeTM.encSum {α : Type u_1} {β : Type u_2} (left : α ↪ List Bool) (right : β ↪ List Bool) : α ⊕ β ↪ List Bool

Encode a sum with one tag bit followed by the corresponding payload.

@[simp]

theorem Turing.MultiTapeTM.encSum_inl {α : Type u_1} {β : Type u_2} (left : α ↪ List Bool) (right : β ↪ List Bool) (a : α) : (encSum left right) (Sum.inl a) = false :: left a

@[simp]

theorem Turing.MultiTapeTM.encSum_inr {α : Type u_1} {β : Type u_2} (left : α ↪ List Bool) (right : β ↪ List Bool) (b : β) : (encSum left right) (Sum.inr b) = true :: right b

theorem Turing.MultiTapeTM.length_encSum {α : Type u_1} {β : Type u_2} (left : α ↪ List Bool) (right : β ↪ List Bool) (value : α ⊕ β) : ((encSum left right) value).length = Sum.elim (fun (a : α) => (left a).length) (fun (b : β) => (right b).length) value + 1

The encoding charges the selected payload and exactly one tag bit.