Proof step 1 from proof square-interval (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i ≠ j, j * (j + 1) + 2 * j0 < (i + 1) * (i + 2), 0 ≤ j0, 0 ≤ i, j0 ≤ j, i * (i + 1) ≤ j * (j + 1) + 2 * j0 ⊦

Rule argument

Additional information

Proof step 2 from proof square-interval (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 3:

  i ≠ j, j * (j + 1) + 2 * j0 < (i + 1) * (i + 2), j * (j + 1) + 2 * j0 < (j + 1) * (j + 2), i * (i + 1) ≤ j * (j + 1) + 2 * j0, j0 ≤ j, 0 ≤ i, 0 ≤ j0 ⊦

• Proof step 9:

  i ≠ j, j * (j + 1) + 2 * j0 < (i + 1) * (i + 2), i * (i + 1) ≤ j * (j + 1) + 2 * j0, j0 ≤ j, 0 ≤ i, 0 ≤ j0, ¬ j * (j + 1) + 2 * j0 < (j + 1) * (j + 2) ⊦

Rule argument

Additional information

Used formulas: j * (j + 1) + 2 * j0 < (j + 1) * (j + 2)

Proof step 3 from proof square-interval (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  i ≠ j, j * (j + 1) + 2 * j0 < (j + 1) * (j + 2), j * (j + 1) + 2 * j0 < (i + 1) * (i + 2), i * (i + 1) < (j + 1) * ((j + 1) + 1), 0 ≤ j0, 0 ≤ i, j0 ≤ j, i * (i + 1) ≤ j * (j + 1) + 2 * j0 ⊦

Rule argument

Additional information

Used simplifier rules: numls-04: ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; numsucc: ⊦ (* i0) * i + i = (i0 + 1) * i; numle-03: ⊦ (* i2) * i + j ≤ i + j0 ↔ (i2 - 1) * i + j ≤ j0; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i + j ≤ i + j0 ↔ j ≤ j0; (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 Used formulas: i * (i + 1) < (j + 1) * ((j + 1) + 1)

Proof step 4 from proof square-interval (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) < j * (j + 1) ↔ i < j)

• Proof step 6:

  i ≠ j, i < j + 1, j * (j + 1) + 2 * j0 < (i + 1) * (i + 2), j * (j + 1) + 2 * j0 < (j + 1) * (j + 2), i * (i + 1) ≤ j * (j + 1) + 2 * j0, j0 ≤ j, 0 ≤ j0, 0 ≤ i, 0 ≤ j + 1 ⊦

Rule argument

Additional information

Used simplifier rules: numls-04: ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; numsucc: ⊦ (* i0) * i + i = (i0 + 1) * i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (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) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ i ≤ j → ¬ j < i; (s) Used terms: j + 1, i

Proof step 5 from proof square-interval (previous step) (back to tree)

Lemma square-ls-02

Proof step 6 from proof square-interval (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  i ≠ j, j * (j + 1) + 2 * j0 < (j + 1) * (j + 2), j * (j + 1) + 2 * j0 < (i + 1) * (i + 2), i < j + 1, j * (j + 1) < (i + 1) * ((i + 1) + 1), 0 ≤ j + 1, 0 ≤ i, 0 ≤ j0, j0 ≤ j, i * (i + 1) ≤ j * (j + 1) + 2 * j0 ⊦

Rule argument

Additional information

Used simplifier rules: numls-04: ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; numsucc: ⊦ (* i0) * i + i = (i0 + 1) * i; zero-ls: ⊦ 0 < i → (i * j < 0 ↔ j < 0); associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-05: ⊦ 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-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i + j < j ↔ 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 formulas: j * (j + 1) < (i + 1) * ((i + 1) + 1)

Proof step 7 from proof square-interval (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) < j * (j + 1) ↔ i < j)

Rule argument

Additional information

Used simplifier rules: numls-04: ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; numsucc: ⊦ (* i0) * i + i = (i0 + 1) * i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; numls-04: ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; numsucc: ⊦ (* i0) * i + i = (i0 + 1) * i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 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 < 0 → (~1 ≤ i ↔ i = ~1); (s) ⊦ i < 0 ∧ 0 ≤ j → ¬ j < i; (s) Used terms: i + 1, j

Proof step 8 from proof square-interval (previous step) (back to tree)

Lemma square-ls-02

Proof step 9 from proof square-interval (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  i ≠ j, (j * j + j) + 2 * j0 < 3 * i + i * i + 2, ~2 < 2 * i, 0 ≤ j, 2 * j + 2 ≤ 2 * j0, i * i + i ≤ (j * j + j) + 2 * j0, j0 ≤ j, 0 ≤ i, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; numsucc: ⊦ (* i0) * i + i = (i0 + 1) * i; numls-04: ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; 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 ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i < i + j ↔ 0 < j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i + j < i + i0 ↔ j < i0; (s)

Proof step 10 from proof square-interval (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 11:

  i ≠ j, ~2 < 2 * i, (j * j + j) + 2 * j0 < 3 * i + i * i + 2, 0 ≤ j0, 0 ≤ i, j0 ≤ j, i * i + i ≤ (j * j + j) + 2 * j0, 2 * j + 2 ≤ 2 * j0, 0 ≤ j, 2 * (j + 1) ≤ 2 * j0 ⊦

Rule argument

Additional information

Used simplifier rules: dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; 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; (s) Used formulas: 2 * (j + 1) ≤ 2 * j0

Proof step 11 from proof square-interval (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ 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: j0, j + 1, 2

Proof step 12 from proof square-interval (previous step) (back to tree)

Lemma le-pos