MsTheory

📁 Source: MRiscX/Semantics/MsTheory.lean

Statistics

Metric	Count
Definitions	0
Theorems `TMap_register_le_zero_eq_zero`, `addMem_incPc_comm`, `addMem_terminated`, `addMemory_unfold`, `addReg_incPc_comm`, `addReg_terminated`, `addRegister_getRegister_eq`, `addRegister_getRegister_neq`, `addRegister_unfold`, `add_mem_code_no_change`, `add_reg_code_no_change`, `currInstruction_unfold`, `getMemoryAt_def`, `getRegisterAt_def`, `get_label_from_code`, `get_register_only_memory`, `get_register_only_memory'`, `get_register_only_register`, `get_register_only_register'`, `incPc_getRegister_indep`, `incPc_increments_pc`, `incPc_terminated`, `jump_register_indep`, `jump_set_pc`, `register_le_zero_eq_zero`, `runNSteps_add`, `runNSteps_code_remains`, `runNSteps_currInstruction`, `runNSteps_diff`, `runNSteps_pc_in_superset`, `runNSteps_pc_nin`, `runNSteps_pc_nin_extra_step`, `runOneSteps_code_remains`, `run_N_comm`, `run_n_m_steps_comp`, `run_n_plus_m_intersect`, `run_n_plus_m_intersect'`, `run_n_run_one`, `run_n_run_one_comm`, `run_one_step_eq_run_n_1`, `run_zero_steps`, `setPc_getMemoryAt_def_indep`, `setPc_getMemory_indep`, `setPc_getRegisterAt_def_indep`, `setPc_getRegister_indep`, `setPc_terminated`, `setReg_incPc_symm`, `set_pc`, `set_pc_code_no_change`, `set_termianted_code_no_change`	50
Total	50

