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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  j ≤ j0, j0 ≤ i, ¬ abs(j0 - j) ≤ abs(i - j) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  abs(i - j) < abs(j0 - j), ¬ i < j0, ¬ j0 < j, ¬ i < j ⊦

Rule argument

Additional information

Used simplifier rules: le-def: ⊦ i ≤ j ↔ ¬ j < i; lf-08: ⊦ ¬ i < j ∧ ¬ i0 < i → ¬ i0 < j; (forward) from specification int-basic1

Proof step 3 from proof abs-ls-02 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  ⊦ i0 = i - j ↔ i = i0 + j

Rule argument

Additional information

Used simplifier rules: Abs-pos: ⊦ ¬ j < 0 → abs(j) = j; abs-06: ⊦ 0 < abs(i) ↔ i ≠ 0; sub-eq: ⊦ i - j = i0 ↔ i = i0 + j; abssub-02: ⊦ j < i → abs(i - j) = i - j; sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; lf-08: ⊦ ¬ i < j ∧ ¬ i0 < i → ¬ i0 < j; (forward) from specification int-basic1 ⊦ 0 + i = i; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ 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; (s) lf-07: ⊦ ¬ i < i0 ∧ j < i0 → j < i; (forward) from specification int-basic1 lf-04: ⊦ ¬ j < i ∧ j < i0 → i < i0; (forward) from specification int-basic1 Used terms: i, j, i0

Proof step 4 from proof abs-ls-02 (previous step) (back to tree)

Lemma elim-sub