Proof: Byte 3 Stays the Same 6

Let's prove the following theorem:

if the following are true:
  • subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12
  • the PC at time 6 = 12
  • value of cell 3 at time 6 = 3

then value of cell 3 at time 7 = 3

Proof:

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

Given
1 subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12
2 the PC at time 6 = 12
3 value of cell 3 at time 6 = 3
Proof Table
# Claim Reason
1 not (3 = 1) not (3 = 1)
2 value of cell 3 at time (6 + 1) = value of cell 3 at time 6 if subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12 and the PC at time 6 = 12 and not (3 = 1), then value of cell 3 at time (6 + 1) = value of cell 3 at time 6
3 6 + 1 = 7 6 + 1 = 7
4 value of cell 3 at time (6 + 1) = value of cell 3 at time 7 if 6 + 1 = 7, then value of cell 3 at time (6 + 1) = value of cell 3 at time 7
5 value of cell 3 at time 7 = value of cell 3 at time 6 if value of cell 3 at time (6 + 1) = value of cell 3 at time 7 and value of cell 3 at time (6 + 1) = value of cell 3 at time 6, then value of cell 3 at time 7 = value of cell 3 at time 6
6 value of cell 3 at time 7 = 3 if value of cell 3 at time 7 = value of cell 3 at time 6 and value of cell 3 at time 6 = 3, then value of cell 3 at time 7 = 3

Comments

Please log in to add comments