Proof: Byte 2 Stays the Same 19

Let's prove the following theorem:

if the following are true:
  • instruction #7 is addi dst=4 src=4 imm=1
  • the PC at time 19 = 7
  • value of cell 2 at time 19 = 3

then value of cell 2 at time 20 = 3

Instructions
Memory Cells
Program Counter Time
0 0
LW Computer Simulator

Proof:

View as a tree | View dependent proofs | Try proving it

Given
1 instruction #7 is addi dst=4 src=4 imm=1
2 the PC at time 19 = 7
3 value of cell 2 at time 19 = 3
Proof Table
# Claim Reason
1 not (2 = 4) not (2 = 4)
2 value of cell 2 at time (19 + 1) = value of cell 2 at time 19 if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 19 = 7 and not (2 = 4), then value of cell 2 at time (19 + 1) = value of cell 2 at time 19
3 19 + 1 = 20 19 + 1 = 20
4 value of cell 2 at time (19 + 1) = value of cell 2 at time 20 if 19 + 1 = 20, then value of cell 2 at time (19 + 1) = value of cell 2 at time 20
5 value of cell 2 at time 20 = value of cell 2 at time 19 if value of cell 2 at time (19 + 1) = value of cell 2 at time 20 and value of cell 2 at time (19 + 1) = value of cell 2 at time 19, then value of cell 2 at time 20 = value of cell 2 at time 19
6 value of cell 2 at time 20 = 3 if value of cell 2 at time 20 = value of cell 2 at time 19 and value of cell 2 at time 19 = 3, then value of cell 2 at time 20 = 3

Comments

Please log in to add comments