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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i0 % j = 0, (i + i0) % j ≠ i % j, i < 0, i0 < 0, 0 < j ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i0 % j = 0, (i + i0) % j ≠ i % j, i0 < j, i < 0, i0 < 0, 0 < j, i + 1 < j, i < j, i0 + 1 < j ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i +1 = i + 1; (s) trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  i0 = i1 * j + j0, j0 = 0, (i + i0) % j ≠ i % j, i0 + 1 < j, i < j, i + 1 < j, 0 < j, i0 < 0, i < 0, i0 < j, abs(j0) < j, j0 ≤ 0 ⊦

Rule argument

Additional information

Used terms: i0, j, i1, j0

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

Lemma div-elim2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (i + i1 * j) % j ≠ i % j, i1 < j, 1 + i1 * j < j, i < j, i + 1 < j, i1 < 0, i < 0, 0 < j, i1 + 1 < j, i1 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i +1 = i + 1; (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 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 ⊦ 0 < i → (i * j < 0 ↔ j < 0); (s) ⊦ i + 0 = i; (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ 0 < i → (i * j < i ↔ j < 1); (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  i = i0 * j + j0, (i + i1 * j) % j ≠ j0, i1 + 1 < j, 0 < j, i < 0, i1 < 0, i + 1 < j, i < j, 1 + i1 * j < j, i1 < j, abs(j0) < j, i1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Used terms: i, j, i0, j0

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

Lemma div-elim2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (j * (i0 + i1) + j0) % j ≠ j0, i0 * j + j0 < j, j0 < j, i1 + 1 < j, 0 < j, i0 * j + j0 < 0, i1 < 0, 1 + i1 * j < j, i1 < j, abs(j0) < j, (i0 * j + j0) + 1 < j, i1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i +1 = i + 1; (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 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 9 from proof mod-add-neg (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ i * j = j * i

• Proof step 11:

  ((i0 + i1) * j + j0) % j ≠ j0, (i0 * j + j0) + 1 < j, abs(j0) < j, i1 < j, 1 + i1 * j < j, i1 < 0, i0 * j + j0 < 0, 0 < j, i1 + 1 < j, j0 < j, i0 * j + j0 < j, j0 ≤ 0, i1 ≤ 0 ⊦

Rule argument

Additional information

Used terms: j, i0 + i1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  i0 * j + j0 < 0, 0 < j, j0 < 0 ⊦ (i0 * j + j0) % j = j0 % j

Rule argument

Additional information

Used simplifier rules: mod-mult-04: j ≠ 0 ⊦ (i * j) % j = 0; mod-zero-05: ⊦ abs(i) < j → i % j = i; ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ i * j + i0 < i * (j + j1) + j0 ↔ i0 < i * j1 + j0; (s) ⊦ i < i + j ↔ 0 < j; (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ i < j → ¬ j < i; (s) ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ 0 + i = i; (s) ⊦ 0 * i = 0; (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: i0 + i1, j, j0

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

Lemma modeq-neg