From 5782461babe0e210f3308e47d2cf9a8b86f8dfc3 Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Tue, 21 Mar 2017 20:17:38 +0100
Subject: [PATCH] modified loop invariant for primes

---
 numbertheory.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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);
-- 
2.1.4