corrected wrong last invariant in sieveSet

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index a26805b..cc7b6aa 100644 (file)
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -83,7 +83,7 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
       invariant start ⊆ 2..m ∧ ret ⊆ 2..m;
       invariant ∀e ∈ ret. isPrime(e);
       invariant start ≠ ∅[nat] ⇒ ∀e ∈ ret. e < SetMin(start);
-      invariant ∀e:nat. e ≤ m ∧ e ∈ start ⇒ ¬ (e ∈ ret);
+      invariant ∀e:nat. e ≤ m ∧ ¬(e ∈ start) ∧ isPrime(e) ⇒ e ∈ ret;
    {
       var locmi:nat = SetMin(start);
       ret = ret ∪ {locmi};
@@ -95,3 +95,4 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
 
 
 
+