Proof: Byte 1 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 1 at time 19 = 2

then value of cell 1 at time 20 = 2

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

Comments

Please log in to add comments