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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  0 < j, 0 ≤ i, ¬ i ^2 < (i + j)^2 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: Square-def: ⊦ i ^2 = i * i; commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ i * i < j * j ↔ abs(i) < abs(j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 0 ≤ i → abs(i) = i

Rule argument

Additional information

Used simplifier rules: ⊦ i + j ≤ i ↔ j ≤ 0; (s) ⊦ i < j → (j ≤ i ↔ false); (as) 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) ⊦ j < 0 → abs(j) = 0 - j; (s) ⊦ 0 - i = ~ i; (s) ⊦ ~ i ≤ j ↔ 0 ≤ i + j; (s) 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 forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i < j → ¬ j < i; (s) Used terms: i + j

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

A spec-lemma