Complete dense-overlay RAM decision machine -- definitions #
def
Complexity.RAM.RegisterStore.Machine.denseProgramDecisionTM
{n : ℕ}
(tapes : ControlInstructionTapes n)
(program : Program)
:
Initialize the immutable public-input bank and one-entry overlay, execute
one fixed program through its first halt, and extract decoded R₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Complexity.RAM.RegisterStore.Machine.denseProgramDecisionTime
{n : ℕ}
(tapes : ControlInstructionTapes n)
(program : Program)
(input : List Bool)
(fuel : ℕ)
:
Exact compositional bound for one fuel-certified dense RAM decision run.
Equations
- One or more equations did not get rendered due to their size.