Selected sparse TM transition actions -- proof internals #
theorem
Complexity.RAM.TMConfig.Sparse.actionOps_represents_internal
{n : ℕ}
{tm : TM n}
{cfg next : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hstep : tm.step cfg = some next)
(hrepresents : Represents tm cfg store)
(hworkStart : ∀ (i : Fin n), (cfg.work i).cells 0 = Γ.start)
(houtputStart : cfg.output.cells 0 = Γ.start)
(hone : store (oneReg n) = 1)
(htapeCount : store (tapeCountReg n) = n + 2)
:
Represents tm next (Structured.Basic.execList (actionOps tm cfg.state (readSymbols cfg)) store)
theorem
Complexity.RAM.TMConfig.Sparse.actionOps_measured_internal
{n : ℕ}
{tm : TM n}
{bound : ℕ}
{cfg next : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hstep : tm.step cfg = some next)
(hrepresents : Represents tm cfg store)
(hheads : HeadsBounded cfg bound)
(hworkStart : ∀ (i : Fin n), (cfg.work i).cells 0 = Γ.start)
(houtputStart : cfg.output.cells 0 = Γ.start)
(hone : store (oneReg n) = 1)
(htapeCount : store (tapeCountReg n) = n + 2)
(henvelope : Structured.Internal.StoreEnvelope (registerBound n (bound + 1)) (wordBound tm bound) store)
:
have final := Structured.Basic.execList (actionOps tm cfg.state (readSymbols cfg)) store;
Structured.Internal.MeasuredRuns (action tm cfg.state (readSymbols cfg)) store final
(actionOps tm cfg.state (readSymbols cfg)).length
(4 * (actionOps tm cfg.state (readSymbols cfg)).length * wordWidth tm bound) (spaceBound tm bound) ∧ Represents tm next final ∧ Structured.Internal.StoreEnvelope (registerBound n (bound + 1)) (wordBound tm bound) final