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 9 Stays the Same 7

Let's prove the following theorem:

if the following are true:
  • instruction #0 is load dst=7 addr=5 imm=0
  • the PC at time 7 = 0
  • value of cell 9 at time 7 = 31

then value of cell 9 at time 8 = 31

Proof:

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

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

Comments

Please log in to add comments