MState

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`TMap_register_le_zero_eq_zero` 📖	mathematical	—	`TMap.get` `Register` `registers`	—	—
`addMem_incPc_comm` 📖	mathematical	—	`incPc` `addMemory`	—	—
`addMem_terminated` 📖	mathematical	—	`terminated` `addMemory`	—	—
`addMemory_unfold` 📖	mathematical	—	`addMemory` `TMap.put` `MemoryAddress` `memory` `registers` `pc` `code` `terminated`	—	—
`addReg_incPc_comm` 📖	mathematical	—	`incPc` `addRegister`	—	—
`addReg_terminated` 📖	mathematical	—	`terminated` `addRegister`	—	—
`addRegister_getRegister_eq` 📖	mathematical	—	`getRegisterAt` `addRegister`	—	`t_update_eq`
`addRegister_getRegister_neq` 📖	mathematical	—	`getRegisterAt` `addRegister`	—	`t_update_neq`
`addRegister_unfold` 📖	mathematical	—	`addRegister` `memory` `TMap.put` `Register` `registers` `pc` `code` `terminated`	—	—
`add_mem_code_no_change` 📖	mathematical	—	`code` `addMemory`	—	—
`add_reg_code_no_change` 📖	mathematical	—	`code` `addRegister`	—	—
`currInstruction_unfold` 📖	mathematical	—	`currInstruction` `TMap.get` `InstructionIndex` `Instr` `Code.instructionMap` `code` `pc`	—	—
`getMemoryAt_def` 📖	mathematical	—	`getMemoryAt` `TMap.get` `MemoryAddress` `memory`	—	—
`getRegisterAt_def` 📖	mathematical	—	`getRegisterAt` `TMap.get` `Register` `registers`	—	—
`get_label_from_code` 📖	mathematical	—	`getLabelAt` `PMap.get` `Code.labels` `code`	—	—
`get_register_only_memory` 📖	mathematical	—	`getMemoryAt` `TMap.get` `MemoryAddress`	—	—
`get_register_only_memory'` 📖	mathematical	—	`getMemoryAt` `registers` `pc` `code` `terminated`	—	—
`get_register_only_register` 📖	mathematical	—	`getRegisterAt` `TMap.get` `Register`	—	—
`get_register_only_register'` 📖	mathematical	—	`getRegisterAt` `memory` `pc` `code` `terminated`	—	—
`incPc_getRegister_indep` 📖	mathematical	—	`getRegisterAt` `incPc`	—	—
`incPc_increments_pc` 📖	mathematical	—	`incPc` `memory` `registers` `ProgramCounter` `pc` `code` `terminated`	—	—
`incPc_terminated` 📖	mathematical	—	`terminated` `incPc`	—	—
`jump_register_indep` 📖	mathematical	—	`pc` `jump` `terminated` `memory` `registers`	—	—
`jump_set_pc` 📖	mathematical	`PMap.get` `Code.labels` `code`	`jump` `memory` `registers` `terminated`	—	—
`register_le_zero_eq_zero` 📖	mathematical	—	`getRegisterAt`	—	`getRegisterAt_def`
`runNSteps_add` 📖	—	`runNSteps`	—	—	`run_n_m_steps_comp`
`runNSteps_code_remains` 📖	mathematical	—	`code` `runNSteps`	—	`runNSteps.eq_def` `run_n_run_one_comm` `runOneSteps_code_remains`
`runNSteps_currInstruction` 📖	mathematical	—	`currInstruction` `runNSteps` `TMap.get` `InstructionIndex` `Instr` `Code.instructionMap` `code` `pc`	—	`runNSteps.eq_def` `TMap.get.congr_simp` `currInstruction_unfold`
`runNSteps_diff` 📖	—	`ProgramCounter` `pc` `runNSteps`	—	—	—
`runNSteps_pc_in_superset` 📖	—	`ProgramCounter` `pc` `runNSteps`	—	—	—
`runNSteps_pc_nin` 📖	—	`runNSteps` `ProgramCounter` `pc`	—	—	`runNSteps_add`
`runNSteps_pc_nin_extra_step` 📖	—	`runNSteps` `ProgramCounter` `pc`	—	—	—
`runOneSteps_code_remains` 📖	mathematical	—	`code` `runOneStep`	—	`currInstruction_unfold` `addRegister_unfold` `incPc_increments_pc` `getRegisterAt_def` `getMemoryAt_def` `addMemory_unfold` `set_termianted_code_no_change`
`run_N_comm` 📖	mathematical	—	`runNSteps`	—	`run_zero_steps` `run_n_run_one` `run_n_run_one_comm`
`run_n_m_steps_comp` 📖	mathematical	—	`runNSteps`	—	`run_zero_steps` `run_n_run_one` `run_n_run_one_comm`
`run_n_plus_m_intersect` 📖	—	`runNSteps` `ProgramCounter` `pc`	—	—	`Nat.lt_sub_left` `run_n_m_steps_comp`
`run_n_plus_m_intersect'` 📖	—	`runNSteps` `ProgramCounter` `pc`	—	—	`Nat.lt_sub_left` `run_n_m_steps_comp`
`run_n_run_one` 📖	mathematical	—	`runOneStep` `runNSteps`	—	`run_zero_steps` `runNSteps.eq_def`
`run_n_run_one_comm` 📖	mathematical	—	`runOneStep` `runNSteps`	—	`run_zero_steps` `runNSteps.eq_def`
`run_one_step_eq_run_n_1` 📖	mathematical	—	`runOneStep` `runNSteps`	—	`runNSteps.eq_def` `run_zero_steps`
`run_zero_steps` 📖	mathematical	—	`runNSteps`	—	`runNSteps.eq_def`
`setPc_getMemoryAt_def_indep` 📖	mathematical	—	`TMap.get` `MemoryAddress` `memory` `setPc`	—	—
`setPc_getMemory_indep` 📖	mathematical	—	`getMemoryAt` `setPc`	—	—
`setPc_getRegisterAt_def_indep` 📖	mathematical	—	`TMap.get` `Register` `registers` `setPc`	—	—
`setPc_getRegister_indep` 📖	mathematical	—	`getRegisterAt` `setPc`	—	—
`setPc_terminated` 📖	mathematical	—	`terminated` `setPc`	—	—
`setReg_incPc_symm` 📖	mathematical	—	`incPc` `setRegister`	—	—
`set_pc` 📖	mathematical	—	`pc` `setPc`	—	—
`set_pc_code_no_change` 📖	mathematical	—	`code` `setPc`	—	—
`set_termianted_code_no_change` 📖	mathematical	—	`code` `setTerminated`	—	—

---

← Back to Index