Proof: Byte 3 Stays the Same 7

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 7 = 7
  • value of cell 3 at time 7 = 1

then value of cell 3 at time 8 = 1

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

Comments

Please log in to add comments