Read-only work-tape certificates

TM.WorkReadOnly tm idx records the local syntactic fact that every transition of tm writes the symbol already read on work tape idx. The head may move, but valid tape contents are preserved through every finite run.

def Complexity.TM.WorkReadOnly {n : ℕ} (tm : TM n) (idx : Fin n) : Prop

Every transition writes back the symbol read on the selected work tape.

Equations

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

theorem Complexity.TM.WorkReadOnly.cells_eq_of_step {n : ℕ} {tm : TM n} {idx : Fin n} (hreadonly : tm.WorkReadOnly idx) {c c' : Cfg n tm.Q} (hstep : tm.step c = some c') (hnostart : ∀ (j : ℕ), 1 ≤ j → (c.work idx).cells j ≠ Γ.start) : (c'.work idx).cells = (c.work idx).cells

A read-only transition preserves all cells of a valid selected tape.

theorem Complexity.TM.WorkReadOnly.cells_eq_of_reachesIn {n : ℕ} {tm : TM n} {idx : Fin n} (hreadonly : tm.WorkReadOnly idx) {time : ℕ} {start final : Cfg n tm.Q} (hreach : tm.reachesIn time start final) (hnostart : ∀ (j : ℕ), 1 ≤ j → (start.work idx).cells j ≠ Γ.start) : (final.work idx).cells = (start.work idx).cells

A read-only work tape retains its complete cell function through an exact finite run.

theorem Complexity.TM.WorkReadOnly.seqTM {n : ℕ} {first second : TM n} {idx : Fin n} (hfirst : first.WorkReadOnly idx) (hsecond : second.WorkReadOnly idx) : (first.seqTM second).WorkReadOnly idx

Sequential composition preserves a shared read-only work tape.