modified loop invariant for primes

diff --git a/numbertheory.txt b/numbertheory.txt
index f83a239..e7e2a4e 100644 (file)
--- a/numbertheory.txt
+++ b/numbertheory.txt
@@ -46,7 +46,7 @@ proc isprime(p:nat): Bool
    if p ≥ 2 then
    {
       while i < integerroot(p)+1 ∧ res = true do
-         invariant 2 ≤ i ∧ i ≤ p;
+         invariant 2 ≤ i ∧ i ≤ integerroot(p)+1;
          decreases p-i;
       {
          res = ¬ divides(i,p);