Proof step 1 from proof modby6-help (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 6 * (i + 1) * (i + 1) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Proof step 2 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 4:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 6 * ((i + 1) * i + (i + 1) * 1) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: 1, i, i + 1

Proof step 3 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 6 * ((i + 1) * i + i + 1) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: 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 ⊦ 1 * i = i; (s)

Proof step 5 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 6 * ((i * i + 1 * i) + i + 1) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: i, 1, i

Proof step 6 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 6 * (2 * i + i * i + 1) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i + i = 2 * i; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s)

Proof step 8 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 10:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ (6 * 2 * i + 6 * (i * i + 1)) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: i * i + 1, 2 * i, 6

Proof step 9 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 12 * i + 6 * (i * i + 1) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 11 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 13:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 12 * i + (6 * i * i + 6 * 1) + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: 1, i * i, 6

Proof step 12 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  (i + 1) * (2 + i) * (2 * (i + 1) + 1) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: 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

Proof step 14 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 16:

  (i + 1) * (2 + i) * ((2 * i + 2 * 1) + 1) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: 1, i, 2

Proof step 15 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  (i + 1) * (2 + i) * (3 + 2 * i) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: associativity: ⊦ i * j * j0 = (i * j) * j0; 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 commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 17 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 19:

  (i + 1) * ((2 + i) * 3 + (2 + i) * 2 * i) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: 2 * i, 3, 2 + i

Proof step 18 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 21:

  (i + 1) * ((3 * 2 + 3 * i) + (2 + i) * 2 * i) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 3, i, 2

Proof step 20 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  (i + 1) * (6 + 3 * i + (2 + i) * 2 * i) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: 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

Proof step 22 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  (i + 1) * (6 + 3 * i + 2 * 2 * i + i * 2 * i) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: 2 * i, i, 2

Proof step 23 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  (i + 1) * (i * 7 + 6 + i * 2 * i) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; 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 * (* i) + i0 * (* j) = i0 * (i + j); (s)

Proof step 25 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  i * (i * 7 + 6 + i * 2 * i) + 1 * (i * 7 + 6 + i * 2 * i) ≠ 12 * i + 6 * i * i + 6 + i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: i * 7 + 6 + i * 2 * i, 1, i

Proof step 26 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ~4 * i * i + ~5 * i + i * (i * 7 + 6 + i * 2 * i) ≠ i * (i + 1) * (2 * i + 1) ⊦

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 ⊦ i + j = i + i0 ↔ j = i0; (s) ⊦ (* i2) * i + j = (* i1) * i + j0 ↔ (i2 - i1) * i + j = j0; (s) ⊦ 1 * i = i; (s)

Proof step 28 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 30:

  ~4 * i * i + ~5 * i + i * i * 7 + i * (6 + i * 2 * i) ≠ i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: 6 + i * 2 * i, i * 7, i

Proof step 29 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  (i * i) * 3 + ~5 * i + i * (6 + i * 2 * i) ≠ i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; 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 * (* i) + i0 * (* j) = i0 * (i + j); (s)

Proof step 31 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 33:

  (i * i) * 3 + ~5 * i + i * 6 + i * i * 2 * i ≠ i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

Used terms: i * 2 * i, 6, i

Proof step 32 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  i + (i * i) * 3 + i * i * 2 * i ≠ i * (i + 1) * (2 * i + 1) ⊦

Rule argument

Additional information

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

Proof step 34 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ i * (j + j0) = i * j + i * j0

• Proof step 36:

  i + (i * i) * 3 + i * i * 2 * i ≠ i * ((i + 1) * 2 * i + (i + 1) * 1) ⊦

Rule argument

Additional information

Used terms: 1, 2 * i, i + 1

Proof step 35 from proof modby6-help (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof modby6-help (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  i + (i * i) * 3 + i * i * 2 * i ≠ i * ((i + 1) * 2 * i + i + 1) ⊦

Rule argument

Additional information

Used simplifier rules: 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 ⊦ 1 * i = i; (s)

Proof step 37 from proof modby6-help (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

Rule argument

Additional information

Used simplifier rules: ⊦ (* i0) * i + i = (i0 + 1) * i; (s) ⊦ (i + j) * i0 = j0 + j * i0 ↔ i * i0 = j0; (s) ⊦ 1 * i = i; (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 terms: 2 * i, 1, i

Proof step 38 from proof modby6-help (previous step) (back to tree)

A spec-lemma