TM-to-RAM step layout -- proof internals

theorem Complexity.RAM.TMConfig.Step.symbolCode_lt_internal (symbol : Γ) : symbolCode symbol < 4

theorem Complexity.RAM.TMConfig.Step.symbolAt_code_internal (symbol : Γ) : symbolAt ⟨symbolCode symbol, ⋯⟩ = symbol

theorem Complexity.RAM.TMConfig.Step.stateCode_lt_internal {n : ℕ} (tm : TM n) (state : tm.Q) : stateCode tm state < Fintype.card tm.Q

theorem Complexity.RAM.TMConfig.Step.headReg_eq_fieldReg_internal {n bound : ℕ} (tape : Fin (n + 2)) : headReg tape = fieldReg (headField tape)

theorem Complexity.RAM.TMConfig.Step.cellBase_add_eq_fieldReg_internal {n bound : ℕ} (tape : Fin (n + 2)) (position : Fin (bound + 1)) : cellBase n bound tape + ↑position = fieldReg (cellField tape position)

theorem Complexity.RAM.TMConfig.Step.zeroReg_ge_internal (n bound : ℕ) : registerCount n bound ≤ zeroReg n bound

theorem Complexity.RAM.TMConfig.Step.oneReg_ge_internal (n bound : ℕ) : registerCount n bound ≤ oneReg n bound

theorem Complexity.RAM.TMConfig.Step.stateScratchReg_ge_internal (n bound : ℕ) : registerCount n bound ≤ stateScratchReg n bound

theorem Complexity.RAM.TMConfig.Step.addressReg_ge_internal (n bound : ℕ) : registerCount n bound ≤ addressReg n bound

theorem Complexity.RAM.TMConfig.Step.valueReg_ge_internal (n bound : ℕ) : registerCount n bound ≤ valueReg n bound

theorem Complexity.RAM.TMConfig.Step.symbolReg_ge_internal (n bound : ℕ) (tape : Fin (n + 2)) : registerCount n bound ≤ symbolReg n bound tape

theorem Complexity.RAM.TMConfig.Step.scratch_lt_registerLimit_internal (n bound : ℕ) : zeroReg n bound < registerLimit n bound ∧ oneReg n bound < registerLimit n bound ∧ stateScratchReg n bound < registerLimit n bound ∧ addressReg n bound < registerLimit n bound ∧ valueReg n bound < registerLimit n bound ∧ ∀ (tape : Fin (n + 2)), symbolReg n bound tape < registerLimit n bound

theorem Complexity.RAM.TMConfig.Step.encodeRegs_storeBounded_internal {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (hheads : HeadsBounded cfg bound) : StoreBounded tm bound (encodeRegs tm bound cfg)

theorem Complexity.RAM.TMConfig.Step.loadTapeOps_represents_internal {n : ℕ} {tm : TM n} {bound : ℕ} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm bound cfg store) (tape : Fin (n + 2)) : Represents tm bound cfg (Structured.Basic.execList (loadTapeOps n bound tape) store)

theorem Complexity.RAM.TMConfig.Step.loadTapeOps_symbol_internal {n : ℕ} {tape : Fin (n + 2)} {tm : TM n} {bound : ℕ} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm bound cfg store) (hhead : (tapeAt cfg tape).head ≤ bound) : Structured.Basic.execList (loadTapeOps n bound tape) store (symbolReg n bound tape) = symbolCode (tapeAt cfg tape).read