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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((i + j) % 2 = 0 ↔ i % 2 = 0 ∧ j % 2 = 0 ∨ i % 2 ≠ 0 ∧ j % 2 ≠ 0) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  (i + j) % 2 = 0 ⊦ i % 2 = 0 ∧ j % 2 = 0, i % 2 ≠ 0 ∧ j % 2 ≠ 0

• Proof step 23:

  (i + j) % 2 ≠ 0, i % 2 = 0 ∧ j % 2 = 0 ∨ i % 2 ≠ 0 ∧ j % 2 ≠ 0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  (i + j) % 2 = 0 ⊦ i % 2 ≠ 0 ∧ j % 2 ≠ 0, i % 2 = 0 ∧ j % 2 = 0

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  i % 2 = 0, (i + j) % 2 = 0 ⊦ i % 2 = 0 ∧ j % 2 = 0

• Proof step 14:

  j % 2 = 0, (i + j) % 2 = 0 ⊦ i % 2 = 0 ∧ j % 2 = 0

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (i + j) % 2 = 0, i % 2 = 0, j % 2 ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  (i + j) % 2 = 0, j % 2 ≠ 0, 2 ≠ 0, ∃ j0. i = j0 * 2 ⊦

Rule argument

Additional information

Used terms: 2, i

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

Lemma modex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (j0 * 2 + j) % 2 = 0, j % 2 ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  (j0 * 2 + j) % 2 = 0, ∃ i0. j = 2 * i0 + 1 ⊦

Rule argument

Additional information

Used terms: j

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

Lemma even-not-ex

Proof step 11 from proof even-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (2 * (j0 + i0) + 1) % 2 = 0 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ (2 * i + 1) % 2 ≠ 0

Rule argument

Additional information

Used terms: j0 + i0

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

Lemma even-not

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (i + j) % 2 = 0, j % 2 = 0, i % 2 ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  (i + j) % 2 = 0, i % 2 ≠ 0, 2 ≠ 0, ∃ j0. j = j0 * 2 ⊦

Rule argument

Additional information

Used terms: 2, j

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

Lemma modex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (i + j0 * 2) % 2 = 0, i % 2 ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  (i + j0 * 2) % 2 = 0, ∃ i0. i = 2 * i0 + 1 ⊦

Rule argument

Additional information

Used terms: i

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

Lemma even-not-ex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  (2 * (i0 + j0) + 1) % 2 = 0 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ (2 * i + 1) % 2 ≠ 0

Rule argument

Additional information

Used terms: i0 + j0

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

Lemma even-not

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

User applied rule case distinction

And obtained the following new goals

• Proof step 24:

  i % 2 = 0, j % 2 = 0, (i + j) % 2 ≠ 0 ⊦

• Proof step 30:

  j % 2 ≠ 0, i % 2 ≠ 0, (i + j) % 2 ≠ 0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  j % 2 = 0, i % 2 = 0, (i + j) % 2 ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  i % 2 = 0, (i + j) % 2 ≠ 0, 2 ≠ 0, ∃ j0. j = j0 * 2 ⊦

Rule argument

Additional information

Used terms: 2, j

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

Lemma modex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  i % 2 = 0, (i + j0 * 2) % 2 ≠ 0 ⊦

Rule argument

Additional information

Proof step 28 from proof even-add (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)

Rule argument

Additional information

Used simplifier rules: mod-two-02: ⊦ (i * 2) % 2 = 0; ⊦ i * j + i * j0 = i * (j + j0); (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 2, i

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

Lemma modex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  j % 2 ≠ 0, i % 2 ≠ 0, (i + j) % 2 ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

  j % 2 ≠ 0, (i + j) % 2 ≠ 0, ∃ i0. i = 2 * i0 + 1 ⊦

Rule argument

Additional information

Used terms: i

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

Lemma even-not-ex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  j % 2 ≠ 0, ((2 * i0 + 1) + j) % 2 ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

Used simplifier rules: mod-two-02: ⊦ (i * 2) % 2 = 0; ⊦ i * j + i * j0 = i * (j + j0); (s) ⊦ i * j + i = i * (j + 1); (s) add-c: ⊦ i + j = j + i; from specification int-basic2 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 Used terms: j

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

Lemma even-not-ex