logic x, p, n, k, found: int

goal intra_loop:
forall a : int farray.

((p<n) and 
(p>=0) and 
p<=n and 
((forall k: int. 0<= k <= p-1 -> not(x=a[k]))  ->
     found=0)
  ->
     (x=a[p]  ->
          ((exists k: int. 0<= k <= n-1 and x=a[k])  ->
     1=1)
 or ((forall k: int. 0<= k <= n-1 -> not(x=a[k]))  ->
     1=0)

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


goal exit:
forall a : int farray.

((p>=n) and 
(p>=0) and 
p<=n and 
((forall k: int. 0<= k <= p-1 -> not(x=a[k]))  ->
     found=0)
  ->
     ((exists k: int. 0<= k <= n-1 and x=a[k])  ->
     found=1)
 or ((forall k: int. 0<= k <= n-1 -> not(x=a[k]))  ->
     found=0)

)


goal start:
forall a : int farray.

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