Proof: Byte 127 Stays the Same 21

Let's prove the following theorem:

if the following are true:
  • instruction #21 is load dst=3 addr=1 imm=0
  • the PC at time 21 = 21
  • value of cell 127 at time 21 = 2

then value of cell 127 at time 22 = 2

Proof:

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

Given
1 instruction #21 is load dst=3 addr=1 imm=0
2 the PC at time 21 = 21
3 value of cell 127 at time 21 = 2
Proof Table
# Claim Reason
1 not (127 = 3) not (127 = 3)
2 value of cell 127 at time (21 + 1) = value of cell 127 at time 21 if instruction #21 is load dst=3 addr=1 imm=0 and the PC at time 21 = 21 and not (127 = 3), then value of cell 127 at time (21 + 1) = value of cell 127 at time 21
3 21 + 1 = 22 21 + 1 = 22
4 value of cell 127 at time (21 + 1) = value of cell 127 at time 22 if 21 + 1 = 22, then value of cell 127 at time (21 + 1) = value of cell 127 at time 22
5 value of cell 127 at time 22 = value of cell 127 at time 21 if value of cell 127 at time (21 + 1) = value of cell 127 at time 22 and value of cell 127 at time (21 + 1) = value of cell 127 at time 21, then value of cell 127 at time 22 = value of cell 127 at time 21
6 value of cell 127 at time 22 = 2 if value of cell 127 at time 22 = value of cell 127 at time 21 and value of cell 127 at time 21 = 2, then value of cell 127 at time 22 = 2

Comments

Please log in to add comments