Proof step 1 from proof modmod-add2-negpos-neg (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof modmod-add2-negpos-neg (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < 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 < j ↔ i < 0; (s) 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 forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs

Proof step 3 from proof modmod-add2-negpos-neg (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) Used terms: i0, j, i1, j0

Proof step 4 from proof modmod-add2-negpos-neg (previous step) (back to tree)

Lemma div-elim-pospos

Proof step 5 from proof modmod-add2-negpos-neg (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ 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 < j ↔ i < 0; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (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 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); (s)

Proof step 6 from proof modmod-add2-negpos-neg (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

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

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 Used formulas: i + i1 * j + j0 = i1 * j + i + j0

Proof step 7 from proof modmod-add2-negpos-neg (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Proof step 8 from proof modmod-add2-negpos-neg (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ i % j = 0 ∧ i + i0 < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0) % j = i0 % j

Rule argument

Additional information

Used simplifier rules: mod-mult-04: j ≠ 0 ⊦ (i * j) % j = 0; mod-mult-pos-01: ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (j * i + i0) % j = i0 % j; ⊦ i * 0 = 0; (s) ⊦ i + 0 = i; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) 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, i + j0, i1 * j

Proof step 9 from proof modmod-add2-negpos-neg (previous step) (back to tree)

Lemma mod-add1-posneg-neg