Proof step 1 from proof euler-four-square-identity (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j1 ^2 + j2 ^2 + j3 ^2 + j4 ^2) ≠ (i1 * j1 - i2 * j2 - i3 * j3 - i4 * j4)^2 + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (((i1 * j3 - i2 * j4) + i3 * j1) + i4 * j2)^2 + ((i1 * j4 + i2 * j3 - i3 * j2) + i4 * j1)^2 ⊦

Rule argument

Additional information

Proof step 2 from proof euler-four-square-identity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j1 ^2 + j2 ^2 + j3 ^2 + j4 ^2) ≠ (i1 * j1 - (i2 * j2 + i3 * j3) + i4 * j4)^2 + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 ⊦

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 + (j - i0) = i + j - i0; (s) ⊦ i - j - i0 = i - j + i0; (s)

Proof step 3 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) ≠ (i1 * j1 - (i2 * j2 + i3 * j3) + i4 * j4)^2 + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 ⊦

Rule argument

Additional information

Used terms: j2 ^2 + j3 ^2 + j4 ^2, j1 ^2, i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2

Proof step 4 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof euler-four-square-identity (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:

  (i1 ^2 * j1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j1 ^2) + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) ≠ (i1 * j1 - (i2 * j2 + i3 * j3) + i4 * j4)^2 + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 ⊦

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 Used terms: j1 ^2, i2 ^2 + i3 ^2 + i4 ^2, i1 ^2

Proof step 6 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  (i1 ^2 * j1 ^2 + i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2) + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) ≠ (i1 * j1 - (i2 * j2 + i3 * j3) + i4 * j4)^2 + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 ⊦

Rule argument

Additional information

Used terms: j1 ^2, i3 ^2 + i4 ^2, i2 ^2

Proof step 8 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ (i - j)^2 = (i ^2 - 2 * i * j) + j ^2

• Proof step 11:

  (i1 ^2 * j1 ^2 + i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2) + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) ≠ (((i1 * j1)^2 - 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4)) + ((i2 * j2 + i3 * j3) + i4 * j4)^2) + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 ⊦

Rule argument

Additional information

Used terms: (i2 * j2 + i3 * j3) + i4 * j4, i1 * j1

Proof step 10 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-minus

Proof step 11 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 13:

  (i1 ^2 * j1 ^2 + i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2) + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) ≠ ((i1 ^2 * j1 ^2 - 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4)) + ((i2 * j2 + i3 * j3) + i4 * j4)^2) + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 ⊦

Rule argument

Additional information

Used terms: j1, i1

Proof step 12 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 13 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 14:

  (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + ((i2 * j2 + i3 * j3) + i4 * j4)^2 ≠ i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) ⊦

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 = i + i0 ↔ j = i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i + (j - i0) = i + j - i0; (s)

Proof step 14 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ (i - j)^2 = (i ^2 - 2 * i * j) + j ^2

• Proof step 16:

  (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + ((((i1 * j2 + i2 * j1) + i3 * j4)^2 - 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3) + (i4 * j3)^2) + ((i2 * j2 + i3 * j3) + i4 * j4)^2 ≠ i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) ⊦

Rule argument

Additional information

Used terms: i4 * j3, (i1 * j2 + i2 * j1) + i3 * j4

Proof step 15 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-minus

Proof step 16 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 18:

  (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (((i1 * j2 + i2 * j1)^2 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 - 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3) + (i4 * j3)^2) + ((i2 * j2 + i3 * j3) + i4 * j4)^2 ≠ i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) ⊦

Rule argument

Additional information

Used terms: i3 * j4, i1 * j2 + i2 * j1

