Proof Obligation 1

Show

   PRE ==> P1  (clause-by-clause in P1)

```
a<=a<=b 
```
simplifies 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)

QED