6.5-5

6.5-5 Argue the correctness of HEAP-INCREASE-KEY using the following loop invariant: At the start of each iteration of the while loop of lines 4–6, the subarray A[1..A.heap-size] satisfies the max-heap property, except that there may be one violation: A[i] may be larger than A[PARENT(i)]. You may assume that the subarray A[1 ..A:heap-size] satisfies the max-heap property at the time HEAP-INCREASE-KEY is called.

Initialization:
Before the start of the loop we replace A[i] with key and key is greater than A[i]. There may be one violation where A[i] may be larger than A[Parent(i)].
Maintenance:
After the iteration of i the sub array A[1...A.heap-size] satisfies the max-heap property but still there may be one violation where A[i] may be larger than A[parent(i)]. Because even after exchanging A[i] with A[j=parent(i)]. A[j] may be larger than A[parent(j)].
Termination: when the loop terminates the sub array A[1..A.heap-size] satisfies the max-heap property.