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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  maxenc(m) < m.2 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  maxenc(m) < m.2 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ m.2 = m - (maxenc(m) * (maxenc(m) + 1)) / 2

• Proof step 5:

  maxenc(m) < m - (maxenc(m) * (maxenc(m) + 1)) / 2 ⊦

Rule argument

Additional information

Used terms: m

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

Lemma dec-snd

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m ⊦

Rule argument

Additional information

Used simplifier rules: max-nls: ⊦ ¬ m < (maxenc(m) * maxenc(m) + maxenc(m)) / 2; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m * (n + 1) = m * n + m; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  ⊦ (maxenc(m) * (maxenc(m) + 1)) / 2 ≤ m ∧ m < ((maxenc(m) + 1) * (maxenc(m) + 2)) / 2

• Proof step 8:

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

Rule argument

Additional information

Used terms: m

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

Lemma max-size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (maxenc(m) + 2) * maxenc(m) + maxenc(m) ≠ 0, maxenc(m) ≠ 0, maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m, maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2, (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ m, m ≤ ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2, (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2 ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws) ⊦ m / 2 = 0 ↔ m = 0 ∨ m = 1; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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 ≤ m; (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ (m + 2) / 2 = m / 2 + 1; (s) ⊦ m * (n + 1) = m * n + m; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ m % 2 = 0 ∧ n % 2 = 0 → (m / 2 ≤ n / 2 ↔ m ≤ n)

• Proof step 11:

  (maxenc(m) * maxenc(m) + maxenc(m)) % 2 = 0, ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) % 2 = 0, (maxenc(m) + 2) * maxenc(m) + maxenc(m) ≠ 0, maxenc(m) ≠ 0, maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2, maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m, maxenc(m) * maxenc(m) + maxenc(m) ≤ (maxenc(m) + 2) * maxenc(m) + maxenc(m), m ≤ ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2, (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (m * m + m) % 2 = 0; (s) ⊦ ((n + 2) * n + n) % 2 = 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: (maxenc(m) + 2) * maxenc(m) + maxenc(m), maxenc(m) * maxenc(m) + maxenc(m)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (maxenc(m) + 2) * maxenc(m) + maxenc(m) ≠ 0, maxenc(m) ≠ 0, maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m, maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2, (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ m, m ≤ ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2 ⊦

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 mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m ≤ m + n; (s) ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ (m * m + m) % 2 = 0; (s) ⊦ ((n + 2) * n + n) % 2 = 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ m % 2 = 0 → (n < m / 2 ↔ n * 2 < m)

• Proof step 14:

  ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) % 2 = 0, (maxenc(m) + 2) * maxenc(m) + maxenc(m) ≠ 0, maxenc(m) ≠ 0, (maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2) * 2 < (maxenc(m) + 2) * maxenc(m) + maxenc(m), maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m, m ≤ ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2, (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ((n + 2) * n + n) % 2 = 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: (maxenc(m) + 2) * maxenc(m) + maxenc(m), maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  maxenc(m) ≠ 0, (maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2) * 2 < (maxenc(m) + 2) * maxenc(m) + maxenc(m), maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m, m ≤ ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2, (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ ((n + 2) * n + n) % 2 = 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ m0 * (m + n) = m0 * m + m0 * n

• Proof step 17:

  maxenc(m) ≠ 0, maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m, 2 * maxenc(m) + 2 * (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < (maxenc(m) + 2) * maxenc(m) + maxenc(m), (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ m, m ≤ ((maxenc(m) + 2) * maxenc(m) + maxenc(m)) / 2 ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: 2, (maxenc(m) * maxenc(m) + maxenc(m)) / 2, maxenc(m)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  maxenc(m) + 2 * (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < (maxenc(m) + 2) * maxenc(m), maxenc(m) + (maxenc(m) * maxenc(m) + maxenc(m)) / 2 < m, (maxenc(m) * maxenc(m) + maxenc(m)) / 2 ≤ m, m * 2 ≤ (maxenc(m) + 2) * maxenc(m) + maxenc(m) ⊦

Rule argument

Additional information

Used simplifier rules: max-zero: ⊦ maxenc(m) = 0 ↔ m = 0; mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m < n → n ≠ 0; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m0 * 1 = m0; (s) m2 ≠ 0 ⊦ (* m2) * m + n < m + n0 ↔ (m2 - 1) * m + n < n0; (s) m0 ≠ 0 ⊦ n ≤ m / m0 ↔ n * m0 ≤ m; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ n % m = 0 ∧ m ≠ 0 → m * n / m = n

Rule argument

Additional information

Used simplifier rules: ⊦ (m * m + m) % 2 = 0; (s) ⊦ m + m = 2 * m; (s) ⊦ m * n + m0 * n < m1 * n ↔ m + m0 < m1 ∧ n ≠ 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ n < n; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: 2, maxenc(m) * maxenc(m) + maxenc(m)

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

A spec-lemma