(* Verification Conditions for Alt-Ergo *)

logic i, n, isqrt: int

goal intra_loop:
(((i*i)<n) and 
(n>=((i-1)*(i-1))) and 
1<=i  ->
     (n>=(i*i)) and 
     0<=i)


goal exit:
(((i*i)>=n) and 
(n>=((i-1)*(i-1))) and 
1<=i  ->
     (((i*i)>n)  ->
          ((i-1)*(i-1))<=n and 
          n<=(i*i))
 and 
     (not(((i*i)>n))  ->
          (i*i)<=n and 
          n<=((i+1)*(i+1)))
)


goal start:
((n>1)  ->
     (n>=(0*0)) and 
     1<=1)