Proof step 1 from proof monge-converges-inf (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  bounded≥(f, r), mon≥(f) ⊦ converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ bounded≥(f, r) ↔ bounded≤(λ n. ~ f(n), ~ r)

• Proof step 4:

  bounded≤(λ n. ~ f(n), ~ r), mon≥(f) ⊦ converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

Used terms: f, r

Proof step 3 from proof monge-converges-inf (previous step) (back to tree)

Lemma boundedge-neg-boundedle

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ mon≥(f) ↔ mon≤(λ n. ~ f(n))

• Proof step 6:

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

Rule argument

Additional information

Used terms: f

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

Lemma monge-neg-monle

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

Used terms: λ n. ~ f(n), ~ r

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

Lemma monle-converges-sup

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

Used simplifier rules: ⊦ ~ r = r0 ↔ r + r0 = 0.r; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ bounded≥(rset) → inf(rset) = ~ sup(λ r. rset(0.r + ~ r))

• Proof step 11:

  bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ bounded≥(λ r. ∃ n. r = f(n)), converges(f, inf(λ r. ∃ n. r = f(n)))

• Proof step 24:

  bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), bounded≥(λ r. ∃ n. r = f(n)), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ converges(f, ~ sup(λ r. ∃ n. 0.r + ~ r = f(n)))

Rule argument

Additional information

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

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

A spec-lemma

Proof step 11 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ bounded≥(rset) ↔ bounded≤(λ r. rset(0.r + ~ r))

• Proof step 13:

  bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ bounded≤(λ r. ∃ n. 0.r + ~ r = f(n)), converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

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

Proof step 12 from proof monge-converges-inf (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ bounded≤(λ r0. ∃ n. r0 + f(n) = 0.r), converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

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

Proof step 14 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  mon≤(λ n. ~ f(n)), ∀ n. ~ f(n) ≤ ~ r, converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ bounded≤(λ r0. ∃ n. r0 + f(n) = 0.r), converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

Used terms: λ n. ~ f(n), ~ r

Proof step 15 from proof monge-converges-inf (previous step) (back to tree)

Lemma boundedle-def

Proof step 16 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  mon≤(λ n. ~ f(n)), ∀ n. r ≤ f(n), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ bounded≤(λ r0. ∃ n. r0 + f(n) = 0.r), converges(f, inf(λ 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 + 0.r = r; (s) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s) ⊦ ~ r ≤ r0 ↔ 0.r ≤ r + r0; (s)

Proof step 17 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  mon≤(λ n. ~ f(n)), ∀ n. r ≤ f(n), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ ∃ r0. (λ r0. ∃ n. r0 + f(n) = 0.r) ≤ r0, converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

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

Proof step 18 from proof monge-converges-inf (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof monge-converges-inf (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 20:

  mon≤(λ n. ~ f(n)), ∀ n. r ≤ f(n), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ converges(f, inf(λ r. ∃ n. r = f(n))), (λ r0. ∃ n. r0 + f(n) = 0.r) ≤ ~ r

Rule argument

Additional information

Used terms: ~ r

Proof step 20 from proof monge-converges-inf (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:

  mon≤(λ n. ~ f(n)), ∀ n. r ≤ f(n), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ ∀ r1. (∃ n. r1 + f(n) = 0.r) → r1 ≤ ~ r, converges(f, inf(λ r. ∃ n. r = f(n)))

Rule argument

Additional information

Used terms: λ r0. ∃ n. r0 + f(n) = 0.r, ~ r

Proof step 21 from proof monge-converges-inf (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  r1 + f(n) = 0.r, 0.r < r1 + r, f(n) < r, mon≤(λ n. ~ f(n)), ∀ n. r ≤ f(n), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ converges(f, inf(λ 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 < r + r1 ↔ r0 < r1; (s) lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) ⊦ r ≤ ~ r0 ↔ r + r0 ≤ 0.r; (s)

Proof step 23 from proof monge-converges-inf (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 24 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), bounded≥(λ r. ∃ n. r = f(n)), converges(λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)) ⊦ converges(f, ~ sup(λ r0. ∃ n. r0 + f(n) = 0.r))

Rule argument

Additional information

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

Proof step 25 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

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

Rule argument

Additional information

Used terms: λ n. ~ f(n), sup(λ r0. ∃ n. f(n) + r0 = 0.r)

Proof step 26 from proof monge-converges-inf (previous step) (back to tree)

Lemma convergesto-def

Proof step 27 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

Proof step 28 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

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

Rule argument

Additional information

Used terms: f, ~ sup(λ r0. ∃ n. r0 + f(n) = 0.r)

Proof step 29 from proof monge-converges-inf (previous step) (back to tree)

Lemma convergesto-def

Proof step 30 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

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

Proof step 31 from proof monge-converges-inf (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

Used terms: ε

Proof step 32 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

Proof step 33 from proof monge-converges-inf (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Used terms: n

Proof step 34 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

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

Proof step 35 from proof monge-converges-inf (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 36:

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

Rule argument

Additional information

Used terms: n0

Proof step 36 from proof monge-converges-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

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

Rule argument

Additional information

Proof step 37 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ ~(r + r0) = ~ r + ~ r0

• Proof step 39:

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

Rule argument

Additional information

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

Proof step 38 from proof monge-converges-inf (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ abs(~ r) = abs(r)

• Proof step 41:

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

Rule argument

Additional information

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

Proof step 40 from proof monge-converges-inf (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof monge-converges-inf (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 42:

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

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic Used formulas: sup(λ r0. ∃ n. f(n) + r0 = 0.r) = sup(λ r0. ∃ n. r0 + f(n) = 0.r)

Proof step 42 from proof monge-converges-inf (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 43:

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

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic

Proof step 43 from proof monge-converges-inf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

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

Rule argument

Additional information

Used terms: abs(f(n0) + sup(λ r0. ∃ n. r0 + f(n) = 0.r)), ε, abs(f(n0) + sup(λ r0. ∃ n. r0 + f(n) = 0.r))

Proof step 44 from proof monge-converges-inf (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof monge-converges-inf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ r < r; (s)

Proof step 46 from proof monge-converges-inf (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information