Proof step 1 from proof euler-four-square-identity2 (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-identity2 (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 + (i4 * j3 + i1 * j2 - i2 * j1 + i3 * j4).^2 + (i1 * j3 + i2 * j4 - i3 * j1 + i4 * j2).^2 + (i3 * j2 + i1 * j4 - i2 * j3 + i4 * j1).^2 ⊦

Rule argument

Additional information

Used simplifier rules: add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i - j - i0 = i - j + i0; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i + (j - i0) = i + j - i0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  (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 + (i4 * j3 + i1 * j2 - i2 * j1 + i3 * j4).^2 + (i1 * j3 + i2 * j4 - i3 * j1 + i4 * j2).^2 + ((i3 * j2 + i1 * j4).^2 - 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1)) + (i2 * j3 + i4 * j1).^2 ⊦

Rule argument

Additional information

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

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

Lemma two-minus

Proof step 5 from proof euler-four-square-identity2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

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

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

Lemma two-minus

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

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

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

Rule argument

Additional information

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

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

Lemma two-minus

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

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

Rule argument

Additional information

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

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

A spec-lemma

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

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

Rule argument

Additional information

Used terms: j2.^2 + j3.^2 + j4.^2, j1.^2, i1.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

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

Rule argument

Additional information

Used terms: j3.^2 + j4.^2, j2.^2, i1.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

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

Rule argument

Additional information

Used terms: j2.^2 + j3.^2 + j4.^2, j1.^2, i2.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

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

Rule argument

Additional information

Used terms: j3.^2 + j4.^2, j2.^2, i2.^2

Proof step 25 from proof euler-four-square-identity2 (previous step) (back to tree)

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

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

Rule argument

Additional information

Used terms: j4.^2, j3.^2, i2.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 32:

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

Rule argument

Additional information

Used terms: j2, i1, j3, i4

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

Lemma two-pm

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (i2 * j3 + i4 * j1).^2 + (i3 * j1 + i4 * j2).^2 + (i2 * j1 + i3 * j4).^2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i3 * j2 + i1 * j4).^2 + (i1 * j3 + i2 * j4).^2 ≠ i1.^2 * j1.^2 + i1.^2 * j3.^2 + i1.^2 * j4.^2 + i2.^2 * j1.^2 + i2.^2 * j2.^2 + i2.^2 * j3.^2 + i2.^2 * j4.^2 + i3.^2 * (j1.^2 + j2.^2 + j3.^2 + j4.^2) + i4.^2 * (j1.^2 + j2.^2 + j3.^2 + j4.^2) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * 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 33 from proof euler-four-square-identity2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

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

Rule argument

Additional information

Used terms: j2.^2 + j3.^2 + j4.^2, j1.^2, i4.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

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

Rule argument

Additional information

Used terms: j3.^2 + j4.^2, j2.^2, i4.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

• Proof step 39:

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

Rule argument

Additional information

Used terms: j4.^2, j3.^2, i4.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

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

• Proof step 41:

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

Rule argument

Additional information

Used terms: j2.^2 + j3.^2 + j4.^2, j1.^2, i3.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

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

• Proof step 43:

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

Rule argument

Additional information

Used terms: j3.^2 + j4.^2, j2.^2, i3.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

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

Rule argument

Additional information

Used terms: j4.^2, j3.^2, i3.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 47:

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

Rule argument

Additional information

Used terms: j4, i1, j2, i3

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

Lemma two-pm

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 49:

  2 * i3 * j2 * i1 * j4 + i1.^2 * j4.^2 + (i3 * j1 + i4 * j2).^2 + (i2 * j1 + i3 * j4).^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 ≠ 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j2.^2 + i4.^2 * j1.^2 + i3.^2 * j4.^2 + i3.^2 * j3.^2 + i3.^2 * j1.^2 + i2.^2 * j4.^2 + i2.^2 * j3.^2 + i2.^2 * j2.^2 + i2.^2 * j1.^2 + i1.^2 * j4.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^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: 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j2.^2 + i4.^2 * j1.^2 + i3.^2 * j4.^2 + i3.^2 * j3.^2 + i3.^2 * j1.^2 + i2.^2 * j4.^2 + i2.^2 * j3.^2 + i2.^2 * j2.^2 + i2.^2 * j1.^2 + i1.^2 * j4.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^2, 2 * i3 * j2 * i1 * j4 + i1.^2 * j4.^2 + (i3 * j1 + i4 * j2).^2 + (i2 * j1 + i3 * j4).^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2, i3.^2 * j2.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

  ⊦ i + j = j + i

• Proof step 51:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 53:

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

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: i1.^2 * j1.^2 + i1.^2 * j3.^2 + i2.^2 * j1.^2 + i2.^2 * j2.^2 + i2.^2 * j3.^2 + i2.^2 * j4.^2 + i3.^2 * j1.^2 + i3.^2 * j3.^2 + i3.^2 * j4.^2 + i4.^2 * j1.^2 + i4.^2 * j2.^2 + i4.^2 * j3.^2 + i4.^2 * j4.^2 + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2), (i3 * j1 + i4 * j2).^2 + (i2 * j1 + i3 * j4).^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4, i1.^2 * j4.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 55:

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

