logic lo, hi, x, p, i, j, k, n: int

goal intra_loop:
forall a : int farray.

(((lo+1)<hi) and 
(forall i, j: int. 0<= i <= j <= n-1 -> a[i]<=a[j]) and 
(forall k: int. 0<= k <= lo -> (a[k]<x)) and 
(forall k: int. hi<= k <= n-1 -> (a[k]>x)) and 
((lo+1)>=0) and 
(lo+1)<=hi and 
hi<=n  ->
     (a[(lo+hi)/2]=x  ->
          x=a[(lo+hi)/2] or (forall k: int. 0<= k <= n-1 -> not(x=a[k]))
)
 and 
     (not((a[(lo+hi)/2]=x))  ->
          ((a[(lo+hi)/2]<x)  ->
               (forall i, j: int. 0<= i <= j <= n-1 -> a[i]<=a[j]) and 
               (forall k: int. 0<= k <= (lo+hi)/2 -> (a[k]<x)) and 
               (forall k: int. hi<= k <= n-1 -> (a[k]>x)) and 
               ((((lo+hi)/2)+1)>=0) and 
               (((lo+hi)/2)+1)<=hi and 
               hi<=n)
 and 
          ((a[(lo+hi)/2]>=x)  ->
               (forall i, j: int. 0<= i <= j <= n-1 -> a[i]<=a[j]) and 
               (forall k: int. 0<= k <= lo -> (a[k]<x)) and 
               (forall k: int. (lo+hi)/2<= k <= n-1 -> (a[k]>x)) and 
               ((lo+1)>=0) and 
               (lo+1)<=((lo+hi)/2) and 
               ((lo+hi)/2)<=n)
)
)


goal exit:
forall a : int farray.

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


goal start:
forall a : int farray.

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