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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  sqrt(j) < i, i ^2 ≤ j ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  sqrt(j) < i, i ^2 ≤ j ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 0 ≤ i → sqrt(i) ^2 ≤ i ∧ i < sqrt(i) +1 ^2

• Proof step 5:

  sqrt(j) < i, i ^2 ≤ j, 0 ≤ j → sqrt(j) ^2 ≤ j ∧ j < sqrt(j) +1 ^2 ⊦

Rule argument

Additional information

Used terms: j

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

Lemma Sqrt-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  sqrt(j) < i, i ^2 ≤ j, 0 ≤ j → sqrt(j) ^2 ≤ j ∧ j < (sqrt(j) + 1)^2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i +1 = i + 1; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  sqrt(j) < i, i ^2 ≤ j, 0 ≤ j, 0 ≤ j → sqrt(j) ^2 ≤ j ∧ j < (sqrt(j) + 1)^2 ⊦

• Proof step 10:

  sqrt(j) < i, i ^2 ≤ j, ¬ 0 ≤ j, 0 ≤ j → sqrt(j) ^2 ≤ j ∧ j < (sqrt(j) + 1)^2 ⊦

Rule argument

Additional information

Used formulas: 0 ≤ j

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  0 < (sqrt(j) + 1)^2, sqrt(j) ^2 < (sqrt(j) + 1)^2, i ^2 < (sqrt(j) + 1)^2, j < (sqrt(j) + 1)^2, sqrt(j) < i, sqrt(j) ^2 ≤ j, i ^2 ≤ j, 0 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ 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 forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ 0 ≤ i ∧ 0 ≤ j → (i ^2 < j ^2 ↔ i < j)

Rule argument

Additional information

Used simplifier rules: square-not-neg: ⊦ 0 ≤ i → ¬ sqrt(i) < 0; ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (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 numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 ⊦ 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 forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ ~1 < i ↔ 0 ≤ i; (s) Used terms: sqrt(j) + 1, i

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

Lemma two-ls-pospos

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: two-not-neg: ⊦ ¬ i ^2 < 0; ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-lels: ⊦ 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 ≤ j ↔ ¬ j < i; (ss)