Bounded Turing-machine configuration encoding -- proof internals

theorem Complexity.RAM.TMConfig.fieldReg_state_internal {n bound : ℕ} : fieldReg stateField = 0

theorem Complexity.RAM.TMConfig.fieldReg_head_internal {n bound : ℕ} (tape : Fin (n + 2)) : fieldReg (headField tape) = 1 + ↑tape

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

theorem Complexity.RAM.TMConfig.symbolDecode_code_internal (symbol : Γ) : symbolDecode (symbolCode symbol) = symbol

theorem Complexity.RAM.TMConfig.stateDecode_code_internal {n : ℕ} (tm : TM n) (state : tm.Q) : stateDecode tm (stateCode tm state) = state

theorem Complexity.RAM.TMConfig.tapeAt_input_internal {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) : tapeAt cfg ⟨0, ⋯⟩ = cfg.input

theorem Complexity.RAM.TMConfig.tapeAt_work_internal {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) (i : Fin n) : tapeAt cfg ⟨↑i + 1, ⋯⟩ = cfg.work i

theorem Complexity.RAM.TMConfig.tapeAt_output_internal {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) : tapeAt cfg ⟨n + 1, ⋯⟩ = cfg.output

theorem Complexity.RAM.TMConfig.encodeRegs_field_internal {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (field : Field n bound) : encodeRegs tm bound cfg (fieldReg field) = fieldValue tm bound cfg field

theorem Complexity.RAM.TMConfig.fieldReg_lt_internal {n bound : ℕ} (field : Field n bound) : fieldReg field < registerCount n bound

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

theorem Complexity.RAM.TMConfig.Represents.update_outside_internal {n : ℕ} {tm : TM n} {bound reg value : ℕ} {cfg : Complexity.Cfg n tm.Q} {regs : ℕ → ℕ} (hrepresents : Represents tm bound cfg regs) (hreg : registerCount n bound ≤ reg) : Represents tm bound cfg (Function.update regs reg value)

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

theorem Complexity.RAM.TMConfig.decode_of_represents_internal {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (regs : ℕ → ℕ) (hrepresents : Represents tm bound cfg regs) (hbounded : Bounded cfg bound) : decode tm bound regs = cfg

theorem Complexity.RAM.TMConfig.decode_encode_internal {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (hbounded : Bounded cfg bound) : decode tm bound (encode tm bound cfg).regs = cfg

theorem Complexity.RAM.TMConfig.encodeRegs_outside_internal {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) {reg : ℕ} (hreg : registerCount n bound ≤ reg) : encodeRegs tm bound cfg reg = 0