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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  abs(j) < j2 +1, j0 < abs(j), 0 ≤ j0, abs(j) * i ≤ abs(j) * i0 + j0, ¬ i ≤ i0, ∀ j0, j, i, i0. ¬(j0 < abs(j) ∧ abs(j) < j2 ∧ abs(j) * i ≤ abs(j) * i0 + j0 ∧ 0 ≤ j0 ∧ ¬ i ≤ i0) ⊦

• Proof step 43:

  abs(j) < j2 -1, j0 < abs(j), 0 ≤ j0, abs(j) * i ≤ abs(j) * i0 + j0, ¬ i ≤ i0, ∀ j0, j, i, i0. ¬(j0 < abs(j) ∧ abs(j) < j2 ∧ abs(j) * i ≤ abs(j) * i0 + j0 ∧ 0 ≤ j0 ∧ ¬ i ≤ i0) ⊦

Rule argument

Additional information

Used simplifier rules: int generated by 0, +1, -1;; ⊦ i < 0 ∧ 0 ≤ j → ¬ j < i; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  j ≠ 0, j0 < j2, i0 < i, j0 < abs(j), 0 < j2, abs(j) ≤ j2, 0 ≤ j0, abs(j) * i ≤ abs(j) * i0 + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 5:

  j ≠ 0, 0 < j2, j0 < abs(j), i0 < i, j0 < j2, j < 0, abs(j) * i ≤ abs(j) * i0 + j0, 0 ≤ j0, abs(j) ≤ j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

• Proof step 30:

  j ≠ 0, 0 < j2, j0 < abs(j), i0 < i, j0 < j2, abs(j) * i ≤ abs(j) * i0 + j0, 0 ≤ j0, abs(j) ≤ j2, ¬ j < 0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used formulas: j < 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  j ≠ 0, j0 + j < 0, i0 < i, j < 0, 0 < j2, j0 < j2, j * i0 ≤ j * i + j0, 0 ≤ j0, 0 ≤ j + j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used simplifier rules: minus-left: ⊦ ~ i * j = ~(i * j); associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) 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 + i0 ↔ j < i0; (s) ⊦ i + j < j ↔ i < 0; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i < ~ j ↔ i + j < 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i + 0 = i; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ ~ i ≤ j ↔ 0 ≤ i + j; (s) ⊦ i + ~ j = i - j; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 7:

  j ≠ 0, j0 < j2, 0 < j2, j < 0, i0 < i, j0 + j < 0, 0 ≤ j + j2, 0 ≤ j0, j * i0 ≤ j * i + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2, ¬ j0 < abs(j + 1) ∨ ¬ abs(j + 1) < j2 ∨ ¬ abs(j + 1) * i ≤ abs(j + 1) * i0 + j0 ∨ ¬ 0 ≤ j0 ∨ i ≤ i0 ⊦

Rule argument

Additional information

Used terms: j0, j + 1, i, i0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  j ≠ 0, j0 + j < j2, j0 < j2, 0 < j2, j < 0, i0 < i, j0 + j < 0, j + 1 < j2, j < j2, (j0 + j) + 1 < j2, 0 ≤ j + j2, 0 ≤ j0, j * i0 ≤ j * i + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2, ¬ j0 + j < ~1 ∨ ¬ (j + 1) * i0 ≤ (j + 1) * i + j0 ⊦

Rule argument

Additional information

