Nested finite dispatch for one TM transition -- proof internals #
theorem
Complexity.RAM.TMConfig.Step.dispatchSymbols_exec_internal
{n : ℕ}
{tm : TM n}
{bound : ℕ}
{cfg next : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(state : tm.Q)
(actual symbols : Fin (n + 2) → Γ)
(remaining : List (Fin (n + 2)))
(hstate : state = cfg.state)
(hstep : tm.step cfg = some next)
(hrepresents : Represents tm bound 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 bound) = 1)
(hactual : actual = readSymbols cfg)
(hloaded : ∀ tape ∈ remaining, store (symbolReg n bound tape) = symbolCode (actual tape))
(hassigned : ∀ tape ∉ remaining, symbols tape = actual tape)
(hnodup : remaining.Nodup)
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (dispatchSymbols tm bound state remaining symbols) store final
(dispatchSteps tm bound state actual remaining) cost space ∧ Represents tm bound next final
theorem
Complexity.RAM.TMConfig.Step.dispatchState_exec_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 bound 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 bound) = 1)
(hstate : store (stateScratchReg n bound) = stateCode tm cfg.state)
(hloaded : ∀ (tape : Fin (n + 2)), store (symbolReg n bound tape) = symbolCode (readSymbols cfg tape))
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (dispatchState tm bound) store final
(Structured.Switch.stepCount (stateCode tm cfg.state)
(dispatchSteps tm bound cfg.state (readSymbols cfg) (List.finRange (n + 2))))
cost space ∧ Represents tm bound next final
theorem
Complexity.RAM.TMConfig.Step.program_exec_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 bound cfg store)
(hwindow : WithinWindow cfg bound)
(hworkStart : ∀ (i : Fin n), (cfg.work i).cells 0 = Γ.start)
(houtputStart : cfg.output.cells 0 = Γ.start)
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (program tm bound) store final (stepCount tm bound cfg) cost space ∧ Represents tm bound next final