Proof: ADDI Instruction Example 2

Let's prove the following theorem:

This proof shows that an ADDI instruction that stores the sum in memory cell #2 does not affect memory cell #1. It uses ADDI Instruction Property 2 and performs some basic algebra to compute the value of memory cell #1 at time 1.

Note that src and imm are left as variables because these values do not affect memory cell #1. In other words, this property is true regardless of the value of src and imm.

For reference, here is the simulator. We cannot use variable values so src is set to 1 and imm is 5:

Proof:

Proof Table

#	Claim	Reason
1	not (1 = 2)	not (1 = 2) (Fixed Value Statement)
2	value of cell 1 at time (0 + 1) = value of cell 1 at time 0	if instruction #0 is addi dst=2 src=src imm=imm and the PC at time 0 = 0 and not (1 = 2), then value of cell 1 at time (0 + 1) = value of cell 1 at time 0 (ADDI Instruction Property 2)
3	0 + 1 = 1	0 + 1 = 1 (Additive Identity Variation)
4	value of cell 1 at time (0 + 1) = value of cell 1 at time 1	if 0 + 1 = 1, then value of cell 1 at time (0 + 1) = value of cell 1 at time 1 (Substitution)
5	value of cell 1 at time 1 = 4	if value of cell 1 at time (0 + 1) = value of cell 1 at time 0 and value of cell 1 at time (0 + 1) = value of cell 1 at time 1 and value of cell 1 at time 0 = 4, then value of cell 1 at time 1 = 4 (Transitive Property Application 2)

Comments

Please log in to add comments