Proof step 1 from proof modlep-03 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  abs(j1) < j, j0 < j, 0 ≤ j0, j * i + j0 ≤ j * i0 + j1, ¬ i ≤ i0 ⊦

Rule argument

Additional information

Proof step 2 from proof modlep-03 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  j * i + j0 ≤ j * i0, abs(j0) < j ⊦ i ≤ i0

• Proof step 4:

  j0 < j, abs(j1) < j, j * i + j0 ≤ j * i0 + j1, 0 ≤ j0, ¬ i ≤ i0 ⊦ j * i + (j0 - j1) ≤ j * i0 ∧ abs(j0 - j1) < j

Rule argument

Additional information

Used terms: j, i, j0 - j1, i0

Proof step 3 from proof modlep-03 (previous step) (back to tree)

Lemma modlep-02

Proof step 4 from proof modlep-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  j0 ≠ j1, abs(j1) < j, j0 < j, i0 < i, 0 < j, abs(j1) < abs(j0 - j1), j0 < abs(j0 - j1), 0 ≤ j0, j * i + j0 ≤ j * i0 + j1, j ≤ abs(j0 - j1) ⊦

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + 0 = i; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ 0 < abs(i) ↔ i ≠ 0; (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i - j ≤ i0 ↔ i ≤ j + i0; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 5 from proof modlep-03 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  j0 = i1 + j1, j0 ≠ j1, j0 < abs(i1), abs(j1) < abs(i1), 0 < j, i0 < i, j0 < j, abs(j1) < j, j ≤ abs(i1), j * i + j0 ≤ j * i0 + j1, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: j0, j1, i1

Proof step 6 from proof modlep-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  i1 ≠ 0, i1 + j1 < abs(i1), abs(j1) < abs(i1), 0 < j, i0 < i, i1 + j1 < j, abs(j1) < j, j * i + i1 ≤ j * i0, 0 ≤ i1 + j1, j ≤ abs(i1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < abs(i) ↔ i ≠ 0; (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + j ≤ i + j0 ↔ j ≤ j0; (s) ⊦ i = i + j ↔ j = 0; (s)

Proof step 7 from proof modlep-03 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  j * i + j0 ≤ j * i0, abs(j0) < j ⊦ i ≤ i0

• Proof step 9:

  i1 ≠ 0, abs(j1) < j, i1 + j1 < j, i0 < i, 0 < j, abs(j1) < abs(i1), i1 + j1 < abs(i1), j ≤ abs(i1), 0 ≤ i1 + j1, j * i + i1 ≤ j * i0 ⊦ j * (i + 1) + (i1 - j) ≤ j * i0 ∧ abs(i1 - j) < j

Rule argument

Additional information

Used simplifier rules: ⊦ i + 1 ≤ j ↔ i < j; (s) ⊦ i < j → ¬ j < 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 terms: j, i + 1, i1 - j, i0

Proof step 8 from proof modlep-03 (previous step) (back to tree)

Lemma modlep-02

Proof step 9 from proof modlep-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  i1 ≠ 0, i1 ≠ j, abs(j1) < j, i1 + j1 < j, i0 < i, 0 < j, abs(j1) < abs(i1), i1 + j1 < abs(i1), abs(j1) < abs(i1 - j), i1 + j1 < abs(i1 - j), j ≤ abs(i1 - j), j ≤ abs(i1), 0 ≤ i1 + j1, j * i + i1 ≤ j * i0 ⊦

Rule argument

Additional information

Used simplifier rules: dist-rsplit: ⊦ i * (j + j0) = i * j + i * j0; one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + 0 = i; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ 0 < abs(i) ↔ i ≠ 0; (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i + (j - i) = j; (s)

Proof step 10 from proof modlep-03 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  i1 = i2 + j, i1 ≠ 0, i1 ≠ j, i1 + j1 < abs(i2), abs(j1) < abs(i2), i1 + j1 < abs(i1), abs(j1) < abs(i1), 0 < j, i0 < i, i1 + j1 < j, abs(j1) < j, j * i + i1 ≤ j * i0, 0 ≤ i1 + j1, j ≤ abs(i1), j ≤ abs(i2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i1, j, i2

Proof step 11 from proof modlep-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  i2 + j ≠ 0, i2 ≠ 0, abs(j1) < abs(i2 + j), abs(j1) < abs(i2), i2 + j1 < 0, abs(j1) < j, (i2 + j) + j1 < abs(i2), (i2 + j) + j1 < abs(i2 + j), i0 < i, (i2 + j1) + 1 < j, i2 + j1 < j, 0 < j, (i2 + j1) + 1 < abs(i2 + j), (i2 + j1) + 1 < abs(i2), i2 + j1 < abs(i2 + j), i2 + j1 < abs(i2), j * i + i2 + j ≤ j * i0, 0 ≤ (i2 + j) + j1, j ≤ abs(i2 + j), j ≤ abs(i2) ⊦

Rule argument

Additional information

Used simplifier rules: forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ 0 < abs(i) ↔ i ≠ 0; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i < i + j ↔ 0 < j; (s) ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i +1 = i + 1; (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs 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 ⊦ i + j < j ↔ i < 0; (s) ⊦ i = i + j ↔ j = 0; (s)

Proof step 12 from proof modlep-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ¬ j < 0 → abs(j) = j

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ i ≤ i + j ↔ 0 ≤ j; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i + j < j ↔ i < 0; (s) ⊦ 0 < i ∧ 0 < j → 0 < i + j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ j < 0 → abs(j) = 0 - j; (s) ⊦ 0 - i = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < j → ¬ j < i; (s) ⊦ i ≤ ~ j ↔ i + j ≤ 0; (s) ⊦ i < ~ j ↔ i + j < 0; (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs 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 < 0 ∧ j < 0 → i + j < 0; (s) ⊦ i +1 = i + 1; (s) ⊦ ¬ abs(i) < i; (s) Used terms: i2 + j

Proof step 13 from proof modlep-03 (previous step) (back to tree)

A spec-lemma