Materializing finite certificates from a witness stream

The bounded guess phase stores at most B bits on an ordinary charged work tape, controlled by an ordinary preloaded unary counter. It can stop early, so every finite certificate up to the bound is available, including the empty one. Only the external source stream is excluded from the space account.

def Complexity.WitnessTM.storeBounded {k : ℕ} (witness counter : Fin k) : WitnessTM k

The online phase that stores a bounded, reusable ordinary certificate.

Equations

• Complexity.WitnessTM.storeBounded witness counter = (Complexity.NTM.guessBoundedNTM witness counter).toWitnessTM

def Complexity.WitnessTM.storeEntry {k : ℕ} (inp₀ : Tape) (work₀ : Fin k → Tape) (out₀ source : Tape) : TapePred (k + 1)

Exact entry frame for a materialization phase.

Equations

• Complexity.WitnessTM.storeEntry inp₀ work₀ out₀ source inp work out = (inp = inp₀ ∧ work = Fin.snoc work₀ source ∧ out = out₀)

def Complexity.WitnessTM.storePost {k : ℕ} (witness counter : Fin k) (B : ℕ) (inp₀ : Tape) (work₀ : Fin k → Tape) (out₀ source : Tape) : TapePred (k + 1)

A stored certificate with all unrelated tapes framed, and a source stream whose cells are unchanged and whose cursor advances by at most the phase time.

Equations

• One or more equations did not get rendered due to their size.