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.heapsize]$ 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[a..heapsize]$ satisfies the max-heap property at the time HEAP-INCREASE-KEY is called.