Proof step 1 from proof pot2-est-div6 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  2 ^ (i / 6) ≤ i + 1, 36 ≤ i ⊦

Rule argument

Additional information

Proof step 2 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  0 < i, 36 ≤ i, 2 ^ (i / 6) ≤ i + 1, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs

Proof step 3 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  i = i0 * 6 + j0, 0 < i, j0 < 6, 0 < 6, 0 ≤ i, 2 ^ i0 ≤ i + 1, 36 ≤ i, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 0 < j ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j ∧ 0 ≤ i0); (elim) Used terms: i, 6, i0, j0

Proof step 4 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  0 < i0 * 6 + j0, j0 < 6, 2 ^ i0 ≤ (i0 * 6 + j0) + 1, 36 ≤ i0 * 6 + j0, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs

Proof step 5 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  j0 < 6, 0 < i0 * 6 + j0, 0 ≤ i0, 0 ≤ j0, 36 ≤ i0 * 6 + j0, 2 ^ i0 ≤ (i0 * 6 + j0) + 1, 2 ^ i0 ≤ (i0 + 1) * 6 ⊦

• Proof step 49:

  j0 < 6, 0 < i0 * 6 + j0, 0 ≤ i0, 0 ≤ j0, 36 ≤ i0 * 6 + j0, 2 ^ i0 ≤ (i0 * 6 + j0) + 1, ¬ 2 ^ i0 ≤ (i0 + 1) * 6 ⊦

Rule argument

Additional information

Used formulas: 2 ^ i0 ≤ (i0 + 1) * 6

Proof step 6 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 8:

  0 < i0 * 6 + j0, j0 < 6, 0 < i0, 2 ^ i0 -1 * 2 ≤ (i0 + 1) * 6, 2 ^ i0 -1 * 2 ≤ (i0 * 6 + j0) + 1, 36 ≤ i0 * 6 + j0, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ 1 ≤ i ↔ 0 < i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i + 0 = i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs Used terms: i0, 2

Proof step 7 from proof pot2-est-div6 (previous step) (back to tree)

Lemma Pot-pos

Proof step 8 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  j0 < 6, 0 < i0 * 6 + j0, 0 < i0, 0 ≤ i0, 0 ≤ j0, 36 ≤ i0 * 6 + j0, 2 ^ (i0 - 1) * 2 ≤ (i0 * 6 + j0) + 1, 2 ^ (i0 - 1) ≤ 3 * (i0 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult 0 < i, i < j, j % i = 0 ⊦ (* i) * i0 ≤ (* j) * j0 ↔ i0 ≤ j / i * j0; (s) ⊦ i -1 = i - 1; (s)

Proof step 9 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  i0 = i1 + 1, 0 < i0, 0 < i0 * 6 + j0, j0 < 6, 2 ^ i1 ≤ 3 * (i0 + 1), 2 ^ i1 * 2 ≤ (i0 * 6 + j0) + 1, 36 ≤ i0 * 6 + j0, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i0, 1, i

Proof step 10 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  0 < (i1 + 1) * 6 + j0, j0 < 6, 0 ≤ i1, 2 ^ i1 ≤ 3 * (2 + i1), 2 ^ i1 * 2 ≤ ((i1 + 1) * 6 + j0) + 1, 36 ≤ (i1 + 1) * 6 + j0, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ 0 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s)

Proof step 11 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 13:

  j0 < 6, 0 < (i1 + 1) * 6 + j0, 0 < i1, 0 ≤ j0, 36 ≤ (i1 + 1) * 6 + j0, (2 ^ i1 -1 * 2) * 2 ≤ ((i1 + 1) * 6 + j0) + 1, 2 ^ i1 -1 * 2 ≤ 3 * (2 + i1), 0 ≤ i1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs Used terms: i1, 2

Proof step 12 from proof pot2-est-div6 (previous step) (back to tree)

Lemma Pot-pos

