logic hi, lo, n, isqrt: int

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


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


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