Proof: Beq No Branch 20

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 20 = 8
  • value of cell 4 at time 20 = 3
  • value of cell 5 at time 20 = 4

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

Comments

Please log in to add comments