Transitive Property of Equality Variation 2

Transitive Property Application 2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Proof: Byte 3 Stays the Same Store 15

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 15 = 1
value of cell 3 at time 15 = 3
value of cell 6 at time 15 = 14

then value of cell 3 at time 16 = 3

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 15 = 1
3	value of cell 3 at time 15 = 3
4	value of cell 6 at time 15 = 14

Proof Table

#	Claim	Reason
1	(value of cell 6 at time 15) + 0 = 14 + 0	if value of cell 6 at time 15 = 14, then (value of cell 6 at time 15) + 0 = 14 + 0 (Substitution)
2	14 + 0 = 14	14 + 0 = 14 (Additive Identity)
3	(value of cell 6 at time 15) + 0 = 14	if (value of cell 6 at time 15) + 0 = 14 + 0 and 14 + 0 = 14, then (value of cell 6 at time 15) + 0 = 14 (Transitive Property of Equality)
4	3 = (value of cell 6 at time 15) + 0 = 3 = 14	if (value of cell 6 at time 15) + 0 = 14, then 3 = (value of cell 6 at time 15) + 0 = 3 = 14 (Substitution)
5	not (3 = (value of cell 6 at time 15) + 0) = not (3 = 14)	if 3 = (value of cell 6 at time 15) + 0 = 3 = 14, then not (3 = (value of cell 6 at time 15) + 0) = not (3 = 14) (Substitution)
6	not (3 = 14)	not (3 = 14) (Fixed Value Statement)
7	not (3 = (value of cell 6 at time 15) + 0)	if not (3 = 14) and not (3 = (value of cell 6 at time 15) + 0) = not (3 = 14), then not (3 = (value of cell 6 at time 15) + 0) (Truth Propagation Property 2)
8	value of cell 3 at time (15 + 1) = value of cell 3 at time 15	if instruction #1 is `store src=7 addr=6 imm=0` and the PC at time 15 = 1 and not (3 = (value of cell 6 at time 15) + 0), then value of cell 3 at time (15 + 1) = value of cell 3 at time 15 (Store Instruction Property 2)
9	15 + 1 = 16	15 + 1 = 16 (Fixed Value Statement)
10	value of cell 3 at time (15 + 1) = value of cell 3 at time 16	if 15 + 1 = 16, then value of cell 3 at time (15 + 1) = value of cell 3 at time 16 (Substitution)
11	value of cell 3 at time 16 = value of cell 3 at time 15	if value of cell 3 at time (15 + 1) = value of cell 3 at time 16 and value of cell 3 at time (15 + 1) = value of cell 3 at time 15, then value of cell 3 at time 16 = value of cell 3 at time 15 (Transitive Property of Equality Variation 2)
12	value of cell 3 at time 16 = 3	if value of cell 3 at time 16 = value of cell 3 at time 15 and value of cell 3 at time 15 = 3, then value of cell 3 at time 16 = 3 (Transitive Property of Equality)

Previous Lesson Next Lesson

Comments

Please log in to add comments