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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i ^ j ≤ i ^ j0 ↔ j ≤ j0), 1 < i, 0 ≤ j ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(i ^ j ≤ i ^ j0 ↔ j ≤ j0), 1 < i, 2 ≤ i, 0 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: numlef-01: ⊦ (* i) ≤ j → i - 1 < j; (forward) from specification int-abs ⊦ ~1 < i ↔ 0 ≤ i; (s) numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs

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

User applied rule induction

And obtained the following new goals

• Proof step 4:

  ¬(i ^ j ≤ i ^ j0 ↔ j ≤ j0), 1 < i, 2 ≤ i, 0 ≤ j, ∀ j0, i, j1. i→n(j0) < i→n(j) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: i→n(j)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(i ^ j ≤ i ^ j0 ↔ j ≤ j0), 1 < i, 0 ≤ j, 2 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(j) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Proof step 5 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 7:

  ¬(i ^ j ≤ i ^ j0 ↔ j ≤ j0), 1 < i, 2 ≤ i, 0 ≤ j, ¬ 0 < j, ∀ j0, i, j1. i→n(j0) < i→n(j) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

• Proof step 9:

  ¬(i ^ j -1 * i ≤ i ^ j0 ↔ j ≤ j0), 1 < i, 0 < j, 2 ≤ i, 0 ≤ j, ∀ j0, i, j1. i→n(j0) < i→n(j) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: j, i

Proof step 6 from proof le-pos (previous step) (back to tree)

Lemma Pot-pos

Proof step 7 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ¬(0 < i ^ j0 ↔ 0 ≤ j0), 0 < i, 0 ≤ i, 2 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(0) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1; ⊦ 1 ≤ i ↔ 0 < i; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s)

Proof step 8 from proof le-pos (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: grz: ⊦ 0 < i → (0 < i ^ j ↔ i = 1 ∨ 0 ≤ j); grz: ⊦ 0 < i → (0 < i ^ j ↔ i = 1 ∨ 0 ≤ j); ⊦ i ≤ j ↔ ¬ j < i; (ss) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s)

