From 7895bf83c46c436b6ce37dd22d2640d6c31392ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 28 May 2020 18:40:33 +0200 Subject: [PATCH] Clean-up in example 2 --- examples/example-2.spec | 9 --------- 1 file changed, 9 deletions(-) diff --git a/examples/example-2.spec b/examples/example-2.spec index 1659662..57bebae 100644 --- a/examples/example-2.spec +++ b/examples/example-2.spec @@ -19,12 +19,6 @@ axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3). axiom: forall N1 (p(N1) and forall N2 (N2 >= N1 and not p(N2) -> not p(N2 + 1)) -> forall N2 (N2 >= N1 -> p(N2))). #axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N p(N). -#lemma(forward): forall N N * N >= N. -#lemma(forward): forall X (q(X) -> exists N X = N). -#lemma(forward): forall X (q(X) <-> exists N (X = N and N >= 0 and N * N <= n and not p(N + 1))). -#lemma(forward): exists N (q(N) <-> N >= 0 and N * N <= n and (N + 1) * (N + 1) > n). -#lemma(forward): exists N p(N). -#lemma(forward): forall N1, N2 (N2 > N1 and N1 >= 0 and p(N2) -> p(N1)). lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= 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): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2). @@ -35,8 +29,5 @@ lemma(forward): forall N (N >= 0 and not p(N + 1) -> (N + 1) * (N + 1) > n). lemma(backward): forall N1, N2 (q(N1) and q(N2) -> N1 = N2). axiom: forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2). -#lemma(backward): exists N (p(N) and not p(N + 1)). -#axiom: forall N (not p(N) -> not p(N + 1)). lemma(backward): forall X1 (q(X1) -> p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))). -#lemma(backward): forall X1 (q(X1) <- p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))).