[Imprint][Data Privacy Statement][E-Mail]
View long theorem info.
View the proof.
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
Proof step 1 from proof monle-boundedle-f-below-bound (conclusion)
(back to tree)
| ⊦ bounded≤(f, r) ∧ mon≤(f) → ¬ limit(f) < f(n) |
System applied rule normalize
And obtained the following new goals
Rule argument
Additional information
Proof step 2 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| limit(f) < f(n), bounded≤(f, r), mon≤(f) ⊦ |
User applied rule apply lemma
And obtained the following new goals
- Proof step 3:
mon≤(f), bounded≤(f, r) ⊦ limit(f) = sup(λ r. ∃ n. r = f(n))
- Proof step 4:
limit(f) < f(n), bounded≤(f, r), mon≤(f), limit(f) = sup(λ r. ∃ n. r = f(n)) ⊦
Rule argument
spec: <toplevel>, name:monle-limit-sup,
seq:mon≤(f), bounded≤(f, r) ⊦ limit(f) = sup(λ r. ∃ n. r = f(n)), subst:[f, r] → [f, r]
Additional information
Used terms: f, r
Proof step 3 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| mon≤(f), bounded≤(f, r) ⊦ limit(f) = sup(λ r. ∃ n. r = f(n)) |
Proof step 4 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| limit(f) < f(n), bounded≤(f, r), mon≤(f), limit(f) = sup(λ r. ∃ n. r = f(n)) ⊦ |
User applied rule subst equation
And obtained the following new goals
Rule argument
pos: left 4, flags: discard
Additional information
Proof step 5 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n) ⊦ |
User applied rule apply lemma
And obtained the following new goals
- Proof step 6:
⊦ bounded≤(rset) → rset ≤ sup(rset)
- Proof step 7:
bounded≤(f, r), mon≤(f), 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) ⊦
Rule argument
spec: real-supinf, name:sup-upperbound, seq: ⊦ bounded≤(rset) → rset ≤ sup(rset),
subst:[rset] → [λ r. ∃ n. r = f(n)]
Additional information
Used terms: λ r. ∃ n. r = f(n)
Proof step 6 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| ⊦ bounded≤(rset) → rset ≤ sup(rset) |
A spec-lemma
Proof step 7 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), 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) ⊦ |
User applied rule case distinction
And obtained the following new goals
- Proof step 8:
bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n) ⊦ bounded≤(λ r. ∃ n. r = f(n))
- Proof step 17:
bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)) ⊦
Rule argument
pos: left 3
Additional information
Proof step 8 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n) ⊦ bounded≤(λ r. ∃ n. r = f(n)) |
User applied rule apply rewrite lemma
And obtained the following new goals
- Proof step 9:
⊦ bounded≤(f, r) ↔ (∀ n. f(n) ≤ r)
- Proof step 10:
mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ bounded≤(λ r. ∃ n. r = f(n))
Rule argument
spec: <toplevel>, name: boundedle-def, seq: ⊦ bounded≤(f, r) ↔ (∀ n. f(n) ≤ r),
subst:[f, r] → [f, r], <all paths>
Additional information
Used terms: f, r
Proof step 10 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ bounded≤(λ r. ∃ n. r = f(n)) |
User applied rule apply rewrite lemma
And obtained the following new goals
- Proof step 11:
⊦ bounded≤(rset) ↔ (∃ r0. rset ≤ r0)
- Proof step 12:
mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ ∃ r0. (λ r. ∃ n. r = f(n)) ≤ r0
Rule argument
spec: real-supinf, name: boundedle-def, seq: ⊦ bounded≤(rset) ↔ (∃ r0. rset ≤ r0),
subst:[rset] → [λ r. ∃ n. r = f(n)], <all paths>
Additional information
Used terms: λ r. ∃ n. r = f(n)
Proof step 11 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| ⊦ bounded≤(rset) ↔ (∃ r0. rset ≤ r0) |
A spec-lemma
Proof step 12 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ ∃ r0. (λ r. ∃ n. r = f(n)) ≤ r0 |
User applied rule exists right
And obtained the following new goals
Rule argument
pos: right 1 terms: r abort: F discard: T computed: F
Additional information
Used terms: r
Proof step 13 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ (λ r. ∃ n. r = f(n)) ≤ r |
User applied rule apply rewrite lemma
And obtained the following new goals
- Proof step 14:
⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0)
- Proof step 15:
mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ ∀ r1. (∃ n. r1 = f(n)) → r1 ≤ r
Rule argument
spec: real-supinf, name: upperbound-def, seq: ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0),
subst:[rset, r0] → [λ r. ∃ n. r = f(n), r], <all paths>
Additional information
Used terms: λ r. ∃ n. r = f(n), r
Proof step 14 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0) |
A spec-lemma
Proof step 15 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ ∀ r1. (∃ n. r1 = f(n)) → r1 ≤ r |
Heuristic simplifier applied rule simplifier
And obtained the following new goals
Rule argument
Additional information
Used simplifier rules:
⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)
Proof step 16 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| r < f(n0), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ n. f(n) ≤ r ⊦ |
User applied rule all left
And closed the goal!
Rule argument
pos: left 4 terms: n0 abort: F discard: T computed: F
Additional information
Used simplifier rules:
⊦ r < r0 → (r0 ≤ r ↔ false); (as)
Used terms: n0
Proof step 17 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), (λ r. ∃ n. r = f(n)) ≤ sup(λ r. ∃ n. r = f(n)) ⊦ |
User applied rule apply rewrite lemma
And obtained the following new goals
- Proof step 18:
⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0)
- Proof step 19:
bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ r. (∃ n. r = f(n)) → r ≤ sup(λ r. ∃ n. r = f(n)) ⊦
Rule argument
spec: real-supinf, name: upperbound-def, seq: ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0),
subst:[rset, r0] → [λ r. ∃ n. r = f(n), sup(λ r. ∃ n. r = f(n))], <all paths>
Additional information
Used terms: λ r. ∃ n. r = f(n), sup(λ r. ∃ n. r = f(n))
Proof step 18 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0) |
A spec-lemma
Proof step 19 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), ∀ r. (∃ n. r = f(n)) → r ≤ sup(λ r. ∃ n. r = f(n)) ⊦ |
User applied rule all left
And obtained the following new goals
- Proof step 20:
bounded≤(f, r), mon≤(f), (∃ n0. f(n) = f(n0)) → f(n) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) ⊦
Rule argument
pos: left 4 terms: f(n) abort: F discard: T computed: F
Additional information
Used terms: f(n)
Proof step 20 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), (∃ n0. f(n) = f(n0)) → f(n) ≤ sup(λ r. ∃ n. r = f(n)), sup(λ r. ∃ n. r = f(n)) < f(n) ⊦ |
User applied rule case distinction
And obtained the following new goals
- Proof step 21:
bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n) ⊦ ∃ n0. f(n) = f(n0)
- Proof step 22:
bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), f(n) ≤ sup(λ r. ∃ n. r = f(n)) ⊦
Rule argument
pos: left 3
Additional information
Proof step 21 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n) ⊦ ∃ n0. f(n) = f(n0) |
Heuristic quantifier closing applied rule exists right
And closed the goal!
Rule argument
pos: right 1 terms: n
Additional information
Used terms: n
Proof step 22 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), f(n) ≤ sup(λ r. ∃ n. r = f(n)) ⊦ |
User applied rule apply lemma
And obtained the following new goals
- Proof step 23:
⊦ r ≤ r0 ∧ r0 < r1 → r < r1
- Proof step 24:
bounded≤(f, r), mon≤(f), f(n) ≤ sup(λ r. ∃ n. r = f(n)) ∧ sup(λ r. ∃ n. r = f(n)) < f(n) → f(n) < f(n), sup(λ r. ∃ n. r = f(n)) < f(n),
f(n) ≤ sup(λ r. ∃ n. r = f(n))
⊦
Rule argument
spec: real-abs, name:forward-lels, seq: ⊦ r ≤ r0 ∧ r0 < r1 → r < r1,
subst:[r, r0, r1] → [f(n), sup(λ r. ∃ n. r = f(n)), f(n)]
Additional information
Used terms: f(n), sup(λ r. ∃ n. r = f(n)), f(n)
Proof step 23 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| ⊦ r ≤ r0 ∧ r0 < r1 → r < r1 |
A spec-lemma
Proof step 24 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), f(n) ≤ sup(λ r. ∃ n. r = f(n)) ∧ sup(λ r. ∃ n. r = f(n)) < f(n) → f(n) < f(n), sup(λ r. ∃ n. r = f(n)) < f(n),
f(n) ≤ sup(λ r. ∃ n. r = f(n))
⊦ |
Heuristic simplifier applied rule simplifier
And obtained the following new goals
- Proof step 25:
bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), f(n) ≤ sup(λ r. ∃ n. r = f(n))
⊦ f(n) ≤ sup(λ r. ∃ n. r = f(n)) ∧ sup(λ r. ∃ n. r = f(n)) < f(n)
Rule argument
Additional information
Used simplifier rules:
⊦ ¬ r < r; (s)
Proof step 25 from proof monle-boundedle-f-below-bound (previous step)
(back to tree)
| bounded≤(f, r), mon≤(f), sup(λ r. ∃ n. r = f(n)) < f(n), f(n) ≤ sup(λ r. ∃ n. r = f(n))
⊦ f(n) ≤ sup(λ r. ∃ n. r = f(n)) ∧ sup(λ r. ∃ n. r = f(n)) < f(n) |
User applied rule case distinction
And closed the goal!
Rule argument
pos: right 1
Additional information
Proof Tree for monle-boundedle-f-below-bound
(View conclusion)
The following image shows the proof tree of sequent calculus. The
proved goal is at the bottom. You can click on the nodes to view
additional rules. See here for details on colors in a proof
tree.