Proof step 17 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 18 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 20:

  (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + ( ( ((i1 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + (i2 * j1)^2) + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 - 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3) + (i4 * j3)^2) + ((i2 * j2 + i3 * j3) + i4 * j4)^2 ≠ i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) ⊦

Rule argument

Additional information

Used terms: i2 * j1, i1 * j2

Proof step 19 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 20 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 22:

  (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + ( ( ((i1 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + i2 ^2 * j1 ^2) + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 - 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3) + (i4 * j3)^2) + ((i2 * j2 + i3 * j3) + i4 * j4)^2 ≠ i2 ^2 * j1 ^2 + (i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) ⊦

Rule argument

Additional information

Used terms: j1, i2

Proof step 21 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 22 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i1 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i + (j - i0) = i + j - i0; (s)

Proof step 23 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i1 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (i1 ^2 * (j2 ^2 + j3 ^2 + j4 ^2) + (i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2)) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j2 ^2 + j3 ^2 + j4 ^2, i2 ^2 + i3 ^2 + i4 ^2, i1 ^2

Proof step 24 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof euler-four-square-identity (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:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + (i1 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + ((j2 ^2 * i1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2) + (i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2)) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 Used terms: i1 ^2, j3 ^2 + j4 ^2, j2 ^2

Proof step 26 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 29:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + i1 ^2 * j2 ^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + ((j2 ^2 * i1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2) + (i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2)) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j2, i1

Proof step 28 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 29 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 30:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * (j2 ^2 + j3 ^2 + j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 30 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + ((i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * (j3 ^2 + j4 ^2)) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j3 ^2 + j4 ^2, j2 ^2, i2 ^2 + i3 ^2 + i4 ^2

Proof step 31 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

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

• Proof step 34:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + ((i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j3 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j4 ^2, j3 ^2, i2 ^2 + i3 ^2 + i4 ^2

Proof step 33 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

• Proof step 36:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + ((i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + (i2 ^2 * j3 ^2 + (i3 ^2 + i4 ^2) * j3 ^2) + (i2 ^2 + i3 ^2 + i4 ^2) * j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 Used terms: j3 ^2, i3 ^2 + i4 ^2, i2 ^2

Proof step 35 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

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

• Proof step 38:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j3)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + ((i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + (i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i4 ^2 * j3 ^2) + (i2 ^2 + i3 ^2 + i4 ^2) * j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j3 ^2, i4 ^2, i3 ^2

Proof step 37 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 40:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + i4 ^2 * j3 ^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + ((i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + (i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i4 ^2 * j3 ^2) + (i2 ^2 + i3 ^2 + i4 ^2) * j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j3, i4

Proof step 39 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 40 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 41:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s)

Proof step 41 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

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

• Proof step 43:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + (i2 ^2 * j4 ^2 + (i3 ^2 + i4 ^2) * j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 Used terms: j4 ^2, i3 ^2 + i4 ^2, i2 ^2

Proof step 42 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i3 * j4)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + (i2 ^2 * j4 ^2 + i3 ^2 * j4 ^2 + i4 ^2 * j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j4 ^2, i4 ^2, i3 ^2

Proof step 44 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 47:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + i3 ^2 * j4 ^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + (i2 ^2 * j4 ^2 + i3 ^2 * j4 ^2 + i4 ^2 * j4 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j4, i3

Proof step 46 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 47 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 48:

  ((i2 * j2 + i3 * j3) + i4 * j4)^2 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + i4 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s)

Proof step 48 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 50:

  ((i2 * j2 + i3 * j3)^2 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j4)^2) + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + i4 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: i4 * j4, i2 * j2 + i3 * j3

Proof step 49 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 50 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 52:

  ((i2 * j2 + i3 * j3)^2 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + i4 ^2 * j4 ^2) + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + i4 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j4, i4

Proof step 51 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 52 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 53:

  (i2 * j2 + i3 * j3)^2 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s)

Proof step 53 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 55:

  ((i2 * j2)^2 + 2 * (i2 * j2) * i3 * j3 + (i3 * j3)^2) + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: i3 * j3, i2 * j2

Proof step 54 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 55 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 57:

  ((i2 * j2)^2 + 2 * (i2 * j2) * i3 * j3 + i3 ^2 * j3 ^2) + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i3 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j3, i3

Proof step 56 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 57 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 58:

  (i2 * j2)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 + i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s)

Proof step 58 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

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

• Proof step 60:

  (i2 * j2)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 * j2 ^2 + (i3 ^2 + i4 ^2) * j2 ^2) + i2 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j2 ^2, i3 ^2 + i4 ^2, i2 ^2

Proof step 59 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 60 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 61:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 62:

  i2 ^2 * j2 ^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i2 ^2 * j2 ^2 + (i3 ^2 + i4 ^2) * j2 ^2) + i2 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j2, i2

Proof step 61 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 62 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 63:

  2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i4 * j2 + i3 * j1 + i1 * j3 - i2 * j4)^2 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s)

Proof step 63 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

  ⊦ (i - j)^2 = (i ^2 - 2 * i * j) + j ^2

• Proof step 65:

  2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (((i4 * j2 + i3 * j1 + i1 * j3)^2 - 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4) + (i2 * j4)^2) + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: i2 * j4, i4 * j2 + i3 * j1 + i1 * j3

Proof step 64 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-minus

Proof step 65 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 67:

  2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (((i4 * j2 + i3 * j1 + i1 * j3)^2 - 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4) + i2 ^2 * j4 ^2) + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + i2 ^2 * j4 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: j4, i2

Proof step 66 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 67 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 68:

  2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i1 * j2) * i2 * j1 + (i4 * j1 + i1 * j4 + i2 * j3 - i3 * j2)^2 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + (i4 * j2 + i3 * j1 + i1 * j3)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 ⊦

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 = i + i0 ↔ j = i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i + (j - i0) = i + j - i0; (s)

Proof step 68 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ (i - j)^2 = (i ^2 - 2 * i * j) + j ^2

• Proof step 70:

  2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i1 * j2) * i2 * j1 + (((i4 * j1 + i1 * j4 + i2 * j3)^2 - 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2) + (i3 * j2)^2) + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + (i4 * j2 + i3 * j1 + i1 * j3)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 ⊦

Rule argument

Additional information

Used terms: i3 * j2, i4 * j1 + i1 * j4 + i2 * j3

Proof step 69 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-minus

Proof step 70 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 72:

  2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i1 * j2) * i2 * j1 + (((i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + (i1 * j4 + i2 * j3)^2 - 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2) + (i3 * j2)^2) + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + (i4 * j2 + i3 * j1 + i1 * j3)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 ⊦

Rule argument

Additional information

Used terms: i1 * j4 + i2 * j3, i4 * j1

Proof step 71 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 72 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 73:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 74:

  2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i1 * j2) * i2 * j1 + ( ( (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + (i1 * j4)^2 + 2 * (i1 * j4) * i2 * j3 + (i2 * j3)^2 - 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2) + (i3 * j2)^2) + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + (i4 * j2 + i3 * j1 + i1 * j3)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 ⊦

Rule argument

Additional information

Used terms: i2 * j3, i1 * j4

Proof step 73 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 74 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 76:

  2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i1 * j2) * i2 * j1 + ( ( (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + (i1 * j4)^2 + 2 * (i1 * j4) * i2 * j3 + i2 ^2 * j3 ^2 - 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2) + (i3 * j2)^2) + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + (i4 * j2 + i3 * j1 + i1 * j3)^2 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + i2 ^2 * j3 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 ⊦

Rule argument

Additional information

Used terms: j3, i2

Proof step 75 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 76 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 77:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + (i1 * j4)^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 + i4 ^2) * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

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 = i + i0 ↔ j = i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i + (j - i0) = i + j - i0; (s)

Proof step 77 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

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

• Proof step 79:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + (i3 * j2)^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + (i1 * j4)^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 * j2 ^2 + i4 ^2 * j2 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j2 ^2, i4 ^2, i3 ^2

Proof step 78 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 79 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 80:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 81:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + i3 ^2 * j2 ^2 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + (i1 * j4)^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + (i3 ^2 * j2 ^2 + i4 ^2 * j2 ^2) + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j2, i3

Proof step 80 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 81 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 82:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + (i1 * j4)^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

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 = i + i0 ↔ j = i0; (s)

Proof step 82 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 83:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 84:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + i1 ^2 * j4 ^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 + j4 ^2) * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j4, i1

Proof step 83 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 84 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

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

• Proof step 86:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + i1 ^2 * j4 ^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 + i4 ^2) * j1 ^2 + (j3 ^2 * i1 ^2 + j4 ^2 * i1 ^2) + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i1 ^2, j4 ^2, j3 ^2

Proof step 85 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 86 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

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

• Proof step 88:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + (i4 * j1)^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + i1 ^2 * j4 ^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 * j1 ^2 + i4 ^2 * j1 ^2) + (j3 ^2 * i1 ^2 + j4 ^2 * i1 ^2) + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j1 ^2, i4 ^2, i3 ^2

Proof step 87 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 88 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 90:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + i4 ^2 * j1 ^2 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + i1 ^2 * j4 ^2 + 2 * (i1 * j4) * i2 * j3 ≠ (i3 ^2 * j1 ^2 + i4 ^2 * j1 ^2) + (j3 ^2 * i1 ^2 + j4 ^2 * i1 ^2) + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j1, i4

Proof step 89 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 90 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 91:

  (i4 * j2 + i3 * j1 + i1 * j3)^2 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ i3 ^2 * j1 ^2 + j3 ^2 * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 91 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 92:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 93:

  ((i4 * j2)^2 + 2 * (i4 * j2) * (i3 * j1 + i1 * j3) + (i3 * j1 + i1 * j3)^2) + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ i3 ^2 * j1 ^2 + j3 ^2 * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i3 * j1 + i1 * j3, i4 * j2

Proof step 92 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 93 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 95:

  (i4 ^2 * j2 ^2 + 2 * (i4 * j2) * (i3 * j1 + i1 * j3) + (i3 * j1 + i1 * j3)^2) + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ i3 ^2 * j1 ^2 + j3 ^2 * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j2, i4

Proof step 94 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 95 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 96:

  ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2

• Proof step 97:

  (i4 ^2 * j2 ^2 + 2 * (i4 * j2) * (i3 * j1 + i1 * j3) + (i3 * j1)^2 + 2 * (i3 * j1) * i1 * j3 + (i1 * j3)^2) + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ i3 ^2 * j1 ^2 + j3 ^2 * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i1 * j3, i3 * j1

Proof step 96 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-plus

Proof step 97 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 99:

  (i4 ^2 * j2 ^2 + 2 * (i4 * j2) * (i3 * j1 + i1 * j3) + i3 ^2 * j1 ^2 + 2 * (i3 * j1) * i1 * j3 + (i1 * j3)^2) + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ i3 ^2 * j1 ^2 + j3 ^2 * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j1, i3

Proof step 98 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 99 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

  ⊦ (i * j)^2 = i ^2 * j ^2

• Proof step 101:

  (i4 ^2 * j2 ^2 + 2 * (i4 * j2) * (i3 * j1 + i1 * j3) + i3 ^2 * j1 ^2 + 2 * (i3 * j1) * i1 * j3 + i1 ^2 * j3 ^2) + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ i3 ^2 * j1 ^2 + j3 ^2 * i1 ^2 + i4 ^2 * j2 ^2 + 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: j3, i1

Proof step 100 from proof euler-four-square-identity (previous step) (back to tree)

Lemma two-mult

Proof step 101 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 102:

  2 * (i4 * j2) * (i3 * j1 + i1 * j3) + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2 + i3 * j1 + i1 * j3) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 102 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 103:

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

