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 4 Stays the Same 10

Let's prove the following theorem:

if the following are true:
  • instruction #3 is addi dst=6 src=6 imm=1
  • the PC at time 10 = 3
  • value of cell 4 at time 10 = 1

then value of cell 4 at time 11 = 1

Proof:

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

Given
1 instruction #3 is addi dst=6 src=6 imm=1
2 the PC at time 10 = 3
3 value of cell 4 at time 10 = 1
Proof Table
# Claim Reason
1 not (4 = 6) not (4 = 6)
2 value of cell 4 at time (10 + 1) = value of cell 4 at time 10 if instruction #3 is addi dst=6 src=6 imm=1 and the PC at time 10 = 3 and not (4 = 6), then value of cell 4 at time (10 + 1) = value of cell 4 at time 10
3 10 + 1 = 11 10 + 1 = 11
4 value of cell 4 at time (10 + 1) = value of cell 4 at time 11 if 10 + 1 = 11, then value of cell 4 at time (10 + 1) = value of cell 4 at time 11
5 value of cell 4 at time 11 = value of cell 4 at time 10 if value of cell 4 at time (10 + 1) = value of cell 4 at time 11 and value of cell 4 at time (10 + 1) = value of cell 4 at time 10, then value of cell 4 at time 11 = value of cell 4 at time 10
6 value of cell 4 at time 11 = 1 if value of cell 4 at time 11 = value of cell 4 at time 10 and value of cell 4 at time 10 = 1, then value of cell 4 at time 11 = 1
Previous Lesson Next Lesson

Comments

Please log in to add comments