Proof: Store 15

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 15 = 1
  • value of cell 6 at time 15 = 14
  • value of cell 7 at time 15 = 45

then value of cell 14 at time 16 = 45

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

Comments

Please log in to add comments