Proof: Byte 13 Stays the Same 17
Let's prove the following theorem:
if the following are true:
- instruction #3 is
addi dst=6 src=6 imm=1 - the PC at time 17 = 3
- value of cell 13 at time 17 = 31
then value of cell 13 at time 18 = 31
Proof:
Given
| 1 | instruction #3 is addi dst=6 src=6 imm=1 |
|---|---|
| 2 | the PC at time 17 = 3 |
| 3 | value of cell 13 at time 17 = 31 |
| # | Claim | Reason |
|---|---|---|
| 1 | not (13 = 6) | not (13 = 6) |
| 2 | value of cell 13 at time (17 + 1) = value of cell 13 at time 17 | if instruction #3 is addi dst=6 src=6 imm=1 and the PC at time 17 = 3 and not (13 = 6), then value of cell 13 at time (17 + 1) = value of cell 13 at time 17 |
| 3 | 17 + 1 = 18 | 17 + 1 = 18 |
| 4 | value of cell 13 at time (17 + 1) = value of cell 13 at time 18 | if 17 + 1 = 18, then value of cell 13 at time (17 + 1) = value of cell 13 at time 18 |
| 5 | value of cell 13 at time 18 = value of cell 13 at time 17 | if value of cell 13 at time (17 + 1) = value of cell 13 at time 18 and value of cell 13 at time (17 + 1) = value of cell 13 at time 17, then value of cell 13 at time 18 = value of cell 13 at time 17 |
| 6 | value of cell 13 at time 18 = 31 | if value of cell 13 at time 18 = value of cell 13 at time 17 and value of cell 13 at time 17 = 31, then value of cell 13 at time 18 = 31 |
Comments
Please log in to add comments