Proof: Load 7

Let's prove the following theorem:

if the following are true:
  • instruction #0 is load dst=7 addr=5 imm=0
  • the PC at time 7 = 0
  • value of cell 5 at time 7 = 9
  • value of cell 9 at time 7 = 31

then value of cell 7 at time 8 = 31

Proof:

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

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

Comments

Please log in to add comments