| Name | Category | Theorems |
|---|
addMemory 📖 | CompOp | 5 mathmath: addMem_terminated, addMem_incPc_comm, specification_StoreWordImmediate, addMemory_unfold, add_mem_code_no_change
|
addRegister 📖 | CompOp | 19 mathmath: addRegister_getRegister_eq, addRegister_unfold, specification_AddRegister, add_reg_code_no_change, specification_AddImmediate, specification_LoadWordImmediate, specification_LoadWordReg, specification_XOR, specification_LoadImmediate, specification_XorImmediate, addReg_terminated, specification_Increment, addReg_incPc_comm, specification_Decrement, specification_CopyRegister, specification_LoadAddress, specification_SubRegister, addRegister_getRegister_neq, specification_SubImmediate
|
code 📖 | CompOp | 14 mathmath: addRegister_unfold, currInstruction_unfold, add_reg_code_no_change, runNSteps_currInstruction, set_pc_code_no_change, incPc_increments_pc, get_register_only_memory', get_register_only_register', set_termianted_code_no_change, runNSteps_code_remains, addMemory_unfold, add_mem_code_no_change, get_label_from_code, runOneSteps_code_remains
|
createStandardState 📖 | CompOp | — |
currInstruction 📖 | CompOp | 2 mathmath: currInstruction_unfold, runNSteps_currInstruction
|
getLabelAt 📖 | CompOp | 9 mathmath: specification_Jump', specification_JumpNeq_true, specification_JumpLe_true, specification_JumpEq_true, specification_JumpGt_true, specification_JumpEqZero_true, specification_JumpNeqZero_true, get_label_from_code, specification_Jump
|
getMemoryAt 📖 | CompOp | 6 mathmath: specification_LoadWordImmediate, get_register_only_memory, specification_LoadWordReg, setPc_getMemory_indep, get_register_only_memory', getMemoryAt_def
|
getRegisterAt 📖 | CompOp | 31 mathmath: addRegister_getRegister_eq, specification_AddRegister, incPc_getRegister_indep, specification_JumpNeqZero_false, specification_AddImmediate, specification_JumpNeq_true, specification_LoadWordReg, specification_XOR, register_le_zero_eq_zero, specification_JumpLe_true, setPc_getRegister_indep, specification_XorImmediate, specification_JumpEq_true, specification_Increment, getRegisterAt_def, specification_JumpGt_true, specification_JumpNeq_false, get_register_only_register', specification_StoreWordImmediate, specification_Decrement, specification_CopyRegister, get_register_only_register, specification_JumpEqZero_true, specification_JumpEqZero_false, specification_SubRegister, specification_JumpNeqZero_true, specification_JumpGt_false, addRegister_getRegister_neq, specification_JumpEq_false, specification_JumpLe_false, specification_SubImmediate
|
incPc 📖 | CompOp | 26 mathmath: specification_AddRegister, incPc_getRegister_indep, specification_JumpNeqZero_false, specification_AddImmediate, addMem_incPc_comm, specification_LoadWordImmediate, specification_LoadWordReg, specification_XOR, specification_LoadImmediate, specification_XorImmediate, specification_Increment, incPc_terminated, incPc_increments_pc, specification_JumpNeq_false, setReg_incPc_symm, addReg_incPc_comm, specification_StoreWordImmediate, specification_Decrement, specification_CopyRegister, specification_LoadAddress, specification_JumpEqZero_false, specification_SubRegister, specification_JumpGt_false, specification_JumpEq_false, specification_JumpLe_false, specification_SubImmediate
|
jump 📖 | CompOp | 2 mathmath: jump_set_pc, jump_register_indep
|
memory 📖 | CompOp | 8 mathmath: addRegister_unfold, jump_set_pc, jump_register_indep, incPc_increments_pc, get_register_only_register', setPc_getMemoryAt_def_indep, addMemory_unfold, getMemoryAt_def
|
pc 📖 | CompOp | 10 mathmath: addRegister_unfold, currInstruction_unfold, specification_Jump', runNSteps_currInstruction, set_pc, jump_register_indep, incPc_increments_pc, get_register_only_memory', get_register_only_register', addMemory_unfold
|
registers 📖 | CompOp | 9 mathmath: addRegister_unfold, jump_set_pc, jump_register_indep, getRegisterAt_def, incPc_increments_pc, get_register_only_memory', TMap_register_le_zero_eq_zero, setPc_getRegisterAt_def_indep, addMemory_unfold
|
setCode 📖 | CompOp | — |
setInstructionMap 📖 | CompOp | — |
setLabels 📖 | CompOp | — |
setMemory 📖 | CompOp | — |
setPc 📖 | CompOp | 15 mathmath: specification_Jump', specification_JumpNeq_true, set_pc, specification_JumpLe_true, setPc_getRegister_indep, set_pc_code_no_change, specification_JumpEq_true, setPc_getMemory_indep, specification_JumpGt_true, setPc_getRegisterAt_def_indep, setPc_terminated, setPc_getMemoryAt_def_indep, specification_JumpEqZero_true, specification_JumpNeqZero_true, specification_Jump
|
setRegister 📖 | CompOp | 1 mathmath: setReg_incPc_symm
|
setTerminated 📖 | CompOp | 1 mathmath: set_termianted_code_no_change
|
terminated 📖 | CompOp | 39 mathmath: addMem_terminated, addRegister_unfold, specification_AddRegister, specification_JumpNeqZero_false, specification_Jump', specification_AddImmediate, specification_JumpNeq_true, specification_LoadWordImmediate, specification_LoadWordReg, specification_XOR, jump_set_pc, specification_JumpLe_true, specification_LoadImmediate, specification_XorImmediate, specification_JumpEq_true, jump_register_indep, addReg_terminated, specification_Increment, incPc_terminated, incPc_increments_pc, specification_JumpGt_true, specification_JumpNeq_false, get_register_only_memory', get_register_only_register', specification_StoreWordImmediate, specification_Decrement, specification_CopyRegister, setPc_terminated, specification_LoadAddress, addMemory_unfold, specification_JumpEqZero_true, specification_JumpEqZero_false, specification_SubRegister, specification_JumpNeqZero_true, specification_JumpGt_false, specification_Jump, specification_JumpEq_false, specification_JumpLe_false, specification_SubImmediate
|