Proof step 1 from proof convergesto-neg-convergesto (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(converges(f, r) ↔ converges(λ n. ~ f(n), ~ r)) ⊦

Rule argument

Additional information

Proof step 2 from proof convergesto-neg-convergesto (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:

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

Rule argument

Additional information

Used terms: f, r

Proof step 3 from proof convergesto-neg-convergesto (previous step) (back to tree)

Lemma convergesto-def

Proof step 4 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⊦ (∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε)) ↔ converges(λ n. ~ f(n), ~ 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 5 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  ⊦ (∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε)) ↔ (∀ ε. ε > 0.r → (∃ n. ∀ n0. n0 ≥ n → abs(~ f(n0) - ~ r) < ε))

Rule argument

Additional information

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

Proof step 6 from proof convergesto-neg-convergesto (previous step) (back to tree)

Lemma convergesto-def

Proof step 7 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ⊦ (∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε)) ↔ (∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(~ f(n0) + 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 8 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  ∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε) ⊦ ∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(~ f(n0) + r) < ε)

• Proof step 27:

  ∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(~ f(n0) + r) < ε) ⊦ ∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε)

Rule argument

Additional information

Proof step 9 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Proof step 10 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used terms: ε

Proof step 11 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Proof step 12 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 13:

  0.r < ε, ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε ⊦ ∀ n0. n ≤ n0 → abs(~ f(n0) + r) < ε

Rule argument

Additional information

Used terms: n

Proof step 13 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  r ≠ f(n0), 0.r < ε, ε ≤ abs(~ f(n0) + r), n ≤ n0, ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε ⊦

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) ⊦ 0.r < abs(r) ↔ r ≠ 0.r; (s) forward-le: ⊦ r ≤ r0 ∧ 0.r < r → 0.r < r0; (forward) from specification real-abs ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss)

Proof step 14 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 15:

  r ≠ f(n0), 0.r < ε, n ≤ n0, ε ≤ abs(~ f(n0) + r), n ≤ n0 → abs(f(n0) + ~ r) < ε ⊦

Rule argument

Additional information

Used terms: n0

Proof step 15 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  r ≠ f(n0), 0.r < ε, abs(f(n0) + ~ r) < ε, abs(f(n0) + ~ r) < abs(~ f(n0) + r), ε ≤ abs(~ f(n0) + r), n ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-lsle: ⊦ r < r0 ∧ r0 ≤ r1 → r < r1; (forward) from specification real-abs

Proof step 16 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  r ≠ f(n0), f(n0) + ~ r < 0.r, abs(f(n0) + ~ r) < abs(~ f(n0) + r), abs(f(n0) + ~ r) < ε, 0.r < ε, n ≤ n0, ε ≤ abs(~ f(n0) + r) ⊦

• Proof step 21:

  r ≠ f(n0), f(n0) + ~ r < abs(~ f(n0) + r), f(n0) + ~ r < ε, 0.r < ε, n ≤ n0, ε ≤ abs(~ f(n0) + r), ¬ f(n0) + ~ r < 0.r ⊦

Rule argument

Additional information

Used terms: f(n0) + ~ r

Proof step 17 from proof convergesto-neg-convergesto (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  r ≠ f(n0), f(n0) < r, 0.r < ε, abs(f(n0) + ~ r) < ε, abs(f(n0) + ~ r) + f(n0) < r, ε + f(n0) ≤ r, n ≤ 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 + ~ r1 ↔ r + r1 < r0; (s) ⊦ r - r0 = r + ~ r0; (s) ⊦ r0 < r → abs(r + ~ r0) = r - r0; (s) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s) ⊦ r + ~ r0 < 0.r ↔ r < r0; (s)

