Proof step 1 from proof monle-converges-sup (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  bounded≤(f, r), mon≤(f) ⊦ converges(f, sup(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

Proof step 2 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ converges(f, r) ↔ (∀ ε. ε > 0.r → (∃ n. ∀ n0. n0 ≥ n → abs(f(n0) - r) < ε))

• Proof step 4:

  bounded≤(f, r), mon≤(f) ⊦ ∀ ε. ε > 0.r → (∃ n. ∀ n0. n0 ≥ n → abs(f(n0) - sup(λ r. ∃ n. r = f(n))) < ε)

Rule argument

Additional information

Used terms: f, sup(λ r. ∃ n. r = f(n))

Proof step 3 from proof monle-converges-sup (previous step) (back to tree)

Lemma convergesto-def

Proof step 4 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  0.r < ε, bounded≤(f, r), mon≤(f) ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used simplifier rules: ⊦ r - r0 = r + ~ r0; (s) ⊦ n ≥ m ↔ m ≤ n; (s) ⊦ r > r0 ↔ r0 < r; (s)

Proof step 5 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ bounded≤(rset) ∧ rset ≤ r → sup(rset) ≤ r

• Proof step 7:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)) ∧ (λ r. ∃ n. r = f(n)) ≤ r → sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n), r

Proof step 6 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof monle-converges-sup (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)) ∧ (λ r. ∃ n. r = f(n)) ≤ r → sup(λ r. ∃ n. r = f(n)) ≤ r, bounded≤(λ r. ∃ n. r = f(n)) ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

• Proof step 63:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)) ∧ (λ r. ∃ n. r = f(n)) ≤ r → sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, bounded≤(λ r. ∃ n. r = f(n))

Rule argument

Additional information

Used formulas: bounded≤(λ r. ∃ n. r = f(n))

Proof step 8 from proof monle-converges-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)) ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, bounded≤(λ r. ∃ n. r = f(n)) ∧ (λ r. ∃ n. r = f(n)) ≤ r

• Proof step 16:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Proof step 9 from proof monle-converges-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)) ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, (λ r. ∃ n. r = f(n)) ≤ r

Rule argument

Additional information

Proof step 10 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ bounded≤(f, r) ↔ (∀ n. f(n) ≤ r)

• Proof step 12:

  0.r < ε, mon≤(f), ∀ n. f(n) ≤ r, bounded≤(λ r. ∃ n. r = f(n)) ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, (λ r. ∃ n. r = f(n)) ≤ r

Rule argument

Additional information

Used terms: f, r

Proof step 11 from proof monle-converges-sup (previous step) (back to tree)

Lemma boundedle-def

Proof step 12 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0)

• Proof step 14:

  0.r < ε, mon≤(f), ∀ n. f(n) ≤ r, bounded≤(λ r. ∃ n. r = f(n)) ⊦ ∀ r1. (∃ n. r1 = f(n)) → r1 ≤ r, ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n), r

Proof step 13 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  0.r < ε, r < f(n), mon≤(f), ∀ n. f(n) ≤ r, bounded≤(λ r. ∃ n. r = f(n)) ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 15 from proof monle-converges-sup (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: n

Proof step 16 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 17:

  ⊦ bounded≤(rset) ∧ rset ≤ r → sup(rset) ≤ r

• Proof step 18:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)) ∧ (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)) - ε * 2.r ^-1 → sup(λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)) - ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n), sup(λ r. ∃ n. r = f(n)) - ε * 2.r ^-1

Proof step 17 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, bounded≤(λ r. ∃ n. r = f(n)) ∧ (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)) + ~(ε * 2.r ^-1)

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic commutativity: ⊦ r * r0 = r0 * r; from specification real-multdiv mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; from specification real-multdiv ⊦ i.r ≤ j.r ↔ i ≤ j; (s) ⊦ 0.r * r = 0.r; (s) 0.r < r ⊦ r ^-1 ≤ r0 ↔ 1.r ≤ r * r0; (s) ⊦ i.r < j.r ↔ i < j; (s) ⊦ 0.r < r → (r * r0 ≤ 0.r ↔ r0 ≤ 0.r); (s) ⊦ r + r0 ≤ r ↔ r0 ≤ 0.r; (s) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s) ⊦ r - r0 = r + ~ r0; (s)

