logic isqrt : int -> int
logic isq : int, int -> int
axiom A1: forall k: int. forall n: int. k*k>n -> isq(k,n)=k-1
axiom A2: forall k: int. forall n: int. k*k=n -> isq(k,n)=k
axiom A3: forall k: int. forall n: int. k*k<n -> isq(k,n)=isq(k+1,n)
axiom I1: isqrt(1)=1
axiom I2: forall n: int. isqrt(n)=n>1 -> isqrt(n)=isq(2,n)

logic i, k, n: int
logic prime: bool

goal intra_loop:
(i<=isqrt(n) and 
2<=i and 
i<=(isqrt(n)+1) and 
(prime <-> (forall k: int. 2<= k <= i-1 -> not(n%k=0)))
  ->
     (n%i=0  ->
          (false <-> (forall k: int. 2<= k <= isqrt(n) -> not(n%k=0)))
)
 and 
     (not((n%i=0))  ->
          2<=(i+1) and 
          i<=isqrt(n) and 
          (prime <-> (forall k: int. 2<= k <= i -> not(n%k=0)))
)
)


goal exit:
((i>=(isqrt(n)+1)) and 
2<=i and 
i<=(isqrt(n)+1) and 
(prime <-> (forall k: int. 2<= k <= i-1 -> not(n%k=0)))
  ->
     (prime <-> (forall k: int. 2<= k <= isqrt(n) -> not(n%k=0)))
)


goal start:
((isqrt(n)>=2)  ->
     2<=2 and 
     2<=(isqrt(n)+1) and 
     (true <-> (forall k: int. 2<= k <= 2-1 -> not(n%k=0)))
)