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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  inf(rset) ≠ ~ sup(λ r. rset(0.r + ~ r)), bounded≥(rset) ⊦

Rule argument

Additional information

Proof step 2 from proof inf-neg-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Used simplifier rules: boundedge-def: ⊦ bounded≥(rset) ↔ (∃ r0. r0 ≤ rset); lowerbound-def: ⊦ r0 ≤ rset ↔ (∀ r. rset(r) → r0 ≤ r); ⊦ ~ 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 3 from proof inf-neg-sup (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ bounded≤(rset) ∧ rset ≤ r → sup(rset) ≤ r

• Proof step 5:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, bounded≤(λ r. rset(~ r)) ∧ (λ r. rset(~ r)) ≤ ~ inf(rset) → sup(λ r. rset(~ r)) ≤ ~ inf(rset), ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Used terms: λ r. rset(~ r), ~ inf(rset)

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

Lemma sup-lowest-upperbound

Proof step 5 from proof inf-neg-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, (∃ r. ∀ r1. rset(~ r1) → r1 ≤ r) ∧ (rset(~ r) → r + inf(rset) ≤ 0.r) → sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Used simplifier rules: boundedle-def: ⊦ bounded≤(rset) ↔ (∃ r0. rset ≤ r0); upperbound-def: ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0); ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s) ⊦ r ≤ ~ r0 ↔ r + r0 ≤ 0.r; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, (∃ r. ∀ r1. rset(~ r1) → r1 ≤ r) ∧ (rset(~ r) → r + inf(rset) ≤ 0.r) → sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r. rset(r) → r0 ≤ r, ∃ r. ∀ r1. rset(~ r1) → r1 ≤ r ⊦

• Proof step 40:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, (∃ r. ∀ r1. rset(~ r1) → r1 ≤ r) ∧ (rset(~ r) → r + inf(rset) ≤ 0.r) → sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. ∀ r1. rset(~ r1) → r1 ≤ r

Rule argument

Additional information

Used formulas: ∃ r. ∀ r1. rset(~ r1) → r1 ≤ r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, (∃ r. ∀ r1. rset(~ r1) → r1 ≤ r) ∧ (rset(~ r) → r + inf(rset) ≤ 0.r) → sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Proof step 8 from proof inf-neg-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦ (∃ r. ∀ r1. rset(~ r1) → r1 ≤ r) ∧ (rset(~ r) → r + inf(rset) ≤ 0.r)

• Proof step 24:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. ∀ r1. rset(~ r1) → r1 ≤ r

• Proof step 13:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, rset(~ r), ¬ r + inf(rset) ≤ 0.r, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 11:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦ ∀ r0. rset(~ r0) → r0 ≤ r1

Rule argument

Additional information

Used terms: r1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, r1 < r, rset(~ r), ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

Proof step 12 from proof inf-neg-sup (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: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 15:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), rset(~ r) → r ≤ r1, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), r ≤ r1, ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 17:

  ⊦ bounded≥(rset) → inf(rset) ≤ rset

• Proof step 18:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), r ≤ r1, bounded≥(rset) → inf(rset) ≤ rset, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Used terms: rset

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

Lemma inf-lowerbound

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), r ≤ r1, (∃ r2. ∀ r. rset(r) → r2 ≤ r) → (∀ r. rset(r) → inf(rset) ≤ r), ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦

Rule argument

Additional information

Used simplifier rules: boundedge-def: ⊦ bounded≥(rset) ↔ (∃ r0. r0 ≤ rset); lowerbound-def: ⊦ r0 ≤ rset ↔ (∀ r. rset(r) → r0 ≤ r);

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

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), r ≤ r1, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r2. ∀ r. rset(r) → r2 ≤ r

• Proof step 23:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), r ≤ r1, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r, ∀ r. rset(r) → inf(rset) ≤ r ⊦

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 21:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), rset(~ r), r ≤ r1, ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦ ∀ r. rset(r) → r0 ≤ r

Rule argument

Additional information

Used terms: r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r + inf(rset), r2 < r0, rset(r2), rset(~ r), r ≤ r1, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

