From 830d7187fd8650b958726bb34d3a7f54e2e965fe Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Thu, 20 Apr 2017 17:34:44 +0200
Subject: [PATCH] corrected wrong last invariant in sieveSet

---
 sieveEratosthenes.txt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index a26805b..cc7b6aa 100644
--- 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]
 
 
 
+
-- 
2.1.4