Rule argument

Additional information

Used terms: j2, i4, j1, i3

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

Lemma two-pm

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 57:

  2 * i3 * j1 * i4 * j2 + i4.^2 * j2.^2 + (i2 * j1 + i3 * j4).^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 ≠ 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j2.^2 + i4.^2 * j1.^2 + i3.^2 * j4.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j3.^2 + i2.^2 * j2.^2 + i2.^2 * j1.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^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: 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j2.^2 + i4.^2 * j1.^2 + i3.^2 * j4.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j3.^2 + i2.^2 * j2.^2 + i2.^2 * j1.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^2, 2 * i3 * j1 * i4 * j2 + i4.^2 * j2.^2 + (i2 * j1 + i3 * j4).^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4, i3.^2 * j1.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ i + j = j + i

• Proof step 59:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 61:

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

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: i1.^2 * j1.^2 + i1.^2 * j3.^2 + i2.^2 * j1.^2 + i2.^2 * j2.^2 + i2.^2 * j3.^2 + i2.^2 * j4.^2 + i3.^2 * j3.^2 + i3.^2 * j4.^2 + i4.^2 * j1.^2 + i4.^2 * j3.^2 + i4.^2 * j4.^2 + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2), (i2 * j1 + i3 * j4).^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2, i4.^2 * j2.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 63:

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

Rule argument

Additional information

Used terms: j4, i3, j1, i2

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

Lemma two-pm

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 65:

  2 * i2 * j1 * i3 * j4 + i3.^2 * j4.^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 ≠ 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j1.^2 + i3.^2 * j4.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j3.^2 + i2.^2 * j2.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^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: 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j1.^2 + i3.^2 * j4.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j3.^2 + i2.^2 * j2.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^2, 2 * i2 * j1 * i3 * j4 + i3.^2 * j4.^2 + (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2, i2.^2 * j1.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

  ⊦ i + j = j + i

• Proof step 67:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 69:

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

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: i1.^2 * j1.^2 + i1.^2 * j3.^2 + i2.^2 * j2.^2 + i2.^2 * j3.^2 + i2.^2 * j4.^2 + i3.^2 * j3.^2 + i4.^2 * j1.^2 + i4.^2 * j3.^2 + i4.^2 * j4.^2 + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2), (i2 * j3 + i4 * j1).^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j1 * i3 * j4, i3.^2 * j4.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 70:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 71:

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

Rule argument

Additional information

Used terms: j1, i4, j3, i2

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

Lemma two-pm

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 73:

  2 * i2 * j3 * i4 * j1 + i4.^2 * j1.^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j1 * i3 * j4 ≠ 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j1.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j2.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^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: 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i4.^2 * j3.^2 + i4.^2 * j1.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j2.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^2, 2 * i2 * j3 * i4 * j1 + i4.^2 * j1.^2 + i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j1 * i3 * j4, i2.^2 * j3.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ⊦ i + j = j + i

