Show
PRE ==> P1 (clause-by-clause in P1)
a<=a<=bsimplifies to a<=b which is in PRE
forall i, a <= i < a : x[i]=x0[i+1]has a null range ( a < a ) so drops out
forall i, a <= i <= b : x[i] = x0[i]the range covers entire array extent, and is essentially the structural definition of x = x0 when x and x0 are arrays, (stated in predicate calculus)