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 7 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 7 at time 1 = 24
value of cell 6 at time 1 = 12

then value of cell 7 at time 2 = 24

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 7 at time 1 = 24
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 (Substitution)
2	12 + 0 = 12	12 + 0 = 12 (Additive Identity)
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 (Transitive Property of Equality)
4	7 = (value of cell 6 at time 1) + 0 = 7 = 12	if (value of cell 6 at time 1) + 0 = 12, then 7 = (value of cell 6 at time 1) + 0 = 7 = 12 (Substitution)
5	not (7 = (value of cell 6 at time 1) + 0) = not (7 = 12)	if 7 = (value of cell 6 at time 1) + 0 = 7 = 12, then not (7 = (value of cell 6 at time 1) + 0) = not (7 = 12) (Substitution)
6	not (7 = 12)	not (7 = 12) (Fixed Value Statement)
7	not (7 = (value of cell 6 at time 1) + 0)	if not (7 = 12) and not (7 = (value of cell 6 at time 1) + 0) = not (7 = 12), then not (7 = (value of cell 6 at time 1) + 0) (Truth Propagation Property 2)
8	value of cell 7 at time (1 + 1) = value of cell 7 at time 1	if instruction #1 is `store src=7 addr=6 imm=0` and the PC at time 1 = 1 and not (7 = (value of cell 6 at time 1) + 0), then value of cell 7 at time (1 + 1) = value of cell 7 at time 1 (Store Instruction Property 2)
9	1 + 1 = 2	1 + 1 = 2 (Fixed Value Statement)
10	value of cell 7 at time (1 + 1) = value of cell 7 at time 2	if 1 + 1 = 2, then value of cell 7 at time (1 + 1) = value of cell 7 at time 2 (Substitution)
11	value of cell 7 at time 2 = value of cell 7 at time 1	if value of cell 7 at time (1 + 1) = value of cell 7 at time 2 and value of cell 7 at time (1 + 1) = value of cell 7 at time 1, then value of cell 7 at time 2 = value of cell 7 at time 1 (Transitive Property of Equality Variation 2)
12	value of cell 7 at time 2 = 24	if value of cell 7 at time 2 = value of cell 7 at time 1 and value of cell 7 at time 1 = 24, then value of cell 7 at time 2 = 24 (Transitive Property of Equality)

Previous Lesson Next Lesson

Comments

Please log in to add comments