• Proof step 75:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 77:

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

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: i1.^2 * j1.^2 + i1.^2 * j3.^2 + i2.^2 * j2.^2 + i2.^2 * j4.^2 + i3.^2 * j3.^2 + i4.^2 * j3.^2 + i4.^2 * j4.^2 + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2), i4.^2 * j3.^2 + 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j1 * i3 * j4 + 2 * i2 * j3 * i4 * j1, i4.^2 * j1.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

  ⊦ i + j = i + i0 ↔ j = i0

• Proof step 79:

  2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j1 * i3 * j4 + 2 * i2 * j3 * i4 * j1 ≠ 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j2.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^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: 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i3.^2 * j3.^2 + i2.^2 * j4.^2 + i2.^2 * j2.^2 + i1.^2 * j3.^2 + i1.^2 * j1.^2, 2 * i4 * j3 * i1 * j2 + (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4).^2 + (i1 * j3 + i2 * j4).^2 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j1 * i3 * j4 + 2 * i2 * j3 * i4 * j1, i4.^2 * j3.^2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 80:

  ⊦ i + j = j + i

• Proof step 81:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 83:

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

Rule argument

Additional information

Used terms: j4, i2, j3, i1

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

Lemma two-pm

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

User applied rule simplifier

And obtained the following new goals

• Proof step 84:

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

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 84 from proof euler-four-square-identity2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

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

• Proof step 86:

  ((i1 * j1 + i2 * j2) + i3 * j3 + i4 * j4).^2 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j1 * i3 * j4 + 2 * i2 * j3 * i4 * j1 + 2 * i4 * j3 * i1 * j2 ≠ 2 * (i1 * j3 + i2 * j4) * (i3 * j1 + i4 * j2) + 2 * (i4 * j3 + i1 * j2) * (i2 * j1 + i3 * j4) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) + i4.^2 * j4.^2 + i3.^2 * j3.^2 + i2.^2 * j2.^2 + i1.^2 * j1.^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: i3 * j3 + i4 * j4, i2 * j2, i1 * j1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

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

• Proof step 88:

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

Rule argument

Additional information

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

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

Lemma two-plus

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 90:

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

Rule argument

Additional information

Used terms: j2, i2, j1, i1

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

Lemma two-pm

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

  ⊦ (i * i0 + j * j0).^2 = i.^2 * i0.^2 + 2 * i * i0 * j * j0 + j.^2 * j0.^2

• Proof step 92:

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

Rule argument

Additional information

Used terms: j4, i4, j3, i3

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

Lemma two-pm

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

User applied rule simplifier

And obtained the following new goals

• Proof step 93:

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

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 93 from proof euler-four-square-identity2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

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

• Proof step 95:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 96:

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

• Proof step 97:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

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

• Proof step 99:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

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

• Proof step 101:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 102:

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

• Proof step 103:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 104:

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

• Proof step 105:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule simplifier

And obtained the following new goals

