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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(abs(i) < abs(j) ↔ j < i), i ≤ 0, j ≤ 0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: le-def: ⊦ i ≤ j ↔ ¬ j < i;

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: Abs-pos: ⊦ ¬ j < 0 → abs(j) = j; abs-08: ⊦ i < 0 → abs(i) = ~ i; Minus-def: ⊦ ~ i = 0 - i; sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; ⊦ ¬ i < j → (j < i ↔ i ≠ j); (ss) ⊦ 0 + i = i; (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: i < 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

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; zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; ⊦ i < j → ¬ j < i; (s)

Proof step 5 from proof absls-02 (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: abs-08: ⊦ i < 0 → abs(i) = ~ i; Minus-def: ⊦ ~ i = 0 - i; sub-zero: ⊦ i + (0 - i0) = i - i0; sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; Abs-pos: ⊦ ¬ j < 0 → abs(j) = j; forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; ⊦ i < j ∧ ¬ i0 < j → ¬ i0 < i; (s) ⊦ ¬ i < j → (j < i ↔ i ≠ j); (ss) lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1 lf-04: ⊦ ¬ j < i ∧ j < i0 → i < i0; (forward) from specification int-basic1 ⊦ 0 + i = 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 < j → ¬ j < i; (s) Used formulas: j < 0