Resource bounds for one TM-to-RAM transition -- proof internals #
@[reducible, inline]
abbrev
Complexity.RAM.TMConfig.Step.StepEnvelope
{n : ℕ}
(tm : TM n)
(bound : ℕ)
(store : Structured.Store)
:
Register and word bounds preserved by a simulated Turing-machine step.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.RAM.TMConfig.Step.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 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)
(henvelope : StepEnvelope tm bound store)
:
∃ (final : Structured.Store),
Structured.Internal.MeasuredRuns (dispatchSymbols tm bound state remaining symbols) store final
(dispatchSteps tm bound state actual remaining) (dispatchCost tm bound state actual remaining)
(spaceBound tm bound) ∧ Represents tm bound next final ∧ StepEnvelope tm bound final
theorem
Complexity.RAM.TMConfig.Step.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 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))
(henvelope : StepEnvelope tm bound store)
:
∃ (final : Structured.Store),
Structured.Internal.MeasuredRuns (dispatchState tm bound) store final
(Structured.Switch.stepCount (stateCode tm cfg.state)
(dispatchSteps tm bound 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 bound next final ∧ StepEnvelope tm bound final
theorem
Complexity.RAM.TMConfig.Step.program_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 bound cfg store)
(hwindow : WithinWindow cfg bound)
(hworkStart : ∀ (i : Fin n), (cfg.work i).cells 0 = Γ.start)
(houtputStart : cfg.output.cells 0 = Γ.start)
(henvelope : StepEnvelope tm bound store)
:
∃ (final : Structured.Store),
Structured.Internal.MeasuredRuns (program tm bound) store final (stepCount tm bound cfg) (timeBound tm bound cfg)
(spaceBound tm bound) ∧ Represents tm bound next final ∧ StepEnvelope tm bound final