• Proof step 104:

  2 * (i4 * j2) * (i3 * j1 + i1 * j3) + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * ((i4 * j2) * i2 * j4 + (i3 * j1 + i1 * j3) * i2 * j4) + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i2 * j4, i3 * j1 + i1 * j3, i4 * j2

Proof step 103 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 104 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 105:

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

• Proof step 106:

  2 * (i4 * j2) * (i3 * j1 + i1 * j3) + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + (2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1 + i1 * j3) * i2 * j4) + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: (i3 * j1 + i1 * j3) * i2 * j4, (i4 * j2) * i2 * j4, 2

Proof step 105 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 106 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 107:

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

• Proof step 108:

  2 * (i4 * j2) * (i3 * j1 + i1 * j3) + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + (2 * (i4 * j2) * i2 * j4 + 2 * ((i3 * j1) * i2 * j4 + (i1 * j3) * i2 * j4)) + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i2 * j4, i1 * j3, i3 * j1

Proof step 107 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 108 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 109:

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

• Proof step 110:

  2 * (i4 * j2) * (i3 * j1 + i1 * j3) + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + (2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j3) * i2 * j4) + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: (i1 * j3) * i2 * j4, (i3 * j1) * i2 * j4, 2

Proof step 109 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 110 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 111:

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

