Proof: Sort Example

Let's prove the following theorem:

Proof:

Proof Table

#	Claim	Reason
1	result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ]	result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] (Sort List Property)
2	index of the mininum value in stack [ [ 0, [ ] ], [ ] ] = [ 0, [ ] ]	index of the mininum value in stack [ [ 0, [ ] ], [ ] ] = [ 0, [ ] ] (minimum_index_one)
3	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ]) = remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ]	if index of the mininum value in stack [ [ 0, [ ] ], [ ] ] = [ 0, [ ] ], then remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ]) = remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] (Substitution)
4	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = [ ]	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = [ ] (pop_index_base)
5	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ]) = [ ]	if remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ]) = remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = [ ], then remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ]) = [ ] (Transitive Property of Equality)
6	minimum value of stack [ [ 0, [ ] ], [ ] ] = [ 0, [ ] ]	minimum value of stack [ [ 0, [ ] ], [ ] ] = [ 0, [ ] ] (Minimum Of A Single Element List)
7	result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ]	if remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ]) = [ ], then result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] (Substitution)
8	[ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]	if minimum value of stack [ [ 0, [ ] ], [ ] ] = [ 0, [ ] ], then [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ] (Substitution)
9	result of sorting [ ] with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ]	if [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ], then result of sorting [ ] with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ] (Substitution)
10	result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ]	if result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] and result of sorting [ ] with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ], then result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ] (Transitive Property of Equality)
11	result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ]	if result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] and result of sorting (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index (index of the mininum value in stack [ [ 0, [ ] ], [ ] ])) with sorted stack [ minimum value of stack [ [ 0, [ ] ], [ ] ], [ ] ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ], then result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ] (Transitive Property of Equality)
12	result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]	result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ] (Sorted List Property)
13	result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = [ [ 0, [ ] ], [ ] ]	if result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ] and result of sorting [ ] with sorted stack [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ], then result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = [ [ 0, [ ] ], [ ] ] (Transitive Property of Equality)
14	result of sorting [ [ 0, [ ] ], [ ] ] = reverse of (result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ])	result of sorting [ [ 0, [ ] ], [ ] ] = reverse of (result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ]) (Sort Begin Property)
15	reverse of (result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ]) = reverse of [ [ 0, [ ] ], [ ] ]	if result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ] = [ [ 0, [ ] ], [ ] ], then reverse of (result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ]) = reverse of [ [ 0, [ ] ], [ ] ] (Substitution)
16	result of sorting [ [ 0, [ ] ], [ ] ] = reverse of [ [ 0, [ ] ], [ ] ]	if result of sorting [ [ 0, [ ] ], [ ] ] = reverse of (result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ]) and reverse of (result of sorting [ [ 0, [ ] ], [ ] ] with sorted stack [ ]) = reverse of [ [ 0, [ ] ], [ ] ], then result of sorting [ [ 0, [ ] ], [ ] ] = reverse of [ [ 0, [ ] ], [ ] ] (Transitive Property of Equality)
17	reverse of [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]	reverse of [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ] (reverse_one)
18	result of sorting [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]	if result of sorting [ [ 0, [ ] ], [ ] ] = reverse of [ [ 0, [ ] ], [ ] ] and reverse of [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ], then result of sorting [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ] (Transitive Property of Equality)

Comments

Please log in to add comments