Proof step 1 from proof div-mult-shift-holds (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof div-mult-shift-holds (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: 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

Proof step 3 from proof div-mult-shift-holds (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

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

Proof step 4 from proof div-mult-shift-holds (previous step) (back to tree)

Lemma div-mult-rew

Proof step 5 from proof div-mult-shift-holds (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: mult-split-mod: ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → i / j * i0 + (i0 * i % j) / j = (i0 * i) / j; 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

Proof step 6 from proof div-mult-shift-holds (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

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

Proof step 7 from proof div-mult-shift-holds (previous step) (back to tree)

Lemma div-elim-pospos

Proof step 8 from proof div-mult-shift-holds (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (i0 * (i1 * j + j0)) / j ≠ i1 * i0, j0 * i0 < j, 0 < j, j0 < j, 0 ≤ i0, 0 ≤ j0, 0 ≤ i1 ⊦

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 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 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); (s)

Proof step 9 from proof div-mult-shift-holds (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  ((i1 * j) * i0 + j0 * i0) / j ≠ i1 * i0, j0 < j, 0 < j, j0 * i0 < j, 0 ≤ i1, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i0, j0, i1 * j

Proof step 10 from proof div-mult-shift-holds (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof div-mult-shift-holds (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: mod-mult-04: j ≠ 0 ⊦ (i * j) % j = 0; ⊦ i * 0 = 0; (s) ⊦ i + 0 = i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) ⊦ 0 ≤ i → (0 ≤ i * j ↔ i = 0 ∨ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, j0 * i0, (i1 * j) * i0

Proof step 12 from proof div-mult-shift-holds (previous step) (back to tree)

Lemma div-add1-pospos

Proof step 13 from proof div-mult-shift-holds (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: div-mult-03: j ≠ 0 ⊦ (i * j) / j = i; commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 0 ≤ i → (0 ≤ i * j ↔ i = 0 ∨ 0 ≤ j); (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ 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 = i + j ↔ j = 0; (s) ⊦ i * 0 = 0; (s) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < 0 → (0 ≤ i * j ↔ j ≤ 0); (s)

Proof step 14 from proof div-mult-shift-holds (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  0 < j, 0 ≤ i, i < j ⊦ i / j = 0

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ i → (0 ≤ i * j ↔ i = 0 ∨ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, j0 * i0

Proof step 15 from proof div-mult-shift-holds (previous step) (back to tree)

Lemma div-zero