Proof step 13 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  0 < (i1 + 1) * 6 + j0, j0 < 6, 0 < i1, 36 ≤ (i1 + 1) * 6 + j0, 0 ≤ j0, 0 ≤ i1, 2 ^ (i1 - 1) * 2 ≤ 3 * (2 + i1), (2 ^ (i1 - 1) * 2) * 2 ≤ ((i1 + 1) * 6 + j0) + 1 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i -1 = i - 1; (s)

Proof step 14 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  i1 = i0 + 1, 0 < i1, j0 < 6, 0 < (i1 + 1) * 6 + j0, (2 ^ i0 * 2) * 2 ≤ ((i1 + 1) * 6 + j0) + 1, 2 ^ i0 * 2 ≤ 3 * (2 + i1), 0 ≤ i1, 0 ≤ j0, 36 ≤ (i1 + 1) * 6 + j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i1, 1, i0

Proof step 15 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  0 < (2 + i0) * 6 + j0, j0 < 6, 0 ≤ i0, 4 * 2 ^ i0 ≤ (2 + i0) * 6 + j0 + 1, 2 ^ i0 * 2 ≤ 3 * (3 + i0), 0 ≤ j0, 36 ≤ (2 + i0) * 6 + j0 ⊦

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ 0 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s)

Proof step 16 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 18:

  j0 < 6, 0 < (2 + i0) * 6 + j0, 0 < i0, 36 ≤ (2 + i0) * 6 + j0, 0 ≤ j0, (2 ^ i0 -1 * 2) * 2 ≤ 3 * (3 + i0), 4 * 2 ^ i0 -1 * 2 ≤ (2 + i0) * 6 + j0 + 1, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs Used terms: i0, 2

Proof step 17 from proof pot2-est-div6 (previous step) (back to tree)

Lemma Pot-pos

Proof step 18 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  0 < (2 + i0) * 6 + j0, j0 < 6, 0 < i0, 0 ≤ j0, 36 ≤ (2 + i0) * 6 + j0, 0 ≤ i0, 4 * 2 ^ (i0 - 1) * 2 ≤ (2 + i0) * 6 + j0 + 1, (2 ^ (i0 - 1) * 2) * 2 ≤ 3 * (3 + i0) ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i -1 = i - 1; (s)

Proof step 19 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  i0 = i1 + 1, 0 < i0, j0 < 6, 0 < (2 + i0) * 6 + j0, (2 ^ i1 * 2) * 2 ≤ 3 * (3 + i0), 4 * 2 ^ i1 * 2 ≤ (2 + i0) * 6 + j0 + 1, 0 ≤ i0, 36 ≤ (2 + i0) * 6 + j0, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i0, 1, i

Proof step 20 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  0 < (3 + i1) * 6 + j0, j0 < 6, 0 ≤ i1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ 0 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s)

Proof step 21 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 22:

  j0 < 6, 0 < (3 + i1) * 6 + j0, 0 ≤ j0, 36 ≤ (3 + i1) * 6 + j0, 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 0 ≤ i1, 1 + 6 * (3 + i1) + j0 ≤ 1 + 6 * (3 + i1) + 5 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i * j + i = i * (j + 1); (s) ⊦ i * (j + i0) + j1 ≤ i * (j0 + i0) ↔ i * j + j1 ≤ i * j0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) i + 1 = i0 ⊦ j < (* i0) → ¬ (* i) < j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used formulas: 1 + 6 * (3 + i1) + j0 ≤ 1 + 6 * (3 + i1) + 5

Proof step 22 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 23:

  1 + 6 * (3 + i1) + 5 = 6 * i1 + 24, 0 < (3 + i1) * 6 + j0, j0 < 6, 1 + 6 * (3 + i1) + j0 ≤ 1 + 6 * (3 + i1) + 5, 0 ≤ i1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i * j + i = i * (j + 1); (s) ⊦ (i + j) * i0 = j0 + j * i0 ↔ i * i0 = j0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: 1 + 6 * (3 + i1) + 5 = 6 * i1 + 24

Proof step 23 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 24:

  j0 < 6, 0 < (3 + i1) * 6 + j0, 0 ≤ j0, 36 ≤ (3 + i1) * 6 + j0, 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 0 ≤ i1, 1 + 6 * (3 + i1) + j0 ≤ 6 * i1 + 24 ⊦

