Example 2 as proven with Vladimir
This commit is contained in:
parent
bd108886dd
commit
789cb4f8f8
@ -1,9 +1,9 @@
|
|||||||
# Multiplication with positive numbers preserves the order of integers
|
# Multiplication with positive numbers preserves the order of integers
|
||||||
axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
|
#axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
|
||||||
|
|
||||||
# Induction principle instantiated for p.
|
# Induction principle instantiated for p.
|
||||||
# This axiom is necessary because we use Vampire without higher-order reasoning
|
# This axiom is necessary because we use Vampire without higher-order reasoning
|
||||||
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: 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).
|
#axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N p(N).
|
||||||
|
|
||||||
lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= n)).
|
lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= n)).
|
||||||
@ -14,7 +14,54 @@ lemma(forward): not p(n + 1).
|
|||||||
lemma(forward): forall N1, N2 (q(N1) and N2 > N1 -> not q(N2)).
|
lemma(forward): forall N1, N2 (q(N1) and N2 > N1 -> not q(N2)).
|
||||||
lemma(forward): forall N (N >= 0 and not p(N + 1) -> (N + 1) * (N + 1) > n).
|
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).
|
# Added completed definition of p/1:
|
||||||
|
# forall X1 (p(X1) <-> exists N1 (0 <= N1 and N1 <= n and X1 = N1)
|
||||||
|
# and exists X2 (exists N2, N3 (X2 = N2 * N3 and N2 = X1 and N3 = X1) and X2 <= n))
|
||||||
|
|
||||||
|
lemma(backward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 * N1 <= N2 * N2 -> N1 <= N2).
|
||||||
|
|
||||||
|
lemma(backward): forall N (p(N) <-> 0 <= N and N <= n and N * N <= n).
|
||||||
|
lemma(backward): forall N (p(N) -> N * N <= n).
|
||||||
|
lemma(backward): forall N (not p(N) and N >= 0 -> N * N > n).
|
||||||
|
lemma(backward): forall N (N >= 0 -> N * N < (N + 1) * (N + 1)).
|
||||||
|
lemma(backward): forall N1, N2 (p(N1) and not p(N2) and N2 >= 0 -> N1 * N1 <= n and N2 * N2 > n).
|
||||||
|
lemma(backward): forall N1, N2 (p(N1) and not p(N2) and N2 >= 0 -> N1 * N1 < N2 * N2).
|
||||||
|
lemma(backward): forall N1, N2 (p(N1) and not p(N2) and N2 >= 0 -> N1 < N2).
|
||||||
|
|
||||||
|
lemma(backward): forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
lemma(backward): exists N (forall X (q(X) <- X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
|
||||||
|
lemma(backward): exists N (q(N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
#axiom: forall N, M (q(N) <- p(N) and not p(M) and M > N).
|
||||||
|
#axiom: forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
#lemma(backward): forall N1, N2 (q(N1) and q(N2) -> N1 = N2).
|
||||||
|
#lemma(backward): forall N (p(N) and N > 0 -> p(N - 1)).
|
||||||
|
|
||||||
|
#lemma(backward): forall N (q(N) <- p(N) and 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))).
|
||||||
|
lemma(backward): forall X1 (q(X1) <- p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))).
|
||||||
|
Loading…
Reference in New Issue
Block a user