Proof step 1 from proof max-def (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  maxenc(m0, m) ≠ n, m < ((n + 1) * (n + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m ⊦

Rule argument

Additional information

Proof step 2 from proof max-def (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  maxenc(m0, m) ≠ n, m < ((n + 1) * (n + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: m - m0

Proof step 3 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ((m + 1) * (m + 2)) / 2 ≤ n → maxenc(m, n) = maxenc(m + 1, n)

• Proof step 5:

  maxenc(m0, m) ≠ n, m < ((n + 1) * (n + 2)) / 2, (m0 * (m0 + 1)) / 2 ≤ m, (n * (n + 1)) / 2 ≤ m, ¬ ((m0 + 1) * (m0 + 2)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

• Proof step 27:

  maxenc(m0 + 1, m) ≠ n, m < ((n + 1) * (n + 2)) / 2, (m0 * (m0 + 1)) / 2 ≤ m, (n * (n + 1)) / 2 ≤ m, ((m0 + 1) * (m0 + 2)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used terms: m, m0

Proof step 4 from proof max-def (previous step) (back to tree)

Lemma maxi-rec

Proof step 5 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ¬ ((m + 1) * (m + 2)) / 2 ≤ n → maxenc(m, n) = m

• Proof step 7:

  m0 ≠ n, m < ((n + 1) * (n + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m, ¬ ((m0 + 1) * (m0 + 2)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used terms: m, m0

Proof step 6 from proof max-def (previous step) (back to tree)

Lemma maxi-found

Proof step 7 from proof max-def (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  (m * (m + 1)) / 2 ≤ (n * (n + 1)) / 2 + n0, (n * (n + 1)) / 2 + n0 < ((m + 1) * (m + 2)) / 2, n0 ≤ n ⊦ m = n

• Proof step 9:

  m0 ≠ n, m < ((n + 1) * (n + 2)) / 2, (m0 * (m0 + 1)) / 2 ≤ m, (n * (n + 1)) / 2 ≤ m, ¬ ((m0 + 1) * (m0 + 2)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦ (n * (n + 1)) / 2 ≤ (m0 * (m0 + 1)) / 2 + 0 ∧ (m0 * (m0 + 1)) / 2 + 0 < ((n + 1) * (n + 2)) / 2 ∧ 0 ≤ m0

Rule argument

Additional information

Used terms: n, m0, 0

Proof step 8 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof max-def (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  m0 ≠ n, m < ((n + 1) * (n + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m, ¬ (n * (n + 1)) / 2 ≤ (m0 * (m0 + 1)) / 2 + 0, ¬ ((m0 + 1) * (m0 + 2)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m * (n + 1) = m * n + m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ (m + 2) / 2 = m / 2 + 1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 0 ≤ m; (s) ⊦ 0 + m = m; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ls-02: n ≠ 0 ⊦ m / n < m0 / n → m < m0; (forward) from specification nat-div let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m / 2 = 0 ↔ m = 0 ∨ m = 1; (s) ⊦ m * m + m ≠ 1; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ ¬ n < n; (s)

Proof step 10 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ n + 0 = n

• Proof step 12:

  m0 ≠ n, m < ((n + 1) * (n + 2)) / 2, (m0 * (m0 + 1)) / 2 ≤ m, (n * (n + 1)) / 2 ≤ m, ¬ (n * (n + 1)) / 2 ≤ (m0 * (m0 + 1)) / 2, ¬ ((m0 + 1) * (m0 + 2)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used terms: (m0 * (m0 + 1)) / 2

Proof step 11 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ m ≤ n ↔ ¬ n < m

• Proof step 14:

  m0 ≠ n, (m0 * (m0 + 1)) / 2 < (n * (n + 1)) / 2, m < ((n + 1) * (n + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m, ¬ ((m0 + 1) * (m0 + 2)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used terms: (m0 * (m0 + 1)) / 2, (n * (n + 1)) / 2

Proof step 13 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ m ≤ n ↔ ¬ n < m

• Proof step 16:

  m0 ≠ n, m < ((m0 + 1) * (m0 + 2)) / 2, m < ((n + 1) * (n + 2)) / 2, (m0 * (m0 + 1)) / 2 < (n * (n + 1)) / 2, (m0 * (m0 + 1)) / 2 ≤ m, (n * (n + 1)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used terms: m, ((m0 + 1) * (m0 + 2)) / 2

Proof step 15 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ (m * (m + 1)) / 2 < (n * (n + 1)) / 2 ↔ m < n

• Proof step 18:

  m0 ≠ n, m0 < n, m < ((n + 1) * (n + 2)) / 2, m < ((m0 + 1) * (m0 + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used terms: n, m0

Proof step 17 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof max-def (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 19:

  (m * (m + 1)) / 2 ≤ (n * (n + 1)) / 2 + n0, (n * (n + 1)) / 2 + n0 < ((m + 1) * (m + 2)) / 2, n0 ≤ n ⊦ m = n

• Proof step 20:

  m0 ≠ n, m < ((m0 + 1) * (m0 + 2)) / 2, m < ((n + 1) * (n + 2)) / 2, m0 < n, (m0 * (m0 + 1)) / 2 ≤ m, (n * (n + 1)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦ (m0 * (m0 + 1)) / 2 ≤ (n * (n + 1)) / 2 + 0 ∧ (n * (n + 1)) / 2 + 0 < ((m0 + 1) * (m0 + 2)) / 2 ∧ 0 ≤ n

Rule argument

Additional information

Used terms: m0, n, 0

Proof step 19 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ n + 0 = n

• Proof step 22:

  m0 ≠ n, m0 < n, m < ((n + 1) * (n + 2)) / 2, m < ((m0 + 1) * (m0 + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦ (m0 * (m0 + 1)) / 2 ≤ (n * (n + 1)) / 2 ∧ (n * (n + 1)) / 2 < ((m0 + 1) * (m0 + 2)) / 2 ∧ 0 ≤ n

Rule argument

Additional information

Used terms: (n * (n + 1)) / 2

Proof step 21 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof max-def (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 23:

  m0 ≠ n, m < ((m0 + 1) * (m0 + 2)) / 2, m < ((n + 1) * (n + 2)) / 2, m0 < n, (m0 * (m0 + 1)) / 2 ≤ m, (n * (n + 1)) / 2 ≤ m, ¬ (m0 * (m0 + 1)) / 2 ≤ (n * (n + 1)) / 2, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m * (n + 1) = m * n + m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ (m + 2) / 2 = m / 2 + 1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 0 ≤ m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ls-02: n ≠ 0 ⊦ m / n < m0 / n → m < m0; (forward) from specification nat-div let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m / 2 = 0 ↔ m = 0 ∨ m = 1; (s) ⊦ m * m + m ≠ 1; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ ¬ n < n; (s)

Proof step 23 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ m ≤ n ↔ ¬ n < m

• Proof step 25:

  m0 ≠ n, (n * (n + 1)) / 2 < (m0 * (m0 + 1)) / 2, m0 < n, m < ((n + 1) * (n + 2)) / 2, m < ((m0 + 1) * (m0 + 2)) / 2, (n * (n + 1)) / 2 ≤ m, (m0 * (m0 + 1)) / 2 ≤ m, ∀ m2, m3, n. m2 - m3 < m - m0 → maxenc(m3, m2) ≠ n ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (n * (n + 1)) / 2 ≤ m2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → false ⊦

Rule argument

Additional information

Used terms: (n * (n + 1)) / 2, (m0 * (m0 + 1)) / 2

Proof step 24 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof max-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ (m * (m + 1)) / 2 < (n * (n + 1)) / 2 ↔ m < n

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → ¬ n < m; (s) Used terms: m0, n

Proof step 26 from proof max-def (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof max-def (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m * (n + 1) = m * n + m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ (m + 2) / 2 = m / 2 + 1; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ ¬ n < n; (s) ⊦ (m + n) / 2 < n ↔ m < n; (s) ⊦ m0 * m < m ↔ m0 = 0 ∧ m ≠ 0; (ws) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ¬ n + (m - n) < m; (s) Used terms: m, m0 + 1, n