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

User applied rule apply lemma

And obtained the following new goals

• Proof step 2:

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

• Proof step 3:

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

Rule argument

Additional information

Used terms: np

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

Lemma maxinf-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

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

• Proof step 11:

  max∞(np) ≠ ∞, np(max∞(np).n), ∀ m. np(m) → ¬ max∞(np) < ⌜m⌝ ⊦ max∞(np) = ⌜n⌝ ↔ np(n) ∧ (∀ m. np(m) → ¬ n < m)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  max∞(np) = ∞, np(n), ∀ m. np(m) → ¬ n < m, (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜n⌝ ≠ ∞; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  max∞(np) = ∞, np(n), ∀ m. np(m) → ¬ n < m, ∀ n. ∃ n0. n < n0 ∧ np(n0) ⊦

• Proof step 10:

  max∞(np) = ∞, np(n), ∀ m. np(m) → ¬ n < m, ∀ n. ¬ np(n) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 8:

  max∞(np) = ∞, np(n), ∀ n. ∃ n0. n < n0 ∧ np(n0), ∀ m. np(m) → ¬ n < m, ∃ n0. n < n0 ∧ np(n0) ⊦

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  max∞(np) = ∞, n < n0, np(n), np(n0), ∀ n. ∃ n0. n < n0 ∧ np(n0), ∀ m. np(m) → ¬ n < m ⊦

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n0

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  max∞(np) ≠ ∞, np(max∞(np).n), ∀ m. np(m) → ¬ max∞(np) < ⌜m⌝ ⊦ max∞(np) = ⌜n⌝ ↔ np(n) ∧ (∀ m. np(m) → ¬ n < m)

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  max∞(np) = ⌜n0⌝ , max∞(np) ≠ ∞, np(n0), ∀ m. np(m) → ¬ max∞(np) < ⌜m⌝ ⊦ max∞(np) = ⌜n⌝ ↔ np(n) ∧ (∀ m. np(m) → ¬ n < m)

Rule argument

Additional information

Used simplifier rules: ⊦ n∞ ≠ ∞ → (n = n∞.n ↔ n∞ = ⌜n⌝ ); (elim) Used terms: max∞(np), n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  max∞(np) = ⌜n0⌝ , np(n0), ∀ m. np(m) → ¬ n0 < m ⊦ n0 = n ↔ np(n) ∧ (∀ m. np(m) → ¬ n < m)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  max∞(np) = ⌜n0⌝ , n0 ≠ n, np(n0), np(n), ∀ m. np(m) → ¬ n0 < m, ∀ m. np(m) → ¬ n < m ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  max∞(np) = ⌜n0⌝ , n0 ≠ n, np(n), np(n0), ∀ m. np(m) → ¬ n < m, ∀ m. np(m) → ¬ n0 < m ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 17:

  max∞(np) = ⌜n0⌝ , n0 ≠ n, np(n0), np(n), np(n0) → ¬ n < n0, ∀ m. np(m) → ¬ n0 < m ⊦

Rule argument

Additional information

Used terms: n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  max∞(np) = ⌜n0⌝ , n0 ≠ n, n0 < n, np(n0), np(n), ∀ m. np(m) → ¬ n0 < m ⊦

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 ↔ ¬ n < m); (ss)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n