Proof step 1 from proof two-even (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  2 * i = j1 ^2 + j2 ^2, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

Rule argument

Additional information

Proof step 2 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  2 * i = j1 ^2 + j2 ^2, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

Rule argument

Additional information

Proof step 3 from proof two-even (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  (j1 - j2) % 2 = 0, 2 * i = j1 ^2 + j2 ^2, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

• Proof step 33:

  2 * i = j1 ^2 + j2 ^2, (j1 - j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

Rule argument

Additional information

Used formulas: (j1 - j2) % 2 = 0

Proof step 4 from proof two-even (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 5:

  (j1 - j2) % 2 = 0, (j1 + j2) % 2 = 0, 2 * i = j1 ^2 + j2 ^2, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

• Proof step 28:

  (j1 - j2) % 2 = 0, 2 * i = j1 ^2 + j2 ^2, (j1 + j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

Rule argument

Additional information

Used formulas: (j1 + j2) % 2 = 0

Proof step 5 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  j ≠ 0 ⊦ i % j = 0 ↔ (∃ j0. i = j0 * j)

• Proof step 7:

  (j1 - j2) % 2 = 0, 2 * i = j1 ^2 + j2 ^2, 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2, ∃ j0. j1 + j2 = j0 * 2 ⊦

Rule argument

Additional information

Used terms: 2, j1 + j2

Proof step 6 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (j1 - j2) % 2 = 0, 2 * i = j1 ^2 + j2 ^2, j1 + j2 = j0 * 2, i ≠ ((j1 - j2) / 2)^2 + j0 ^2 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s) j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j; (s)

Proof step 8 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  j ≠ 0 ⊦ i % j = 0 ↔ (∃ j0. i = j0 * j)

• Proof step 10:

  2 * i = j1 ^2 + j2 ^2, j1 + j2 = j0 * 2, 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + j0 ^2, ∃ j0. j1 - j2 = j0 * 2 ⊦

Rule argument

Additional information

Used terms: 2, j1 - j2

Proof step 9 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  2 * i = (j * 2 + j2)^2 + j2 ^2, 2 * j2 + j * 2 = j0 * 2, i ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s) j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j; (s) 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 = j; (s) ⊦ i + i = 2 * i; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 11 from proof two-even (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 + 2 * i * j + j ^2

• Proof step 13:

  2 * i = ((j * 2)^2 + 2 * (j * 2) * j2 + j2 ^2) + j2 ^2, 2 * j2 + j * 2 = j0 * 2, i ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

Used terms: j2, j * 2

Proof step 12 from proof two-even (previous step) (back to tree)

Lemma two-plus

Proof step 13 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  2 * i = 2 * j2 ^2 + (j * 2)^2 + 4 * j * j2, 2 * j2 + j * 2 = j0 * 2, i ≠ j ^2 + j0 ^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 + i = 2 * i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 14 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ i ^2 = i * i

• Proof step 16:

  2 * i = 2 * j2 ^2 + (j * 2) * j * 2 + 4 * j * j2, 2 * j2 + j * 2 = j0 * 2, i ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

Used terms: j * 2

Proof step 15 from proof two-even (previous step) (back to tree)

Lemma Square-def

Proof step 16 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  2 * i = 2 * j2 ^2 + 4 * j * j + 4 * j * j2, 2 * j2 + j * 2 = j0 * 2, i ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

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

Proof step 17 from proof two-even (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 18:

  2 * i = 2 * j2 ^2 + 4 * j * j + 4 * j * j2, 2 * j2 + j * 2 = j0 * 2, 2 * j2 ^2 + 4 * j * j + 4 * j * j2 = 2 * (j2 ^2 + 2 * j * j + 2 * j * j2), i ≠ j ^2 + j0 ^2 ⊦

• Proof step 25:

  2 * i = 2 * j2 ^2 + 4 * j * j + 4 * j * j2, 2 * j2 + j * 2 = j0 * 2, 2 * j2 ^2 + 4 * j * j + 4 * j * j2 ≠ 2 * (j2 ^2 + 2 * j * j + 2 * j * j2), i ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

Used formulas: 2 * j2 ^2 + 4 * j * j + 4 * j * j2 = 2 * (j2 ^2 + 2 * j * j + 2 * j * j2)

Proof step 18 from proof two-even (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 19:

  2 * i = 2 * (j2 ^2 + 2 * j * j + 2 * j * j2), 2 * j2 + j * 2 = j0 * 2, i ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

Proof step 19 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  2 * j2 + j * 2 = j0 * 2, j2 ^2 + 2 * j * j + 2 * j * j2 ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); (s)

Proof step 20 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  2 * (j2 + j) = j0 * 2, j2 ^2 + 2 * j * j + 2 * j * j2 ≠ j ^2 + j0 ^2 ⊦

Rule argument

Additional information

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

Proof step 21 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  j2 ^2 + 2 * j * j + 2 * j * j2 ≠ j ^2 + (j2 + j)^2 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); (s)

Proof step 23 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used simplifier rules: neq: ⊦ j ^2 = j * j ↔ true; ⊦ i + i = 2 * i; (s) ⊦ i + j = i + i0 ↔ j = i0; (s) ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used terms: j, j2

Proof step 24 from proof two-even (previous step) (back to tree)

Lemma two-plus

Proof step 25 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  2 * i = 2 * j2 ^2 + 4 * j * j + 4 * j * j2, 2 * j2 + j * 2 = j0 * 2, (2 * j * j + 2 * j * j2) * 2 ≠ 4 * j * j + 4 * j * j2, i ≠ j ^2 + j0 ^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 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)

Proof step 26 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

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

Proof step 27 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  j ≠ 0 ⊦ i % j = 0 ↔ (∃ j0. i = j0 * j)

• Proof step 30:

  2 * i = j1 ^2 + j2 ^2, (j1 + j2) % 2 ≠ 0, 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2, ∃ j0. j1 - j2 = j0 * 2 ⊦

Rule argument

Additional information

Used terms: 2, j1 - j2

Proof step 29 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  2 * i = (j0 * 2 + j2)^2 + j2 ^2, (2 * j2 + j0 * 2) % 2 ≠ 0, i ≠ j0 ^2 + ((2 * j2 + j0 * 2) / 2)^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 + i = 2 * i; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s) j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j; (s) ⊦ i + j - i = j; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 31 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

Used simplifier rules: ⊦ (i * 2) % 2 = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0, j2, 2

Proof step 32 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof two-even (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 34:

  (j1 + j2) % 2 = 0, 2 * i = j1 ^2 + j2 ^2, (j1 - j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

• Proof step 42:

  2 * i = j1 ^2 + j2 ^2, (j1 + j2) % 2 ≠ 0, (j1 - j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

Rule argument

Additional information

Used formulas: (j1 + j2) % 2 = 0

Proof step 34 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  j ≠ 0 ⊦ i % j = 0 ↔ (∃ j0. i = j0 * j)

• Proof step 36:

  2 * i = j1 ^2 + j2 ^2, (j1 - j2) % 2 ≠ 0, 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2, ∃ j0. j1 + j2 = j0 * 2 ⊦

Rule argument

Additional information

Used terms: 2, j1 + j2

Proof step 35 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  2 * i = j1 ^2 + j2 ^2, j1 + j2 = j0 * 2, (j1 - j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + j0 ^2 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s) j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j; (s)

Proof step 37 from proof two-even (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 38:

  2 * i = j1 ^2 + j2 ^2, j1 + j2 = j0 * 2, j1 = j0 * 2 - j2, (j1 - j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + j0 ^2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i - j = i0 ↔ i = i0 + j; (s) Used formulas: j1 = j0 * 2 - j2

Proof step 38 from proof two-even (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 39:

  2 * i = (j0 * 2 - j2)^2 + j2 ^2, (j0 * 2 - j2) + j2 = j0 * 2, (j0 * 2 - j2 - j2) % 2 ≠ 0, i ≠ ((j0 * 2 - j2 - j2) / 2)^2 + j0 ^2 ⊦

Rule argument

Additional information

Proof step 39 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  2 * i = (j0 * 2 - j2)^2 + j2 ^2, (j0 * 2 - 2 * j2) % 2 ≠ 0, i ≠ ((j0 * 2 - 2 * j2) / 2)^2 + j0 ^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 + i = 2 * i; (s) ⊦ i - j - i0 = i - j + i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); (s) ⊦ i + (j - i) = j; (s)

Proof step 40 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

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

Rule argument

Additional information

Used simplifier rules: ⊦ (i * 2) % 2 = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j2, 2, j0

Proof step 41 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ i % 2 = 0 ↔ ¬(∃ i0. i = 2 * i0 + 1)

• Proof step 44:

  2 * i = j1 ^2 + j2 ^2, (j1 - j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2, ∃ i0. j1 + j2 = 2 * i0 + 1 ⊦

Rule argument

Additional information

Used terms: j1 + j2

Proof step 43 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  2 * i = j1 ^2 + j2 ^2, j1 + j2 = 2 * i0 + 1, (j1 - j2) % 2 ≠ 0, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 ⊦

Rule argument

Additional information

Proof step 45 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ i % 2 = 0 ↔ ¬(∃ i0. i = 2 * i0 + 1)

• Proof step 47:

  2 * i = j1 ^2 + j2 ^2, j1 + j2 = 2 * i0 + 1, i ≠ ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2, ∃ i0. j1 - j2 = 2 * i0 + 1 ⊦

Rule argument

Additional information

Used terms: j1 - j2

Proof step 46 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  2 * i = ((2 * i1 + 1) + j2)^2 + j2 ^2, 2 * j2 + 2 * i1 = 2 * i0, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^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 + i = 2 * i; (s) ⊦ i + j - i = j; (s) ⊦ i + j = i + i0 ↔ j = i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 48 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  2 * (j2 + i1) = 2 * i0, 2 * i = ((2 * i1 + 1) + j2)^2 + j2 ^2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used terms: i1, j2, 2

Proof step 49 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  2 * i = ((2 * i1 + 1) + j2)^2 + j2 ^2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); (s)

Proof step 51 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

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

• Proof step 53:

  2 * i = ((2 * i1 + 1)^2 + 2 * (2 * i1 + 1) * j2 + j2 ^2) + j2 ^2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used terms: j2, 2 * i1 + 1

Proof step 52 from proof two-even (previous step) (back to tree)

Lemma two-plus

Proof step 53 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  2 * i = 2 * j2 ^2 + (2 * i1 + 1)^2 + 2 * (2 * i1 + 1) * j2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^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 + i = 2 * i; (s)

Proof step 54 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

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

• Proof step 56:

  2 * i = 2 * j2 ^2 + ((2 * i1)^2 + 2 * (2 * i1) * 1 + 1 ^2) + 2 * (2 * i1 + 1) * j2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used terms: 1, 2 * i1

Proof step 55 from proof two-even (previous step) (back to tree)

Lemma two-plus

Proof step 56 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  2 * i = 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 ^2 + 2 * (2 * i1 + 1) * j2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

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

Proof step 57 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ 1 ^2 = 1

• Proof step 59:

  2 * i = 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used terms:

Proof step 58 from proof two-even (previous step) (back to tree)

Lemma one

Proof step 59 from proof two-even (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 60:

  2 * i = 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2 = 2 * (j2 ^2 + 2 * i1 ^2 + 2 * i1 + (2 * i1 + 1) * j2) + 1, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

• Proof step 61:

  2 * i = 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2 ≠ 2 * (j2 ^2 + 2 * i1 ^2 + 2 * i1 + (2 * i1 + 1) * j2) + 1, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used formulas: 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2 = 2 * (j2 ^2 + 2 * i1 ^2 + 2 * i1 + (2 * i1 + 1) * j2) + 1

Proof step 60 from proof two-even (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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

Proof step 61 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  2 * i = 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, (2 * i1 ^2 + 2 * i1) * 2 ≠ (2 * i1)^2 + 4 * i1, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^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 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)

Proof step 62 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

• Proof step 64:

  2 * i = 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, (2 * i1 ^2) * 2 + (2 * i1) * 2 ≠ (2 * i1)^2 + 4 * i1, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used terms: 2, 2 * i1, 2 * i1 ^2

Proof step 63 from proof two-even (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  2 * i = 2 * j2 ^2 + (2 * i1)^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, 4 * i1 ^2 ≠ (2 * i1)^2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^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) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 65 from proof two-even (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 * i = 2 * j2 ^2 + 2 ^2 * i1 ^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, 4 * i1 ^2 ≠ 2 ^2 * i1 ^2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2 ⊦

Rule argument

Additional information

Used terms: i1, 2

Proof step 66 from proof two-even (previous step) (back to tree)

Lemma two-mult

Proof step 67 from proof two-even (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  2 * i = 2 * j2 ^2 + 2 ^2 * i1 ^2 + 4 * i1 + 1 + 2 * (2 * i1 + 1) * j2, 4 * i1 ^2 ≠ 2 ^2 * i1 ^2, i ≠ ((2 * i1 + 1) / 2)^2 + ((2 * j2 + 2 * i1 + 1) / 2)^2, i1 ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: zero: ⊦ i ^2 = 0 ↔ i = 0; commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult neq-not-zero: ⊦ i * j ≠ i * j0 → i ≠ 0; (forward) from specification int-mult

Proof step 68 from proof two-even (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ i ^2 = i * i

Rule argument

Additional information

Used simplifier rules: add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 2

Proof step 69 from proof two-even (previous step) (back to tree)

Lemma Square-def