Proof step 1 from proof div-div-pred-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ((i - 3) / 4 - 1) / 2 ≠ (i - 7) / 8, i < 0 ⊦

Rule argument

Additional information

Proof step 2 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ((i - 3) / 4 - 1) / 2 ≠ (i - 7) / 8, i < 0 ⊦

Rule argument

Additional information

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

Proof step 3 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ i < 0 → ((i - 1) / 2 - 1) / 2 = (i - 3) / 4

• Proof step 5:

  (((i - 1) / 2 - 1) / 2 - 1) / 2 ≠ (i - 7) / 8, i < 0 ⊦

Rule argument

Additional information

Used terms: i

Proof step 4 from proof div-div-pred-01 (previous step) (back to tree)

Lemma div-div-pred

Proof step 5 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ i < 0 → ((i - 1) / 2 - 1) / 2 = (i - 3) / 4

• Proof step 7:

  ((i - 1) / 2 - 3) / 4 ≠ (i - 7) / 8, i < 0, (i - 1) / 2 < 0 ⊦

Rule argument

Additional information

Used simplifier rules: div-ls-zero: 0 < j ⊦ i / (* j) < 0 ↔ i + j ≤ 0; ⊦ i + (j - i0) = i + j - i0; (s) ⊦ (* i) + i0 - (* j) = (i - j) + i0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i ≤ ~1 ↔ i < 0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used terms: (i - 1) / 2

Proof step 6 from proof div-div-pred-01 (previous step) (back to tree)

Lemma div-div-pred

Proof step 7 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ((i - 1) / 2 - 3) / 4 ≠ (i - 7) / 8, i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: div-ls-zero: 0 < j ⊦ i / (* j) < 0 ↔ i + j ≤ 0; 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 ≤ ~1 ↔ i < 0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ (* i) + i0 - (* j) = (i - j) + i0; (s) ⊦ i + (j - i0) = i + j - i0; (s)

Proof step 8 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  i - 1 = i0 * 2 + j0, (i0 - 3) / 4 ≠ (i - 7) / 8, i < 0, abs(j0) < 2, 0 < 2, i - 1 < 0, j0 ≤ 0, i0 ≤ 0 ⊦

Rule argument

Additional information

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

Proof step 9 from proof div-div-pred-01 (previous step) (back to tree)

Lemma div-elim-negpos

Proof step 10 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (i0 - 3) / 4 ≠ (j0 + i0 * 2 - 6) / 8, abs(j0) < 2, i0 * 2 + j0 < ~1, i0 * 2 + j0 < 0, j0 ≤ 0, i0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i + (j - i0) = i + j - i0; (s) i < 0 ⊦ (* i) + j = j - ~ i; (s) ⊦ (* i) + i0 - (* j) = (i - j) + i0; (s) forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 11 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  i0 - 3 = i1 * 4 + j1, i1 ≠ (j0 + i0 * 2 - 6) / 8, i0 * 2 + j0 < 0, i0 * 2 + j0 < ~1, abs(j0) < 2, abs(j1) < 4, 0 < 4, i0 - 3 < 0, i0 ≤ 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i - j < i0 ↔ i < 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 j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) Used terms: i0 - 3, 4, i, j

Proof step 12 from proof div-div-pred-01 (previous step) (back to tree)

Lemma div-elim-negpos

