Proof: Store 1

Let's prove the following theorem:

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

then value of cell 8 at time 2 = 11

Proof:

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

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

Comments

Please log in to add comments