Proof: BEQ Instruction Example 3

Let's prove the following theorem:

The following example shows that when the BEQ instruction is executed, memory values remain unchanged.

Proof:

Proof Table

#	Claim	Reason
1	value of cell x at time (0 + 1) = value of cell x at time 0	if instruction #0 is beq left=left right=right imm=imm and the PC at time 0 = 0, then value of cell x at time (0 + 1) = value of cell x at time 0 (BEQ Instruction Property 3)
2	0 + 1 = 1	0 + 1 = 1 (Additive Identity Variation)
3	value of cell x at time (0 + 1) = value of cell x at time 1	if 0 + 1 = 1, then value of cell x at time (0 + 1) = value of cell x at time 1 (Substitution)
4	value of cell x at time 1 = value of cell x at time 0	if value of cell x at time (0 + 1) = value of cell x at time 1 and value of cell x at time (0 + 1) = value of cell x at time 0, then value of cell x at time 1 = value of cell x at time 0 (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments