I am trying to prove the invariant of the inner while of Insertion sort here is the code:   for i = 1 to length(A)    x = A[i]    j = i - 1    while j >= 0 and A[j] > x        A[j+1]  A[j]        j  j - 1    end while    A[j+1] = x end forNow the invariant of the while is this : Let A' [] be the original array and A[] be the array when it is manipulated by the while loop,then : every time we reach the line with the while loop every element x of the current sub-array A[j+2,..i], x> key and the current  subarray A[j+2,..i] is the same as A'[j+1,...,i-1].Now for the first part of the invariant why exactly the lower bound is j+2 ? I guess since we cannot count how many times we will j <- j-1 let's just pick something in the form j+k .Let k be 1 then in the original array it will be A'[j+1,....,i] and in the subarray it will be A[j+2,...,i-1] because of the shift it performs.So j+2 is just some number ofcourse we could have pick j+2 or j+3 for example?
Invariant of Insertion sort
algorithms;algorithm analysis;invariants