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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i * (i + 1) < 2, 0 < i ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i * i + i < 2, 0 < i ⊦

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; forward-le-05: ⊦ 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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  0 < i, i * i + i < 2, ¬ 1 + i * i < 2 ⊦

Rule argument

Additional information

Used simplifier rules: square-lez-01: ⊦ i * i ≤ 0 ↔ i = 0; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i < 1 ↔ 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 formulas: 1 + i * i < 2

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ i + j = j + i

• Proof step 6:

  i * i + i < 2, 0 < i, ¬ i * i + 1 < 2 ⊦

Rule argument

Additional information

Used terms: i * i, 1

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

A spec-lemma

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  ⊦ i + j < i0 ∧ ¬ j < j0 → i + j0 < i0

Rule argument

Additional information

Used simplifier rules: square-lez-01: ⊦ i * i ≤ 0 ↔ i = 0; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; j0 ≠ 0, j ≤ j0 ⊦ i < (* j) → i < (* j0); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i < 1 ↔ 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: i * i, i, 2, 1

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

A spec-lemma