Loading represented TM states and head symbols -- proof internals

theorem Complexity.RAM.TMConfig.Step.loadOps_loaded_internal {n : ℕ} {tm : TM n} {bound : ℕ} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm bound cfg store) (hheads : HeadsBounded cfg bound) : have final := Structured.Basic.execList (loadOps n bound) store; Represents tm bound cfg final ∧ final (zeroReg n bound) = 0 ∧ final (oneReg n bound) = 1 ∧ final (stateScratchReg n bound) = stateCode tm cfg.state ∧ ∀ (tape : Fin (n + 2)), final (symbolReg n bound tape) = symbolCode (readSymbols cfg tape)

theorem Complexity.RAM.TMConfig.Step.loadOps_measured_internal {n : ℕ} {tm : TM n} {bound : ℕ} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm bound cfg store) (hheads : HeadsBounded cfg bound) (henvelope : Structured.Internal.StoreEnvelope (registerLimit n bound) (wordBound tm bound) store) : have final := Structured.Basic.execList (loadOps n bound) store; Structured.Internal.MeasuredRuns (Structured.Cmd.basics (loadOps n bound)) store final (loadOps n bound).length (4 * (loadOps n bound).length * wordWidth tm bound) (spaceBound tm bound) ∧ Structured.Internal.StoreEnvelope (registerLimit n bound) (wordBound tm bound) final