Proof step 22 from proof inf-neg-sup (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: r2

Proof step 23 from proof inf-neg-sup (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 ↔ r + r0 ≤ 0.r; (s) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: ~ r

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 25:

  ⊦ bounded≥(rset) ∧ r ≤ rset → r ≤ inf(rset)

• Proof step 26:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, bounded≥(rset) ∧ ~ sup(λ r. rset(~ r)) ≤ rset → ~ sup(λ r. rset(~ r)) ≤ inf(rset), ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Used terms: rset, ~ sup(λ r. rset(~ r))

Proof step 25 from proof inf-neg-sup (previous step) (back to tree)

Lemma inf-highest-lowerbound

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦ (∃ r. ∀ r1. rset(r1) → r ≤ r1) ∧ (rset(r) → 0.r ≤ sup(λ r. rset(~ r)) + r)

Rule argument

Additional information

Used simplifier rules: boundedge-def: ⊦ bounded≥(rset) ↔ (∃ r0. r0 ≤ rset); lowerbound-def: ⊦ r0 ≤ rset ↔ (∀ r. rset(r) → r0 ≤ r); ⊦ r < r0 → (r0 ≤ r ↔ false); (as) ⊦ ~ r ≤ r0 ↔ 0.r ≤ r + r0; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 28:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. ∀ r1. rset(r1) → r ≤ r1

• Proof step 31:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, rset(r), ¬ 0.r ≤ sup(λ r. rset(~ r)) + r, ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 29:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦ ∀ r1. rset(r1) → r0 ≤ r1

Rule argument

Additional information

Used terms: r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, r < r0, rset(r), ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

Proof step 30 from proof inf-neg-sup (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: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, sup(λ r. rset(~ r)) + r < 0.r, rset(r), ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 33:

  ⊦ bounded≤(rset) → rset ≤ sup(rset)

• Proof step 34:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + r < 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, rset(r), bounded≤(λ r. rset(~ r)) → (λ r. rset(~ r)) ≤ sup(λ r. rset(~ r)), ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

Used terms: λ r. rset(~ r)

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

Lemma sup-upperbound

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, sup(λ r. rset(~ r)) + r < 0.r, rset(r), (∃ r2. ∀ r. rset(~ r) → r ≤ r2) → (∀ r. rset(~ r) → r ≤ sup(λ r. rset(~ r))), ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦

Rule argument

Additional information

Used simplifier rules: boundedle-def: ⊦ bounded≤(rset) ↔ (∃ r0. rset ≤ r0); upperbound-def: ⊦ rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0);

Proof step 35 from proof inf-neg-sup (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 36:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + r < 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, rset(r), ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r2. ∀ r. rset(~ r) → r ≤ r2

• Proof step 39:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + r < 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, rset(r), ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r, ∀ r. rset(~ r) → r ≤ sup(λ r. rset(~ r)) ⊦

Rule argument

Additional information

Proof step 36 from proof inf-neg-sup (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 37:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, sup(λ r. rset(~ r)) + r < 0.r, rset(r), ∀ r. rset(r) → r0 ≤ r, ∀ r0. rset(~ r0) → r0 ≤ r1 ⊦ ∀ r. rset(~ r) → r ≤ r1

Rule argument

Additional information

Used terms: r1

Proof step 37 from proof inf-neg-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, sup(λ r. rset(~ r)) + r < 0.r, sup(λ r. rset(~ r)) + inf(rset) < 0.r, r1 < r2, rset(~ r2), rset(r), ∀ r0. rset(~ r0) → r0 ≤ r1, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

Proof step 38 from proof inf-neg-sup (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: r2

Proof step 39 from proof inf-neg-sup (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 40 from proof inf-neg-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. ∀ r1. rset(~ r1) → r1 ≤ r

Rule argument

Additional information

Proof step 41 from proof inf-neg-sup (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 42:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, ∀ r. rset(r) → r0 ≤ r ⊦ ∀ r1. rset(~ r1) → r1 ≤ ~ r0

Rule argument

Additional information

Used terms: ~ r0

Proof step 42 from proof inf-neg-sup (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  sup(λ r. rset(~ r)) + inf(rset) ≠ 0.r, 0.r < r1 + r0, rset(~ r1), ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

Proof step 43 from proof inf-neg-sup (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 ↔ r + r0 ≤ 0.r; (s) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: ~ r1