Zero Plus a
Transitive Property of Equality Variation 2
Load 0
Transitive Property Application 2
Pc 0
Byte 3 Stays the Same 0
Byte 4 Stays the Same 0
Byte 5 Stays the Same 0
Byte 6 Stays the Same 0
Byte 8 Stays the Same 0
Byte 9 Stays the Same 0
Byte 10 Stays the Same 0
Transitive With Four
Store 1
Pc 1
Truth Propagation Property 2
Byte 3 Stays the Same Store 1
Byte 4 Stays the Same Store 1
Byte 5 Stays the Same Store 1
Byte 6 Stays the Same Store 1
Byte 8 Stays the Same Store 1
Byte 9 Stays the Same Store 1
Byte 10 Stays the Same Store 1
Byte 7 Stays the Same Store 1
Commutative Property Variation 1
Substitution 2
Substitution 6
Addi Insn 2
Pc 2
Byte 3 Stays the Same 2
Byte 4 Stays the Same 2
Byte 6 Stays the Same 2
Byte 8 Stays the Same 2
Byte 9 Stays the Same 2
Byte 10 Stays the Same 2
Byte 7 Stays the Same 2
Byte 12 Stays the Same 2
Addi Insn 3
Pc 3
Byte 3 Stays the Same 3
Byte 4 Stays the Same 3
Byte 5 Stays the Same 3
Byte 8 Stays the Same 3
Byte 9 Stays the Same 3
Byte 10 Stays the Same 3
Byte 7 Stays the Same 3
Byte 12 Stays the Same 3
Addi Insn 4
Pc 4
Byte 3 Stays the Same 4
Byte 5 Stays the Same 4
Byte 6 Stays the Same 4
Byte 8 Stays the Same 4
Byte 9 Stays the Same 4
Byte 10 Stays the Same 4
Byte 7 Stays the Same 4
Byte 12 Stays the Same 4
Beq No Branch 5
Byte 3 Stays the Same 5
Byte 4 Stays the Same 5
Byte 5 Stays the Same 5
Byte 6 Stays the Same 5
Byte 8 Stays the Same 5
Byte 9 Stays the Same 5
Byte 10 Stays the Same 5
Byte 7 Stays the Same 5
Byte 12 Stays the Same 5
Jump Help 6
Byte 3 Stays the Same 6
Byte 4 Stays the Same 6
Byte 5 Stays the Same 6
Byte 6 Stays the Same 6
Byte 8 Stays the Same 6
Byte 9 Stays the Same 6
Byte 10 Stays the Same 6
Byte 7 Stays the Same 6
Byte 12 Stays the Same 6
Load 7
Pc 7
Byte 3 Stays the Same 7
Byte 4 Stays the Same 7
Byte 5 Stays the Same 7
Byte 6 Stays the Same 7
Byte 8 Stays the Same 7
Byte 9 Stays the Same 7
Byte 10 Stays the Same 7
Byte 12 Stays the Same 7
Store 8
Pc 8
Byte 3 Stays the Same Store 8
Byte 4 Stays the Same Store 8
Byte 5 Stays the Same Store 8
Byte 6 Stays the Same Store 8
Byte 8 Stays the Same Store 8
Byte 9 Stays the Same Store 8
Byte 10 Stays the Same Store 8
Byte 7 Stays the Same Store 8
Byte 12 Stays the Same Store 8
Addi Insn 9
Pc 9
Byte 3 Stays the Same 9
Byte 4 Stays the Same 9
Byte 6 Stays the Same 9
Byte 8 Stays the Same 9
Byte 9 Stays the Same 9
Byte 10 Stays the Same 9
Byte 7 Stays the Same 9
Byte 12 Stays the Same 9
Byte 13 Stays the Same 9
Addi Insn 10
Pc 10
Byte 3 Stays the Same 10
Byte 4 Stays the Same 10
Byte 5 Stays the Same 10
Byte 8 Stays the Same 10
Byte 9 Stays the Same 10
Byte 10 Stays the Same 10
Byte 7 Stays the Same 10
Byte 12 Stays the Same 10
Byte 13 Stays the Same 10
Addi Insn 11
Pc 11
Byte 3 Stays the Same 11
Byte 5 Stays the Same 11
Byte 6 Stays the Same 11
Byte 8 Stays the Same 11
Byte 9 Stays the Same 11
Byte 10 Stays the Same 11
Byte 7 Stays the Same 11
Byte 12 Stays the Same 11
Byte 13 Stays the Same 11
Beq No Branch 12
Byte 3 Stays the Same 12
Byte 4 Stays the Same 12
Byte 5 Stays the Same 12
Byte 6 Stays the Same 12
Byte 8 Stays the Same 12
Byte 9 Stays the Same 12
Byte 10 Stays the Same 12
Byte 7 Stays the Same 12
Byte 12 Stays the Same 12
Byte 13 Stays the Same 12
Jump Help 13
Byte 3 Stays the Same 13
Byte 4 Stays the Same 13
Byte 5 Stays the Same 13
Byte 6 Stays the Same 13
Byte 8 Stays the Same 13
Byte 9 Stays the Same 13
Byte 10 Stays the Same 13
Byte 7 Stays the Same 13
Byte 12 Stays the Same 13
Byte 13 Stays the Same 13
Load 14
Pc 14
Byte 3 Stays the Same 14
Byte 4 Stays the Same 14
Byte 5 Stays the Same 14
Byte 6 Stays the Same 14
Byte 8 Stays the Same 14
Byte 9 Stays the Same 14
Byte 10 Stays the Same 14
Byte 12 Stays the Same 14
Byte 13 Stays the Same 14
Store 15
Pc 15
Byte 3 Stays the Same Store 15
Byte 4 Stays the Same Store 15
Byte 5 Stays the Same Store 15
Byte 6 Stays the Same Store 15
Byte 8 Stays the Same Store 15
Byte 9 Stays the Same Store 15
Byte 10 Stays the Same Store 15
Byte 7 Stays the Same Store 15
Byte 12 Stays the Same Store 15
Byte 13 Stays the Same Store 15
Addi Insn 16
Pc 16
Byte 3 Stays the Same 16
Byte 4 Stays the Same 16
Byte 6 Stays the Same 16
Byte 8 Stays the Same 16
Byte 9 Stays the Same 16
Byte 10 Stays the Same 16
Byte 7 Stays the Same 16
Byte 12 Stays the Same 16
Byte 13 Stays the Same 16
Byte 14 Stays the Same 16
Addi Insn 17
Pc 17
Byte 3 Stays the Same 17
Byte 4 Stays the Same 17
Byte 5 Stays the Same 17
Byte 8 Stays the Same 17
Byte 9 Stays the Same 17
Byte 10 Stays the Same 17
Byte 7 Stays the Same 17
Byte 12 Stays the Same 17
Byte 13 Stays the Same 17
Byte 14 Stays the Same 17
Addi Insn 18
Pc 18
Byte 3 Stays the Same 18
Byte 5 Stays the Same 18
Byte 6 Stays the Same 18
Byte 8 Stays the Same 18
Byte 9 Stays the Same 18
Byte 10 Stays the Same 18
Byte 7 Stays the Same 18
Byte 12 Stays the Same 18
Byte 13 Stays the Same 18
Byte 14 Stays the Same 18
Transitive Property of Equality Variation 1
Beq Branch
Byte 3 Stays the Same 19
Byte 4 Stays the Same 19
Byte 5 Stays the Same 19
Byte 6 Stays the Same 19
Byte 8 Stays the Same 19
Byte 9 Stays the Same 19
Byte 10 Stays the Same 19
Byte 7 Stays the Same 19
Byte 12 Stays the Same 19
Byte 13 Stays the Same 19
Byte 14 Stays the Same 19
Copyloadstore