Rule argument

Additional information

Proof step 24 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 25:

  6 * i1 + 24 = 6 * (i1 + 4), 0 < (3 + i1) * 6 + j0, j0 < 6, 1 + 6 * (3 + i1) + j0 ≤ 6 * i1 + 24, 0 ≤ i1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (i + j) * i0 = j0 + j * i0 ↔ i * i0 = j0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used formulas: 6 * i1 + 24 = 6 * (i1 + 4)

Proof step 25 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 26:

  j0 < 6, 0 < (3 + i1) * 6 + j0, 0 ≤ j0, 36 ≤ (3 + i1) * 6 + j0, 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 0 ≤ i1, 1 + 6 * (3 + i1) + j0 ≤ 6 * (i1 + 4) ⊦

Rule argument

Additional information

Proof step 26 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 27:

  0 < (3 + i1) * 6 + j0, j0 < 6, 1 + 6 * (3 + i1) + j0 ≤ 6 * (i1 + 4), 0 ≤ i1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0, 8 * 2 ^ i1 ≤ 6 * (i1 + 4) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i * (j + i0) + j1 ≤ i * (j0 + i0) ↔ i * j + j1 ≤ i * j0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i * (j + i0) < i * (j0 + i0) + j1 ↔ i * j < i * j0 + j1; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i ≤ j → ¬ j < i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: 8 * 2 ^ i1 ≤ 6 * (i1 + 4)