Proof step 19 from proof monle-converges-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)) + ~(ε * 2.r ^-1)

Rule argument

Additional information

Proof step 20 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0)

• Proof step 22:

  0.r < ε, bounded≤(f, r), mon≤(f), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∀ r. (∃ n. r = f(n)) → r ≤ sup(λ r. ∃ n. r = f(n)) + ~(ε * 2.r ^-1), ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n), sup(λ r. ∃ n. r = f(n)) + ~(ε * 2.r ^-1)

Proof step 21 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  0.r < ε, bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s)

Proof step 23 from proof monle-converges-sup (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 24:

  0.r < ε, bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used terms: n

Proof step 24 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss)

Proof step 25 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 26:

  ⊦ bounded≤(rset) → rset ≤ sup(rset)

• Proof step 27:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, bounded≤(λ r. ∃ n. r = f(n)) → (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n)

Proof step 26 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof monle-converges-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 28:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)) ⊦

Rule argument

Additional information

Proof step 28 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ r < 0.r → abs(r) = ~ r

• Proof step 30:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ f(n0) + ~ sup(λ r. ∃ n. r = f(n)) < 0.r

• Proof step 47:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) + ~ sup(λ r. ∃ n. r = f(n)) < 0.r, bounded≤(λ r. ∃ n. r = f(n)), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε ≤ ~(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Used terms: f(n0) + ~ sup(λ r. ∃ n. r = f(n))

Proof step 29 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ f(n0) ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r + ~ r0 < 0.r ↔ r < r0; (s)

Proof step 31 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0)

• Proof step 33:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, ∀ r. (∃ n. r = f(n)) → r ≤ sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ f(n0), ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n), sup(λ r. ∃ n. r = f(n))

Proof step 32 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof monle-converges-sup (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 34:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, (∃ n. f(n0) = f(n)) → f(n0) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ f(n0) ⊦

Rule argument

Additional information

Used terms: f(n0)

Proof step 34 from proof monle-converges-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 35:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ f(n0), ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ ∃ n. f(n0) = f(n)

• Proof step 36:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ f(n0), ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ r, f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ⊦

Rule argument

Additional information

Proof step 35 from proof monle-converges-sup (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n0

Proof step 36 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0)

• Proof step 38:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) = f(n0), sup(λ r. ∃ n. r = f(n)) ≤ r, ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ f(n0) ⊦

Rule argument

Additional information

Used terms: f(n0), sup(λ r. ∃ n. r = f(n))

Proof step 37 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ ¬ r < 0.r → abs(r) = r

• Proof step 40:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, f(n0) + ~ sup(λ r. ∃ n. r = f(n)) < 0.r, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) = f(n0), sup(λ r. ∃ n. r = f(n)) ≤ f(n0), ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

• Proof step 43:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) = f(n0), sup(λ r. ∃ n. r = f(n)) ≤ f(n0), ε ≤ f(n0) + ~ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦ f(n0) + ~ sup(λ r. ∃ n. r = f(n)) < 0.r

Rule argument

Additional information

Used terms: f(n0) + ~ sup(λ r. ∃ n. r = f(n))

Proof step 39 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) = f(n0), sup(λ r. ∃ n. r = f(n)) ≤ r, ε ≤ abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))), sup(λ r. ∃ n. r = f(n)) ≤ f(n0) ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r + ~ r0 < 0.r ↔ r < r0; (s)

Proof step 41 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ r < r0 ↔ ¬ r0 ≤ r

Rule argument

Additional information

Used terms: f(n0), sup(λ r. ∃ n. r = f(n))

Proof step 42 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) = f(n0), sup(λ r. ∃ n. r = f(n)) ≤ r, ε + sup(λ r. ∃ n. r = f(n)) ≤ f(n0), sup(λ r. ∃ n. r = f(n)) ≤ f(n0) ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r + ~ r0 < 0.r ↔ r < r0; (s) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s)

Proof step 44 from proof monle-converges-sup (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 45:

  f(n0) < f(n) + ε * 2.r ^-1, 0.r < ε, bounded≤(f, r), mon≤(f), f(n0) ≤ f(n0), ε + f(n0) ≤ f(n0), f(n0) ≤ r, n ≤ n0, bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) = f(n0) ⊦

