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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

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 2 from proof inf-exists (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ⊦ ∀ rset. bounded≤(rset) → (∃ r0. rset ≤ r0 ∧ (∀ r1. r1 < r0 → ¬ rset ≤ r1))

• Proof step 4:

  ∀ r. rset(r) → r0 ≤ r, ∀ rset. bounded≤(rset) → (∃ r0. rset ≤ r0 ∧ (∀ r1. r1 < r0 → ¬ rset ≤ r1)) ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

Rule argument

Additional information

Used terms:

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

Lemma sup-exists

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ∀ r. rset(r) → r0 ≤ r, ∀ rset0. (∃ r. ∀ r1. rset0(r1) → r1 ≤ r) → (∃ r. (∀ r1. rset0(r1) → r1 ≤ r) ∧ (∀ r1. r1 < r → ¬(∀ r. rset0(r) → r ≤ r1))) ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

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 5 from proof inf-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  (∃ r. ∀ r1. rset(~ r1) → r1 ≤ r) → (∃ r. (∀ r1. rset(~ r1) → r1 ≤ r) ∧ (∀ r1. r1 < r → ¬(∀ r. rset(~ r) → r ≤ r1))), ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

Rule argument

Additional information

Used terms: λ r. rset(~ r)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (∃ r. ∀ r1. rset(~ r1) → r1 ≤ r) → (∀ r1. rset(~ r1) → r1 ≤ r) ∧ (∀ r1. r1 < r → ¬(∀ r. rset(~ r) → r ≤ r1)), ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r)), ∃ r. ∀ r1. rset(~ r1) → r1 ≤ r

• Proof step 11:

  ∀ r. rset(r) → r0 ≤ r, ∀ r1. rset(~ r1) → r1 ≤ r, ∀ r1. r1 < r → ¬(∀ r. rset(~ r) → r ≤ r1) ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  ∀ r. rset(r) → r0 ≤ r ⊦ ∀ r1. rset(~ r1) → r1 ≤ ~ r0, ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

Rule argument

Additional information

Used terms: ~ r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  0.r < r1 + r0, rset(~ r1), ∀ r. rset(r) → r0 ≤ r ⊦ ∃ r. (∀ r1. rset(r1) → r ≤ r1) ∧ (∀ r1. r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

Rule argument

Additional information

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

Proof step 10 from proof inf-exists (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

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

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  ∀ r1. r1 < r → ¬(∀ r. rset(~ r) → r ≤ r1), ∀ r1. rset(~ r1) → r1 ≤ r, ∀ r. rset(r) → r0 ≤ r ⊦ (∀ r1. rset(r1) → ~ r ≤ r1) ∧ (∀ r1. ~ r < r1 → ¬(∀ r. rset(r) → r1 ≤ r))

Rule argument

Additional information

Used terms: ~ r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ∀ r. rset(r) → r0 ≤ r, ∀ r1. rset(~ r1) → r1 ≤ r, ∀ r1. r1 < r → ¬(∀ r. rset(~ r) → r ≤ r1) ⊦ (rset(r1) → 0.r ≤ r + r1) ∧ (0.r < r2 + r → ¬(∀ r. rset(r) → r2 ≤ r))

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

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

• Proof step 18:

  0.r < r2 + r, ∀ r. rset(r) → r2 ≤ r, ∀ r1. r1 < r → ¬(∀ r. rset(~ r) → r ≤ r1), ∀ r1. rset(~ r1) → r1 ≤ r, ∀ r. rset(r) → r0 ≤ r ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used terms: r1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Proof step 17 from proof inf-exists (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: ~ r1

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

User applied rule all left

And obtained the following new goals

• Proof step 19:

  0.r < r2 + r, ~ r2 < r → ¬(∀ r. rset(~ r) → r ≤ ~ r2), ∀ r. rset(r) → r0 ≤ r, ∀ r1. rset(~ r1) → r1 ≤ r, ∀ r. rset(r) → r2 ≤ r ⊦

Rule argument

Additional information

Used terms: ~ r2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

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

Proof step 20 from proof inf-exists (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