Proof step 9 from proof le-pos (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  j = i0 +1, ¬(i ^ i0 * i ≤ i ^ j0 ↔ j ≤ j0), 0 < j, 1 < i, 0 ≤ j, 2 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(j) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

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

Proof step 10 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ¬(i ^ i0 * i ≤ i ^ j0 ↔ i0 + 1 ≤ j0), ~2 < i0, 1 < i, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs ⊦ ~1 < i ↔ 0 ≤ i; (s) numlef-01: ⊦ (* i) ≤ j → i - 1 < j; (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 ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i +1 = i + 1; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s)

Proof step 11 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 13:

  ¬(i ^ i0 * i ≤ i ^ j0 ↔ i0 + 1 ≤ j0), 1 < i, ~2 < i0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, ¬ 0 < j0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

• Proof step 32:

  ¬(i ^ i0 * i ≤ i ^ j0 -1 * i ↔ i0 + 1 ≤ j0), 1 < i, ~2 < i0, 0 < j0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: j0, i

Proof step 12 from proof le-pos (previous step) (back to tree)

Lemma Pot-pos

Proof step 13 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ¬(i ^ i0 * i ≤ i ^ j0 ↔ i0 + 1 ≤ j0), ~2 < i0, 1 < i, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, j0 ≤ 0, j0 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 14 from proof le-pos (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

  j0 = 0, ¬(i ^ i0 * i ≤ i ^ j0 ↔ i0 + 1 ≤ j0), 1 < i, ~2 < i0, j0 ≤ i0, j0 ≤ 0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

• Proof step 21:

  ¬(i ^ i0 * i ≤ i ^ j0 ↔ i0 + 1 ≤ j0), j0 ≠ 0, 1 < i, ~2 < i0, j0 ≤ i0, j0 ≤ 0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used formulas: j0 = 0

Proof step 15 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ¬(i ^ i0 ≤ 0 ↔ i0 + 1 ≤ 0), ~2 < i0, 1 < i, 2 ≤ i, ~1 ≤ i0, 0 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1; commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 < j → (i * j ≤ 1 ↔ i ≤ 0); (s)

Proof step 16 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ 0 < i ∧ 0 ≤ j → ¬ i ^ j ≤ 0

• Proof step 18:

  ¬(false ↔ i0 + 1 ≤ 0), 1 < i, ~2 < i0, 0 < i, ~1 ≤ i0, 2 ≤ i, 0 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs Used terms: i0, i

Proof step 17 from proof le-pos (previous step) (back to tree)

Lemma notneg-01

Proof step 18 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  0 < i, ~2 < i0, 1 < i, 0 ≤ i0, 2 ≤ i, ~1 ≤ i0, i0 + 1 ≤ 0, i0 + 1 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs

Proof step 19 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ i ≤ j ↔ ¬ j < i

Rule argument

Additional information

Used simplifier rules: i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i ≤ ~1 ↔ i < 0; (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: i0, i0 + 1

Proof step 20 from proof le-pos (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ¬(i ^ i0 * i ≤ 1 / i ^ abs(j0) ↔ i0 + 1 ≤ j0), j0 ≠ 0, ~2 < i0, 1 < i, j0 < 0, j0 < i0, j0 ≤ i0, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: Pot-neg: ⊦ i < 0 → j ^ i = 1 / j ^ abs(i); forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

Proof step 22 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  ¬(i ^ i0 * i ≤ 1 / i ^ (0 - j0) ↔ i0 + 1 ≤ j0), j0 ≠ 0, j0 < i0, 1 < i, ~2 < i0, j0 < 0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, j0 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: j0

Proof step 23 from proof le-pos (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ¬(i ^ i0 * i ≤ 1 / i ^ ~ j0 ↔ i0 + 1 ≤ j0), j0 ≠ 0, j0 < 0, ~2 < i0, 1 < i, j0 < i0, j0 ≤ i0, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 - i = ~ i; (s)

Proof step 25 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ 1 < j → 1 / j = 0

• Proof step 27:

  ¬(i ^ i0 * i ≤ 1 / i ^ ~ j0 ↔ i0 + 1 ≤ j0), j0 ≠ 0, j0 < i0, 1 < i, ~2 < i0, j0 < 0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, j0 ≤ i0, ¬ 1 < i ^ ~ j0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

• Proof step 30:

  ¬(i ^ i0 * i ≤ 0 ↔ i0 + 1 ≤ j0), j0 ≠ 0, j0 < i0, 1 < i, ~2 < i0, j0 < 0, 1 < i ^ ~ j0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, j0 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: i ^ ~ j0

Proof step 26 from proof le-pos (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ¬(i ^ i0 * i ≤ 1 / i ^ ~ j0 ↔ i0 + 1 ≤ j0), j0 ≠ 0, j0 < 0, ~2 < i0, 1 < i, j0 < i0, i ^ ~ j0 < i, j0 ≤ i0, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, i ^ ~ j0 ≤ 1, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 28 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ 1 < i ∧ 0 < j → ¬ i ^ j ≤ 1

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < ~ i ↔ i < 0; (s) Used terms: ~ j0, i

Proof step 29 from proof le-pos (previous step) (back to tree)

Lemma notone

Proof step 30 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  ¬(i ^ i0 * i ≤ 0 ↔ i0 + 1 ≤ j0), j0 ≠ 0, j0 < i0, 1 < i, ~2 < i0, j0 < 0, 1 < i ^ ~ j0, 2 ≤ i ^ ~ j0, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, j0 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: numlef-01: ⊦ (* i) ≤ j → i - 1 < j; (forward) from specification int-abs numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs

Proof step 31 from proof le-pos (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: notneg-01: ⊦ 0 < i ∧ 0 ≤ j → ¬ i ^ j ≤ 0; ⊦ 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 i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ 0 < i → (i * j ≤ 0 ↔ j ≤ 0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 32 from proof le-pos (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 33:

  j0 = i1 +1, ¬(i ^ i0 * i ≤ i ^ i1 * i ↔ i0 + 1 ≤ j0), 0 < j0, ~2 < i0, 1 < i, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

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

Proof step 33 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  ¬(i ^ i0 * i ≤ i ^ i1 * i ↔ i0 < i1 + 1), ~2 < i0, 1 < i, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, 0 ≤ i1, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~1 < i ↔ 0 ≤ i; (s) numlef-01: ⊦ (* i) ≤ j → i - 1 < j; (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 ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i +1 = i + 1; (s) ⊦ i + 1 ≤ j ↔ i < j; (s)

Proof step 34 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ 0 < i → (j * i ≤ i0 * i ↔ j ≤ i0)

• Proof step 36:

  ¬(i ^ i0 ≤ i ^ i1 ↔ i0 < i1 + 1), 1 < i, ~2 < i0, 0 < i, 0 ≤ i1, ~1 ≤ i0, 0 ≤ i0, 2 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs Used terms: i ^ i1, i, i ^ i0

Proof step 35 from proof le-pos (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof le-pos (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 37:

  ¬(i ^ i0 ≤ i ^ i1 ↔ i0 < i1 + 1), 0 < i, ~2 < i0, 1 < i, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, 0 ≤ i1, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦ ¬(i ^ i0 ≤ i ^ i1 ↔ i0 ≤ i1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ i0

Rule argument

Additional information

Used simplifier rules: ⊦ i +1 = i + 1; (s) ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ ¬ i < i; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: i0, i, i1

Proof step 37 from proof le-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  ~2 < i0, 1 < i, 0 < i, 2 ≤ i, 0 ≤ i0, ~1 ≤ i0, 0 ≤ i1, i ^ i0 ≤ i ^ i1, i0 ≤ i1, i1 + 1 ≤ i0, ∀ j0, i, j1. i→n(j0) < i→n(i0 +1) → ¬(i ^ j0 ≤ i ^ j1 ↔ j0 ≤ j1) ∧ 1 < i ∧ 2 ≤ i ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 1 ≤ i ↔ 0 < i; (s) ⊦ ¬ i < i; (s) ⊦ i +1 = i + 1; (s) trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 ⊦ i ≤ j ↔ ¬ j < i; (ss) numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs

Proof step 38 from proof le-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ i ≤ j ↔ ¬ j < i

Rule argument

Additional information

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

Proof step 39 from proof le-pos (previous step) (back to tree)

A spec-lemma