Proof step 19 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r + ~ r0 < 0.r ↔ r < r0; (s) ⊦ ~(r + r0) = ~ r + ~ r0; (s) ⊦ ~ ~ r = r; (s) ⊦ r + ~ r0 < r1 ↔ r < r0 + r1; (s) ⊦ 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 ⊦ ¬ r < 0.r → abs(r) = r; (s) ⊦ r + r = 2.r * r; (s) ⊦ i > 0 → (i.r * r0 < i.r * r2 ↔ r0 < r2); (s) mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; from specification real-multdiv commutativity: ⊦ r * r0 = r0 * r; from specification real-multdiv ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: f(n0) + ~ r

Proof step 20 from proof convergesto-neg-convergesto (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  r ≠ f(n0), r < f(n0), f(n0) < r + abs(~ f(n0) + r), f(n0) < r + ε, 0.r < ε, n ≤ n0, ε ≤ abs(~ f(n0) + r) ⊦

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 ⊦ 0.r < r → r0 < r0 + r; (s) ⊦ r + 0.r = r; (s) ⊦ r + ~ r0 = r1 ↔ r = r1 + r0; (s) ⊦ 0.r < abs(r) ↔ r ≠ 0.r; (s) ⊦ r < r + r0 ↔ 0.r < r0; (s) trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s) ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r + ~ r0 < 0.r ↔ r < r0; (s) ⊦ r + ~ r0 < r1 ↔ r < r0 + r1; (s)

Proof step 22 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  r ≠ f(n0), ~ f(n0) + r < 0.r, 0.r < ε, f(n0) < r + ε, f(n0) < r + abs(~ f(n0) + r), r < f(n0), ε ≤ abs(~ f(n0) + r), n ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s) ⊦ r < r0 + ~ r1 ↔ r + r1 < r0; (s) ⊦ r + r = 2.r * r; (s) ⊦ i > 0 → (i.r * r0 < i.r * r2 ↔ r0 < r2); (s) ⊦ r < r0 → ¬ r0 < r; (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(n0) + r

Proof step 23 from proof convergesto-neg-convergesto (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  r ≠ f(n0), f(n0) < r + abs(~ f(n0) + r), f(n0) < r + ε, 0.r < ε, r < f(n0), n ≤ n0, ε ≤ abs(~ f(n0) + r) ⊦

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 25 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ~(r + r0) = ~ r + ~ r0; (s) ⊦ ~ ~ r = r; (s) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (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 ⊦ ¬ r < 0.r → abs(r) = r; (s) ⊦ r < r0 + ~ r1 ↔ r + r1 < r0; (s) ⊦ r + r = 2.r * r; (s) ⊦ i > 0 → (i.r * r0 < i.r * r2 ↔ r0 < r2); (s) ⊦ r < r0 → ¬ r0 < r; (s) mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; from specification real-multdiv commutativity: ⊦ r * r0 = r0 * r; from specification real-multdiv Used terms: ~ f(n0) + r

Proof step 26 from proof convergesto-neg-convergesto (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

Proof step 28 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule apply proof lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

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

• Proof step 32:

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

Rule argument

Additional information

Proof step 29 from proof convergesto-neg-convergesto (previous step) (back to tree)

Proof step 10 used as proof-lemma

Proof step 30 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ~ ~ r = r; (s)

Proof step 31 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ε0

Proof step 32 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ~ ~ r = r; (s)

Proof step 33 from proof convergesto-neg-convergesto (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Used terms: n

Proof step 34 from proof convergesto-neg-convergesto (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  f(n0) ≠ r, 0.r < ε, ε ≤ abs(f(n0) + ~ r), n ≤ n0, ∀ n0. n ≤ n0 → abs(f(n0) + ~ r) < ε, ∀ ε. 0.r < ε → (∃ n. ∀ n0. n ≤ n0 → abs(~ f(n0) + r) < ε) ⊦

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) ⊦ 0.r < abs(r) ↔ r ≠ 0.r; (s) forward-le: ⊦ r ≤ r0 ∧ 0.r < r → 0.r < r0; (forward) from specification real-abs ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss)

Proof step 35 from proof convergesto-neg-convergesto (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; (s) Used terms: n0