Proof step 27 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 28:

  j0 < 6, 0 < (3 + i1) * 6 + j0, 6 * (i1 + 4) < 8 * (i1 + 4), 8 * 2 ^ i1 ≤ 6 * (i1 + 4), 0 ≤ j0, 36 ≤ (3 + i1) * 6 + j0, 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 0 ≤ i1, 1 + 6 * (3 + i1) + j0 ≤ 6 * (i1 + 4) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i * (j + i0) + j1 ≤ i * (j0 + i0) ↔ i * j + j1 ≤ i * j0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ (* i1) * j < (* i2) * j ↔ 0 < (i2 - i1) * j; (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: 6 * (i1 + 4) < 8 * (i1 + 4)

Proof step 28 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 29:

  6 * (i1 + 4) < 8 * (i1 + 4), 0 < (3 + i1) * 6 + j0, j0 < 6, 8 * 2 ^ i1 < 8 * (i1 + 4), 1 + 6 * (3 + i1) + j0 ≤ 6 * (i1 + 4), 0 ≤ i1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0, 8 * 2 ^ i1 ≤ 6 * (i1 + 4) ⊦

• Proof step 47:

  6 * (i1 + 4) < 8 * (i1 + 4), 0 < (3 + i1) * 6 + j0, j0 < 6, 1 + 6 * (3 + i1) + j0 ≤ 6 * (i1 + 4), 0 ≤ i1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0, 8 * 2 ^ i1 ≤ 6 * (i1 + 4), ¬ 8 * 2 ^ i1 < 8 * (i1 + 4) ⊦

Rule argument

Additional information

Used formulas: 8 * 2 ^ i1 < 8 * (i1 + 4)

Proof step 29 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ 0 < i → (i * j < i * j0 ↔ j < j0)

• Proof step 31:

  2 ^ i1 < i1 + 4, j0 < 6, 0 < (3 + i1) * 6 + j0, 6 * (i1 + 4) < 8 * (i1 + 4), 0 < 8, 8 * 2 ^ i1 ≤ 6 * (i1 + 4), 0 ≤ j0, 36 ≤ (3 + i1) * 6 + j0, 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 0 ≤ i1, 1 + 6 * (3 + i1) + j0 ≤ 6 * (i1 + 4) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i * (j + i0) + j1 ≤ i * (j0 + i0) ↔ i * j + j1 ≤ i * j0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ (* i1) * j < (* i2) * j ↔ 0 < (i2 - i1) * j; (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i1 + 4, 2 ^ i1, 8

Proof step 30 from proof pot2-est-div6 (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  0 < (3 + i1) * 6 + j0, 2 ^ i1 < i1 + 4, 0 ≤ i1, 4 * 2 ^ i1 ≤ 3 * (4 + i1), 8 * 2 ^ i1 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0, 8 * 2 ^ i1 ≤ 6 * (i1 + 4), j0 ≤ 5 ⊦

Rule argument

Additional information

Used simplifier rules: j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ (* i1) * j < (* i2) * j ↔ 0 < (i2 - i1) * j; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i * (j + i0) + j1 ≤ i * (j0 + i0) ↔ i * j + j1 ≤ i * j0; (s)

Proof step 32 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 34:

  2 ^ i1 -1 * 2 < i1 + 4, 0 < (3 + i1) * 6 + j0, 0 < i1, j0 ≤ 5, 8 * 2 ^ i1 -1 * 2 ≤ 6 * (i1 + 4), 0 ≤ j0, 36 ≤ (3 + i1) * 6 + j0, 8 * 2 ^ i1 -1 * 2 ≤ (3 + i1) * 6 + j0 + 1, 4 * 2 ^ i1 -1 * 2 ≤ 3 * (4 + i1), 0 ≤ i1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs Used terms: i1, 2

Proof step 33 from proof pot2-est-div6 (previous step) (back to tree)

Lemma Pot-pos

Proof step 34 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  0 < (3 + i1) * 6 + j0, 2 ^ (i1 - 1) * 2 < i1 + 4, 0 < i1, 0 ≤ i1, 4 * 2 ^ (i1 - 1) * 2 ≤ 3 * (4 + i1), 8 * 2 ^ (i1 - 1) * 2 ≤ (3 + i1) * 6 + j0 + 1, 36 ≤ (3 + i1) * 6 + j0, 0 ≤ j0, 8 * 2 ^ (i1 - 1) * 2 ≤ 6 * (i1 + 4), j0 ≤ 5 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i -1 = i - 1; (s)

Proof step 35 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 36:

  i1 = i0 + 1, 0 < i1, 2 ^ i0 * 2 < i1 + 4, 0 < (3 + i1) * 6 + j0, j0 ≤ 5, 8 * 2 ^ i0 * 2 ≤ 6 * (i1 + 4), 0 ≤ j0, 36 ≤ (3 + i1) * 6 + j0, 8 * 2 ^ i0 * 2 ≤ (3 + i1) * 6 + j0 + 1, 4 * 2 ^ i0 * 2 ≤ 3 * (4 + i1), 0 ≤ i1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i1, 1, i0

Proof step 36 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  2 ^ i0 * 2 < 5 + i0, 0 < (4 + i0) * 6 + j0, 4 * 2 ^ i0 * 2 ≤ 3 * (5 + i0), 8 * 2 ^ i0 * 2 ≤ (4 + i0) * 6 + j0 + 1, 36 ≤ (4 + i0) * 6 + j0, 0 ≤ j0, 8 * 2 ^ i0 * 2 ≤ 6 * (5 + i0), j0 ≤ 5, 0 ≤ (4 + i0) * 6 + j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s)

Proof step 37 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 39:

  0 < (4 + i0) * 6 + j0, (2 ^ i0 -1 * 2) * 2 < 5 + i0, 0 < i0, 0 ≤ i0, 0 ≤ (4 + i0) * 6 + j0, j0 ≤ 5, 8 * (2 ^ i0 -1 * 2) * 2 ≤ 6 * (5 + i0), 0 ≤ j0, 36 ≤ (4 + i0) * 6 + j0, 8 * (2 ^ i0 -1 * 2) * 2 ≤ (4 + i0) * 6 + j0 + 1, 4 * (2 ^ i0 -1 * 2) * 2 ≤ 3 * (5 + i0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs Used terms: i0, 2

Proof step 38 from proof pot2-est-div6 (previous step) (back to tree)

Lemma Pot-pos

Proof step 39 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  0 < (4 + i0) * 6 + j0, (2 ^ (i0 - 1) * 2) * 2 < 5 + i0, 0 < i0, 4 * (2 ^ (i0 - 1) * 2) * 2 ≤ 3 * (5 + i0), 8 * (2 ^ (i0 - 1) * 2) * 2 ≤ (4 + i0) * 6 + j0 + 1, 36 ≤ (4 + i0) * 6 + j0, 0 ≤ j0, 8 * (2 ^ (i0 - 1) * 2) * 2 ≤ 6 * (5 + i0), j0 ≤ 5, 0 ≤ (4 + i0) * 6 + j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i -1 = i - 1; (s)

Proof step 40 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 41:

  i0 = i1 + 1, 0 < i0, (2 ^ i1 * 2) * 2 < 5 + i0, 0 < (4 + i0) * 6 + j0, 0 ≤ i0, 0 ≤ (4 + i0) * 6 + j0, j0 ≤ 5, 8 * (2 ^ i1 * 2) * 2 ≤ 6 * (5 + i0), 0 ≤ j0, 36 ≤ (4 + i0) * 6 + j0, 8 * (2 ^ i1 * 2) * 2 ≤ (4 + i0) * 6 + j0 + 1, 4 * (2 ^ i1 * 2) * 2 ≤ 3 * (5 + i0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i0, 1, i

Proof step 41 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  (2 ^ i1 * 2) * 2 < 6 + i1, 0 < (5 + i1) * 6 + j0, 4 * (2 ^ i1 * 2) * 2 ≤ 3 * (6 + i1), 8 * (2 ^ i1 * 2) * 2 ≤ (5 + i1) * 6 + j0 + 1, 36 ≤ (5 + i1) * 6 + j0, 0 ≤ j0, 8 * (2 ^ i1 * 2) * 2 ≤ 6 * (6 + i1), j0 ≤ 5, 0 ≤ (5 + i1) * 6 + j0, 0 ≤ i1 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s)

Proof step 42 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 44:

  0 < (5 + i1) * 6 + j0, ((2 ^ i1 -1 * 2) * 2) * 2 < 6 + i1, 0 < i1, 0 ≤ i1, 0 ≤ (5 + i1) * 6 + j0, j0 ≤ 5, 8 * ((2 ^ i1 -1 * 2) * 2) * 2 ≤ 6 * (6 + i1), 0 ≤ j0, 36 ≤ (5 + i1) * 6 + j0, 8 * ((2 ^ i1 -1 * 2) * 2) * 2 ≤ (5 + i1) * 6 + j0 + 1, 4 * ((2 ^ i1 -1 * 2) * 2) * 2 ≤ 3 * (6 + i1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ 1 ≤ i ↔ 0 < i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs Used terms: i1, 2

Proof step 43 from proof pot2-est-div6 (previous step) (back to tree)

Lemma Pot-pos

Proof step 44 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  0 < (5 + i1) * 6 + j0, ((2 ^ (i1 - 1) * 2) * 2) * 2 < 6 + i1, 0 < i1, 4 * ((2 ^ (i1 - 1) * 2) * 2) * 2 ≤ 3 * (6 + i1), 8 * ((2 ^ (i1 - 1) * 2) * 2) * 2 ≤ (5 + i1) * 6 + j0 + 1, 36 ≤ (5 + i1) * 6 + j0, 0 ≤ j0, 8 * ((2 ^ (i1 - 1) * 2) * 2) * 2 ≤ 6 * (6 + i1), j0 ≤ 5, 0 ≤ (5 + i1) * 6 + j0, 0 ≤ i1 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i -1 = i - 1; (s)

Proof step 45 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 46:

  i1 = i0 + 1, 0 < i1, ((2 ^ i0 * 2) * 2) * 2 < 6 + i1, 0 < (5 + i1) * 6 + j0, 0 ≤ i1, 0 ≤ (5 + i1) * 6 + j0, j0 ≤ 5, 8 * ((2 ^ i0 * 2) * 2) * 2 ≤ 6 * (6 + i1), 0 ≤ j0, 36 ≤ (5 + i1) * 6 + j0, 8 * ((2 ^ i0 * 2) * 2) * 2 ≤ (5 + i1) * 6 + j0 + 1, 4 * ((2 ^ i0 * 2) * 2) * 2 ≤ 3 * (6 + i1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i1, 1, i0

Proof step 46 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: pot2-est-mult8: ⊦ 0 ≤ i → ¬ 8 * 2 ^ i < i + 7; commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s)

Proof step 47 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  ⊦ i ≤ j ∧ j < j0 → i < j0

Rule argument

Additional information

Used simplifier rules: ⊦ i * (j + i0) + j1 ≤ i * (j0 + i0) ↔ i * j + j1 ≤ i * j0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ (* i1) * j < (* i2) * j ↔ 0 < (i2 - i1) * j; (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 6 * (i1 + 4), 8 * (i1 + 4), 8 * 2 ^ i1

Proof step 48 from proof pot2-est-div6 (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof pot2-est-div6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  (i0 + 1) * 6 < 2 ^ i0, j0 < 6, 0 < i0 * 6 + j0, 0 ≤ i0, 0 ≤ j0, 36 ≤ i0 * 6 + j0, 2 ^ i0 ≤ (i0 * 6 + j0) + 1, (i0 + 1) * 6 ≤ i0 * 6 + j0 ⊦

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i < j + 1 ↔ i ≤ j; (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 50 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 51:

  0 < i0 * 6 + j0, j0 < 6, (i0 + 1) * 6 < 2 ^ i0, (i0 + 1) * 6 ≤ i0 * 6 + j0, 2 ^ i0 ≤ (i0 * 6 + j0) + 1, 36 ≤ i0 * 6 + j0, 0 ≤ j0, 0 ≤ i0, ¬ (i0 * 6 + j0) + 1 ≤ i0 * 6 + 6 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i * j + i = i * (j + 1); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i + 1 ≤ j ↔ i < j; (s) ⊦ i ≤ j → ¬ j < i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used formulas: (i0 * 6 + j0) + 1 ≤ i0 * 6 + 6

Proof step 51 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ i + j + i0 = (i + j) + i0

• Proof step 53:

  (i0 + 1) * 6 < 2 ^ i0, j0 < 6, 0 < i0 * 6 + j0, 0 ≤ i0, 0 ≤ j0, 36 ≤ i0 * 6 + j0, 2 ^ i0 ≤ i0 * 6 + j0 + 1, (i0 + 1) * 6 ≤ i0 * 6 + j0, ¬ i0 * 6 + j0 + 1 ≤ i0 * 6 + 6 ⊦

Rule argument

Additional information

Used terms: 1, j0, i0 * 6

Proof step 52 from proof pot2-est-div6 (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ i + j = j + i

• Proof step 55:

  0 < i0 * 6 + j0, j0 < 6, (i0 + 1) * 6 < 2 ^ i0, (i0 + 1) * 6 ≤ i0 * 6 + j0, 2 ^ i0 ≤ (j0 + 1) + i0 * 6, 36 ≤ i0 * 6 + j0, 0 ≤ j0, 0 ≤ i0, ¬ (j0 + 1) + i0 * 6 ≤ i0 * 6 + 6 ⊦

Rule argument

Additional information

Used terms: j0 + 1, i0 * 6

Proof step 54 from proof pot2-est-div6 (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ i + j = j + i

• Proof step 57:

  (i0 + 1) * 6 < 2 ^ i0, j0 < 6, 0 < i0 * 6 + j0, 0 ≤ i0, 0 ≤ j0, 36 ≤ i0 * 6 + j0, 2 ^ i0 ≤ (j0 + 1) + i0 * 6, (i0 + 1) * 6 ≤ i0 * 6 + j0, ¬ (j0 + 1) + i0 * 6 ≤ 6 + i0 * 6 ⊦

Rule argument

Additional information

Used terms: 6, i0 * 6

Proof step 56 from proof pot2-est-div6 (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof pot2-est-div6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ i + j ≤ i0 + j ↔ i ≤ i0

Rule argument

Additional information

Used simplifier rules: ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) i + 1 = i0 ⊦ j < (* i0) → ¬ (* i) < j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used terms: 6, i0 * 6, j0 + 1

Proof step 58 from proof pot2-est-div6 (previous step) (back to tree)

A spec-lemma