Selected TM transition actions -- proof internals #
theorem
Complexity.RAM.TMConfig.Step.writeMoveOps_one_internal
(n bound : ℕ)
(slot : Fin (n + 2))
(write : Γw)
(direction : Dir3)
(store : Structured.Store)
(hhead : store (headReg slot) ≤ bound)
:
Structured.Basic.execList (writeMoveOps n bound slot write direction) store (oneReg n bound) = store (oneReg n bound)
theorem
Complexity.RAM.TMConfig.Step.actionOps_represents_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)
:
Represents tm bound next (Structured.Basic.execList (actionOps tm bound cfg.state (readSymbols cfg)) store)
theorem
Complexity.RAM.TMConfig.Step.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 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)
(henvelope : Structured.Internal.StoreEnvelope (registerLimit n bound) (wordBound tm bound) store)
:
have final := Structured.Basic.execList (actionOps tm bound cfg.state (readSymbols cfg)) store;
Structured.Internal.MeasuredRuns (action tm bound cfg.state (readSymbols cfg)) store final
(actionOps tm bound cfg.state (readSymbols cfg)).length
(4 * (actionOps tm bound cfg.state (readSymbols cfg)).length * wordWidth tm bound) (spaceBound tm bound) ∧ Represents tm bound next final ∧ Structured.Internal.StoreEnvelope (registerLimit n bound) (wordBound tm bound) final