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

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


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


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