Proof step 1 from proof divup-half (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (m /↑ 2^ n) /↑ 2 ≠ m /↑ 2^(n + 1) ⊦

Rule argument

Additional information

Proof step 2 from proof divup-half (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ n /↑ 2 = (even(n) ⊃ n / 2;(n + 1) / 2)

• Proof step 4:

  (even(m /↑ 2^ n) ⊃ (m /↑ 2^ n) / 2;(m /↑ 2^ n + 1) / 2) ≠ m /↑ 2^(n + 1) ⊦

Rule argument

Additional information

Used terms: m /↑ 2^ n

Proof step 3 from proof divup-half (previous step) (back to tree)

Lemma divup2-def

Proof step 4 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (even(m /↑ 2^ n) ⊃ (m /↑ 2^ n) / 2;(m /↑ 2^ n + 1) / 2) ≠ m /↑ (2 * 2^ n) ⊦

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 ⊦ 2^(n + 1) = 2 * 2^ n; (s)

Proof step 5 from proof divup-half (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1)

• Proof step 7:

  ⊦ (even((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1)) ⊃ (∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) / 2 ;((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) + 1) / 2 ) = m /↑ (2 * 2^ n)

Rule argument

Additional information

Used terms: m, 2^ n

Proof step 6 from proof divup-half (previous step) (back to tree)

Lemma divup-def

Proof step 7 from proof divup-half (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1)

• Proof step 9:

  ⊦ (even((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1)) ⊃ (∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) / 2 ;((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) + 1) / 2 ) = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

Rule argument

Additional information

Used terms: m, 2 * 2^ n

Proof step 8 from proof divup-half (previous step) (back to tree)

Lemma divup-def

Proof step 9 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  even((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1)) ⊦ (∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

• Proof step 43:

  ⊦ ((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1), even((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1))

Rule argument

Additional information

Proof step 10 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  ∃ n0. m = n0 * 2^ n, even((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1)) ⊦ (m / 2^ n) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

• Proof step 21:

  ∀ n0. m ≠ n0 * 2^ n, even((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1)) ⊦ (m / 2^ n + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

Rule argument

Additional information

Proof step 11 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  even((∃ n1. n0 * 2^ n = n1 * 2^ n ⊃ n0;n0 + 1)) ⊦ n0 / 2 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n0 * 2^ n) / (2 * 2^ n);(n0 * 2^ n) / (2 * 2^ n) + 1)

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 n ≠ 0 ⊦ (m * n) / n = m; (s) ⊦ 2^ n ≠ 0; (s)

Proof step 12 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  n0 = m0 * 2 + n2, 2 ≠ 0, n2 < 2, even((∃ n1. n0 * 2^ n = n1 * 2^ n ⊃ n0;n0 + 1)) ⊦ m0 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n0 * 2^ n) / (2 * 2^ n);(n0 * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n0, 2, m0, n2

Proof step 13 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  n2 < 2, even((∃ n1. (m0 * 2 + n2) * 2^ n = n1 * 2^ n ⊃ m0 * 2 + n2;(m0 * 2 + n2) + 1)) ⊦ m0 = (∃ n1. (m0 * 2 + n2) * 2^ n = n1 * 2 * 2^ n ⊃ ((m0 * 2 + n2) * 2^ n) / (2 * 2^ n);((m0 * 2 + n2) * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

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

Proof step 14 from proof divup-half (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 15:

  n2 = 0, n2 < 2, even((∃ n1. (m0 * 2 + n2) * 2^ n = n1 * 2^ n ⊃ m0 * 2 + n2;(m0 * 2 + n2) + 1)) ⊦ m0 = (∃ n1. (m0 * 2 + n2) * 2^ n = n1 * 2 * 2^ n ⊃ ((m0 * 2 + n2) * 2^ n) / (2 * 2^ n);((m0 * 2 + n2) * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ even(n + 1) ↔ odd(n); (s) ⊦ m * n + n = m1 * n ↔ m + 1 = m1 ∨ n = 0; (s) ⊦ 2^ n ≠ 0; (s) ⊦ m +1 = m + 1; (s) ⊦ m * (n + 1) = m * n + m; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ odd(2 * m); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 15 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  even((∃ n1. (m0 * 2) * 2^ n = n1 * 2^ n ⊃ m0 * 2;1 + m0 * 2)) ⊦ m0 = (∃ n1. (m0 * 2) * 2^ n = n1 * 2 * 2^ n ⊃ m0;m0 + 1)

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 n ≠ 0 ⊦ (m * n) / n = m; (s) ⊦ 2^ n ≠ 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s) 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 16 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 17:

  even(m0 * 2), ∃ n1. (m0 * 2) * 2^ n = n1 * 2^ n ⊦ m0 = (∃ n1. (m0 * 2) * 2^ n = n1 * 2 * 2^ n ⊃ m0;m0 + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ even(n + 1) ↔ odd(n); (s) ⊦ ¬ odd(2 * m); (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

Proof step 17 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (m0 * 2) * 2^ n = n1 * 2^ n ⊦ m0 = (∃ n1. (m0 * 2) * 2^ n = n1 * 2 * 2^ n ⊃ m0;m0 + 1)

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 ⊦ even(2 * m); (s)

Proof step 18 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  (m0 * 2) * 2^ n = n1 * 2^ n, m0 ≠ m0 + 1, ∀ n1. (m0 * 2) * 2^ n ≠ n1 * 2 * 2^ n ⊦

Rule argument

Additional information

Proof step 19 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (m0 * 2) * 2^ n = n1 * 2^ n, ∀ n1. (m0 * 2) * 2^ n ≠ n1 * 2 * 2^ n ⊦

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)

Proof step 20 from proof divup-half (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: m0

Proof step 21 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 22:

  m = m0 * 2^ n + n1, 2^ n ≠ 0, n1 < 2^ n, ∀ n0. m ≠ n0 * 2^ n, even((∃ n0. m = n0 * 2^ n ⊃ m0;m0 + 1)) ⊦ (m0 + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ 2^ n ≠ 0; (s) n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: m, 2^ n, m0, n1

Proof step 22 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  n1 < 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n, even((∃ n0. m0 * 2^ n + n1 = n0 * 2^ n ⊃ m0;m0 + 1)) ⊦ (m0 + 1) / 2 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

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

Proof step 23 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  m0 + 1 = m1 * 2 + n2, 2 ≠ 0, n1 < 2^ n, n2 < 2, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n, even((∃ n0. m0 * 2^ n + n1 = n0 * 2^ n ⊃ m0;m0 + 1)) ⊦ m1 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: m0 + 1, 2, m, n2

Proof step 24 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  m0 + 1 = m1 * 2 + n2, n2 < 2, n1 < 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n, even((∃ n0. m0 * 2^ n + n1 = n0 * 2^ n ⊃ m0;m0 + 1)) ⊦ m1 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

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

Proof step 25 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  m0 + 1 = m1 * 2 + n2, n1 < 2^ n, n2 < 2, even(m0 + 1), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦ m1 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) 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

Proof step 26 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  m0 + 1 = m1 * 2 + n2, n2 < 2, n1 < 2^ n, odd(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦ m1 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

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 ⊦ even(n + 1) ↔ odd(n); (s)

Proof step 27 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 28:

  m0 + 1 = m1 * 2 + n2, m1 ≠ (m0 * 2^ n + n1) / (2 * 2^ n) + 1, n1 < 2^ n, n2 < 2, odd(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) 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

Proof step 28 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 29:

  m0 + 1 = m1 * 2 + n2, m0 * 2^ n + n1 = m2 * 2 * 2^ n + n3, 2 * 2^ n ≠ 0, m1 ≠ m2 + 1, n2 < 2, n1 < 2^ n, n3 < 2 * 2^ n, odd(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2 * 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦

Rule argument

Additional information

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

Proof step 29 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  m0 + 1 = m1 * 2 + n2, m0 * 2^ n + n1 = m2 * 2 * 2^ n + n3, m1 ≠ m2 + 1, n2 < 2, n1 < 2^ n, n3 < 2 * 2^ n, odd(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2 * 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦

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 ⊦ 2^ n ≠ 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 30 from proof divup-half (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 31:

  m0 * 2^ n + n1 = m2 * 2 * 2^ n + n3, m0 + 1 = m1 * 2 + n2, n2 = 0, m1 ≠ m2 + 1, n3 < 2 * 2^ n, n1 < 2^ n, n2 < 2, odd(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ odd(2 * m); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 31 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  m0 * 2^ n + n1 = m2 * 2 * 2^ n + n3, m0 + 1 = m1 * 2, m1 ≠ m2 + 1, n1 < 2^ n, n3 < 2 * 2^ n, odd(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2 * 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦

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 32 from proof divup-half (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 33:

  m0 + 1 = m1 * 2, m0 * 2^ n + n1 = m2 * 2 * 2^ n + n3, m0 = m +1, m1 ≠ m2 + 1, n3 < 2 * 2^ n, n1 < 2^ n, odd(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n, ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ 0 * n = 0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m0 * m = 1 ↔ m0 = 1 ∧ m = 1; (ws) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 33 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  (2^ n * m + 2^ n) + n1 = m2 * 2 * 2^ n + n3, 2 + m = m1 * 2, m1 ≠ m2 + 1, n1 < 2^ n, n3 < 2 * 2^ n, even(m), ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: 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 c: ⊦ m + n = n + m; from specification nat-basic ⊦ m * (n + 1) = m * n + m; (s) ⊦ m +1 = m + 1; (s) ⊦ odd(n + 1) ↔ even(n); (s)

Proof step 34 from proof divup-half (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 35:

  2 + m = m1 * 2, (2^ n * m + 2^ n) + n1 = m2 * 2 * 2^ n + n3, m1 = m0 +1, m1 ≠ m2 + 1, n3 < 2 * 2^ n, n1 < 2^ n, even(m), ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 35 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  (2^ n * 2 * m0 + 2^ n) + n1 = m2 * 2 * 2^ n + n3, m0 ≠ m2, n3 < 2 * 2^ n, n1 < 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2 * 2^ n ⊦

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 ⊦ even(2 * m); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ m * (n + 1) = m * n + m; (s)

Proof step 36 from proof divup-half (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 37:

  (2^ n * 2 * m0 + 2^ n) + n1 = m2 * 2 * 2^ n + n3, (m0 * 2 * 2^ n + 2^ n + n1) / (2 * 2^ n) ≠ (m2 * 2 * 2^ n + n3) / (2 * 2^ n), m0 ≠ m2, n1 < 2^ n, n3 < 2 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ (n0 + m * n) / n = n0 / n + m; (s) ⊦ m < n → m / n = 0; (s) ⊦ n + 0 = n; (s) ⊦ m = m + n ↔ n = 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ 2^ n ≠ 0; (s) m0 ≠ 0 ⊦ n0 / m0 = 0 ↔ n0 < m0; (s) m1 ≠ 0 ⊦ m + n < (* m1) * m ↔ n < (m1 - 1) * m; (s) ⊦ m0 * 1 = m0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (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 formulas: (m0 * 2 * 2^ n + 2^ n + n1) / (2 * 2^ n) = (m2 * 2 * 2^ n + n3) / (2 * 2^ n)

Proof step 37 from proof divup-half (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  n ≠ 0 ⊦ (n0 + m * n) / n = n0 / n + m

• Proof step 39:

  (2^ n * 2 * m0 + 2^ n) + n1 = m2 * 2 * 2^ n + n3, 2^ n * 2 ≠ 0, (n1 + 2^ n) / (2^ n * 2) + m0 ≠ (m2 * 2 * 2^ n + n3) / (2 * 2^ n), m0 ≠ m2, n3 < 2 * 2^ n, n1 < 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ 2^ n ≠ 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: m0, 2^ n * 2, n1 + 2^ n

Proof step 38 from proof divup-half (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof divup-half (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  n ≠ 0 ⊦ (n0 + m * n) / n = n0 / n + m

• Proof step 41:

  (2^ n * 2 * m0 + 2^ n) + n1 = m2 * 2 * 2^ n + n3, 2^ n * 2 ≠ 0, (n1 + 2^ n) / (2^ n * 2) + m0 ≠ n3 / (2^ n * 2) + m2, m0 ≠ m2, n1 < 2^ n, n3 < 2 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2 * 2^ n, ∀ n0. m2 * 2 * 2^ n + n3 ≠ n0 * 2^ n ⊦

Rule argument

Additional information

Used simplifier rules: mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult c: ⊦ m + n = n + m; from specification nat-basic Used terms: m2, 2^ n * 2, n3

Proof step 40 from proof divup-half (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof divup-half (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ m < n → m / n = 0

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n ∧ n1 < n → (m * n + n0 = m0 * n + n1 ↔ m = m0 ∧ n0 = n1); (ws) 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 ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ 2^ n ≠ 0; (s) ⊦ m < n → m / n = 0; (s) ⊦ n + 0 = n; (s) m1 ≠ 0 ⊦ m + n < (* m1) * m ↔ n < (m1 - 1) * m; (s) ⊦ m0 * 1 = m0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: n1 + 2^ n, 2^ n * 2

Proof step 42 from proof divup-half (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  odd((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1)) ⊦ ((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ even(n) ↔ ¬ odd(n); (ss)

Proof step 44 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 45:

  odd(m / 2^ n), ∃ n0. m = n0 * 2^ n ⊦ ((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

• Proof step 55:

  odd(m / 2^ n + 1), ∀ n0. m ≠ n0 * 2^ n ⊦ ((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

Rule argument

Additional information

Proof step 45 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  odd(n0) ⊦ ((∃ n1. n0 * 2^ n = n1 * 2^ n ⊃ n0;n0 + 1) + 1) / 2 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n0 * 2^ n) / (2 * 2^ n);(n0 * 2^ n) / (2 * 2^ n) + 1)

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 n ≠ 0 ⊦ (m * n) / n = m; (s) ⊦ 2^ n ≠ 0; (s)

Proof step 46 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 47:

  odd(n0), ∃ n1. n0 * 2^ n = n1 * 2^ n ⊦ (n0 + 1) / 2 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n0 * 2^ n) / (2 * 2^ n);(n0 * 2^ n) / (2 * 2^ n) + 1)

• Proof step 51:

  odd(n0), ∀ n1. n0 * 2^ n ≠ n1 * 2^ n ⊦ ((n0 + 1) + 1) / 2 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n0 * 2^ n) / (2 * 2^ n);(n0 * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

Proof step 47 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  n0 * 2^ n = n1 * 2^ n, odd(n0) ⊦ n0 / 2 + 1 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n1 * 2^ n) / (2 * 2^ n);(n1 * 2^ n) / (2 * 2^ n) + 1)

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 ⊦ odd(n) → (n + 1) / 2 = n / 2 + 1; (s)

Proof step 48 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 49:

  n0 * 2^ n = n1 * 2^ n, n0 = m0 * 2 + n2, 2 ≠ 0, n2 < 2, odd(n0) ⊦ m0 + 1 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n1 * 2^ n) / (2 * 2^ n);(n1 * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n0, 2, m0, n2

Proof step 49 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  (m0 * 2 + n2) * 2^ n = n1 * 2^ n, n2 < 2, odd(m0 * 2 + n2) ⊦ m0 + 1 = (∃ n1. (m0 * 2 + n2) * 2^ n = n1 * 2 * 2^ n ⊃ (n1 * 2^ n) / (2 * 2^ n);(n1 * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

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

Proof step 50 from proof divup-half (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ odd(n + 1) ↔ even(n); (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m +1 = m + 1; (s) ⊦ m * n + n = m1 * n ↔ m + 1 = m1 ∨ n = 0; (s) ⊦ n + 0 = n; (s) ⊦ even(2 * m); (s) ⊦ 2 * m ≠ 2 * n + 1; (s) ⊦ m * (n + 1) = m * n + m; (s) n ≠ 0 ⊦ (n0 + m * n) / n = n0 / n + m; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws) ⊦ 2 * m = 0 ↔ m = 0; (s) m0 ≠ 0 ⊦ n0 / m0 = 0 ↔ n0 < m0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ 2 * n ≤ n ↔ n = 0; (s) ⊦ 2^ n ≠ 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ ¬ odd(2 * m); (s)

Proof step 51 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  odd(n0), ∀ n1. n0 * 2^ n ≠ n1 * 2^ n ⊦ n0 / 2 + 1 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n0 * 2^ n) / (2 * 2^ n);(n0 * 2^ n) / (2 * 2^ n) + 1)

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 + 2) / 2 = m / 2 + 1; (s)

Proof step 52 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 53:

  n0 = m0 * 2 + n2, 2 ≠ 0, n2 < 2, odd(n0), ∀ n1. n0 * 2^ n ≠ n1 * 2^ n ⊦ m0 + 1 = (∃ n1. n0 * 2^ n = n1 * 2 * 2^ n ⊃ (n0 * 2^ n) / (2 * 2^ n);(n0 * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n0, 2, m0, n2

Proof step 53 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  n2 < 2, odd(m0 * 2 + n2), ∀ n1. (m0 * 2 + n2) * 2^ n ≠ n1 * 2^ n ⊦ m0 + 1 = (∃ n1. (m0 * 2 + n2) * 2^ n = n1 * 2 * 2^ n ⊃ ((m0 * 2 + n2) * 2^ n) / (2 * 2^ n);((m0 * 2 + n2) * 2^ n) / (2 * 2^ n) + 1)

Rule argument

Additional information

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

Proof step 54 from proof divup-half (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m0 * 2 + n2

Proof step 55 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  even(m / 2^ n), ∀ n0. m ≠ n0 * 2^ n ⊦ ((∃ n0. m = n0 * 2^ n ⊃ m / 2^ n;m / 2^ n + 1) + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

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 ⊦ odd(n + 1) ↔ even(n); (s)

Proof step 56 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 57:

  m = m0 * 2^ n + n1, 2^ n ≠ 0, n1 < 2^ n, even(m0), ∀ n0. m ≠ n0 * 2^ n ⊦ ((∃ n0. m = n0 * 2^ n ⊃ m0;m0 + 1) + 1) / 2 = (∃ n0. m = n0 * 2 * 2^ n ⊃ m / (2 * 2^ n);m / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ 2^ n ≠ 0; (s) n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: m, 2^ n, m0, n1

Proof step 57 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  n1 < 2^ n, even(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦ ((∃ n0. m0 * 2^ n + n1 = n0 * 2^ n ⊃ m0;m0 + 1) + 1) / 2 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

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

Proof step 58 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 59:

  n1 < 2^ n, even(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦ ((m0 + 1) + 1) / 2 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) 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

Proof step 59 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  n1 < 2^ n, even(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦ m0 / 2 + 1 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

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 + 2) / 2 = m / 2 + 1; (s)

Proof step 60 from proof divup-half (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 61:

  m0 = m1 * 2 + n2, 2 ≠ 0, n1 < 2^ n, n2 < 2, even(m0), ∀ n0. m0 * 2^ n + n1 ≠ n0 * 2^ n ⊦ m1 + 1 = (∃ n0. m0 * 2^ n + n1 = n0 * 2 * 2^ n ⊃ (m0 * 2^ n + n1) / (2 * 2^ n);(m0 * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: m0, 2, m, n2

Proof step 61 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  n2 < 2, n1 < 2^ n, even(m1 * 2 + n2), ∀ n0. (m1 * 2 + n2) * 2^ n + n1 ≠ n0 * 2^ n ⊦ m1 + 1 = (∃ n0. (m1 * 2 + n2) * 2^ n + n1 = n0 * 2 * 2^ n ⊃ ((m1 * 2 + n2) * 2^ n + n1) / (2 * 2^ n);((m1 * 2 + n2) * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

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

Proof step 62 from proof divup-half (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 63:

  n2 = 0, n1 < 2^ n, n2 < 2, even(m1 * 2 + n2), ∀ n0. (m1 * 2 + n2) * 2^ n + n1 ≠ n0 * 2^ n ⊦ m1 + 1 = (∃ n0. (m1 * 2 + n2) * 2^ n + n1 = n0 * 2 * 2^ n ⊃ ((m1 * 2 + n2) * 2^ n + n1) / (2 * 2^ n);((m1 * 2 + n2) * 2^ n + n1) / (2 * 2^ n) + 1)

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ even(n + 1) ↔ odd(n); (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m +1 = m + 1; (s) ⊦ m * (n + 1) = m * n + m; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ odd(2 * m); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 63 from proof divup-half (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  n1 < 2^ n, ∀ n0. (m1 * 2) * 2^ n + n1 ≠ n0 * 2^ n ⊦ m1 + 1 = (∃ n0. (m1 * 2) * 2^ n + n1 = n0 * 2 * 2^ n ⊃ n1 / (2 * 2^ n) + m1;(n1 / (2 * 2^ n) + m1) + 1)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; 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 ≠ 0 ⊦ (n0 + m * n) / n = n0 / n + m; (s) ⊦ 2^ n ≠ 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ n + 0 = n; (s) ⊦ even(2 * m); (s)

Proof step 64 from proof divup-half (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

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