Polynomial-time sum constructors

The two injections retain the supplied payload encoding and add its tag bit. Their certificates reuse the existing bit-string constructor and charge the entire payload, with no finite-domain assumption on either summand.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.sumInl, .sumInr: tagged sum construction.

theorem Turing.MultiTapeTM.ComputableInPolyTime.sumInl {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInPolyTime Sum.inl left (encSum left right)

Tag an encoded value as belonging to the left summand.

theorem Turing.MultiTapeTM.ComputableInPolyTime.sumInr {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInPolyTime Sum.inr right (encSum left right)

Tag an encoded value as belonging to the right summand.