• Proof step 112:

  2 * ((i4 * j2) * i3 * j1 + (i4 * j2) * i1 * j3) + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + (2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j3) * i2 * j4) + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i1 * j3, i3 * j1, i4 * j2

Proof step 111 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 112 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 113:

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

• Proof step 114:

  (2 * (i4 * j2) * i3 * j1 + 2 * (i4 * j2) * i1 * j3) + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) + 2 * (i1 * j4) * i2 * j3 ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + (2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j3) * i2 * j4) + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: (i4 * j2) * i1 * j3, (i4 * j2) * i3 * j1, 2

Proof step 113 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 114 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 115:

  2 * (i4 * j2) * i3 * j1 + 2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i4 * j1 + i1 * j4 + i2 * j3) * i3 * j2 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult

Proof step 115 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 116:

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

• Proof step 117:

  2 * (i4 * j2) * i3 * j1 + 2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * ((i4 * j1) * i3 * j2 + (i1 * j4 + i2 * j3) * i3 * j2) ⊦

Rule argument

Additional information

Used terms: i3 * j2, i1 * j4 + i2 * j3, i4 * j1

Proof step 116 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 117 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 118:

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

• Proof step 119:

  2 * (i4 * j2) * i3 * j1 + 2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i4 * j1) * i3 * j2 + 2 * (i1 * j4 + i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: (i1 * j4 + i2 * j3) * i3 * j2, (i4 * j1) * i3 * j2, 2

Proof step 118 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 119 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 120:

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

• Proof step 121:

  2 * (i4 * j2) * i3 * j1 + 2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i4 * j1) * i3 * j2 + 2 * ((i1 * j4) * i3 * j2 + (i2 * j3) * i3 * j2) ⊦

