From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Tue, 21 Mar 2017 19:17:38 +0000 (+0100)
Subject: modified loop invariant for primes
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=5782461babe0e210f3308e47d2cf9a8b86f8dfc3;p=cfuerst%2Fformal-numbers.git

modified loop invariant for primes
---

diff --git a/numbertheory.txt b/numbertheory.txt
index f83a239..e7e2a4e 100644
--- 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);