Rule argument

Additional information

Proof step 45 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ r + r0 = r0 + r

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r; (s) ⊦ r + r0 ≤ r ↔ r0 ≤ 0.r; (s) ⊦ r < r0 → (r0 ≤ r ↔ false); (as) add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic Used terms: ε, f(n0)

Proof step 46 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  0.r < ε, bounded≤(f, r), mon≤(f), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r + ~ r0 < 0.r ↔ r < r0; (s) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s) ⊦ ~ ~ r = r; (s) ⊦ ~(r + r0) = ~ r + ~ r0; (s)

Proof step 48 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ mon≤(f) ↔ (∀ n, n0. n ≤ n0 → f(n) ≤ f(n0))

• Proof step 50:

  0.r < ε, bounded≤(f, r), n ≤ n0, f(n0) < sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, ∀ n, n0. n ≤ n0 → f(n) ≤ f(n0), bounded≤(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Used terms: f

Proof step 49 from proof monle-converges-sup (previous step) (back to tree)

Lemma monle-def

Proof step 50 from proof monle-converges-sup (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 51:

  0.r < ε, bounded≤(f, r), n ≤ n0, n ≤ n0 → f(n) ≤ f(n0), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ⊦

Rule argument

Additional information

Used terms: n, n0

Proof step 51 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  0.r < ε, bounded≤(f, r), n ≤ n0, f(n) ≤ f(n0), f(n0) < sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Proof step 52 from proof monle-converges-sup (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 53:

  0.r < ε, ε + f(n0) < f(n) + ε * 2.r ^-1, bounded≤(f, r), f(n) ≤ f(n0), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ⊦

• Proof step 59:

  0.r < ε, bounded≤(f, r), f(n) ≤ f(n0), n ≤ n0, ¬ ε + f(n0) < f(n) + ε * 2.r ^-1, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ⊦

Rule argument

Additional information

Used formulas: ε + f(n0) < f(n) + ε * 2.r ^-1

Proof step 53 from proof monle-converges-sup (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 54:

  ε + f(n0) < f(n) + ε * 2.r ^-1, 0.r < ε, bounded≤(f, r), n ≤ n0, f(n) ≤ f(n0), ¬ ε + f(n) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r + r0 < r + r1 ↔ r0 < r1; (s) 0.r < r ⊦ r0 < r ^-1 * r1 ↔ r * r0 < r1; (s) ⊦ 0.r < r → (r * r0 < r ↔ r0 < 1.r); (s) ⊦ i.r < j.r ↔ i < j; (s) mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; from specification real-multdiv commutativity: ⊦ r * r0 = r0 * r; from specification real-multdiv add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic Used formulas: ε + f(n) < f(n) + ε * 2.r ^-1

Proof step 54 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

  ⊦ r < r0 ↔ ¬ r0 ≤ r

• Proof step 56:

  0.r < ε, ε + f(n0) < f(n) + ε * 2.r ^-1, bounded≤(f, r), f(n) + ε * 2.r ^-1 ≤ ε + f(n), f(n) ≤ f(n0), n ≤ n0, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ⊦

Rule argument

Additional information

Used terms: ε + f(n), f(n) + ε * 2.r ^-1

Proof step 55 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof monle-converges-sup (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 57:

  ε + f(n0) < f(n) + ε * 2.r ^-1, 0.r < ε, bounded≤(f, r), n ≤ n0, f(n) ≤ f(n0), f(n) + ε * 2.r ^-1 ≤ ε + f(n), ε + f(n) ≤ ε + f(n0), f(n0) < sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0.r < r → (r * r0 ≤ r ↔ r0 ≤ 1.r); (s) ⊦ i.r < j.r ↔ i < j; (s) 0.r < r ⊦ r ^-1 ≤ r0 ↔ 1.r ≤ r * r0; (s) ⊦ 1.r * r = r; (s) ⊦ i.r ≤ j.r ↔ i ≤ j; (s) mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; from specification real-multdiv commutativity: ⊦ r * r0 = r0 * r; from specification real-multdiv ⊦ r + r0 ≤ r + r2 ↔ r0 ≤ r2; (s) ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) ⊦ r ≤ r0 → ¬ r0 < r; (s) add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic Used formulas: ε + f(n) ≤ ε + f(n0)

Proof step 57 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 58:

  ⊦ r ≤ r0 ∧ r0 < r1 → r < r1

Rule argument

Additional information

Used simplifier rules: ⊦ 0.r < r → (r * r0 ≤ r ↔ r0 ≤ 1.r); (s) 0.r < r ⊦ r ^-1 ≤ r0 ↔ 1.r ≤ r * r0; (s) ⊦ 1.r * r = r; (s) ⊦ i.r ≤ j.r ↔ i ≤ j; (s) ⊦ r + r0 ≤ r + r2 ↔ r0 ≤ r2; (s) ⊦ r + r0 < r + r1 ↔ r0 < r1; (s) 0.r < r ⊦ r0 < r ^-1 * r1 ↔ r * r0 < r1; (s) ⊦ 0.r < r → (r * r0 < r ↔ r0 < 1.r); (s) ⊦ i.r < j.r ↔ i < j; (s) mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; from specification real-multdiv commutativity: ⊦ r * r0 = r0 * r; from specification real-multdiv add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic Used terms: ε + f(n), ε + f(n0), f(n) + ε * 2.r ^-1

Proof step 58 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 59 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 60:

  ⊦ r ≤ r0 ∧ r0 < r1 → r < r1

• Proof step 61:

  0.r < ε, bounded≤(f, r), n ≤ n0, f(n) ≤ f(n0), ¬ ε + f(n0) < f(n) + ε * 2.r ^-1, ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ∧ sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1 → ε + f(n0) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, bounded≤(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r ⊦

Rule argument

Additional information

Used terms: ε + f(n0), sup(λ r. ∃ n. r = f(n)), f(n) + ε * 2.r ^-1

Proof step 60 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof monle-converges-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 62:

  0.r < ε, bounded≤(f, r), f(n) ≤ f(n0), n ≤ n0, ¬ ε + f(n0) < f(n) + ε * 2.r ^-1, sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1, f(n0) < sup(λ r. ∃ n. r = f(n)), bounded≤(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) ≤ r, (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)), ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ⊦ ε + f(n0) ≤ sup(λ r. ∃ n. r = f(n)) ∧ sup(λ r. ∃ n. r = f(n)) < f(n) + ε * 2.r ^-1

Rule argument

Additional information

Proof step 62 from proof monle-converges-sup (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Proof step 63 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  0.r < ε, bounded≤(f, r), mon≤(f) ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, bounded≤(λ r. ∃ n. r = f(n))

Rule argument

Additional information

Proof step 64 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

  ⊦ bounded≤(rset) ↔ (∃ r0. rset ≤ r0)

• Proof step 66:

  0.r < ε, bounded≤(f, r), mon≤(f) ⊦ ∃ r0. (λ r. ∃ n. r = f(n)) ≤ r0, ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n)

Proof step 65 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 66 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ bounded≤(f, r) ↔ (∀ n. f(n) ≤ r)

• Proof step 68:

  0.r < ε, mon≤(f), ∀ n. f(n) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, ∃ r0. (λ r. ∃ n. r = f(n)) ≤ r0

Rule argument

Additional information

Used terms: f, r

Proof step 67 from proof monle-converges-sup (previous step) (back to tree)

Lemma boundedle-def

Proof step 68 from proof monle-converges-sup (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 69:

  0.r < ε, mon≤(f), ∀ n. f(n) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε, (λ r. ∃ n. r = f(n)) ≤ r

Rule argument

Additional information

Used terms: r

Proof step 69 from proof monle-converges-sup (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 70:

  ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0)

• Proof step 71:

  0.r < ε, mon≤(f), ∀ n. f(n) ≤ r ⊦ ∀ r1. (∃ n. r1 = f(n)) → r1 ≤ r, ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used terms: λ r. ∃ n. r = f(n), r

Proof step 70 from proof monle-converges-sup (previous step) (back to tree)

A spec-lemma

Proof step 71 from proof monle-converges-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  0.r < ε, r < f(n), mon≤(f), ∀ n. f(n) ≤ r ⊦ ∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ sup(λ r. ∃ n. r = f(n))) < ε

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 72 from proof monle-converges-sup (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: n