Proof: Store 4

Let's prove the following theorem:

if the following are true:

instruction #10 is store src=3 addr=1 imm=0
the PC at time 4 = 10
value of cell 1 at time 4 = 127
value of cell 3 at time 4 = 2

then value of cell 127 at time 5 = 2

Proof:

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

Given

1	instruction #10 is `store src=3 addr=1 imm=0`
2	the PC at time 4 = 10
3	value of cell 1 at time 4 = 127
4	value of cell 3 at time 4 = 2

Proof Table

#	Claim	Reason
1	value of cell ((value of cell 1 at time 4) + 0) at time (4 + 1) = value of cell 3 at time 4	if instruction #10 is `store src=3 addr=1 imm=0` and the PC at time 4 = 10, then value of cell ((value of cell 1 at time 4) + 0) at time (4 + 1) = value of cell 3 at time 4 (Store Instruction Property)
2	(value of cell 1 at time 4) + 0 = 127 + 0	if value of cell 1 at time 4 = 127, then (value of cell 1 at time 4) + 0 = 127 + 0 (Additive Property of Equality)
3	127 + 0 = 127	127 + 0 = 127 (Additive Identity)
4	(value of cell 1 at time 4) + 0 = 127	if (value of cell 1 at time 4) + 0 = 127 + 0 and 127 + 0 = 127, then (value of cell 1 at time 4) + 0 = 127 (Transitive Property of Equality)
5	value of cell ((value of cell 1 at time 4) + 0) at time (4 + 1) = value of cell 127 at time (4 + 1)	if (value of cell 1 at time 4) + 0 = 127, then value of cell ((value of cell 1 at time 4) + 0) at time (4 + 1) = value of cell 127 at time (4 + 1) (Substitution)
6	4 + 1 = 5	4 + 1 = 5 (Fixed Value Statement)
7	value of cell 127 at time (4 + 1) = value of cell 127 at time 5	if 4 + 1 = 5, then value of cell 127 at time (4 + 1) = value of cell 127 at time 5 (Substitution)
8	value of cell 127 at time 5 = value of cell 3 at time 4	if value of cell ((value of cell 1 at time 4) + 0) at time (4 + 1) = value of cell 127 at time (4 + 1) and value of cell 127 at time (4 + 1) = value of cell 127 at time 5 and value of cell ((value of cell 1 at time 4) + 0) at time (4 + 1) = value of cell 3 at time 4, then value of cell 127 at time 5 = value of cell 3 at time 4 (Transitive With Four)
9	value of cell 127 at time 5 = 2	if value of cell 127 at time 5 = value of cell 3 at time 4 and value of cell 3 at time 4 = 2, then value of cell 127 at time 5 = 2 (Transitive Property of Equality)

Comments

Please log in to add comments