Rule argument

Additional information

Used terms: i3 * j2, i2 * j3, i1 * j4

Proof step 120 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 121 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 122:

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

• Proof step 123:

  2 * (i4 * j2) * i3 * j1 + 2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2) * i3 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i4 * j1) * i3 * j2 + 2 * (i1 * j4) * i3 * j2 + 2 * (i2 * j3) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: (i2 * j3) * i3 * j2, (i1 * j4) * i3 * j2, 2

Proof step 122 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 123 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 124:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i2 * j2 + i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j4) * i3 * j2 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult

Proof step 124 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 125:

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

• Proof step 126:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * ((i2 * j2) * i4 * j4 + (i3 * j3) * i4 * j4) + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j4) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i4 * j4, i3 * j3, i2 * j2

Proof step 125 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 126 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 127:

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

• Proof step 128:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + (2 * (i2 * j2) * i4 * j4 + 2 * (i3 * j3) * i4 * j4) + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i4 * j2) * i2 * j4 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j4) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: (i3 * j3) * i4 * j4, (i2 * j2) * i4 * j4, 2

Proof step 127 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 128 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 129:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i1 * j2 + i2 * j1) * i3 * j4 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j4) * i3 * j2 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult

Proof step 129 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 130:

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

• Proof step 131:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * ((i1 * j2) * i3 * j4 + (i2 * j1) * i3 * j4) + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j4) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: i3 * j4, i2 * j1, i1 * j2

Proof step 130 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 131 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 132:

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

• Proof step 133:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + (2 * (i1 * j2) * i3 * j4 + 2 * (i2 * j1) * i3 * j4) + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 + 2 * (i3 * j1) * i2 * j4 + 2 * (i1 * j4) * i3 * j2 ⊦

Rule argument

Additional information

Used terms: (i2 * j1) * i3 * j4, (i1 * j2) * i3 * j4, 2

