logic i, k, max, n: int

goal intra_loop:
forall a : int farray.

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


goal exit:
forall a : int farray.

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


goal start:
forall a : int farray.

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