Proof: Store 1

Let's prove the following theorem:

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

then value of cell 12 at time 2 = 24

Proof:

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

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

Comments

Please log in to add comments