Proof Obligation 3

Show

   INV and ~(k < b) ==> POST

Rewrite boolean:

   INV and k >= b  ==>  k = b

so substitute b in for k in INV:

   INV k/b :  
      a <= b <= b  
         and  forall i, a <= i <  b : x[i] = x0[i+1]  
         and  forall i, b <= i <= b : x[i] = x0[i]

POST is a direct clause of this assertion.

QED

Note: We could also prove x[b] is not shifted, if had included such an assertion in POST.