Used simplifier rules: minus-left: ⊦ ~ i * j = ~(i * j); associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i +1 = i + 1; (s) 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 ↔ false); (as) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ 0 + i = i; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ ~ i ≤ j ↔ 0 ≤ i + j; (s) ⊦ i + ~ j = i - j; (s) ⊦ ~ i - j = ~(i + j); (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i < 0 → abs(i + 1) = abs(i) - 1; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i < ~ j ↔ i + j < 0; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  j = ~1 - j0, j ≠ 0, (j0 + j) + 1 < j2, j < j2, j + 1 < j2, j0 + j < 0, i0 < i, j < 0, 0 < j2, j0 < j2, j0 + j < j2, j * i0 ≤ j * i + j0, 0 ≤ j0, 0 ≤ j + j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2, ¬ j0 + j < ~1 ∨ ¬ (j + 1) * i0 ≤ (j + 1) * i + j0 ⊦

• Proof step 22:

  j ≠ ~1 - j0, j ≠ 0, (j0 + j) + 1 < j2, j < j2, j + 1 < j2, j0 + j < 0, i0 < i, j < 0, 0 < j2, j0 < j2, j0 + j < j2, j * i0 ≤ j * i + j0, 0 ≤ j0, 0 ≤ j + j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2, ¬ j0 + j < ~1 ∨ ¬ (j + 1) * i0 ≤ (j + 1) * i + j0 ⊦

Rule argument

Additional information

Used formulas: j = ~1 - j0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ~1 ≠ j0, j0 < j2, i0 < i, 0 < j0 + j2, 0 < j2, 0 ≤ j0, (~1 - j0) * i0 ≤ (~1 - j0) * i + j0, 0 ≤ j2, 0 ≤ j0 + j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

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 + (j - i) = j; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i + 0 = i; (s) ⊦ i + 1 ≤ j ↔ i < j; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ i - j - i0 = i - j + i0; (s) i < 0 ⊦ (* i) + j = j - ~ i; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ (i - j) * j0 = i * j0 - j * j0

• Proof step 12:

  ~1 ≠ j0, 0 < j2, 0 < j0 + j2, i0 < i, j0 < j2, 0 ≤ j0 + j2, 0 ≤ j2, ~1 * i0 - j0 * i0 ≤ (~1 - j0) * i + j0, 0 ≤ j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used terms: i0, j0, ~1

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

Lemma dist-sub-split

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ (i - j) * j0 = i * j0 - j * j0

• Proof step 14:

  ~1 ≠ j0, j0 < j2, i0 < i, 0 < j0 + j2, 0 < j2, 0 ≤ j0, ~1 * i0 - j0 * i0 ≤ (~1 * i - j0 * i) + j0, 0 ≤ j2, 0 ≤ j0 + j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used terms: i, j0, ~1

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

Lemma dist-sub-split

Proof step 14 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ~1 ≠ j0, 0 < j2, 0 < j0 + j2, i0 < i, j0 < j2, 0 ≤ j0, 0 ≤ j0 + j2, 0 ≤ j2, i + j0 * i ≤ j0 * i0 + i0 + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

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

Proof step 15 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 16:

  i < j, i0 ≤ j0 ⊦ i + i0 < j + j0

• Proof step 17:

  ~1 ≠ j0, j0 < j2, i0 < i, 0 < j0 + j2, 0 < j2, i + j0 * i ≤ j0 * i0 + i0 + j0, 0 ≤ j2, 0 ≤ j0 + j2, 0 ≤ j0, ¬ (i0 + 1) * j0 ≤ i * j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used simplifier rules: dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; 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 ≤ j → ¬ j < i; (s) Used terms: i0, i, (i0 + 1) * j0, i * j0

Proof step 16 from proof noeth-modlep (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  ~1 ≠ j0, 0 < j2, 0 < j0 + j2, i0 < i, j0 < j2, i * j0 < i0 * j0 + j0, 0 ≤ j0, 0 ≤ j0 + j2, 0 ≤ j2, i + j0 * i ≤ j0 * i0 + i0 + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used simplifier rules: dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i ≤ j ↔ ¬ j < i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2

Proof step 18 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ (* i0) * i + i = (i0 + 1) * i

• Proof step 20:

  ~1 ≠ j0, i * j0 < (i0 + 1) * j0, j0 < j2, i0 < i, 0 < j0 + j2, 0 < j2, i + j0 * i ≤ j0 * i0 + i0 + j0, 0 ≤ j2, 0 ≤ j0 + j2, 0 ≤ j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; Used terms: i0, j0

Proof step 19 from proof noeth-modlep (previous step) (back to tree)

Lemma numsucc

Proof step 20 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Used simplifier rules: dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; Mult-zero: ⊦ i * 0 = 0; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i < j + 1 ↔ i ≤ j; (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) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) Used terms: i0 + 1, j0, i

Proof step 21 from proof noeth-modlep (previous step) (back to tree)

Lemma ls-pos-01

Proof step 22 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ~1 ≠ j + j0, j ≠ 0, j0 + j < j2, j0 < j2, 0 < j2, j < 0, i0 < i, j0 + j < 0, j + 1 < j2, j < j2, (j0 + j) + 1 < j2, 0 ≤ j + j2, 0 ≤ j0, j * i0 ≤ j * i + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2, ¬ j0 + j < ~1 ∨ ¬ (j + 1) * i0 ≤ (j + 1) * i + j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 23 from proof noeth-modlep (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

  ~1 ≠ j + j0, j ≠ 0, (j0 + j) + 1 < j2, j < j2, j + 1 < j2, j0 + j < 0, i0 < i, j < 0, 0 < j2, j0 < j2, j0 + j < j2, j0 + j < ~1, j * i0 ≤ j * i + j0, 0 ≤ j0, 0 ≤ j + j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2, ¬ j0 + j < ~1 ∨ ¬ (j + 1) * i0 ≤ (j + 1) * i + j0 ⊦

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i < j → (j ≤ i ↔ false); (as) Used formulas: j0 + j < ~1

Proof step 24 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ~1 ≠ j + j0, j ≠ 0, j0 + j < ~1, j0 + j < j2, j0 < j2, 0 < j2, j < 0, i0 < i, j0 + j < 0, j + 1 < j2, j < j2, (j0 + j) + 1 < j2, (j + 1) * i + j0 < (j + 1) * i0, 0 ≤ j + j2, 0 ≤ j0, j * i0 ≤ j * i + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 25 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ (i + i0) * j = i * j + i0 * j

• Proof step 27:

  ~1 ≠ j + j0, j ≠ 0, (j * i + 1 * i) + j0 < (j + 1) * i0, (j0 + j) + 1 < j2, j < j2, j + 1 < j2, j0 + j < 0, i0 < i, j < 0, 0 < j2, j0 < j2, j0 + j < j2, j0 + j < ~1, j * i0 ≤ j * i + j0, 0 ≤ j0, 0 ≤ j + j2, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used terms: j, 1, i

Proof step 26 from proof noeth-modlep (previous step) (back to tree)

Lemma dist-lsplit

Proof step 27 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ~1 ≠ j + j0, j ≠ 0, j0 + j < ~1, j0 + j < j2, j0 < j2, 0 < j2, j < 0, i0 < i, j0 + j < 0, j + 1 < j2, j < j2, (j0 + j) + 1 < j2, j * i + i + j0 < (j + 1) * i0, 0 ≤ j + j2, 0 ≤ j0, j * i0 ≤ j * i + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used simplifier rules: one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2

Proof step 28 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ (i + i0) * j = i * j + i0 * j

Rule argument

Additional information

Used simplifier rules: one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i < i1 ∧ i2 ≤ i3 → (i1 + i3 < i + i2 ↔ false); (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, 1, i0

Proof step 29 from proof noeth-modlep (previous step) (back to tree)

Lemma dist-lsplit

Proof step 30 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  0 < j2, j0 < j2, i0 < i, j0 < j, 0 < j, j ≤ j2, 0 ≤ j0, j * i ≤ j * i0 + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i < j → ¬ j < i; (s) ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss)

Proof step 31 from proof noeth-modlep (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 32:

  0 < j, j0 < j, i0 < i, j0 < j2, 0 < j2, j * i ≤ j * i0 + j0, 0 ≤ j0, j ≤ j2, ¬ j0 < abs(j - 1) ∨ ¬ abs(j - 1) < j2 ∨ ¬ abs(j - 1) * i ≤ abs(j - 1) * i0 + j0 ∨ ¬ 0 ≤ j0 ∨ i ≤ i0 ⊦

Rule argument

Additional information

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

Proof step 32 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  0 < j2, j0 < j2, i0 < i, j0 < j, 0 < j, j ≤ j2, 0 ≤ j0, j * i ≤ j * i0 + j0, ¬ j0 + 1 < j ∨ ¬ (j - 1) * i ≤ (j - 1) * i0 + j0 ⊦

Rule argument

Additional information

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

Proof step 33 from proof noeth-modlep (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 34:

  j = i1 + 1, 0 < j, j0 < j, i0 < i, j0 < j2, 0 < j2, j * i ≤ j * i0 + j0, 0 ≤ j0, j ≤ j2, ¬ j0 + 1 < j ∨ ¬ i1 * i ≤ i1 * i0 + j0 ⊦

Rule argument

Additional information

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

Proof step 34 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  i1 < j2, 0 < j2, j0 < j2, i0 < i, 0 ≤ j0, (i1 + 1) * i ≤ (i1 + 1) * i0 + j0, j0 ≤ i1, 0 ≤ i1, ¬ j0 < i1 ∨ ¬ i1 * i ≤ i1 * i0 + j0 ⊦

Rule argument

Additional information

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

Proof step 35 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ (i + i0) * j = i * j + i0 * j

• Proof step 37:

  i0 < i, j0 < j2, 0 < j2, i1 < j2, 0 ≤ i1, j0 ≤ i1, i1 * i + 1 * i ≤ (i1 + 1) * i0 + j0, 0 ≤ j0, ¬ j0 < i1 ∨ ¬ i1 * i ≤ i1 * i0 + j0 ⊦

Rule argument

Additional information

Used terms: i, 1, i1

Proof step 36 from proof noeth-modlep (previous step) (back to tree)

Lemma dist-lsplit

Proof step 37 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  i1 < j2, 0 < j2, j0 < j2, i0 < i, j0 ≤ i1, 0 ≤ i1, 0 ≤ j0, i1 * i + i ≤ (i1 + 1) * i0 + j0, ¬ j0 < i1 ∨ ¬ i1 * i ≤ i1 * i0 + j0 ⊦

Rule argument

Additional information

Used simplifier rules: one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i;

Proof step 38 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ (i + i0) * j = i * j + i0 * j

• Proof step 40:

  i0 < i, j0 < j2, 0 < j2, i1 < j2, i1 * i + i ≤ (i1 * i0 + 1 * i0) + j0, 0 ≤ j0, 0 ≤ i1, j0 ≤ i1, ¬ j0 < i1 ∨ ¬ i1 * i ≤ i1 * i0 + j0 ⊦

Rule argument

Additional information

Used terms: i0, 1, i1

Proof step 39 from proof noeth-modlep (previous step) (back to tree)

Lemma dist-lsplit

Proof step 40 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  0 < j2, i1 < j2, i0 < i, i1 * i ≤ i1 * i0 + i1, 0 ≤ i1, i1 * i + i ≤ i1 * i0 + i0 + i1 ⊦

Rule argument

Additional information

Used simplifier rules: one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i ≤ i; (s) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i < i1 ∧ i2 < i3 → (i1 + i3 ≤ i + i2 ↔ false); (s) ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 41 from proof noeth-modlep (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 42:

  i < j, i0 ≤ j0 ⊦ i + i0 < j + j0

Rule argument

Additional information

Used simplifier rules: ls-forward: ⊦ i * j < i * j0 → i ≠ 0; ls-pos: ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ls-add-02: ⊦ i * (j + j1) + i0 < i * j + j0 ↔ i * j1 + i0 < j0; one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ ¬ 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; (ss) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: i0, i, (i0 + 1) * i1, i * i1

Proof step 42 from proof noeth-modlep (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof noeth-modlep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  j ≠ 0, i0 < i, abs(j) + 1 < j2, j0 < abs(j), 0 ≤ j0, abs(j) * i ≤ abs(j) * i0 + j0, ∀ j1, j3, i1, i2. ¬ j1 < abs(j3) ∨ ¬ abs(j3) < j2 ∨ ¬ abs(j3) * i1 ≤ abs(j3) * i2 + j1 ∨ ¬ 0 ≤ j1 ∨ i1 ≤ i2 ⊦

Rule argument

Additional information

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

Proof step 44 from proof noeth-modlep (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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