From b29422cfbf9b54a31c181dd2df43e7c2d3f7d042 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 5 Jun 2020 18:54:17 +0200
Subject: [PATCH] Format exact cover example like in paper

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

diff --git a/examples/example-exact-cover.lp b/examples/example-exact-cover.lp
index cd4990d..b8e4acb 100644
--- a/examples/example-exact-cover.lp
+++ b/examples/example-exact-cover.lp
@@ -1,5 +1,5 @@
-{in(1..n)}.
+{in_cover(1..n)}.
 
-:- I != J, in(I), in(J), s(X, I), s(X, J).
-covered(X) :- in(I), s(X, I).
+:- I != J, in_cover(I), in_cover(J), s(X, I), s(X, J).
+covered(X) :- in_cover(I), s(X, I).
 :- s(X, I), not covered(X).
diff --git a/examples/example-exact-cover.spec b/examples/example-exact-cover.spec
index 63b3144..eefd859 100644
--- a/examples/example-exact-cover.spec
+++ b/examples/example-exact-cover.spec
@@ -8,15 +8,15 @@ input: s/2.
 
 # Only the in/1 predicate is an actual output, s/2 is an input and covered/1 and is_int/1 are
 # auxiliary
-output: in/1.
+output: in_cover/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 Y (exists X s(X, Y) -> exists N (Y = N and N >= 1 and N <= n)).
+assume: forall Y (exists X s(X, Y) -> exists I (Y = I and I >= 1 and I <= n)).
 
 # Only valid sets can be included in the solution
-spec: forall Y (in(Y) -> exists N (Y = N and N >= 1 and N <= n)).
+spec: forall Y (in_cover(Y) -> exists I (Y = I and I >= 1 and I <= n)).
 # If an element is contained in an input set, it must be covered by all solutions
-spec: forall X (exists Y s(X, Y) -> exists Y (in(Y) and s(X, Y))).
+spec: forall X (exists Y s(X, Y) -> exists Y (s(X, Y) and in_cover(Y))).
 # Elements may not be covered by two input sets
-spec: forall Y, Z (exists X (s(X, Y) and s(X, Z)) and in(Y) and in(Z) -> Y = Z).
+spec: forall Y, Z (exists X (s(X, Y) and s(X, Z)) and in_cover(Y) and in_cover(Z) -> Y = Z).