Sparse unbounded TM configuration encoding -- proof internals

theorem Complexity.RAM.TMConfig.Sparse.control_lt_cellBase_internal (n : ℕ) : valueReg n < cellBase n ∧ ∀ (tape : Fin (n + 2)), symbolReg n tape < cellBase n

theorem Complexity.RAM.TMConfig.Sparse.headReg_lt_control_internal {n : ℕ} (tape : Fin (n + 2)) : headReg tape < n + 3

theorem Complexity.RAM.TMConfig.Sparse.cellBase_le_cellReg_internal {n : ℕ} (tape : Fin (n + 2)) (position : ℕ) : cellBase n ≤ cellReg n tape position

theorem Complexity.RAM.TMConfig.Sparse.decodeCellTape_cellReg_internal {n : ℕ} (tape : Fin (n + 2)) (position : ℕ) : decodeCellTape n (cellReg n tape position) = tape

theorem Complexity.RAM.TMConfig.Sparse.decodeCellPosition_cellReg_internal {n : ℕ} (tape : Fin (n + 2)) (position : ℕ) : decodeCellPosition n (cellReg n tape position) = position

theorem Complexity.RAM.TMConfig.Sparse.cellReg_injective_internal {n : ℕ} : Function.Injective fun (field : Fin (n + 2) × ℕ) => cellReg n field.1 field.2

theorem Complexity.RAM.TMConfig.Sparse.fieldReg_injective_internal {n : ℕ} : Function.Injective fieldReg

theorem Complexity.RAM.TMConfig.Sparse.fieldReg_ne_control_internal {n : ℕ} (field : Field n) {reg : ℕ} (hlow : n + 3 ≤ reg) (hhigh : reg < cellBase n) : fieldReg field ≠ reg

theorem Complexity.RAM.TMConfig.Sparse.Represents.update_control_internal {n : ℕ} {tm : TM n} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} {reg value : ℕ} (hrepresents : Represents tm cfg store) (hlow : n + 3 ≤ reg) (hhigh : reg < cellBase n) : Represents tm cfg (Function.update store reg value)

theorem Complexity.RAM.TMConfig.Sparse.scratch_range_internal (n : ℕ) : (n + 3 ≤ zeroReg n ∧ zeroReg n < cellBase n) ∧ (n + 3 ≤ oneReg n ∧ oneReg n < cellBase n) ∧ (n + 3 ≤ tapeCountReg n ∧ tapeCountReg n < cellBase n) ∧ (n + 3 ≤ stateScratchReg n ∧ stateScratchReg n < cellBase n) ∧ (n + 3 ≤ addressReg n ∧ addressReg n < cellBase n) ∧ (n + 3 ≤ valueReg n ∧ valueReg n < cellBase n) ∧ ∀ (tape : Fin (n + 2)), n + 3 ≤ symbolReg n tape ∧ symbolReg n tape < cellBase n

theorem Complexity.RAM.TMConfig.Sparse.encodeRegs_state_internal {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) : encodeRegs tm cfg stateReg = stateCode tm cfg.state

theorem Complexity.RAM.TMConfig.Sparse.encodeRegs_head_internal {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) (tape : Fin (n + 2)) : encodeRegs tm cfg (headReg tape) = (tapeAt cfg tape).head

theorem Complexity.RAM.TMConfig.Sparse.encodeRegs_cell_internal {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) (tape : Fin (n + 2)) (position : ℕ) : encodeRegs tm cfg (cellReg n tape position) = symbolCode ((tapeAt cfg tape).cells position)

theorem Complexity.RAM.TMConfig.Sparse.encodeRegs_represents_internal {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) : Represents tm cfg (encodeRegs tm cfg)

theorem Complexity.RAM.TMConfig.Sparse.decode_of_represents_internal {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) (store : Structured.Store) (hrepresents : Represents tm cfg store) : decode tm store = cfg

theorem Complexity.RAM.TMConfig.Sparse.decode_encode_internal {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) : decode tm (encodeRegs tm cfg) = cfg