Is the invariant the following?? (Wondering)
At the beginning of each iteration of the for loop, if $A[a]=A, a<b \leq j-1$, then $A[a]$ appears before $A$.
Initialization:
We have to show that the invariant holds before the first iteration of the loop where $j=2$. In this case, the subarray $A[1 \dots j-1]$ consists of only the element $A[1]$, so there are no $a<b \leq j-1=1$. So, the invariant holds trivially.
Maintenance:
We have to check if the property maintains at each iteration. The body of the outer for loop shifts the elements $A[j-1], A[j-2], A[j-3], \dots$ one position to the right until the right position for $A[j]$ is found, at which the value of $A[j]$ will be inserted, but it doesn't change their order. SO, if the invariant holds before an iteration of the loop, it still holds before the next iteration.
Termination:
We have to check what happens when the loop stops. The outer for loop stops when $j=n+1$. Setting $j=n+1$ at the invariant loop, we have that for each $A[a]=A, a<b \leq n$, it implies that $A[a]$ appears before $A$ at the initial subarray. But the subarray $A[1 \dots n]$ is the whole array. So, Insertion Sort is stable.
Is this correct?? (Wondering) Could I improve something?? (Wondering)