Sparse TM-step address and loading layout -- proof internals #
theorem
Complexity.RAM.TMConfig.Sparse.addressOps_represents_internal
{n : ℕ}
{tm : TM n}
{cfg : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hrepresents : Represents tm cfg store)
(tape : Fin (n + 2))
:
Represents tm cfg (Structured.Basic.execList (addressOps n tape) store)
theorem
Complexity.RAM.TMConfig.Sparse.loadTapeOps_represents_internal
{n : ℕ}
{tm : TM n}
{cfg : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hrepresents : Represents tm cfg store)
(tape : Fin (n + 2))
:
Represents tm cfg (Structured.Basic.execList (loadTapeOps n tape) store)
theorem
Complexity.RAM.TMConfig.Sparse.addressOps_address_internal
{n : ℕ}
{tm : TM n}
{cfg : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hrepresents : Represents tm cfg store)
(tape : Fin (n + 2))
(htapeCount : store (tapeCountReg n) = n + 2)
:
Structured.Basic.execList (addressOps n tape) store (addressReg n) = cellReg n tape (tapeAt cfg tape).head
theorem
Complexity.RAM.TMConfig.Sparse.loadTapeOps_symbol_internal
{n : ℕ}
{tm : TM n}
{cfg : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hrepresents : Represents tm cfg store)
(tape : Fin (n + 2))
(htapeCount : store (tapeCountReg n) = n + 2)
:
Structured.Basic.execList (loadTapeOps n tape) store (symbolReg n tape) = symbolCode (tapeAt cfg tape).read