Nested finite dispatch for the fixed sparse TM transition -- proof internals #
theorem
Complexity.RAM.TMConfig.Sparse.dispatchSymbols_exec_internal
{n : ℕ}
{tm : TM n}
{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 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)
(hactual : actual = readSymbols cfg)
(hloaded : ∀ tape ∈ remaining, store (symbolReg n tape) = symbolCode (actual tape))
(hassigned : ∀ tape ∉ remaining, symbols tape = actual tape)
(hnodup : remaining.Nodup)
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (dispatchSymbols tm state remaining symbols) store final (dispatchSteps tm state actual remaining)
cost space ∧ Represents tm next final
theorem
Complexity.RAM.TMConfig.Sparse.dispatchState_exec_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)
(hstate : store (stateScratchReg n) = stateCode tm cfg.state)
(hloaded : ∀ (tape : Fin (n + 2)), store (symbolReg n tape) = symbolCode (readSymbols cfg tape))
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (dispatchState tm) store final
(Structured.Switch.stepCount (stateCode tm cfg.state)
(dispatchSteps tm cfg.state (readSymbols cfg) (List.finRange (n + 2))))
cost space ∧ Represents tm next final
theorem
Complexity.RAM.TMConfig.Sparse.program_exec_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)
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (program tm) store final (stepCount tm cfg) cost space ∧ Represents tm next final
@[reducible, inline]
abbrev
Complexity.RAM.TMConfig.Sparse.ResourceEnvelope
{n : ℕ}
(tm : TM n)
(bound : ℕ)
(store : Structured.Store)
:
Register and word bounds preserved by sparse step dispatch.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.RAM.TMConfig.Sparse.dispatchSymbols_measured_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 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)
(hactual : actual = readSymbols cfg)
(hloaded : ∀ tape ∈ remaining, store (symbolReg n tape) = symbolCode (actual tape))
(hassigned : ∀ tape ∉ remaining, symbols tape = actual tape)
(hnodup : remaining.Nodup)
(henvelope : ResourceEnvelope tm bound store)
:
∃ (final : Structured.Store),
Structured.Internal.MeasuredRuns (dispatchSymbols tm state remaining symbols) store final
(dispatchSteps tm state actual remaining) (dispatchCost tm bound state actual remaining) (spaceBound tm bound) ∧ Represents tm next final ∧ ResourceEnvelope tm bound final
theorem
Complexity.RAM.TMConfig.Sparse.dispatchState_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)
(hstate : store (stateScratchReg n) = stateCode tm cfg.state)
(hloaded : ∀ (tape : Fin (n + 2)), store (symbolReg n tape) = symbolCode (readSymbols cfg tape))
(henvelope : ResourceEnvelope tm bound store)
:
∃ (final : Structured.Store),
Structured.Internal.MeasuredRuns (dispatchState tm) store final
(Structured.Switch.stepCount (stateCode tm cfg.state)
(dispatchSteps tm cfg.state (readSymbols cfg) (List.finRange (n + 2))))
(Structured.Switch.costBound (stateCode tm cfg.state)
(dispatchCost tm bound cfg.state (readSymbols cfg) (List.finRange (n + 2))) (wordWidth tm bound))
(spaceBound tm bound) ∧ Represents tm next final ∧ ResourceEnvelope tm bound final