Proof: Load 14

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 14 = 0
  • value of cell 5 at time 14 = 10
  • value of cell 10 at time 14 = 45

then value of cell 7 at time 15 = 45

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 14 = 0
3 value of cell 5 at time 14 = 10
4 value of cell 10 at time 14 = 45
Proof Table
# Claim Reason
1 value of cell 7 at time (14 + 1) = value of cell ((value of cell 5 at time 14) + 0) at time 14 if instruction #0 is load dst=7 addr=5 imm=0 and the PC at time 14 = 0, then value of cell 7 at time (14 + 1) = value of cell ((value of cell 5 at time 14) + 0) at time 14
2 (value of cell 5 at time 14) + 0 = 10 + 0 if value of cell 5 at time 14 = 10, then (value of cell 5 at time 14) + 0 = 10 + 0
3 10 + 0 = 10 10 + 0 = 10
4 (value of cell 5 at time 14) + 0 = 10 if (value of cell 5 at time 14) + 0 = 10 + 0 and 10 + 0 = 10, then (value of cell 5 at time 14) + 0 = 10
5 value of cell ((value of cell 5 at time 14) + 0) at time 14 = value of cell 10 at time 14 if (value of cell 5 at time 14) + 0 = 10, then value of cell ((value of cell 5 at time 14) + 0) at time 14 = value of cell 10 at time 14
6 value of cell ((value of cell 5 at time 14) + 0) at time 14 = 45 if value of cell ((value of cell 5 at time 14) + 0) at time 14 = value of cell 10 at time 14 and value of cell 10 at time 14 = 45, then value of cell ((value of cell 5 at time 14) + 0) at time 14 = 45
7 value of cell 7 at time (14 + 1) = 45 if value of cell 7 at time (14 + 1) = value of cell ((value of cell 5 at time 14) + 0) at time 14 and value of cell ((value of cell 5 at time 14) + 0) at time 14 = 45, then value of cell 7 at time (14 + 1) = 45
8 14 + 1 = 15 14 + 1 = 15
9 value of cell 7 at time (14 + 1) = value of cell 7 at time 15 if 14 + 1 = 15, then value of cell 7 at time (14 + 1) = value of cell 7 at time 15
10 value of cell 7 at time 15 = 45 if value of cell 7 at time (14 + 1) = value of cell 7 at time 15 and value of cell 7 at time (14 + 1) = 45, then value of cell 7 at time 15 = 45

Comments

Please log in to add comments