Proof: Load 8

Let's prove the following theorem:

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

then value of cell 3 at time 9 = 2

Proof:

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

Given
1 instruction #14 is load dst=3 addr=1 imm=1
2 the PC at time 8 = 14
3 value of cell 1 at time 8 = 126
4 value of cell 127 at time 8 = 2
Proof Table
# Claim Reason
1 value of cell 3 at time (8 + 1) = value of cell ((value of cell 1 at time 8) + 1) at time 8 if instruction #14 is load dst=3 addr=1 imm=1 and the PC at time 8 = 14, then value of cell 3 at time (8 + 1) = value of cell ((value of cell 1 at time 8) + 1) at time 8
2 (value of cell 1 at time 8) + 1 = 126 + 1 if value of cell 1 at time 8 = 126, then (value of cell 1 at time 8) + 1 = 126 + 1
3 126 + 1 = 127 126 + 1 = 127
4 (value of cell 1 at time 8) + 1 = 127 if (value of cell 1 at time 8) + 1 = 126 + 1 and 126 + 1 = 127, then (value of cell 1 at time 8) + 1 = 127
5 value of cell ((value of cell 1 at time 8) + 1) at time 8 = value of cell 127 at time 8 if (value of cell 1 at time 8) + 1 = 127, then value of cell ((value of cell 1 at time 8) + 1) at time 8 = value of cell 127 at time 8
6 value of cell ((value of cell 1 at time 8) + 1) at time 8 = 2 if value of cell ((value of cell 1 at time 8) + 1) at time 8 = value of cell 127 at time 8 and value of cell 127 at time 8 = 2, then value of cell ((value of cell 1 at time 8) + 1) at time 8 = 2
7 value of cell 3 at time (8 + 1) = 2 if value of cell 3 at time (8 + 1) = value of cell ((value of cell 1 at time 8) + 1) at time 8 and value of cell ((value of cell 1 at time 8) + 1) at time 8 = 2, then value of cell 3 at time (8 + 1) = 2
8 8 + 1 = 9 8 + 1 = 9
9 value of cell 3 at time (8 + 1) = value of cell 3 at time 9 if 8 + 1 = 9, then value of cell 3 at time (8 + 1) = value of cell 3 at time 9
10 value of cell 3 at time 9 = 2 if value of cell 3 at time (8 + 1) = value of cell 3 at time 9 and value of cell 3 at time (8 + 1) = 2, then value of cell 3 at time 9 = 2

Comments

Please log in to add comments