Proof: Byte 4 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 4 at time 5 = 0

then value of cell 4 at time 6 = 0

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

Comments

Please log in to add comments