Proof step 1 from proof modex-odd-neg-01 (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ i % 2 = ~1 ↔ (∃ j. i = 2 * j + 1 ∧ j < 0)

Rule argument

Additional information

Proof step 2 from proof modex-odd-neg-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ i % 2 = ~1 ↔ (∃ j. i = 2 * j - 1 ∧ j ≤ 0)

• Proof step 4:

  ⊦ (∃ j. i = 2 * j - 1 ∧ j ≤ 0) ↔ (∃ j. i = 2 * j + 1 ∧ j < 0)

Rule argument

Additional information

Used terms: i

Proof step 3 from proof modex-odd-neg-01 (previous step) (back to tree)

Lemma modex-odd-neg

Proof step 4 from proof modex-odd-neg-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  2 * j = i + 1, j ≤ 0 ⊦ ∃ j. i = 2 * j + 1 ∧ j < 0

Rule argument

Additional information

Used simplifier rules: forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i ≤ ~1 ↔ i < 0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (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 = i * (j + 1); (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 5 from proof modex-odd-neg-01 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  2 * j = i + 1, j ≤ 0 ⊦ i = 2 * (j - 1) + 1 ∧ j - 1 < 0

Rule argument

Additional information

Used terms: j - 1

Proof step 6 from proof modex-odd-neg-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  2 * j = i + 1, j ≤ 0 ⊦ i = 2 * (j - 1) + 1 ∧ j - 1 < 0

Rule argument

Additional information

Proof step 7 from proof modex-odd-neg-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  2 * j = i + 1, j = i0 + 1, j ≤ 0 ⊦ i = 2 * i0 + 1 ∧ i0 < 0

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: j, 1, i0

Proof step 8 from proof modex-odd-neg-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  2 * (i0 + 1) = i + 1, i ≠ 2 * i0 + 1, i0 < 0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i ≤ ~1 ↔ i < 0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s)

Proof step 9 from proof modex-odd-neg-01 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  2 * (i0 + 1) = i + 1, i ≠ 2 * i0 + 1, i0 < 0 ⊦

Rule argument

Additional information

Used formulas: i = 2 * i0 + 1

Proof step 10 from proof modex-odd-neg-01 (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

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