Documentation

Complexity.Computability.Machines.Turing.MultiTape.Internal.LinearPairPrimitives

Direct linear projections of the standard framed pair encoding #

This separate consumer module keeps the word-machine core independent of pair codec providers.

source
theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.fst {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) :
ComputableInLinearTimeAndSpace Prod.fst (encPair enc₁ enc₂) enc₁

The first component of a standard framed pair.

source
theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.snd {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) :
ComputableInLinearTimeAndSpace Prod.snd (encPair enc₁ enc₂) enc₂

The second component of a standard framed pair.