Proof: BEQ Instruction Example 2

Let's prove the following theorem:

if the following are true:

instruction #0 is beq left=1 right=2 imm=2
the PC at time 0 = 0
value of cell 1 at time 0 = 1
value of cell 2 at time 0 = 2

then the PC at time 1 = 1

The following example shows that when the value stored in the left cell (cell #1) is not equal to the value in the right cell (cell #2), the PC is incremented by 1.

Instructions

Memory Cells

Program Counter	Time
0	0

LW Computer Simulator

Proof:

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

Given

1	instruction #0 is `beq left=1 right=2 imm=2`
2	the PC at time 0 = 0
3	value of cell 1 at time 0 = 1
4	value of cell 2 at time 0 = 2

Proof Table

#	Claim	Reason
1	not (1 = 2)	not (1 = 2) (Fixed Value Statement)
2	value of cell 1 at time 0 = 2 = 1 = 2	if value of cell 1 at time 0 = 1, then value of cell 1 at time 0 = 2 = 1 = 2 (Substitution)
3	value of cell 1 at time 0 = value of cell 2 at time 0 = value of cell 1 at time 0 = 2	if value of cell 2 at time 0 = 2, then value of cell 1 at time 0 = value of cell 2 at time 0 = value of cell 1 at time 0 = 2 (Substitution)
4	value of cell 1 at time 0 = value of cell 2 at time 0 = 1 = 2	if value of cell 1 at time 0 = value of cell 2 at time 0 = value of cell 1 at time 0 = 2 and value of cell 1 at time 0 = 2 = 1 = 2, then value of cell 1 at time 0 = value of cell 2 at time 0 = 1 = 2 (Transitive Property of Equality)
5	not (value of cell 1 at time 0 = value of cell 2 at time 0) = not (1 = 2)	if value of cell 1 at time 0 = value of cell 2 at time 0 = 1 = 2, then not (value of cell 1 at time 0 = value of cell 2 at time 0) = not (1 = 2) (Substitution)
6	not (value of cell 1 at time 0 = value of cell 2 at time 0)	if not (1 = 2) and not (value of cell 1 at time 0 = value of cell 2 at time 0) = not (1 = 2), then not (value of cell 1 at time 0 = value of cell 2 at time 0) (Truth Propagation Property 2)
7	the PC at time (0 + 1) = 0 + 1	if instruction #0 is `beq left=1 right=2 imm=2` and the PC at time 0 = 0 and not (value of cell 1 at time 0 = value of cell 2 at time 0), then the PC at time (0 + 1) = 0 + 1 (BEQ Instruction Property 2)
8	0 + 1 = 1	0 + 1 = 1 (Additive Identity Variation)
9	the PC at time (0 + 1) = the PC at time 1	if 0 + 1 = 1, then the PC at time (0 + 1) = the PC at time 1 (Substitution)
10	the PC at time 1 = 0 + 1	if the PC at time (0 + 1) = the PC at time 1 and the PC at time (0 + 1) = 0 + 1, then the PC at time 1 = 0 + 1 (Transitive Property of Equality Variation 2)
11	the PC at time 1 = 1	if the PC at time 1 = 0 + 1 and 0 + 1 = 1, then the PC at time 1 = 1 (Transitive Property of Equality)

Comments

Please log in to add comments