Proof: Store 8

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 8 = 1
  • value of cell 6 at time 8 = 13
  • value of cell 7 at time 8 = 31

then value of cell 13 at time 9 = 31

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 8 = 1
3 value of cell 6 at time 8 = 13
4 value of cell 7 at time 8 = 31
Proof Table
# Claim Reason
1 value of cell ((value of cell 6 at time 8) + 0) at time (8 + 1) = value of cell 7 at time 8 if instruction #1 is store src=7 addr=6 imm=0 and the PC at time 8 = 1, then value of cell ((value of cell 6 at time 8) + 0) at time (8 + 1) = value of cell 7 at time 8
2 (value of cell 6 at time 8) + 0 = 13 + 0 if value of cell 6 at time 8 = 13, then (value of cell 6 at time 8) + 0 = 13 + 0
3 13 + 0 = 13 13 + 0 = 13
4 (value of cell 6 at time 8) + 0 = 13 if (value of cell 6 at time 8) + 0 = 13 + 0 and 13 + 0 = 13, then (value of cell 6 at time 8) + 0 = 13
5 value of cell ((value of cell 6 at time 8) + 0) at time (8 + 1) = value of cell 13 at time (8 + 1) if (value of cell 6 at time 8) + 0 = 13, then value of cell ((value of cell 6 at time 8) + 0) at time (8 + 1) = value of cell 13 at time (8 + 1)
6 8 + 1 = 9 8 + 1 = 9
7 value of cell 13 at time (8 + 1) = value of cell 13 at time 9 if 8 + 1 = 9, then value of cell 13 at time (8 + 1) = value of cell 13 at time 9
8 value of cell 13 at time 9 = value of cell 7 at time 8 if value of cell ((value of cell 6 at time 8) + 0) at time (8 + 1) = value of cell 13 at time (8 + 1) and value of cell 13 at time (8 + 1) = value of cell 13 at time 9 and value of cell ((value of cell 6 at time 8) + 0) at time (8 + 1) = value of cell 7 at time 8, then value of cell 13 at time 9 = value of cell 7 at time 8
9 value of cell 13 at time 9 = 31 if value of cell 13 at time 9 = value of cell 7 at time 8 and value of cell 7 at time 8 = 31, then value of cell 13 at time 9 = 31

Comments

Please log in to add comments