anthem-rs/examples/example-2.lemmas

19 lines
1.1 KiB
Plaintext

# Induction principle instantiated for p.
# This axiom is necessary because we use Vampire without higher-order reasoning
axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N (N >= 0 -> p(N)).
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).
lemma(forward): forall N (N >= 0 and p(N + 1) -> p(N)).
lemma(forward): not p(n + 1).
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(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 (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 < N2).
lemma(backward): forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).