Hello!!
I want to show that Insetion Sort is stable...
Is the invariant the following??
At the beginning of each iteration of the for loop, if $A[a]=A[b], a<b \leq j-1$, then $A[a]$ appears before $A[b]$.
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[…