Proof: Store 19

Let's prove the following theorem:

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

then value of cell 123 at time 20 = 5

Proof:

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

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

Comments

Please log in to add comments