(* Verification Conditions for Alt-Ergo *)


logic i, j, n, temp: int

goal intra_loop:
forall a : int farray.

((j<i) and 
(forall p, q: int. 0<= p<i+1=q <= n-1 -> a[p]<=a[q]) and 
(forall p, q: int. i<= p<=q <= n-1 -> a[p]<=a[q]) and 
(forall k: int. 0<= k <= j -> a[k]<=a[j]) and 
0<=j and 
j<=i and 
(i<n) and 
(i>0)  ->
     ((a[j]>a[j+1])  ->
          (forall p, q: int. 0<= p<i+1=q <= n-1 -> a[p]<=a[q]) and 
          (forall p, q: int. i<= p<=q <= n-1 -> a[p]<=a[q]) and 
          (forall k: int. 0<= k <= j+1 -> a[k]<=a[j]) and 
          0<=(j+1) and 
          (j+1)<=i and 
          (i<n) and 
          (i>0))
 and 
     (not((a[j]>a[j+1]))  ->
          (forall p, q: int. 0<= p<i+1=q <= n-1 -> a[p]<=a[q]) and 
          (forall p, q: int. i<= p<=q <= n-1 -> a[p]<=a[q]) and 
          (forall k: int. 0<= k <= j+1 -> a[k]<=a[j+1]) and 
          0<=(j+1) and 
          (j+1)<=i and 
          (i<n) and 
          (i>0))
)


goal exit:
forall a : int farray.

((j>=i) and 
(forall p, q: int. 0<= p<i+1=q <= n-1 -> a[p]<=a[q]) and 
(forall p, q: int. i<= p<=q <= n-1 -> a[p]<=a[q]) and 
(forall k: int. 0<= k <= j -> a[k]<=a[j]) and 
0<=j and 
j<=i and 
(i<n) and 
(i>0)  ->
     (forall p, q: int. i-1<= p<=q <= n-1 -> a[p]<=a[q]) and 
     (forall p, q: int. 0<= p<i=q <= n-1 -> a[p]<=a[q]) and 
     ((i-1)>=0) and 
     ((i-1)<n))


goal intra_loop:
forall a : int farray.

((i>0) and 
(forall p, q: int. i<= p<=q <= n-1 -> a[p]<=a[q]) and 
(forall p, q: int. 0<= p<i+1=q <= n-1 -> a[p]<=a[q]) and 
(i>=0) and 
(i<n)  ->
     (forall p, q: int. 0<= p<i+1=q <= n-1 -> a[p]<=a[q]) and 
     (forall p, q: int. i<= p<=q <= n-1 -> a[p]<=a[q]) and 
     (forall k: int. 0<= k <= 0 -> a[k]<=a[0]) and 
     0<=0 and 
     0<=i and 
     (i<n) and 
     (i>0))


goal exit:
forall a : int farray.

(not((i>0)) and 
(forall p, q: int. i<= p<=q <= n-1 -> a[p]<=a[q]) and 
(forall p, q: int. 0<= p<i+1=q <= n-1 -> a[p]<=a[q]) and 
(i>=0) and 
(i<n)  ->
     (forall p, q: int. 0<= p<=q <= n-1 -> a[p]<=a[q]))


goal start:
forall a : int farray.

((n>=1)  ->
     (forall p, q: int. n-1<= p<=q <= n-1 -> a[p]<=a[q]) and 
     (forall p, q: int. 0<= p<n=q <= n-1 -> a[p]<=a[q]) and 
     ((n-1)>=0) and 
     ((n-1)<n))