Proof: Store 24

Let's prove the following theorem:

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

then value of cell 125 at time 25 = 5

Proof:

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

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

Comments

Please log in to add comments