Argue the correctness of HEAPSORT using the following loop invariant:

At the start of each iteration of the for loop on lines 2-5, the subarray \(A[1\dots i]\) is a max-heap containing the \(i\) smallest elements of \(A[1 \dots n]\), and the subarray \(A[i+1\dots n]\) contains the \(n - i\) largest elements of \(A[1\dots n]\), sorted.

Initialization: Immediately prior to the first iteration of the loop we perform BUILD-MAX-HEAP on our heap and the subarray \(A[1\dots i]\) is in fact the entire heap because \(i = n\). Therefore \(A[1\dots i]\) trivially contains the \(i\) smallest elements of \(A\), and \(A[i+1\dots n]\) is empty.

Maintenance: Each iteration of the for loop decrements \(i\) by \(1\) after shifting the largest element from \(A[i\dots 1]\) to \(A[i+1\dots n]\). Because we are always shifting the largest element, it must be true that only the smallest elements remain in \(A[1\dots i]\). Likewise, \(A[i+1\dots n]\) represents the \(n-i\) elements that have already been shifted and so must contain the largest elements of \(A\) in increasing order.

Termination: The loop terminates when \(i=1\) at which point \(A[1\dots i]\) contains one element: the smallest element of \(A\). In addition, we have shifted \(n-1\) elements into \(A[2\dots n]\) which are the \(n-1\) largest elements of \(A\) in increasing order. Thus \(A\) is sorted.