Can we provide a proof for the correctness of the following quick sort algorithm:
quicksort(a1,a2,...an) {
(b) less := the empty list (c) greater := the empty list
pivot = a1
for i := 2 to n
if ai < a1, adjoin ai to the list "less"
else adjoin ai to the list "greater"
(m = length(less) and k = length(greater))
if m /= 0, then quicksort (b1,b2...bm)
if k /= 0, then quicksort (c1,c2,..ck)
to put the sorted lists back into a
for i := 1 to m
ai = bi
am+1 = pivot
for i := 1 to k
am+i+1 = ci }