Proof step 13 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  i1 ≠ (j0 + ((i1 * 4 + j1) + 3) * 2 - 6) / 8, i1 * 4 + j1 < 0, ((i1 * 4 + j1) + 3) * 2 + j0 < 0, abs(j1) < 4, abs(j0) < 2, ((i1 * 4 + j1) + 3) * 2 + j0 < ~1, i1 * 4 + j1 ≤ ~3, i1 ≤ 0, j1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-le-03: ⊦ j ≤ i ∧ i < 0 → j < 0; (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 ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 14 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  j0 + ((i1 * 4 + j1) + 3) * 2 = i0 + 6, i1 ≠ i0 / 8, ((i1 * 4 + j1) + 3) * 2 + j0 < ~1, abs(j0) < 2, abs(j1) < 4, ((i1 * 4 + j1) + 3) * 2 + j0 < 0, i1 * 4 + j1 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: j0 + ((i1 * 4 + j1) + 3) * 2, 6, i0

Proof step 15 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  j0 + ((i1 * 4 + j1) + 3) * 2 = i0 + 6, i1 ≠ i0 / 8, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, i0 < ~7, i0 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

Rule argument

Additional information

Used simplifier rules: numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 j0 ≠ 0, j < j0 ⊦ i < (* j) → i < (* j0); (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) < (* j0) ↔ i < j0 - j; (s)

Proof step 16 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0

• Proof step 18:

  j0 + ((i1 * 4 + j1) + 3) * 2 - 6 = i0, i1 ≠ i0 / 8, i0 < 0, i0 < ~7, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, i1 * 4 + j1 ≤ ~3, i1 ≤ 0, j1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Used terms: 6, i0, j0 + ((i1 * 4 + j1) + 3) * 2

Proof step 17 from proof div-div-pred-01 (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 19:

  i1 ≠ (j0 + ((i1 * 4 + j1) + 3) * 2 - 6) / 8, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 + ((i1 * 4 + j1) + 3) * 2 - 6 < ~7, j0 + ((i1 * 4 + j1) + 3) * 2 - 6 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

Rule argument

Additional information

Proof step 19 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  i1 ≠ (j0 + ((i1 * 4 + j1) + 3) * 2 - 6) / 8, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, j0 + ((i1 * 4 + j1) + 3) * 2 < ~1, i1 * 4 + j1 ≤ ~3, i1 ≤ 0, j1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

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

Proof step 20 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  i1 ≠ (j0 + (i1 * 4 + j1) * 2 + 3 * 2 - 6) / 8, j0 + (i1 * 4 + j1) * 2 + 3 * 2 < ~1, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

Rule argument

Additional information

Used terms: 2, 3, i1 * 4 + j1

Proof step 21 from proof div-div-pred-01 (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  i1 ≠ (j0 + (i1 * 4 + j1) * 2) / 8, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, j0 + (i1 * 4 + j1) * 2 < ~7, j0 + (i1 * 4 + j1) * 2 < 0, i1 * 4 + j1 ≤ ~3, i1 ≤ 0, j1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i + 0 = i; (s) ⊦ (* i) + i0 - (* j) = (i - j) + i0; (s)

Proof step 23 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  i1 ≠ (j0 + (i1 * 4) * 2 + j1 * 2) / 8, j0 + (i1 * 4) * 2 + j1 * 2 < 0, j0 + (i1 * 4) * 2 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

Rule argument

Additional information

Used terms: 2, j1, i1 * 4

Proof step 24 from proof div-div-pred-01 (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  i1 ≠ (j0 + 8 * i1 + j1 * 2) / 8, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, j0 + 8 * i1 + j1 * 2 < ~7, j0 + 8 * i1 + j1 * 2 < 0, i1 * 4 + j1 ≤ ~3, i1 ≤ 0, j1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 26 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 27:

  j0 + 8 * i1 + j1 * 2 = 8 * i1 + j0 + j1 * 2, i1 ≠ (j0 + 8 * i1 + j1 * 2) / 8, j0 + 8 * i1 + j1 * 2 < 0, j0 + 8 * i1 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

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: j0 + 8 * i1 + j1 * 2 = 8 * i1 + j0 + j1 * 2

Proof step 27 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 28:

  i1 ≠ (8 * i1 + j0 + j1 * 2) / 8, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, 8 * i1 + j0 + j1 * 2 < ~7, 8 * i1 + j0 + j1 * 2 < 0, i1 * 4 + j1 ≤ ~3, i1 ≤ 0, j1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Proof step 28 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  i1 ≠ (8 * i1 + j0 + j1 * 2) / 8, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦ (8 * i1) % 8 = 0 ∧ 8 * i1 < 0 ∧ j0 + j1 * 2 < 0 ∧ 0 < 8

• Proof step 37:

  (8 * i1) % 8 = 0, i1 ≠ (8 * i1) / 8 + (j0 + j1 * 2) / 8, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, 8 * i1 < 0, j0 + j1 * 2 < 0, 0 < 8, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

Rule argument

Additional information

Used terms: 8, j0 + j1 * 2, 8 * i1

Proof step 29 from proof div-div-pred-01 (previous step) (back to tree)

Lemma div-add1-negneg

Proof step 30 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  i1 ≠ (8 * i1 + j0 + j1 * 2) / 8, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, 8 * i1 + j0 + j1 * 2 < ~7, 8 * i1 + j0 + j1 * 2 < 0, i1 * 4 + j1 ≤ ~3, i1 ≤ 0, j1 ≤ 0, j0 ≤ 0 ⊦ i1 < 0 ∧ j0 + j1 * 2 < 0

Rule argument

Additional information

Used simplifier rules: mod-zero-num: i0 % j = 0, j ≠ 0 ⊦ (i * (* i0)) % (* j) = 0; 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)

Proof step 31 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 32:

  i1 ≠ 0, i1 ≠ (8 * i1 + j0 + j1 * 2) / 8, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 ≤ 0, j1 ≤ 0, i1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦ i1 < 0 ∧ j0 + j1 * 2 < 0

Rule argument

Additional information

Used simplifier rules: ⊦ i + 0 = i; (s) i + 1 = i0 ⊦ (* i) < j → (j ≤ (* i0) ↔ j = i0); (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult i < 0 ⊦ (* i) + j = j - ~ i; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < 0 → abs(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 Used formulas: i1 = 0

Proof step 32 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  i1 ≠ (8 * i1 + j0 + j1 * 2) / 8, i1 ≠ 0, i1 < 0, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, 8 * i1 + j1 * 2 < j1 * 2, i1 * 4 < j1 + j0, 0 ≤ j0 + j1 * 2, i1 * 4 + j1 ≤ ~3, j0 ≤ 0, j1 ≤ 0 ⊦

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 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s) ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; (s) ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-02: ⊦ 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 ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

Proof step 33 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ i < 0 ∧ j < 0 → ¬ 0 ≤ i + j

• Proof step 35:

  i1 ≠ (8 * i1 + j0 + j1 * 2) / 8, i1 ≠ 0, i1 * 4 < j1 + j0, 8 * i1 + j1 * 2 < j1 * 2, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, 8 * i1 + j0 + j1 * 2 < ~7, 8 * i1 + j0 + j1 * 2 < 0, i1 < 0, j1 ≤ 0, j0 ≤ 0, i1 * 4 + j1 ≤ ~3, 0 ≤ j0 + j1 * 2 ⊦ j0 < 0 ∧ j1 * 2 < 0

Rule argument

Additional information

Used terms: j1 * 2, j0

Proof step 34 from proof div-div-pred-01 (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  i1 ≠ (8 * i1 + j0 + j1 * 2) / 8, i1 ≠ 0, i1 < 0, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, 8 * i1 + j1 * 2 < j1 * 2, i1 * 4 < j1 + j0, 0 ≤ j0 + j1 * 2, i1 * 4 + j1 ≤ ~3, j0 ≤ 0, j1 ≤ 0 ⊦ j0 < 0 ∧ j1 < 0

Rule argument

Additional information

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

Proof step 36 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: nummult-le-01: ⊦ 0 < i ∧ j < 0 → ((* i) * i0 ≤ (* j) ↔ i0 ≤ (j + 1 - i) / i); div-mult-num: j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j; ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ ¬ 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) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ 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 ⊦ i < 0 → (i < i * j ↔ j < 1); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≤ ~1 ↔ i < 0; (s) ⊦ 0 < i → (i * j < 0 ↔ j < 0); (s) ⊦ 1 * i = i; (s) Used formulas: j1 = 0

Proof step 37 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  (j0 + j1 * 2) / 8 ≠ 0, i1 * 4 + j1 < 0, abs(j1) < 4, abs(j0) < 2, 8 * i1 + j0 + j1 * 2 < ~7, 8 * i1 + j0 + j1 * 2 < 0, j0 + j1 * 2 < 0, i1 < 0, i1 * 4 + j1 ≤ ~3, j1 ≤ 0, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: mod-zero-num: i0 % j = 0, j ≠ 0 ⊦ (i * (* i0)) % (* j) = 0; div-mult-num: j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j; forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) 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) 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) ⊦ 1 * i = i; (s)

Proof step 38 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  abs(i) < abs(j) ⊦ i / j = 0

• Proof step 40:

  (j0 + j1 * 2) / 8 ≠ 0, i1 < 0, j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 ≤ 0, j1 ≤ 0, i1 * 4 + j1 ≤ ~3, ¬ abs(j0 + j1 * 2) < abs(8) ⊦

Rule argument

Additional information

Used terms: 8, j0 + j1 * 2

Proof step 39 from proof div-div-pred-01 (previous step) (back to tree)

Lemma div-zero-02

Proof step 40 from proof div-div-pred-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  (j0 + j1 * 2) / 8 ≠ 0, i1 < 0, j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, abs(j0) < 2, abs(j1) < 4, i1 * 4 + j1 < 0, j0 + j1 * 2 ≤ ~8, j0 ≤ 0, j1 ≤ 0, i1 * 4 + j1 ≤ ~3 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (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 ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < 0 → abs(i) = ~ i; (s)

Proof step 41 from proof div-div-pred-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ 0 < j → (j < 2 ↔ j = 1)

Rule argument

Additional information

Used simplifier rules: div-mult-num-01: j % j0 = 0, j ≠ 0, j0 ≠ 0 ⊦ (i * (* j0)) / (* j) = i / j / j0; nummult-le-01: ⊦ 0 < i ∧ j < 0 → ((* i) * i0 ≤ (* j) ↔ i0 ≤ (j + 1 - i) / i); nummult-le-01: ⊦ 0 < i ∧ j < 0 → ((* i) * i0 ≤ (* j) ↔ i0 ≤ (j + 1 - i) / i); nummult-ls: ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 < (* j) ↔ i0 < (i + j - 1) / i); ⊦ 0 < abs(i) ↔ i ≠ 0; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i - j ≤ i0 ↔ i ≤ j + i0; (s) ⊦ i + (j - i0) = i + j - i0; (s) i < 0 ⊦ (* i) + j = j - ~ i; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 forward-le-03: ⊦ j ≤ i ∧ i < 0 → j < 0; (forward) from specification int-abs ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (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 ⊦ 0 < i → (i * j < 0 ↔ j < 0); (s) ⊦ i + 0 = i; (s) Used terms: abs(j0)

Proof step 42 from proof div-div-pred-01 (previous step) (back to tree)

A spec-lemma