Proof: Load 11

Let's prove the following theorem:

if the following are true:
  • instruction #17 is load dst=3 addr=1 imm=1
  • the PC at time 11 = 17
  • value of cell 1 at time 11 = 125
  • value of cell 126 at time 11 = 3

then value of cell 3 at time 12 = 3

Proof:

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

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

Comments

Please log in to add comments