Proof: Sort Example

Let's prove the following theorem:

In this example, we prove that when we sort

[3,[2,[1,[]]]]

we get

[1, [2, [3, []]]]

First, we use the "Sort Begin Property" to initialize the "sorted list" to [ ]. Then we begin popping maximum values from the original list and pushing them into the "sorted list."

First, we pop 3 at index 0 and push it into the "sorted list." Step 9 shows that the remainig elements are now [2, [1, []]] and the "sorted list" is [3, []].

Then we pop 2 at index 0. Step 18 shows that the remainig elements are now [1, []] and the "sorted list" is [2, [3, []]].

Finally, we pop 1 at index 0. Step 25 shows that the remainig elements are now [ ] and the "sorted list" is [1, [2, [3, []]]].

Since the remaining list is now empty, the "sorted list" is the final result of the sorting operation.

Proof:

Proof Table

#	Claim	Reason
1	result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ]	result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] (Sort Begin Property)
2	result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ]	result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] (Sort List Property)
3	maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 3	maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 3 (maximum_example_2)
4	index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 0	index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 0 (maximum_index_example)
5	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0	if index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 0, then remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0 (Substitution)
6	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0 = [ 2, [ 1, [ ] ] ]	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0 = [ 2, [ 1, [ ] ] ] (pop_index_example_2)
7	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = [ 2, [ 1, [ ] ] ]	if remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0 and remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0 = [ 2, [ 1, [ ] ] ], then remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = [ 2, [ 1, [ ] ] ] (Transitive Property of Equality)
8	[ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = [ 3, [ ] ]	if maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 3, then [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = [ 3, [ ] ] (Substitution)
9	result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ]	if remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = [ 2, [ 1, [ ] ] ] and [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = [ 3, [ ] ], then result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] (Substitution)
10	result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ]	result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] (Sort List Property)
11	maximum value in stack [ 2, [ 1, [ ] ] ] = 2	maximum value in stack [ 2, [ 1, [ ] ] ] = 2 (maximum_example)
12	index of the maximum value in stack [ 2, [ 1, [ ] ] ] = 0	index of the maximum value in stack [ 2, [ 1, [ ] ] ] = 0 (maximum_index_example_2)
13	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0	if index of the maximum value in stack [ 2, [ 1, [ ] ] ] = 0, then remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0 (Substitution)
14	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0 = [ 1, [ ] ]	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0 = [ 1, [ ] ] (pop_index_example_3)
15	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = [ 1, [ ] ]	if remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0 and remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0 = [ 1, [ ] ], then remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = [ 1, [ ] ] (Transitive Property of Equality)
16	[ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ]	if maximum value in stack [ 2, [ 1, [ ] ] ] = 2, then [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ] (Substitution)
17	result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ]	if remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = [ 1, [ ] ] and [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ], then result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] (Substitution)
18	result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ]	result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] (Sort List Property)
19	maximum value in stack [ 1, [ ] ] = 1	maximum value in stack [ 1, [ ] ] = 1 (Maximum Of A Single Element List)
20	index of the maximum value in stack [ 1, [ ] ] = 0	index of the maximum value in stack [ 1, [ ] ] = 0 (maximum_index_one_element_example)
21	remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = remaining elements after [ 1, [ ] ] is popped at index 0	if index of the maximum value in stack [ 1, [ ] ] = 0, then remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = remaining elements after [ 1, [ ] ] is popped at index 0 (Substitution)
22	remaining elements after [ 1, [ ] ] is popped at index 0 = [ ]	remaining elements after [ 1, [ ] ] is popped at index 0 = [ ] (pop_index_one_element_example)
23	remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = [ ]	if remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = remaining elements after [ 1, [ ] ] is popped at index 0 and remaining elements after [ 1, [ ] ] is popped at index 0 = [ ], then remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = [ ] (Transitive Property of Equality)
24	[ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]	if maximum value in stack [ 1, [ ] ] = 1, then [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Substitution)
25	result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ]	if remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = [ ] and [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ], then result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ] (Substitution)
26	result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]	result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Sorted List Property)
27	result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]	if result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] and result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ] and result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ], then result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Transitive Property Application 1)
28	result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]	if result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] and result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] and result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ], then result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Transitive Property Application 1)
29	result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = [ 1, [ 2, [ 3, [ ] ] ] ]	if result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] and result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] and result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = [ 1, [ 2, [ 3, [ ] ] ] ], then result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Transitive Property Application 1)
30	result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]	if result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] and result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = [ 1, [ 2, [ 3, [ ] ] ] ], then result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments