From b94ee5134a4984c5effad37f86d9f6f3aeb193d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 29 May 2020 12:09:28 +0200
Subject: [PATCH] Improve examples after meeting

---
 examples/example-exact-cover.spec | 10 +++++-----
 examples/example-prime.spec       |  1 -
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/examples/example-exact-cover.spec b/examples/example-exact-cover.spec
index 9cb672e..1ba6168 100644
--- a/examples/example-exact-cover.spec
+++ b/examples/example-exact-cover.spec
@@ -4,7 +4,7 @@
 # Perform the proofs under the assumption that n is a nonnegative integer input constant. n stands
 # for the total number of input sets
 input: n -> integer.
-#assume: n >= 0.
+assume: n >= 0.
 
 # s/2 is the input predicate defining the sets for which the program searches for exact covers
 input: s/2.
@@ -15,11 +15,11 @@ output: in/1.
 
 # Perform the proofs under the assumption that the second parameter of s/2 (the number of the set)
 # is always an integer
-#assume: forall X, Y (s(X, Y) -> exists N (Y = N)).
+assume: forall Y (exists X s(X, Y) -> exists N (Y = N and N >= 1 and N <= n)).
 
 # Only valid sets can be included in the solution
-spec: forall X (in(X) -> X >= 1 and X <= n).
+spec: forall Y (in(Y) -> exists N (Y = N and N >= 1 and N <= n)).
 # If an element is contained in an input set, it must be covered by all solutions
-spec: forall X (exists I s(X, I) -> exists I (in(I) and s(X, I))).
+spec: forall X (exists Y s(X, Y) -> exists Y (in(Y) and s(X, Y))).
 # Elements may not be covered by two input sets
-spec: forall I, J (exists X (s(X, I) and s(X, J)) and in(I) and in(J) -> I = J).
+spec: forall Y, Z (exists X (s(X, Y) and s(X, Z)) and in(Y) and in(Z) -> Y = Z).
diff --git a/examples/example-prime.spec b/examples/example-prime.spec
index af690c0..bd63ee1 100644
--- a/examples/example-prime.spec
+++ b/examples/example-prime.spec
@@ -1,7 +1,6 @@
 input: n -> integer.
 output: prime/1.
 
-# TODO: not necessary if using the lemma below in both directions
 assume: n >= 1.
 
 spec: forall X (prime(X) -> exists N (X = N)).