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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i - j = i0 ↔ i = i0 + j; (s)

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 0 < j ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j ∧ 0 ≤ i0)

• Proof step 4:

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

• Proof step 11:

  i = i0 * 2 + j0, j0 < 2, 0 < 2, 0 ≤ j0, 0 ≤ i0, 0 ≤ i ⊦ j0 = ~1 ↔ (∃ j. 2 * j = i + 1 ∧ j ≤ 0)

Rule argument

Additional information

Used terms: i, 2, i0, j0

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

Lemma div-elim-pospos

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss)

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 0 < j ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0)

• Proof step 7:

  i = i0 * 2 + j0, i < 0, abs(j0) < 2, 0 < 2, j0 ≤ 0, i0 ≤ 0 ⊦ j0 = ~1 ↔ (∃ j. 2 * j = i + 1 ∧ j ≤ 0)

Rule argument

Additional information

Used terms: i, 2, i0, j0

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

Lemma div-elim-negpos

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  2 * j = (i0 * 2 + j0) + 1, j0 ≠ ~1, abs(j0) < 2, i0 * 2 + j0 < 0, i0 ≤ 0, j0 ≤ 0, j ≤ 0 ⊦

Rule argument

Additional information

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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  2 * j = (i0 * 2 + j0) + 1, j0 ≠ ~1, i0 * 2 + j0 < 0, abs(j0) < 2, j ≤ 0, j0 ≤ 0, i0 ≤ 0 ⊦

Rule argument

Additional information

Used formulas: j0 = ~1

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ j < 0 → abs(j) = 0 - j

Rule argument

Additional information

Used simplifier rules: ⊦ 0 - i = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i < 0 → (~2 < i ↔ i = ~1); (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ ¬ j < 0 → abs(j) = j; (s) j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ 2 * i + 1 ≠ 2 * j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  2 * j = (i0 * 2 + j0) + 1, j0 ≠ ~1, j0 < 2, j ≤ 0, 0 ≤ i0, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (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 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ 0 ≤ i0 → 0 ≤ i0 * j + j0; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  2 * j = (i0 * 2 + j0) + 1, j0 = 1, j0 ≠ ~1, j0 < 2, 0 ≤ j0, 0 ≤ i0, j ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≠ 1 ∧ 0 ≤ i → (i < 2 ↔ i = 0); (s) ⊦ abs(j1) < abs(i) ∧ j1 ≠ 0 → i * j ≠ i * j0 + j1; (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 formulas: j0 = 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  2 * j = 2 + i0 * 2, j ≤ 0, 0 ≤ i0 ⊦

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 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 ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i ≤ ~1 ↔ i < 0; (s) ⊦ i ≤ j → ¬ j < i; (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, i0

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

A spec-lemma