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