Proof step 1 from proof maxinf-skolemf (conclusion) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 2:

  ⊦ (∞ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));(∃ n. np(∞.n)) ∧ (∀ m. np(m) → ¬ ∞ < ⌜m⌝ )), ∃ n∞. (n∞ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));(∃ n. np(n∞.n)) ∧ (∀ m. np(m) → ¬ n∞ < ⌜m⌝ ))

Rule argument

Additional information

Used terms: ∞

Proof step 2 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  np(n0) ⊦ ∃ n∞. (n∞ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));np(n∞.n) ∧ (∀ m. np(m) → ¬ n∞ < ⌜m⌝ )), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Proof step 3 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  np(n0), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)) ⊦ ∃ n0. n < n0 ∧ np(n0), ∃ n∞. (n∞ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));np(n∞.n) ∧ (∀ m. np(m) → ¬ n∞ < ⌜m⌝ ))

• Proof step 8:

  np(n0) ⊦ ∃ n0. n < n0 ∧ np(n0), ∃ n∞. (n∞ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));np(n∞.n) ∧ (∀ m. np(m) → ¬ n∞ < ⌜m⌝ )), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Used formulas: ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Proof step 4 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  np(n1), np(n0), ∀ n0. n1 < n0 → ¬ np(n0) ⊦ ∃ n∞. (n∞ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));np(n∞.n) ∧ (∀ m. np(m) → ¬ n∞ < ⌜m⌝ )), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Proof step 5 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  np(n0), np(n1), ∀ n0. n1 < n0 → ¬ np(n0) ⊦ (⌜n1⌝ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));np(⌜n1⌝ .n) ∧ (∀ m. np(m) → ¬ ⌜n1⌝ < ⌜m⌝ )), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Used terms: ⌜n1⌝

Proof step 6 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  n1 < n2, np(n2), np(n0), np(n1), ∀ n0. n1 < n0 → ¬ np(n0) ⊦ ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 7 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n2

Proof step 8 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 9:

  np(n0) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Proof step 9 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 10:

  np(n0), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: n - n0

Proof step 10 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  np(n0), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n0. n < n0 ∧ np(n0), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Proof step 11 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  np(n0), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0), np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Used terms: n

Proof step 12 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  np(n0), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n0. n < n0 ∧ np(n0), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), np(n) ∧ (n < n1 → ¬ np(n1))

Rule argument

Additional information

Proof step 13 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  np(n0), ¬ np(n), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

• Proof step 30:

  n < n1, np(n1), np(n0), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Proof step 14 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 15:

  np(n0), ¬ np(n), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n0. n < n0 ∧ np(n0), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), n < n0 ∧ np(n0)

Rule argument

Additional information

Used terms: n0

Proof step 15 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  np(n0), n0 ≤ n, ¬ np(n), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 16 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  n = n1 + n0, np(n0), n0 ≤ n, ¬ np(n), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n0. n < n0 ∧ np(n0), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, n0, n1

Proof step 17 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  np(n0), ¬ np(n1 + n0), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n2. n1 + n0 < n2 ∧ np(n2)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 18 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 19:

  np(n0), ¬ n1 + n0 - 1 - n0 < n1, ¬ np(n1 + n0), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n2. n1 + n0 < n2 ∧ np(n2), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

• Proof step 26:

  np(n0), ¬ np(n1 + n0), (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n. n1 + n0 - 1 < n ∧ np(n)), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n2. n1 + n0 < n2 ∧ np(n2), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Used terms: n1 + n0 - 1, n0, np

Proof step 19 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  n1 + n0 = n4 + 1, n1 + n0 ≠ 0, np(n0), ¬ n4 - n0 < n1, ¬ np(n1 + n0), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n2. n1 + n0 < n2 ∧ np(n2)

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) leprf: ⊦ m ≤ m - 1 → m = 0; (forward) from specification nat ⊦ 0 ≤ m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n1 + n0, m

Proof step 20 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  n1 + n0 = n4 + 1, np(n0), n1 ≤ n4 - n0, ¬ np(n4 + 1), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n2. n4 + 1 < n2 ∧ np(n2)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 21 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 22:

  n1 + n0 = n4 + 1, np(n0), n1 ≤ n4 - n0, ¬ np(n4 + 1), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n2. n4 + 1 < n2 ∧ np(n2), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), n4 + 1 < n0 ∧ np(n0)

Rule argument

Additional information

Used terms: n0

Proof step 22 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  n1 + n0 = n4 + 1, np(n0), n1 ≤ n4 - n0, n0 ≤ n4 + 1, ¬ np(n4 + 1), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n2. n4 + 1 < n2 ∧ np(n2)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 23 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 24:

  n1 + n0 = n4 + 1, np(n0), n0 ≤ n4 + 1, n1 ≤ n4 - n0, ¬ np(n4 + 1), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n2. n4 + 1 < n2 ∧ np(n2), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), np(n0) ∧ (∀ n1. n0 < n1 → ¬ np(n1))

Rule argument

Additional information

Used terms: n0

Proof step 24 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  n1 + n0 = n4 + 1, n0 < n, np(n), np(n0), n0 ≤ n4 + 1, n1 ≤ n4 - n0, ¬ np(n4 + 1), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n2. n4 + 1 < n2 ∧ np(n2), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 25 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat le-one: ⊦ m ≤ n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m ≤ m; (s) ⊦ m + m0 ≤ m ↔ m0 = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (s) n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s) ⊦ m = n + 1 → ¬ m ≤ n; (s) Used terms: n

Proof step 26 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  n1 + n0 - 1 < n, np(n), np(n0), ¬ np(n1 + n0), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n2. n1 + n0 < n2 ∧ np(n2), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 27 from proof maxinf-skolemf (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 28:

  n1 + n0 = n4 + 1, n1 + n0 ≠ 0, n4 < n, np(n0), np(n), ¬ np(n1 + n0), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n2. n1 + n0 < n2 ∧ np(n2)

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n1 + n0, m

Proof step 28 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  n1 + n0 = n4 + 1, n4 < n, np(n), np(n0), ¬ np(n4 + 1), ∀ n2, n3, np. n2 - n3 < n1 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n2. n4 + 1 < n2 ∧ np(n2), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m + 1 ≠ 0; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat

Proof step 29 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n

Proof step 30 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  n < n1, np(n1), np(n0), ∀ n2, n3, np. n2 - n3 < n - n0 → np(n3) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n2 < n0 ∧ np(n0)) ⊦ ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 31 from proof maxinf-skolemf (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n1