Proof: Store 10

Let's prove the following theorem:

if the following are true:
  • instruction #16 is store src=3 addr=1 imm=0
  • the PC at time 10 = 16
  • value of cell 1 at time 10 = 125
  • value of cell 3 at time 10 = 2

then value of cell 125 at time 11 = 2

Proof:

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

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

Comments

Please log in to add comments