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)) / 2, 0 ≤ j0, 0 ≤ i, j0 ≤ j, (i * (i + 1)) / 2 ≤ (j * (j + 1)) / 2 + j0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: square-ls-01: ⊦ 0 ≤ i ∧ 0 ≤ j → ((i * (i + 1)) / 2 < ((j + 1) * (j + 2)) / 2 ↔ i < j + 1); commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i ≤ i; (s) ⊦ i < j + 1 ↔ i ≤ j; (s) 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 forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used terms: i, j, j0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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 < ((i + 1) * (i + 2)) / 2, 2 * ((j * (j + 1)) / 2 + j0) < 2 * ((i + 1) * (i + 2)) / 2, (i * (i + 1)) / 2 ≤ (j * (j + 1)) / 2 + j0, j0 ≤ j, 0 ≤ i, 0 ≤ j0, 0 ≤ j ⊦ i * (i + 1) ≤ j * (j + 1) + 2 * j0 ∧ j * (j + 1) + 2 * j0 < (i + 1) * (i + 2)

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: 2 * ((j * (j + 1)) / 2 + j0) < 2 * ((i + 1) * (i + 2)) / 2

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:

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

• Proof step 9:

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

Rule argument

Additional information

Used terms: j0, (j * (j + 1)) / 2, 2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ i % 2 ≠ 1 ∧ 0 < i → i / 2 * 2 = i

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: square-even-02: ⊦ ((i + 1) * (i + 2)) % 2 = 0; ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 ≤ i → ¬ (i + 1) * (i + 2) ≤ 0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: (i + 1) * (i + 2)

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

Lemma div2zero

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:

  ⊦ i % 2 ≠ 1 ∧ 0 < i → i / 2 * 2 = i

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: square-even-02: ⊦ ((i + 1) * (i + 2)) % 2 = 0; square-even: ⊦ 0 ≤ i → (i * (i + 1)) % 2 = 0; mult-ls-01: ⊦ 0 < j ∧ i0 < i / j → i0 * j < i; div-lezero: ⊦ 0 < j → (i / j ≤ 0 ↔ i < j); ⊦ 0 ≤ i → (0 < i * j ↔ 0 < j ∧ i ≠ 0); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 0 + i = i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ 0 < i → ¬ i * (i + 1) < 2; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j * (j + 1)

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

Lemma div2zero

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

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: square-even: ⊦ 0 ≤ i → (i * (i + 1)) % 2 = 0; square-even-02: ⊦ ((i + 1) * (i + 2)) % 2 = 0; ⊦ 0 ≤ i → (0 < i * j ↔ 0 < j ∧ i ≠ 0); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ 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 → (i ≤ j ↔ i < j); (s) ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i ≤ j → ¬ j < i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: 2 * (i * (i + 1)) / 2 ≤ 2 * ((j * (j + 1)) / 2 + j0)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ i % 2 ≠ 1 ∧ 0 < i → i / 2 * 2 = i

• Proof step 17:

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

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i * (i + 1)

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

Lemma div2zero

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (j * (j + 1)) / 2 + j0 = 0, 0 ≠ j, j * j + 2 * j0 < j, j * j + 2 * j0 < 0, j * j + 2 * j0 < ~1, 0 < j, j * (j + 1) + 2 * j0 < 0, (j * j + 2 * j0) + 1 < j, j0 ≤ j, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: square-even-02: ⊦ ((i + 1) * (i + 2)) % 2 = 0; square-even: ⊦ 0 ≤ i → (i * (i + 1)) % 2 = 0; ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i +1 = i + 1; (s) 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 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 add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * (j + 1) + j1 < i ↔ i * j + j1 < 0; (s) ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) j0 ≠ 0, j < j0 ⊦ i < (* j) → i < (* j0); (s) ⊦ i < 1 ↔ i ≤ 0; (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ 0 ≤ i → (0 < i * j ↔ 0 < j ∧ i ≠ 0); (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 0 < i → ((* i) * j ≤ (* i) * j0 ↔ j ≤ j0); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ 0 ≤ i ∧ 0 ≤ j → (i + j = 0 ↔ i = 0 ∧ j = 0)

Rule argument

Additional information

Used simplifier rules: div-two-zero-01: ⊦ 0 ≤ i / 2 ↔ ~1 ≤ i; div-two-zero-01: ⊦ 0 ≤ i / 2 ↔ ~1 ≤ i; ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 0 + 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 ⊦ 0 < i → (i * j < 0 ↔ j < 0); (s) ⊦ i < j → ¬ j < i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i < j ∧ ¬ i0 < j → ¬ i0 < i; (s) Used terms: j0, (j * (j + 1)) / 2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

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

Rule argument

Additional information

Used terms: j0, (j * (j + 1)) / 2, 2

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ i % 2 ≠ 1 ∧ 0 < i → i / 2 * 2 = i

Rule argument

Additional information

Used simplifier rules: square-even: ⊦ 0 ≤ i → (i * (i + 1)) % 2 = 0; square-even-02: ⊦ ((i + 1) * (i + 2)) % 2 = 0; square-even-01: ⊦ (i * (i + 1)) % 2 = 0; ⊦ 0 ≤ i → (0 < i * j ↔ 0 < j ∧ i ≠ 0); (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (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 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j * (j + 1)

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

Lemma div2zero