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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof monge-limit-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) ⊦ limit(f) = inf(λ r. ∃ n. r = f(n))

Rule argument

Additional information

Used terms: f, r

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

Lemma boundedge-neg-boundedle

Proof step 4 from proof monge-limit-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)) ⊦ limit(f) = inf(λ r. ∃ n. r = f(n))

Rule argument

Additional information

Used terms: f

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

Lemma monge-neg-monle

Proof step 6 from proof monge-limit-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) ⊦ limit(f) = sup(λ r. ∃ n. r = f(n))

• Proof step 8:

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

Rule argument

Additional information

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

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

Lemma monle-limit-sup

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ converges(f) → limit(f) = ~ limit(λ n. ~ f(n))

• Proof step 10:

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

• Proof step 12:

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

Rule argument

Additional information

Used terms: f

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

Lemma limit-neg-limit

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ converges(f) ↔ converges(λ n. ~ f(n))

Rule argument

Additional information

Used simplifier rules: monle-boundedle-converges: ⊦ bounded≤(f, r) ∧ mon≤(f) → converges(f); Used terms: f

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

Lemma converges-neg-converges

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r + 0.r = 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 = r0 ↔ r + r0 = 0.r; (s) ⊦ ~ r = ~ r0 ↔ r = r0; (s) Used terms: λ r. ∃ n. r = f(n)

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

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

Rule argument

Additional information

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

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

Lemma boundedle-def

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

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

Rule argument

Additional information

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

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

A spec-lemma

Proof step 20 from proof monge-limit-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

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) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s) ⊦ ~ r ≤ r0 ↔ 0.r ≤ r + r0; (s)

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

User applied rule exists right

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

Used terms: ~ r

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

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

Rule argument

Additional information

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

Proof step 23 from proof monge-limit-inf (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof monge-limit-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  r1 + f(n) = 0.r, 0.r < r1 + r, f(n) < r, converges(f), mon≤(λ n. ~ f(n)), ∀ n. r ≤ f(n), limit(λ n. ~ f(n)) = sup(λ r0. ∃ n. f(n) + r0 = 0.r) ⊦ limit(λ n. ~ f(n)) + inf(λ r. ∃ n. r = f(n)) = 0.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 < 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 25 from proof monge-limit-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