Proof: Byte 10 Stays the Same Store 1

Let's prove the following theorem:

if the following are true:
  • instruction #1 is store src=7 addr=6 imm=0
  • the PC at time 1 = 1
  • value of cell 10 at time 1 = 45
  • value of cell 6 at time 1 = 12

then value of cell 10 at time 2 = 45

Proof:

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

Given
1 instruction #1 is store src=7 addr=6 imm=0
2 the PC at time 1 = 1
3 value of cell 10 at time 1 = 45
4 value of cell 6 at time 1 = 12
Proof Table
# Claim Reason
1 (value of cell 6 at time 1) + 0 = 12 + 0 if value of cell 6 at time 1 = 12, then (value of cell 6 at time 1) + 0 = 12 + 0
2 12 + 0 = 12 12 + 0 = 12
3 (value of cell 6 at time 1) + 0 = 12 if (value of cell 6 at time 1) + 0 = 12 + 0 and 12 + 0 = 12, then (value of cell 6 at time 1) + 0 = 12
4 10 = (value of cell 6 at time 1) + 0 = 10 = 12 if (value of cell 6 at time 1) + 0 = 12, then 10 = (value of cell 6 at time 1) + 0 = 10 = 12
5 not (10 = (value of cell 6 at time 1) + 0) = not (10 = 12) if 10 = (value of cell 6 at time 1) + 0 = 10 = 12, then not (10 = (value of cell 6 at time 1) + 0) = not (10 = 12)
6 not (10 = 12) not (10 = 12)
7 not (10 = (value of cell 6 at time 1) + 0) if not (10 = 12) and not (10 = (value of cell 6 at time 1) + 0) = not (10 = 12), then not (10 = (value of cell 6 at time 1) + 0)
8 value of cell 10 at time (1 + 1) = value of cell 10 at time 1 if instruction #1 is store src=7 addr=6 imm=0 and the PC at time 1 = 1 and not (10 = (value of cell 6 at time 1) + 0), then value of cell 10 at time (1 + 1) = value of cell 10 at time 1
9 1 + 1 = 2 1 + 1 = 2
10 value of cell 10 at time (1 + 1) = value of cell 10 at time 2 if 1 + 1 = 2, then value of cell 10 at time (1 + 1) = value of cell 10 at time 2
11 value of cell 10 at time 2 = value of cell 10 at time 1 if value of cell 10 at time (1 + 1) = value of cell 10 at time 2 and value of cell 10 at time (1 + 1) = value of cell 10 at time 1, then value of cell 10 at time 2 = value of cell 10 at time 1
12 value of cell 10 at time 2 = 45 if value of cell 10 at time 2 = value of cell 10 at time 1 and value of cell 10 at time 1 = 45, then value of cell 10 at time 2 = 45
Previous Lesson Next Lesson

Comments

Please log in to add comments