Proof step 132 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 133 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 134:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * ((i2 * j2 + i3 * j3) + i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult

Proof step 134 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 135:

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

• Proof step 136:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * ((i1 * j1) * (i2 * j2 + i3 * j3) + (i1 * j1) * i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: i4 * j4, i2 * j2 + i3 * j3, i1 * j1

Proof step 135 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 136 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 137:

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

• Proof step 138:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ (2 * (i1 * j1) * (i2 * j2 + i3 * j3) + 2 * (i1 * j1) * i4 * j4) + 2 * ((i1 * j2 + i2 * j1) + i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: (i1 * j1) * i4 * j4, (i1 * j1) * (i2 * j2 + i3 * j3), 2

Proof step 137 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 138 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 139:

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

• Proof step 140:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ (2 * (i1 * j1) * (i2 * j2 + i3 * j3) + 2 * (i1 * j1) * i4 * j4) + 2 * ((i1 * j2 + i2 * j1) * i4 * j3 + (i3 * j4) * i4 * j3) ⊦

Rule argument

Additional information

Used terms: i4 * j3, i3 * j4, i1 * j2 + i2 * j1

Proof step 139 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 140 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 141:

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

• Proof step 142:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i3 * j3) * i4 * j4 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ (2 * (i1 * j1) * (i2 * j2 + i3 * j3) + 2 * (i1 * j1) * i4 * j4) + 2 * (i1 * j2 + i2 * j1) * i4 * j3 + 2 * (i3 * j4) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: (i3 * j4) * i4 * j3, (i1 * j2 + i2 * j1) * i4 * j3, 2

Proof step 141 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 142 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And obtained the following new goals

• Proof step 143:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * (i1 * j4 + i2 * j3) ≠ 2 * (i1 * j1) * (i2 * j2 + i3 * j3) + 2 * (i1 * j1) * i4 * j4 + 2 * (i1 * j2 + i2 * j1) * i4 * j3 ⊦

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 = i + i0 ↔ j = i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult

Proof step 143 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 144:

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

• Proof step 145:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i1 * j2) * i2 * j1 + 2 * ((i4 * j1) * i1 * j4 + (i4 * j1) * i2 * j3) ≠ 2 * (i1 * j1) * (i2 * j2 + i3 * j3) + 2 * (i1 * j1) * i4 * j4 + 2 * (i1 * j2 + i2 * j1) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: i2 * j3, i1 * j4, i4 * j1

Proof step 144 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 145 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 146:

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

• Proof step 147:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * i1 * j4 + 2 * (i4 * j1) * i2 * j3 ≠ 2 * (i1 * j1) * (i2 * j2 + i3 * j3) + 2 * (i1 * j1) * i4 * j4 + 2 * (i1 * j2 + i2 * j1) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: (i4 * j1) * i2 * j3, (i4 * j1) * i1 * j4, 2

Proof step 146 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 147 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 148:

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

• Proof step 149:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * i1 * j4 + 2 * (i4 * j1) * i2 * j3 ≠ 2 * ((i1 * j1) * i2 * j2 + (i1 * j1) * i3 * j3) + 2 * (i1 * j1) * i4 * j4 + 2 * (i1 * j2 + i2 * j1) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: i3 * j3, i2 * j2, i1 * j1

Proof step 148 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 149 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 150:

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

• Proof step 151:

  2 * (i4 * j2) * i1 * j3 + 2 * (i3 * j1) * i1 * j3 + 2 * (i1 * j2) * i2 * j1 + 2 * (i4 * j1) * i1 * j4 + 2 * (i4 * j1) * i2 * j3 ≠ (2 * (i1 * j1) * i2 * j2 + 2 * (i1 * j1) * i3 * j3) + 2 * (i1 * j1) * i4 * j4 + 2 * (i1 * j2 + i2 * j1) * i4 * j3 ⊦

Rule argument

Additional information

Used terms: (i1 * j1) * i3 * j3, (i1 * j1) * i2 * j2, 2

Proof step 150 from proof euler-four-square-identity (previous step) (back to tree)

A spec-lemma

Proof step 151 from proof euler-four-square-identity (previous step) (back to tree)

User applied rule simplifier

And closed the goal!

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