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

Let's prove the following theorem:

if the following are true:
  • instruction #5 is beq left=3 right=4 imm=1
  • the PC at time 12 = 5
  • value of cell 7 at time 12 = 31

then value of cell 7 at time 13 = 31

Proof:

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

Given
1 instruction #5 is beq left=3 right=4 imm=1
2 the PC at time 12 = 5
3 value of cell 7 at time 12 = 31
Proof Table
# Claim Reason
1 value of cell 7 at time (12 + 1) = value of cell 7 at time 12 if instruction #5 is beq left=3 right=4 imm=1 and the PC at time 12 = 5, then value of cell 7 at time (12 + 1) = value of cell 7 at time 12
2 12 + 1 = 13 12 + 1 = 13
3 value of cell 7 at time (12 + 1) = value of cell 7 at time 13 if 12 + 1 = 13, then value of cell 7 at time (12 + 1) = value of cell 7 at time 13
4 value of cell 7 at time 13 = value of cell 7 at time 12 if value of cell 7 at time (12 + 1) = value of cell 7 at time 13 and value of cell 7 at time (12 + 1) = value of cell 7 at time 12, then value of cell 7 at time 13 = value of cell 7 at time 12
5 value of cell 7 at time 13 = 31 if value of cell 7 at time 13 = value of cell 7 at time 12 and value of cell 7 at time 12 = 31, then value of cell 7 at time 13 = 31
Previous Lesson Next Lesson

Comments

Please log in to add comments