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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 3:

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

• Proof step 12:

  (i + i0 % j) % j ≠ (i0 < 0 ⊃ (i + i0) % j;(i + i0 < 0 ⊃ (i + i0) % j;(0 ≤ i + i0 % j ⊃ (i + i0) % j;((i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j - j;0)))), 0 < j, ¬ 0 ≤ i ⊦

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) Used terms: i, j, i0

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

Lemma modmod-add

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (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 ⊦ i ≤ j ↔ ¬ j < i; (ss)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: modmod-add2-posneg-pos: ⊦ 0 ≤ i + i0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j; add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

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-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 ≤ j ↔ ¬ j < i; (ss)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: modmod-add2-posneg-neg: ⊦ i + i0 % j < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j; add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: mod-ls-same-02: j ≠ 0 ⊦ i < i % j ↔ i < 0 ∧ (abs(j) = 1 ∨ abs(j) ≤ abs(i)); mod-one: ⊦ i % 1 = 0; ⊦ 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 < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i + j < j ↔ i < 0; (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-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i + 0 = i; (s) ⊦ i ≤ ~ j ↔ i + j ≤ 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i + j < i + i0 ↔ j < i0; (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss)

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

Heuristic if-then-else split applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: modmod-add2-posneg-neg-01: ⊦ 0 ≤ i + i0 % j ∧ i + i0 < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ (i + i0 % j) % j ≠ 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j + j; ⊦ i + j = i + i0 ↔ j = i0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: 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 ⊦ i ≤ j ↔ ¬ j < i; (ss)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 14:

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

• Proof step 16:

  (i + i0 % j) % j ≠ (i + i0 < 0 ⊃ (i + i0) % j;(0 ≤ i + i0 % j ⊃ (i + i0) % j;((i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j - j;0))), i < 0, 0 < j, ¬ i0 < 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs Used terms: i, j, i0

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

Lemma modmod-add-02

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

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

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 18:

  (i + i0 % j) % j ≠ (0 ≤ i + i0 % j ⊃ (i + i0) % j;((i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j - j;0)), 0 < j, i < 0, 0 ≤ i0, ¬ i + i0 < 0 ⊦

Rule argument

Additional information

Used simplifier rules: modmod-add2-negpos-neg: ⊦ i + i0 < 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j; add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

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

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 20:

  (i + i0 % j) % j ≠ ((i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j - j;0), i < 0, 0 < j, 0 ≤ i0, 0 ≤ i + i0, ¬ 0 ≤ i + i0 % j ⊦

Rule argument

Additional information

Used simplifier rules: modmod-add2-negpos-pos: ⊦ 0 ≤ i + i0 % j ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j; add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  (i + i0 % j) % j ≠ ((i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j - j;0), j ≠ 1, i + i0 % j < 0, i < 0, 0 < j, 0 < i0, 0 ≤ i0, 0 ≤ i + i0, j ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: mod-ls-same-01: j ≠ 0 ⊦ i % j < i ↔ 0 < i ∧ (abs(j) = 1 ∨ abs(j) ≤ i); mod-one: ⊦ i % 1 = 0; mod-zero-09: ⊦ 0 < i ∧ i < j → i % j = i; forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs ⊦ i ≤ j → ¬ j < i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + 0 = i; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i - 0 = i; (s) ⊦ i + j < i + i0 ↔ j < i0; (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

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

Heuristic if-then-else split applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: modmod-add2-negpos-pos-01: ⊦ i + i0 % j < 0 ∧ 0 ≤ i + i0 ∧ i < 0 ∧ 0 ≤ i0 ∧ (i + i0 % j) % j ≠ 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j - j; ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i + (j - i) = j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2