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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  j < 0, 0 < i + j, ¬ abs(j) < i ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: abs-08: ⊦ i < 0 → abs(i) = ~ i; Minus-def: ⊦ ~ i = 0 - i; sub-ls: ⊦ i - j < i0 ↔ i < j + i0; forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; lf-04: ⊦ ¬ j < i ∧ j < i0 → i < i0; (forward) from specification int-basic1 lf-07: ⊦ ¬ i < i0 ∧ j < i0 → j < i; (forward) from specification int-basic1 add-c: ⊦ i + j = j + i; from specification int-basic2 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