@[simp]

theorem MState.incPc_increments_pc (ms : MState) : (pc++ ; ms) = { memory := ms.memory, registers := ms.registers, pc := ms.pc + 1, code := ms.code, terminated := ms.terminated }

@[simp]

theorem MState.setReg_incPc_symm (ms : MState) (r : Registers) : (pc++ ; ms.setRegister r) = (pc++ ; ms).setRegister r

@[simp]

theorem MState.addReg_incPc_comm (ms : MState) (r v : UInt64) : (pc++ ; x[r] ← v ; ms) = x[r] ← v ; pc++ ; ms

@[simp]

theorem MState.addMem_incPc_comm (ms : MState) (r v : UInt64) : (pc++ ; mem[r] ← v ; ms) = mem[r] ← v ; pc++ ; ms

@[simp]

theorem MState.incPc_terminated (ms : MState) : (pc++ ; ms).terminated = ms.terminated

@[simp]

theorem MState.setPc_terminated (ms : MState) (p : UInt64) : (ms.setPc p).terminated = ms.terminated

@[simp]

theorem MState.addReg_terminated (ms : MState) (r v : UInt64) : (x[r] ← v ; ms).terminated = ms.terminated

@[simp]

theorem MState.addMem_terminated (ms : MState) (r v : UInt64) : (mem[r] ← v ; ms).terminated = ms.terminated

@[simp]

theorem MState.addRegister_getRegister_neq (ms : MState) (r1 r2 v : UInt64) : r1 ≠ r2 → (x[r1] ← v ; ms).getRegisterAt r2 = ms.getRegisterAt r2

@[simp]

theorem MState.addRegister_getRegister_eq (ms : MState) (r1 r2 v : UInt64) : r1 = r2 → (x[r1] ← v ; ms).getRegisterAt r2 = v

@[simp]

theorem MState.setPc_getRegister_indep (ms : MState) (i r : UInt64) : (ms.setPc i).getRegisterAt r = ms.getRegisterAt r

@[simp]

theorem MState.setPc_getRegisterAt_def_indep (ms : MState) (r l : UInt64) : TMap.get ms.registers r = TMap.get (ms.setPc l).registers r

@[simp]

theorem MState.setPc_getMemory_indep (ms : MState) (i r : UInt64) : (ms.setPc i).getMemoryAt r = ms.getMemoryAt r

@[simp]

theorem MState.setPc_getMemoryAt_def_indep (ms : MState) (m l : UInt64) : TMap.get ms.memory m = TMap.get (ms.setPc l).memory m

@[simp]

theorem MState.set_pc (ms : MState) (i : UInt64) : (ms.setPc i).pc = i

@[simp]

theorem MState.incPc_getRegister_indep (ms : MState) (r : UInt64) : (pc++ ; ms).getRegisterAt r = ms.getRegisterAt r

@[simp]

theorem MState.jump_set_pc (ms : MState) (s : String) (i : UInt64) : PMap.get ms.code.labels s = some i → ms.jump s = { memory := ms.memory, registers := ms.registers, pc := i, code := ms.code, terminated := ms.terminated }

@[simp]

theorem MState.currInstruction_unfold (ms : MState) : ms.currInstruction = TMap.get ms.code.instructionMap ms.pc

@[simp]

theorem MState.runNSteps_currInstruction (ms : MState) (n : ℕ) : (ms.runNSteps n).currInstruction = TMap.get (ms.runNSteps n).code.instructionMap (ms.runNSteps n).pc

@[simp]

theorem MState.addRegister_unfold (ms : MState) (i1 i2 : UInt64) : (x[i1] ← i2 ; ms) = { memory := ms.memory, registers := (i1 ↦ i2 ; ms.registers), pc := ms.pc, code := ms.code, terminated := ms.terminated }

@[simp]

theorem MState.addMemory_unfold (ms : MState) (i1 i2 : UInt64) : (mem[i1] ← i2 ; ms) = { memory := (i1 ↦ i2 ; ms.memory), registers := ms.registers, pc := ms.pc, code := ms.code, terminated := ms.terminated }

@[simp]

theorem MState.run_zero_steps (ms : MState) : ms.runNSteps 0 = ms

@[simp]

theorem MState.run_n_run_one (ms : MState) (n : ℕ) : (ms.runNSteps n).runOneStep = ms.runNSteps (n + 1)

@[simp]

theorem MState.run_n_run_one_comm (ms : MState) (n : ℕ) : (ms.runNSteps n).runOneStep = ms.runOneStep.runNSteps n

@[simp]

theorem MState.run_one_step_eq_run_n_1 (ms : MState) : ms.runOneStep = ms.runNSteps 1

@[simp]

theorem MState.run_N_comm (ms : MState) (n m : ℕ) : (ms.runNSteps n).runNSteps m = (ms.runNSteps m).runNSteps n

@[simp]

theorem MState.run_n_m_steps_comp (ms : MState) (n m : ℕ) : (ms.runNSteps n).runNSteps m = ms.runNSteps (n + m)

@[simp]

theorem MState.add_reg_code_no_change (ms : MState) (r v : UInt64) : (x[r] ← v ; ms).code = ms.code

@[simp]

theorem MState.add_mem_code_no_change (ms : MState) (r v : UInt64) : (mem[r] ← v ; ms).code = ms.code

