Proof step 1 from proof le-abs-numerator (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  j ≠ 0 ⊦ 0 ≤ abs(i) + i / j ∧ i / j ≤ abs(i)

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i ≤ j ↔ 0 ≤ i + j; (s)

Proof step 2 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 0 ≤ i ∧ 0 < j → i / j * j ≤ i

• Proof step 4:

  j ≠ 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦ 0 ≤ abs(i) + i / j ∧ i / j ≤ abs(i)

Rule argument

Additional information

Used terms: i, j

Proof step 3 from proof le-abs-numerator (previous step) (back to tree)

Lemma ls-same-pos

Proof step 4 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  j ≠ 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦ 0 ≤ abs(i) + i / j ∧ i / j ≤ abs(i)

Rule argument

Additional information

Proof step 5 from proof le-abs-numerator (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  j ≠ 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦ 0 ≤ abs(i) + i / j ∧ i / j ≤ abs(i), ¬ i < 0 ∧ ¬ j < 0

Rule argument

Additional information

Used simplifier rules: div-zero-nls: ⊦ 0 ≤ i ∧ 0 < j → ¬ i / j < 0; div-ls-same: ⊦ 0 < j → (i < i / j ↔ i < 0 ∧ 1 < j); ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ i < j → ¬ j < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 ≤ i → abs(i) = i; (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 ⊦ i ≤ 0 ∧ 0 ≤ j → 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 + j < j ↔ 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 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i ≤ j → ¬ j < i; (s) Used formulas: ¬ i < 0 ∧ ¬ j < 0

Proof step 6 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  j ≠ 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦ ¬ i < 0 ∧ ¬ j < 0, 0 ≤ abs(i) + i / j ∧ i / j ≤ abs(i)

Rule argument

Additional information

Proof step 7 from proof le-abs-numerator (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  j ≠ 0, i < 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦ 0 ≤ abs(i) + i / j ∧ i / j ≤ abs(i), ¬ i < 0 ∧ ¬ j < 0

• Proof step 30:

  j ≠ 0, ¬ i < 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦ 0 ≤ abs(i) + i / j ∧ i / j ≤ abs(i), ¬ i < 0 ∧ ¬ j < 0

Rule argument

Additional information

Used formulas: i < 0

Proof step 8 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  j ≠ 0, 0 < i / j + i, i < 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: zero-05: j ≠ 0 ⊦ i < 0 → i ≤ i / j; ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i ≤ ~ j ↔ i + j ≤ 0; (s) ⊦ i < 0 → abs(i) = ~ i; (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 = i; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ i + ~ j = i - j; (s)

Proof step 9 from proof le-abs-numerator (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  j ≠ 0, i < 0, 0 < i / j + i, j < 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦

• Proof step 17:

  j ≠ 0, i < 0, 0 < i / j + i, ¬ j < 0, 0 ≤ i ∧ 0 < j → i / j * j ≤ i ⊦

Rule argument

Additional information

Used formulas: j < 0

Proof step 10 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  j ≠ 0, 0 < i / j + i, i < 0, j < 0 ⊦

Rule argument

Additional information

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

Proof step 11 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  i = i0 * j + j0, j ≠ 0, j < 0, i < 0, 0 < i0 + i, j < j0, j0 ≤ 0, 0 ≤ i0 ⊦

Rule argument

Additional information

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

Proof step 12 from proof le-abs-numerator (previous step) (back to tree)

Lemma div-elim-negneg

Proof step 13 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  j ≠ 0, j < 0, i0 * j + j0 < 0, j < j0, 0 < i0 + i0 * j + j0, j0 < i0 + i0 * j, 0 < i0 + i0 * j, j0 ≤ 0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (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 < i + j ↔ 0 < j; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs 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-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 14 from proof le-abs-numerator (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

  j ≠ 0, 0 < i0 + i0 * j, j0 < i0 + i0 * j, 0 < i0 + i0 * j + j0, j < j0, i0 * j + j0 < 0, j < 0, 0 ≤ i0, j0 ≤ 0, ¬ 0 < i0 * (j + 1) + j0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < i + j ↔ 0 < j; (s) ⊦ 0 ≤ i → (0 < i * j ↔ 0 < j ∧ i ≠ 0); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) 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 formulas: 0 < i0 * (j + 1) + j0

Proof step 15 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 1 * i = i; (s) 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 ⊦ i < j ↔ ¬ j ≤ i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: i0, 1, j

Proof step 16 from proof le-abs-numerator (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  0 < j, i < 0, 0 < i / j + i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i < j → ¬ j < i; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss)

Proof step 18 from proof le-abs-numerator (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 19:

  i = ~ abs(i), 0 < i / j + i, i < 0, 0 < j ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ ~ i = i; (s) Used formulas: i = ~ abs(i)

Proof step 19 from proof le-abs-numerator (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 20:

  0 < j, ~ abs(i) < 0, 0 < ~ abs(i) / j + ~ abs(i) ⊦

Rule argument

Additional information

Proof step 20 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ j ≠ 0 → ~ i / j = ~(i / j)

• Proof step 22:

  j ≠ 0, 0 < ~(abs(i) / j) + ~ abs(i), ~ abs(i) < 0, 0 < j ⊦

Rule argument

Additional information

Used terms: j, abs(i)

Proof step 21 from proof le-abs-numerator (previous step) (back to tree)

Lemma Div-left

Proof step 22 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 23:

  ⊦ 0 ≤ i ∧ 0 < j → i / j * j ≤ i

• Proof step 24:

  j ≠ 0, 0 < j, ~ abs(i) < 0, 0 < ~(abs(i) / j) + ~ abs(i), 0 ≤ abs(i) ∧ 0 < j → abs(i) / j * j ≤ abs(i) ⊦

Rule argument

Additional information

Used terms: abs(i), j

Proof step 23 from proof le-abs-numerator (previous step) (back to tree)

Lemma ls-same-pos

Proof step 24 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

Rule argument

Additional information

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

Proof step 25 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  i ≠ 0, j ≠ 0, abs(i) / j + abs(i) < 0, 0 < j, abs(i) / j * j ≤ abs(i) ⊦ 0 ≤ abs(i) / j ∧ 0 ≤ abs(i)

Rule argument

Additional information

Used terms: abs(i) / j, abs(i)

Proof step 26 from proof le-abs-numerator (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

Proof step 28 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  0 < j ⊦ i / (* j) < 0 ↔ i + j ≤ 0

Rule argument

Additional information

Used simplifier rules: forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs ⊦ i + j < j ↔ i < 0; (s) ⊦ ¬ abs(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 Used terms: j, abs(i)

Proof step 29 from proof le-abs-numerator (previous step) (back to tree)

Lemma div-ls-zero

Proof step 30 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  j ≠ 0, i / j < 0, j < 0, i + i / j < 0, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: div-zero-ngr-01: ⊦ 0 ≤ i ∧ j < 0 → ¬ 0 < i / j; ⊦ 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) ⊦ i ≤ j ↔ ¬ j < i; (ss) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ i < j → ¬ j < i; (s) ⊦ i ≤ j → ¬ j < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 31 from proof le-abs-numerator (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

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

Rule argument

Additional information

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

Proof step 32 from proof le-abs-numerator (previous step) (back to tree)

Lemma div-elim-posneg

Proof step 33 from proof le-abs-numerator (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

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

Proof step 34 from proof le-abs-numerator (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 35:

  j ≠ 0, i0 < 0, j0 + j < 0, (i0 * j + j0) + i0 < 0, j < 0, i0 * j + i0 < 0, 0 ≤ i0 * j + j0, 0 ≤ j0, ¬ i0 * (j + 1) + j0 < 0 ⊦

Rule argument

Additional information

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

Proof step 35 from proof le-abs-numerator (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 1 * i = i; (s) 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 ⊦ i < j ↔ ¬ j ≤ i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: i0, 1, j

Proof step 36 from proof le-abs-numerator (previous step) (back to tree)

A spec-lemma