Proof: Subtracti Insn 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 1 at time 6 = 127

then value of cell 1 at time 7 = 126

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 1 at time 6 = 127
Proof Table
# Claim Reason
1 value of cell 1 at time (6 + 1) = (value of cell 1 at time 6) - 1 if subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12 and the PC at time 6 = 12, then value of cell 1 at time (6 + 1) = (value of cell 1 at time 6) - 1
2 6 + 1 = 7 6 + 1 = 7
3 value of cell 1 at time (6 + 1) = value of cell 1 at time 7 if 6 + 1 = 7, then value of cell 1 at time (6 + 1) = value of cell 1 at time 7
4 value of cell 1 at time 7 = (value of cell 1 at time 6) - 1 if value of cell 1 at time (6 + 1) = value of cell 1 at time 7 and value of cell 1 at time (6 + 1) = (value of cell 1 at time 6) - 1, then value of cell 1 at time 7 = (value of cell 1 at time 6) - 1
5 (value of cell 1 at time 6) - 1 = 127 - 1 if value of cell 1 at time 6 = 127, then (value of cell 1 at time 6) - 1 = 127 - 1
6 value of cell 1 at time 7 = 127 - 1 if value of cell 1 at time 7 = (value of cell 1 at time 6) - 1 and (value of cell 1 at time 6) - 1 = 127 - 1, then value of cell 1 at time 7 = 127 - 1
7 127 - 1 = 126 127 - 1 = 126
8 value of cell 1 at time 7 = 126 if value of cell 1 at time 7 = 127 - 1 and 127 - 1 = 126, then value of cell 1 at time 7 = 126

Comments

Please log in to add comments