Proof step 1 from proof maxinf-inf (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. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n))

Rule argument

Additional information

Used terms: np

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

Lemma maxinf-def

Proof step 3 from proof maxinf-inf (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. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n))

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

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

• Proof step 12:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used terms: n1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  max∞(np) = ⌜n1⌝ , n1 < n0, np(n1), np(n0), ∀ m. np(m) → ¬ n1 < 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 11 from proof maxinf-inf (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 12 from proof maxinf-inf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n1