Proof: Subtracti Insn 12

Let's prove the following theorem:

if the following are true:
  • subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
  • the PC at time 12 = 18
  • value of cell 1 at time 12 = 125

then value of cell 1 at time 13 = 124

Proof:

View as a tree | View dependent proofs | Try proving it

Given
1 subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
2 the PC at time 12 = 18
3 value of cell 1 at time 12 = 125
Proof Table
# Claim Reason
1 value of cell 1 at time (12 + 1) = (value of cell 1 at time 12) - 1 if subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18 and the PC at time 12 = 18, then value of cell 1 at time (12 + 1) = (value of cell 1 at time 12) - 1
2 12 + 1 = 13 12 + 1 = 13
3 value of cell 1 at time (12 + 1) = value of cell 1 at time 13 if 12 + 1 = 13, then value of cell 1 at time (12 + 1) = value of cell 1 at time 13
4 value of cell 1 at time 13 = (value of cell 1 at time 12) - 1 if value of cell 1 at time (12 + 1) = value of cell 1 at time 13 and value of cell 1 at time (12 + 1) = (value of cell 1 at time 12) - 1, then value of cell 1 at time 13 = (value of cell 1 at time 12) - 1
5 (value of cell 1 at time 12) - 1 = 125 - 1 if value of cell 1 at time 12 = 125, then (value of cell 1 at time 12) - 1 = 125 - 1
6 value of cell 1 at time 13 = 125 - 1 if value of cell 1 at time 13 = (value of cell 1 at time 12) - 1 and (value of cell 1 at time 12) - 1 = 125 - 1, then value of cell 1 at time 13 = 125 - 1
7 125 - 1 = 124 125 - 1 = 124
8 value of cell 1 at time 13 = 124 if value of cell 1 at time 13 = 125 - 1 and 125 - 1 = 124, then value of cell 1 at time 13 = 124

Comments

Please log in to add comments