Proof: Beq No Branch 14

Let's prove the following theorem:

if the following are true:
  • instruction #8 is beq left=4 right=5 imm=1
  • the PC at time 14 = 8
  • value of cell 4 at time 14 = 2
  • value of cell 5 at time 14 = 4

then the PC at time 15 = 9

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 #8 is beq left=4 right=5 imm=1
2 the PC at time 14 = 8
3 value of cell 4 at time 14 = 2
4 value of cell 5 at time 14 = 4
Proof Table
# Claim Reason
1 value of cell 4 at time 14 = 4 = 2 = 4 if value of cell 4 at time 14 = 2, then value of cell 4 at time 14 = 4 = 2 = 4
2 not (value of cell 4 at time 14 = 4) = not (2 = 4) if value of cell 4 at time 14 = 4 = 2 = 4, then not (value of cell 4 at time 14 = 4) = not (2 = 4)
3 not (2 = 4) not (2 = 4)
4 not (value of cell 4 at time 14 = 4) if not (2 = 4) and not (value of cell 4 at time 14 = 4) = not (2 = 4), then not (value of cell 4 at time 14 = 4)
5 value of cell 4 at time 14 = value of cell 5 at time 14 = value of cell 4 at time 14 = 4 if value of cell 5 at time 14 = 4, then value of cell 4 at time 14 = value of cell 5 at time 14 = value of cell 4 at time 14 = 4
6 not (value of cell 4 at time 14 = value of cell 5 at time 14) = not (value of cell 4 at time 14 = 4) if value of cell 4 at time 14 = value of cell 5 at time 14 = value of cell 4 at time 14 = 4, then not (value of cell 4 at time 14 = value of cell 5 at time 14) = not (value of cell 4 at time 14 = 4)
7 not (value of cell 4 at time 14 = value of cell 5 at time 14) if not (value of cell 4 at time 14 = 4) and not (value of cell 4 at time 14 = value of cell 5 at time 14) = not (value of cell 4 at time 14 = 4), then not (value of cell 4 at time 14 = value of cell 5 at time 14)
8 the PC at time (14 + 1) = 8 + 1 if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 14 = 8 and not (value of cell 4 at time 14 = value of cell 5 at time 14), then the PC at time (14 + 1) = 8 + 1
9 14 + 1 = 15 14 + 1 = 15
10 the PC at time (14 + 1) = the PC at time 15 if 14 + 1 = 15, then the PC at time (14 + 1) = the PC at time 15
11 8 + 1 = 9 8 + 1 = 9
12 the PC at time 15 = 9 if the PC at time (14 + 1) = 8 + 1 and the PC at time (14 + 1) = the PC at time 15 and 8 + 1 = 9, then the PC at time 15 = 9

Comments

Please log in to add comments