Proof: Subtracti Insn 18
Let's prove the following theorem:
if the following are true:
- subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5
- the PC at time 18 = 5
- value of cell 1 at time 18 = 124
then value of cell 1 at time 19 = 123
Proof:
Given
| 1 | subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5 |
|---|---|
| 2 | the PC at time 18 = 5 |
| 3 | value of cell 1 at time 18 = 124 |
| # | Claim | Reason |
|---|---|---|
| 1 | value of cell 1 at time (18 + 1) = (value of cell 1 at time 18) - 1 | if subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5 and the PC at time 18 = 5, then value of cell 1 at time (18 + 1) = (value of cell 1 at time 18) - 1 |
| 2 | 18 + 1 = 19 | 18 + 1 = 19 |
| 3 | value of cell 1 at time (18 + 1) = value of cell 1 at time 19 | if 18 + 1 = 19, then value of cell 1 at time (18 + 1) = value of cell 1 at time 19 |
| 4 | value of cell 1 at time 19 = (value of cell 1 at time 18) - 1 | if value of cell 1 at time (18 + 1) = value of cell 1 at time 19 and value of cell 1 at time (18 + 1) = (value of cell 1 at time 18) - 1, then value of cell 1 at time 19 = (value of cell 1 at time 18) - 1 |
| 5 | (value of cell 1 at time 18) - 1 = 124 - 1 | if value of cell 1 at time 18 = 124, then (value of cell 1 at time 18) - 1 = 124 - 1 |
| 6 | value of cell 1 at time 19 = 124 - 1 | if value of cell 1 at time 19 = (value of cell 1 at time 18) - 1 and (value of cell 1 at time 18) - 1 = 124 - 1, then value of cell 1 at time 19 = 124 - 1 |
| 7 | 124 - 1 = 123 | 124 - 1 = 123 |
| 8 | value of cell 1 at time 19 = 123 | if value of cell 1 at time 19 = 124 - 1 and 124 - 1 = 123, then value of cell 1 at time 19 = 123 |
Comments
Please log in to add comments