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