Iterating the fixed sparse TM transition -- proof internals #
theorem
Complexity.RAM.TMConfig.Sparse.continueCheck_exec_internal
{n : ℕ}
{tm : TM n}
{cfg : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hrepresents : Represents tm cfg store)
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (continueCheck tm) store final (continueSteps tm cfg) cost space ∧ Represents tm cfg final ∧ final (valueReg n) = runningFlag tm cfg.state ∧ final (oneReg n) = 1 ∧ final (tapeCountReg n) = n + 2
theorem
Complexity.RAM.TMConfig.Sparse.loop_exec_internal
{n : ℕ}
{tm : TM n}
{steps : ℕ}
{cfg halted : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hreach : tm.reachesIn steps cfg halted)
(hhalted : tm.halted halted)
(hrepresents : Represents tm cfg store)
(hflag : store (valueReg n) = runningFlag tm cfg.state)
(hworkStart : ∀ (i : Fin n), (cfg.work i).cells 0 = Γ.start)
(houtputStart : cfg.output.cells 0 = Γ.start)
:
∃ (final : Structured.Store) (cost : ℕ) (space : ℕ),
Structured.Exec (Structured.Cmd.whileNonzero (valueReg n) (loopBody tm)) store final (loopSteps tm steps cfg) cost
space ∧ Represents tm halted final
theorem
Complexity.RAM.TMConfig.Sparse.runUntilHalt_exec_internal
{n : ℕ}
{tm : TM n}
{steps : ℕ}
{cfg halted : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hreach : tm.reachesIn steps cfg halted)
(hhalted : tm.halted halted)
(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 (runUntilHalt tm) store final (runSteps tm steps cfg) cost space ∧ Represents tm halted final