Proof: Byte 5 Stays the Same 5

Let's prove the following theorem:

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

then value of cell 5 at time 6 = 4

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

Comments

Please log in to add comments