(* Verification Conditions for Alt-Ergo *)


logic i, j, n, temp: int

goal intra_loop:
forall a : int farray.

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


goal exit:
forall a : int farray.

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


goal intra_loop:
forall a : int farray.

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


goal exit:
forall a : int farray.

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


goal start:
forall a : int farray.

((n>=1)  ->
     (forall k: int. n-1<= k <= n-2 -> a[k]<=a[k+1]) and 
     ((n-1)>=0) and 
     (n-1)<=(n-1))