Proof step 1 from proof bounded-any-postfix (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ n ≥ m ↔ m ≤ n; (s)

Proof step 2 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 3:

  n ≤ n0, bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

• Proof step 17:

  ¬ n ≤ n0, bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used formulas: n ≤ n0

Proof step 3 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  n ≤ n0, ∃ r0. (λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ≤ r0 ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

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

Proof step 4 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  n ≤ n0, (λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ≤ r0 ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Proof step 6 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  n ≤ n0, (λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)

Proof step 7 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  n ≤ n0, (λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ≤ r0 ⊦ (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: r0

Proof step 9 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  n ≤ n0, ∀ r. (∃ n1. n ≤ n1 ∧ r = f(n1)) → r ≤ r0 ⊦ (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: λ r. ∃ n1. n ≤ n1 ∧ r = f(n1), r0

Proof step 10 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  n ≤ n0, ∀ r. (∃ n1. n ≤ n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∀ r. (∃ n1. n0 ≤ n1 ∧ r = f(n1)) → r ≤ r0

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1), r0

Proof step 12 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  r0 < f(n1), n0 ≤ n1, n ≤ n0, n ≤ n1, ∀ r. (∃ n1. n ≤ n1 ∧ r = f(n1)) → r ≤ r0 ⊦

Rule argument

Additional information

Used simplifier rules: let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 14 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 15:

  r0 < f(n1), n ≤ n1, n ≤ n0, n0 ≤ n1, (∃ n0. n ≤ n0 ∧ f(n1) = f(n0)) → f(n1) ≤ r0 ⊦

Rule argument

Additional information

Used terms: f(n1)

Proof step 15 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  r0 < f(n1), n0 ≤ n1, n ≤ n0, n ≤ n1 ⊦ ∃ n0. n ≤ n0 ∧ f(n1) = f(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 → (r0 ≤ r ↔ false); (as)

Proof step 16 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n1

Proof step 17 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  n0 < n, bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 18 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 19:

  n2.+1 = n - n0, n0 < n, ∀ n, n0, f. n2 = n - n0 ∧ n0 < n ∧ bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) → bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1; ⊦ n < m → m - n ≠ 0; (s)

Proof step 19 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  n2 + 1 = n - n0, n0 < n, ∀ n, n0, f. n2 = n - n0 ∧ n0 < n ∧ bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) → bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ m.+1 = m + 1; (s)

Proof step 20 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  n2 + 1 = n3, n = n3 + n0, n0 < n, n0 ≤ n, ∀ n, n0, f. n2 = n - n0 ∧ n0 < n ∧ bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) → bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, n0, n3

Proof step 21 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ∀ n, n0, f. n2 = n - n0 ∧ n0 < n ∧ bounded≤(λ r. ∃ n1. n ≤ n1 ∧ r = f(n1)) → bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ ¬ m + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n → m ≤ n; (s)

Proof step 22 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  n2 = n0 + n2 - n0 ∧ n0 < n0 + n2 ∧ bounded≤(λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) → bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: n0 + n2, n0, f

Proof step 23 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  n2 ≠ 0 ∧ bounded≤(λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) → bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m + n - m = n; (s)

Proof step 24 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 25:

  bounded≤(λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ⊦ n2 ≠ 0 ∧ bounded≤(λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Proof step 25 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  n2 = 0, bounded≤(λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

• Proof step 49:

  bounded≤(λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Proof step 26 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  bounded≤(λ r. ∃ n1. n0 < n1 ∧ r = f(n1)) ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s)

Proof step 27 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  ∃ r0. (λ r. ∃ n1. n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 < n1 ∧ r = f(n1)

Proof step 28 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  (λ r. ∃ n1. n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Proof step 30 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

  (λ r. ∃ n1. n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)

Proof step 31 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 33:

  (λ r. ∃ n1. n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0, (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: r0

Proof step 33 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  (λ r. ∃ n1. n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∀ r. (∃ n1. n0 ≤ n1 ∧ r = f(n1)) → r ≤ r0, ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1), r0

Proof step 34 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  r0 < f(n1), n0 ≤ n1, (λ r. ∃ n1. n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

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

Proof step 36 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

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

• Proof step 38:

  r0 < f(n1), n0 ≤ n1, ∀ r. (∃ n1. n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 < n1 ∧ r = f(n1), r0

Proof step 37 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 39:

  r0 < f(n1), n0 ≤ n1, (∃ n. n0 < n ∧ f(n1) = f(n)) → f(n1) ≤ r0, ∀ r. (∃ n1. n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: f(n1)

Proof step 39 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  r0 < f(n1), n0 ≤ n1, ∀ r. (∃ n1. n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0, ∃ n. n0 < n ∧ f(n1) = f(n)

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 → (r0 ≤ r ↔ false); (as)

Proof step 40 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 41:

  r0 < f(n1), n0 ≤ n1, ∀ r. (∃ n1. n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ n. n0 < n ∧ f(n1) = f(n), ∃ r0. (λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)) ≤ r0, n0 < n1 ∧ f(n1) = f(n1)

Rule argument

Additional information

Used terms: n1

Proof step 41 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  r0 < f(n1), ∀ r. (∃ n. n1 < n ∧ r = f(n)) → r ≤ r0 ⊦ ∃ n. n1 < n ∧ f(n1) = f(n), ∃ r0. (λ r. ∃ n. n1 ≤ n ∧ r = f(n)) ≤ r0

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 42 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 43:

  r0 < f(n1), ∀ r. (∃ n. n1 < n ∧ r = f(n)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n. n1 ≤ n ∧ r = f(n)) ≤ r0, ∃ n. n1 < n ∧ f(n1) = f(n), (λ r. ∃ n. n1 ≤ n ∧ r = f(n)) ≤ f(n1)

Rule argument

Additional information

Used terms: f(n1)

Proof step 43 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

  r0 < f(n1), ∀ r. (∃ n. n1 < n ∧ r = f(n)) → r ≤ r0 ⊦ ∀ r. (∃ n. n1 ≤ n ∧ r = f(n)) → r ≤ f(n1), ∃ n. n1 < n ∧ f(n1) = f(n), ∃ r0. (λ r. ∃ n. n1 ≤ n ∧ r = f(n)) ≤ r0

Rule argument

Additional information

Used terms: λ r. ∃ n. n1 ≤ n ∧ r = f(n), f(n1)

Proof step 44 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  r0 < f(n1), f(n1) < f(n), r0 < f(n), n1 ≤ n, ∀ r. (∃ n. n1 < n ∧ r = f(n)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n. n1 ≤ n ∧ r = f(n)) ≤ r0, ∃ n. n1 < n ∧ f(n1) = f(n)

Rule argument

Additional information

Used simplifier rules: trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 46 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 47:

  r0 < f(n), f(n1) < f(n), r0 < f(n1), n1 ≤ n, (∃ n0. n1 < n0 ∧ f(n) = f(n0)) → f(n) ≤ r0, ∀ r. (∃ n. n1 < n ∧ r = f(n)) → r ≤ r0 ⊦ ∃ n. n1 < n ∧ f(n1) = f(n), ∃ r0. (λ r. ∃ n. n1 ≤ n ∧ r = f(n)) ≤ r0

Rule argument

Additional information

Used terms: f(n)

Proof step 47 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  r0 < f(n1), f(n1) < f(n), r0 < f(n), n1 ≤ n, ∀ r. (∃ n. n1 < n ∧ r = f(n)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n. n1 ≤ n ∧ r = f(n)) ≤ r0, ∃ n. n1 < n ∧ f(n1) = f(n), ∃ n0. n1 < n0 ∧ f(n) = f(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 → (r0 ≤ r ↔ false); (as)

Proof step 48 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ ¬ r < r; (s) Used terms: n

Proof step 49 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

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

• Proof step 51:

  ∃ r0. (λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ bounded≤(λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)

Proof step 50 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 51 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  (λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), bounded≤(λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Proof step 52 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 53:

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

• Proof step 54:

  (λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)

Proof step 53 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 54 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 55:

  (λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0

Rule argument

Additional information

Used terms: r0

Proof step 55 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

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

• Proof step 57:

  (λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∀ r. (∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) → r ≤ r0, ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1), r0

Proof step 56 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  r0 < f(n1), n0 + n2 ≤ n1, (λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1)) ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

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

Proof step 58 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

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

• Proof step 60:

  r0 < f(n1), n0 + n2 ≤ n1, ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: λ r. ∃ n1. n2 + n0 < n1 ∧ r = f(n1), r0

Proof step 59 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 60 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 61:

  r0 < f(n1), n0 + n2 ≤ n1, (∃ n. n2 + n0 < n ∧ f(n1) = f(n)) → f(n1) ≤ r0, ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: f(n1)

Proof step 61 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  r0 < f(n1), n0 + n2 ≤ n1, ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, ∃ n. n2 + n0 < n ∧ f(n1) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 → (r0 ≤ r ↔ false); (as)

Proof step 62 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 63:

  r0 < f(n1), n0 + n2 ≤ n1, ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ n. n2 + n0 < n ∧ f(n1) = f(n), ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, n2 + n0 < n1 ∧ f(n1) = f(n1), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: n1

Proof step 63 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  r0 < f(n2 + n0), ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), ∃ r0. (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ r0, bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 64 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 65:

  r0 < f(n2 + n0), ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1)), (λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) ≤ f(n2 + n0)

Rule argument

Additional information

Used terms: f(n2 + n0)

Proof step 65 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

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

• Proof step 67:

  r0 < f(n2 + n0), ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∀ r. (∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1)) → r ≤ f(n2 + n0), ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: λ r. ∃ n1. n0 + n2 ≤ n1 ∧ r = f(n1), f(n2 + n0)

Proof step 66 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 67 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  r0 < f(n2 + n0), f(n2 + n0) < f(n1), r0 < f(n1), n0 + n2 ≤ n1, ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 68 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ m ≤ n → (n ≤ m ↔ m = n)

• Proof step 70:

  r0 < f(n1), f(n2 + n0) < f(n1), r0 < f(n2 + n0), n0 + n2 ≤ n1, ¬ n1 ≤ n0 + n2, ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m ≤ m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ r < r; (s) Used terms: n0 + n2, n1

Proof step 69 from proof bounded-any-postfix (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  n0 + n2 ≠ n1, n0 + n2 < n1, r0 < f(n1), f(n2 + n0) < f(n1), r0 < f(n2 + n0), ∀ r. (∃ n1. n2 + n0 < n1 ∧ r = f(n1)) → r ≤ r0 ⊦ ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s)

Proof step 71 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 72:

  n0 + n2 ≠ n1, r0 < f(n2 + n0), f(n2 + n0) < f(n1), r0 < f(n1), n0 + n2 < n1, (∃ n. n2 + n0 < n ∧ f(n1) = f(n)) → f(n1) ≤ r0 ⊦ ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used terms: f(n1)

Proof step 72 from proof bounded-any-postfix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  n0 + n2 ≠ n1, n0 + n2 < n1, r0 < f(n1), f(n2 + n0) < f(n1), r0 < f(n2 + n0) ⊦ ∃ n. n2 + n0 < n ∧ f(n2 + n0) = f(n), ∃ n. n2 + n0 < n ∧ f(n1) = f(n), bounded≤(λ r. ∃ n1. n0 ≤ n1 ∧ r = f(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 → (r0 ≤ r ↔ false); (as)

Proof step 73 from proof bounded-any-postfix (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: n1