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