@[simp]

theorem MState.set_pc_code_no_change (ms : MState) (v : UInt64) : (ms.setPc v).code = ms.code

@[simp]

theorem MState.set_termianted_code_no_change (ms : MState) (v : Bool) : (ms.setTerminated v).code = ms.code

@[simp]

theorem MState.jump_register_indep (ms : MState) (m : Memory) (r : Registers) (c : Code) (s : String) : ({ memory := m, registers := r, pc := ms.pc, code := c, terminated := ms.terminated }.jump s).pc = ({ memory := ms.memory, registers := ms.registers, pc := ms.pc, code := c, terminated := ms.terminated }.jump s).pc

@[simp]

theorem MState.get_register_only_register (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getRegisterAt i = TMap.get r i

@[simp]

theorem MState.get_register_only_register' (ms : MState) (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getRegisterAt i = { memory := ms.memory, registers := r, pc := ms.pc, code := ms.code, terminated := ms.terminated }.getRegisterAt i

@[simp]

theorem MState.get_register_only_memory (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getMemoryAt i = TMap.get m i

@[simp]

theorem MState.get_register_only_memory' (ms : MState) (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getMemoryAt i = { memory := m, registers := ms.registers, pc := ms.pc, code := ms.code, terminated := ms.terminated }.getMemoryAt i

@[simp]

theorem MState.get_label_from_code (ms : MState) (s : String) (l : UInt64) : (ms.getLabelAt s = some l) = (PMap.get ms.code.labels s = some l)

@[simp]

theorem MState.getRegisterAt_def (ms : MState) (l : UInt64) : ms.getRegisterAt l = TMap.get ms.registers l

@[simp]

theorem MState.getMemoryAt_def (ms : MState) (l : UInt64) : ms.getMemoryAt l = TMap.get ms.memory l

@[simp]

theorem MState.TMap_register_le_zero_eq_zero (ms : MState) (l : UInt64) : (TMap.get ms.registers l ≤ 0) = (TMap.get ms.registers l = 0)

@[simp]

theorem MState.register_le_zero_eq_zero (ms : MState) (l : UInt64) : (ms.getRegisterAt l ≤ 0) = (ms.getRegisterAt l = 0)

@[simp]

theorem MState.runOneSteps_code_remains (ms : MState) : ms.runOneStep.code = ms.code

@[simp]

theorem MState.runNSteps_code_remains (ms : MState) (n : ℕ) : (ms.runNSteps n).code = ms.code

theorem MState.runNSteps_diff (s : MState) (n : ℕ) (L1 L2 : Set UInt64) : L2 ⊆ L1 → (s.runNSteps n).pc ∉ L1 → (s.runNSteps n).pc ∉ L2

theorem MState.runNSteps_pc_in_superset (s : MState) (n : ℕ) (L1 L2 : Set UInt64) : L2 ⊆ L1 → (s.runNSteps n).pc ∈ L2 → (s.runNSteps n).pc ∈ L1

theorem MState.runNSteps_add (s s' s'' : MState) (n n' : ℕ) : s.runNSteps n = s' → s'.runNSteps n' = s'' → s.runNSteps (n + n') = s''

theorem MState.runNSteps_pc_nin (s s' s'' : MState) (n n' : ℕ) (L : Set UInt64) : s.runNSteps n = s' → s'.runNSteps n' = s'' → (s.runNSteps n).pc ∉ L → (s'.runNSteps n').pc ∉ L → (s.runNSteps (n + n')).pc ∉ L

theorem MState.runNSteps_pc_nin_extra_step (s s' : MState) (n : ℕ) (L : Set UInt64) : s.runNSteps n = s' → s'.pc ∉ L → (∀ (n' : ℕ), 0 < n' ∧ n' < n → (s.runNSteps n').pc ∉ L) → ∀ (n'' : ℕ), 0 < n'' ∧ n'' ≤ n → (s.runNSteps n'').pc ∉ L

theorem MState.run_n_plus_m_intersect (s s' : MState) (m m' : ℕ) (L_b L_b' : Set UInt64) : s.runNSteps m = s' → (∀ (n : ℕ), 0 < n ∧ n ≤ m → (s.runNSteps n).pc ∉ L_b) → (∀ (n' : ℕ), 0 < n' ∧ n' < m' → (s'.runNSteps n').pc ∉ L_b') → ∀ (n'' : ℕ), 0 < n'' ∧ n'' < m + m' → (s.runNSteps n'').pc ∉ L_b ∩ L_b'

theorem MState.run_n_plus_m_intersect' {s' : MState} (s : MState) (m m' : ℕ) (L_w L_b L_w' L_b' : Set UInt64) : L_w' ⊆ L_b ∧ L_w ∩ L_w' = ∅ → s.runNSteps m = s' → s'.pc ∈ L_w → s'.pc ∉ L_b → (∀ (n : ℕ), 0 < n ∧ n < m → (s.runNSteps n).pc ∉ L_w ∪ L_b) → (∀ (n' : ℕ), 0 < n' ∧ n' < m' → (s'.runNSteps n').pc ∉ L_w' ∪ L_b') → ∀ (n'' : ℕ), 0 < n'' ∧ n'' < m + m' → (s.runNSteps n'').pc ∉ L_w' ∪ L_b ∩ L_b'