Show
INV and ~(k < b) ==> POSTRewrite boolean:
INV and k >= b ==> k = bso 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.