Proof step 1 from proof monge-boundedge-f-above-bound (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  f(n) < limit(f), bounded≥(f, r), mon≥(f) ⊦

Rule argument

Additional information

Proof step 2 from proof monge-boundedge-f-above-bound (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:

  f(n) < limit(f), bounded≤(λ n. ~ f(n), ~ r), mon≥(f) ⊦

Rule argument

Additional information

Used terms: f, r

Proof step 3 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Lemma boundedge-neg-boundedle

Proof step 4 from proof monge-boundedge-f-above-bound (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:

  f(n) < limit(f), bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)) ⊦

Rule argument

Additional information

Used terms: f

Proof step 5 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Lemma monge-neg-monle

Proof step 6 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  ⊦ bounded≤(f, r) ∧ mon≤(f) → ¬ limit(f) < f(n)

• Proof step 8:

  f(n) < limit(f), bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), bounded≤(λ n. ~ f(n), ~ r) ∧ mon≤(λ n. ~ f(n)) → ¬ limit(λ n. ~ f(n)) < ~ f(n) ⊦

Rule argument

Additional information

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

Proof step 7 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Lemma monle-boundedle-f-below-bound

Proof step 8 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  f(n) < limit(f), bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), 0.r ≤ limit(λ n. ~ f(n)) + f(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r0 < ~ r ↔ r0 + r < 0.r; (s)

Proof step 9 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  f(n) < limit(f), bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), 0.r ≤ limit(λ n. ~ f(n)) + f(n), ¬ converges(f) ⊦

Rule argument

Additional information

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

Proof step 10 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Lemma limit-neg-limit

Proof step 11 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  ⊦ bounded≤(f, r) ∧ mon≤(f) → converges(f)

• Proof step 13:

  f(n) < limit(f), bounded≤(λ n. ~ f(n), ~ r), mon≤(λ n. ~ f(n)), 0.r ≤ limit(λ n. ~ f(n)) + f(n), ¬ converges(f), bounded≤(λ n. ~ f(n), ~ r) ∧ mon≤(λ n. ~ f(n)) → converges(λ n. ~ f(n)) ⊦

Rule argument

Additional information

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

Proof step 12 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Lemma monle-boundedle-converges

Proof step 13 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  f(n) < limit(f), bounded≤(λ n. ~ f(n), ~ r), converges(λ n. ~ f(n)), mon≤(λ n. ~ f(n)), 0.r ≤ limit(λ n. ~ f(n)) + f(n), ¬ converges(f) ⊦

Rule argument

Additional information

Proof step 14 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used terms: f

Proof step 15 from proof monge-boundedge-f-above-bound (previous step) (back to tree)

Lemma converges-neg-converges