From eab3520e449db38ea757f489f408223417ac8bc6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Mon, 11 May 2020 04:14:17 +0200
Subject: [PATCH] Minor formatting

---
 examples/example-2.spec | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/examples/example-2.spec b/examples/example-2.spec
index 277038b..f273fba 100644
--- a/examples/example-2.spec
+++ b/examples/example-2.spec
@@ -9,20 +9,17 @@ assert: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1
 
 
 
+
 lemma(forward): forall N N * N >= N.
 lemma(forward): forall X (q(X) -> exists N X = N).
 lemma(forward): forall X (p(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n)).
 lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and not p(N2 + 1))).
 lemma(forward): forall N2 (N2 >= 0 and not p(N2 + 1) -> (N2 + 1) * (N2 + 1) > n).
 lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)).
-
-
 lemma(forward): exists N2 (forall X (X = N2 -> (q(X) <-> N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n))).
 lemma(forward): exists N2 p(N2).
 lemma(forward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2).
 lemma(forward): forall N (N >= 0 and p(N + 1) -> p(N)).
-
 lemma(forward): not p(n + 1).
 lemma(forward): forall N1, N2 (N2 > N1 and N1 >= 0 and p(N2) -> p(N1)).
-
 lemma(forward): forall N2, N3 (q(N2) and N3 > N2 -> not q(N3)).