Loading sparse TM states and head symbols -- proof internals

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