• Proof step 106:

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

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 106 from proof euler-four-square-identity2 (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 * i1 * j1 * i2 * j2 + 2 * (i1 * j1 + i2 * j2) * (i3 * j3 + i4 * j4) + 2 * i3 * j3 * i4 * j4 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j3 * i4 * j1 ≠ 2 * (i1 * j3) * i3 * j1 + 2 * (i2 * j4) * i4 * j2 + 2 * ((i4 * j3) * (i2 * j1 + i3 * j4) + (i1 * j2) * (i2 * j1 + i3 * j4)) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

Proof step 108 from proof euler-four-square-identity2 (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 * i1 * j1 * i2 * j2 + 2 * (i1 * j1 + i2 * j2) * (i3 * j3 + i4 * j4) + 2 * i3 * j3 * i4 * j4 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j3 * i4 * j1 ≠ 2 * (i1 * j3) * i3 * j1 + 2 * (i2 * j4) * i4 * j2 + (2 * (i4 * j3) * (i2 * j1 + i3 * j4) + 2 * (i1 * j2) * (i2 * j1 + i3 * j4)) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

Proof step 110 from proof euler-four-square-identity2 (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 * i1 * j1 * i2 * j2 + 2 * (i1 * j1 + i2 * j2) * (i3 * j3 + i4 * j4) + 2 * i3 * j3 * i4 * j4 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j3 * i4 * j1 ≠ 2 * (i1 * j3) * i3 * j1 + 2 * (i2 * j4) * i4 * j2 + (2 * ((i4 * j3) * i2 * j1 + (i4 * j3) * i3 * j4) + 2 * (i1 * j2) * (i2 * j1 + i3 * j4)) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

Proof step 112 from proof euler-four-square-identity2 (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 * i1 * j1 * i2 * j2 + 2 * (i1 * j1 + i2 * j2) * (i3 * j3 + i4 * j4) + 2 * i3 * j3 * i4 * j4 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j2 * i1 * j4 + 2 * i3 * j1 * i4 * j2 + 2 * i2 * j3 * i4 * j1 ≠ 2 * (i1 * j3) * i3 * j1 + 2 * (i2 * j4) * i4 * j2 + (2 * ((i4 * j3) * i2 * j1 + (i4 * j3) * i3 * j4) + 2 * ((i1 * j2) * i2 * j1 + (i1 * j2) * i3 * j4)) + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 115:

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

• Proof step 116:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 117:

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

• Proof step 118:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule simplifier

And obtained the following new goals

• Proof step 119:

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

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 119 from proof euler-four-square-identity2 (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 * ((i1 * j1) * (i3 * j3 + i4 * j4) + (i2 * j2) * (i3 * j3 + i4 * j4)) + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j1 * i4 * j2 ≠ 2 * (i1 * j3) * i3 * j1 + 2 * (i2 * j4) * i4 * j2 + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

Proof step 121 from proof euler-four-square-identity2 (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 * (i1 * j1) * (i3 * j3 + i4 * j4) + 2 * (i2 * j2) * (i3 * j3 + i4 * j4)) + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j1 * i4 * j2 ≠ 2 * (i1 * j3) * i3 * j1 + 2 * (i2 * j4) * i4 * j2 + 2 * (i3 * j2 + i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 124:

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

• Proof step 125:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 126:

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

• Proof step 127:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 128:

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

• Proof step 129:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 130:

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

• Proof step 131:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule simplifier

And obtained the following new goals

• Proof step 132:

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

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 132 from proof euler-four-square-identity2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 133:

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

• Proof step 134:

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

Rule argument

Additional information

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

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

A spec-lemma

Proof step 134 from proof euler-four-square-identity2 (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 * (i1 * j1) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j1 * i4 * j2 ≠ 2 * (i3 * j2) * (i2 * j3 + i4 * j1) + 2 * (i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

Proof step 136 from proof euler-four-square-identity2 (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 * (i1 * j1) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j1 * i4 * j2 ≠ 2 * ((i3 * j2) * i2 * j3 + (i3 * j2) * i4 * j1) + 2 * (i1 * j4) * (i2 * j3 + i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 139:

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

• Proof step 140:

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

Rule argument

Additional information

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

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

A spec-lemma

Proof step 140 from proof euler-four-square-identity2 (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 * (i1 * j1) * i4 * j4 + 2 * (i2 * j2) * i3 * j3 + 2 * i1 * j3 * i2 * j4 + 2 * i3 * j1 * i4 * j2 ≠ (2 * (i3 * j2) * i2 * j3 + 2 * (i3 * j2) * i4 * j1) + 2 * ((i1 * j4) * i2 * j3 + (i1 * j4) * i4 * j1) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 143:

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

• Proof step 144:

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

Rule argument

Additional information

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

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

A spec-lemma

Proof step 144 from proof euler-four-square-identity2 (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