Dense-overlay RAM decision-machine resource-bound proof internals

theorem Complexity.RAM.RegisterStore.Machine.denseProgramStepTime_le_envelope_internal {m : ℕ} (tapes : ControlInstructionTapes m) (program : Program) (input : List Bool) (snapshot : DenseOverlay.Snapshot) (hvalid : DenseOverlay.Valid snapshot.overlay) (hpc : snapshot.pc ≤ programResourceMagnitude program) : denseProgramStepTime tapes program input snapshot.pc snapshot.overlay ≤ denseStepEnvelope program input snapshot

theorem Complexity.RAM.RegisterStore.Machine.denseProgramLoopTime_le_envelope_internal {m : ℕ} (tapes : ControlInstructionTapes m) (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : DenseOverlay.Snapshot) (hvalid : DenseOverlay.Valid snapshot.overlay) (hpc : snapshot.pc ≤ programResourceMagnitude program) : denseProgramLoopTime tapes program input fuel snapshot ≤ denseProgramLoopEnvelope program input fuel snapshot

theorem Complexity.RAM.RegisterStore.Machine.denseProgramDecisionTime_le_envelope_internal {m : ℕ} (tapes : ControlInstructionTapes m) (program : Program) (input : List Bool) (fuel : ℕ) (hhalted : Halted program (run program fuel (initCfg input))) (hfuel : fuel ≤ logTimeUpto program fuel (initCfg input)) : denseProgramDecisionTime tapes program input fuel ≤ denseProgramDecisionEnvelope program input.length (logTimeUpto program fuel (initCfg input))