Proof step 17 from proof square-interval (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (j * (j + 1)) / 2 + j0 = 0, j * j + 2 * j0 < 0, j0 + j * (j + 1) < (j * (j + 1)) / 2, j * j + 2 * j0 < ~1, 0 < j, j * (j + 1) + 2 * j0 < 0, (j * j + 2 * j0) + 1 < j, j * j + 2 * j0 < j, j0 + j * j < (j * (j + 1)) / 2, j0 ≤ j, 0 ≤ j0 ⊦ j = 0

Rule argument

Additional information

Used simplifier rules: square-even-02: ⊦ ((i + 1) * (i + 2)) % 2 = 0;%square-even: ⊦ 0 ≤ i → (i * (i + 1)) % 2 = 0;%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs% ⊦ i < 0 ∧ 0 ≤ j → i < j; (s)% ⊦ 1 * i = i; (s)% ⊦ (* i2) * i + j < i + j0 ↔ (i2 - 1) * i + j < j0; (s)% ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s)% ⊦ i * (j + 1) + j1 < i ↔ i * j + j1 < 0; (s)% ⊦ i +1 = i + 1; (s)%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs% ⊦ i ≤ j → (j ≤ i ↔ i = j); (s)%j0 ≠ 0, j < j0 ⊦ i < (* j) → i < (* j0); (s)% ⊦ i < 1 ↔ i ≤ 0; (s)%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs% ⊦ i ≤ j ↔ ¬ j < i; (ss)% ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)% ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)% ⊦ ~1 < i ↔ 0 ≤ i; (s)% ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s)% ⊦ 0 ≤ i → (0 < i * j ↔ 0 < j ∧ i ≠ 0); (s)% ⊦ 0 < i → ((* i) * j ≤ (* i) * j0 ↔ j ≤ j0); (s)%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2