Proof: Byte 12 Stays the Same 16
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 16 = 2
- value of cell 12 at time 16 = 24
then value of cell 12 at time 17 = 24
Proof:
Given
1 | instruction #2 is addi dst=5 src=5 imm=1 |
---|---|
2 | the PC at time 16 = 2 |
3 | value of cell 12 at time 16 = 24 |
# | Claim | Reason |
---|---|---|
1 | not (12 = 5) | not (12 = 5) |
2 | value of cell 12 at time (16 + 1) = value of cell 12 at time 16 | if instruction #2 is addi dst=5 src=5 imm=1 and the PC at time 16 = 2 and not (12 = 5), then value of cell 12 at time (16 + 1) = value of cell 12 at time 16 |
3 | 16 + 1 = 17 | 16 + 1 = 17 |
4 | value of cell 12 at time (16 + 1) = value of cell 12 at time 17 | if 16 + 1 = 17, then value of cell 12 at time (16 + 1) = value of cell 12 at time 17 |
5 | value of cell 12 at time 17 = value of cell 12 at time 16 | if value of cell 12 at time (16 + 1) = value of cell 12 at time 17 and value of cell 12 at time (16 + 1) = value of cell 12 at time 16, then value of cell 12 at time 17 = value of cell 12 at time 16 |
6 | value of cell 12 at time 17 = 24 | if value of cell 12 at time 17 = value of cell 12 at time 16 and value of cell 12 at time 16 = 24, then value of cell 12 at time 17 = 24 |
Comments
Please log in to add comments