Proof step 1 from proof pot-root-est (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i ⊦

Rule argument

Additional information

Proof step 2 from proof pot-root-est (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  0 < i, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs

Proof step 3 from proof pot-root-est (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 0 ≤ i → (∃ j, j0. i = j * j + j0 ∧ j0 ≤ 2 * j ∧ 0 ≤ j ∧ 0 ≤ j0 ∧ j = sqrt(i))

• Proof step 5:

  0 < i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, 0 ≤ 2 * i → (∃ j, j0. 2 * i = j * j + j0 ∧ j0 ≤ 2 * j ∧ 0 ≤ j ∧ 0 ≤ j0 ∧ j = sqrt(2 * i)) ⊦

Rule argument

Additional information

Used terms: 2 * i

Proof step 4 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof pot-root-est (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  0 < i, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, ∃ j, j0. 2 * i = j * j + j0 ∧ j0 ≤ 2 * j ∧ 0 ≤ j ∧ 0 ≤ j0 ∧ j = sqrt(2 * i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 6 from proof pot-root-est (previous step) (back to tree)

User applied rule exists left

And obtained the following new goals

• Proof step 7:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0 ⊦

Rule argument

Additional information

Proof step 7 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < i, 2 * i < (j + 1) ^ 2, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i ⊦

• Proof step 57:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < i, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, ¬ 2 * i < (j + 1) ^ 2 ⊦

Rule argument

Additional information

Used formulas: 2 * i < (j + 1) ^ 2

Proof step 8 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0 ⊦

• Proof step 52:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, ¬ (2 * i) ^ j < ((j + 1) ^ 2) ^ j ⊦

Rule argument

Additional information

Used formulas: (2 * i) ^ j < ((j + 1) ^ 2) ^ j

Proof step 9 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i ⊦

• Proof step 49:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, ¬ j ^ 2 ≤ 2 * i ⊦

Rule argument

Additional information

Used formulas: j ^ 2 ≤ 2 * i

Proof step 10 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  0 < i, 0 ≤ j ⊦ ¬ j / i ≤ i0 → ¬ j ≤ i * i0

• Proof step 12:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0 ⊦ 0 < 2 ∧ 0 ≤ j ^ 2 ∧ ¬ j ^ 2 / 2 ≤ i

Rule argument

Additional information

Used terms: i, 2, j ^ 2

Proof step 11 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof pot-root-est (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, j ^ 2 / 2 ≤ i, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i ⊦

Rule argument

Additional information

Used simplifier rules: notneg: ⊦ 0 ≤ i ∧ 0 ≤ j → ¬ i ^ j < 0; ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 13 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3 ⊦

• Proof step 47:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, j ^ 2 / 2 ≤ i, ¬ (j ^ 2 / 2) / 3 ≤ i / 3 ⊦

Rule argument

Additional information

Used formulas: (j ^ 2 / 2) / 3 ≤ i / 3

Proof step 14 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i, j * j / 6 ≤ (j ^ 2 / 2) / 3 ⊦

• Proof step 45:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i, ¬ j * j / 6 ≤ (j ^ 2 / 2) / 3 ⊦

Rule argument

Additional information

Used formulas: j * j / 6 ≤ (j ^ 2 / 2) / 3

Proof step 15 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 16:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, j * j / 6 ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, 4 ^ (j * j / 6) ≤ 4 ^ (i / 3) ⊦

• Proof step 41:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, j * j / 6 ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, ¬ 4 ^ (j * j / 6) ≤ 4 ^ (i / 3) ⊦

Rule argument

Additional information

Used formulas: 4 ^ (j * j / 6) ≤ 4 ^ (i / 3)

Proof step 16 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 17:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, 4 ^ (j * j / 6) < ((j + 1) ^ 2) ^ j, 4 ^ (j * j / 6) ≤ 4 ^ (i / 3), (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i, j * j / 6 ≤ (j ^ 2 / 2) / 3 ⊦

Rule argument

Additional information

Used simplifier rules: j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i < j ↔ ¬ j ≤ i; (ss) 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-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ i < j → (j ≤ i ↔ false); (as) Used formulas: 4 ^ (j * j / 6) < ((j + 1) ^ 2) ^ j

Proof step 17 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ i * j = j * i

• Proof step 19:

  2 * i = j * j + j0, j = sqrt(2 * i), 4 ^ (j / 6 * j) < ((j + 1) ^ 2) ^ j, 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, j / 6 * j ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, 4 ^ (j / 6 * j) ≤ 4 ^ (i / 3) ⊦

Rule argument

Additional information

Used terms: j / 6, j

Proof step 18 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ 0 ≤ j ∧ 0 ≤ j0 → i ^ (j * j0) = (i ^ j) ^ j0

• Proof step 21:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, (4 ^ (j / 6)) ^ j < ((j + 1) ^ 2) ^ j, (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ (j ^ 2 / 2) / 3, 0 ≤ j / 6, 0 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i / j; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) Used terms: j, j / 6, 4

Proof step 20 from proof pot-root-est (previous step) (back to tree)

Lemma pot-pot-02

Proof step 21 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

  2 * i = j * j + j0, j = sqrt(2 * i), (4 ^ (j / 6)) ^ j < ((j + 1) ^ 2) ^ j, 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 ≤ j, 0 ≤ j / 6, j / 6 * j ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3) ⊦ 0 ≤ 4 ^ (j / 6) ∧ 0 ≤ (j + 1) ^ 2 ∧ 0 < j

• Proof step 26:

  2 * i = j * j + j0, j = sqrt(2 * i), 4 ^ (j / 6) < (j + 1) ^ 2, 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < j, 0 ≤ j, 0 ≤ j / 6, j / 6 * j ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), 0 ≤ 4 ^ (j / 6), 0 ≤ (j + 1) ^ 2 ⊦

Rule argument

Additional information

Used terms: (j + 1) ^ 2, j, 4 ^ (j / 6)

Proof step 22 from proof pot-root-est (previous step) (back to tree)

Lemma ls-pos-03

Proof step 23 from proof pot-root-est (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  2 * i = sqrt(2 * i) * sqrt(2 * i) + j0, (sqrt(2 * i) + 1) ^ 2 < 0, 0 < sqrt(2 * i), (2 * i) ^ sqrt(2 * i) < ((sqrt(2 * i) + 1) ^ 2) ^ sqrt(2 * i), 0 < i, 2 * i < (sqrt(2 * i) + 1) ^ 2, (4 ^ (sqrt(2 * i) / 6)) ^ sqrt(2 * i) < ((sqrt(2 * i) + 1) ^ 2) ^ sqrt(2 * i), 4 ^ (i / 3) < ((sqrt(2 * i) + 1) ^ 2) ^ sqrt(2 * i), sqrt(2 * i) ^ 2 < (sqrt(2 * i) + 1) ^ 2, 0 ≤ 4 ^ (sqrt(2 * i) / 6), 0 ≤ sqrt(2 * i), (4 ^ (sqrt(2 * i) / 6)) ^ sqrt(2 * i) ≤ 4 ^ (i / 3), sqrt(2 * i) ^ 2 / 6 ≤ i / 3, sqrt(2 * i) ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * sqrt(2 * i), 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, sqrt(2 * i) ^ 2 ≤ 2 * i, sqrt(2 * i) / 6 * sqrt(2 * i) ≤ sqrt(2 * i) ^ 2 / 6, (4 ^ (sqrt(2 * i) / 6)) ^ sqrt(2 * i) ≤ (2 * i) ^ sqrt(2 * i), sqrt(2 * i) / 6 * sqrt(2 * i) ≤ i / 3 ⊦

Rule argument

Additional information

Used simplifier rules: notneg-02: ⊦ 0 < i → ¬ i ^ j < 0; ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) 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 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 ↔ ¬ j < i; (ss) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → ¬ sqrt(2 * i) ≤ 0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i / j; (s) j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s)

Proof step 24 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ i ^ 2 = i * i

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ i * i < 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: sqrt(2 * i) + 1

Proof step 25 from proof pot-root-est (previous step) (back to tree)

Lemma pot-square-04

Proof step 26 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ i ^ 2 = i * i

• Proof step 28:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < j, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < i, 2 * i < (j + 1) * (j + 1), 4 ^ (j / 6) < (j + 1) * (j + 1), 0 ≤ (j + 1) * (j + 1), 0 ≤ 4 ^ (j / 6), (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ (j ^ 2 / 2) / 3, 0 ≤ j / 6, 0 ≤ j ⊦

Rule argument

Additional information

Used terms: j + 1

Proof step 27 from proof pot-root-est (previous step) (back to tree)

Lemma pot-square-04

Proof step 28 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ 36 ≤ i → ¬ 4 ^ (i / 6) < (i + 1) * (i + 1)

• Proof step 30:

  2 * i = j * j + j0, j = sqrt(2 * i), 4 ^ (j / 6) < (j + 1) * (j + 1), 2 * i < (j + 1) * (j + 1), 0 < i, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < j, 0 ≤ j, 0 ≤ j / 6, j / 6 * j ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), 0 ≤ 4 ^ (j / 6), 0 ≤ (j + 1) * (j + 1), ¬ 36 ≤ j ⊦

Rule argument

Additional information

Used terms: j

Proof step 29 from proof pot-root-est (previous step) (back to tree)

Lemma pot-square-est

Proof step 30 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 31:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < j, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < i, 2 * i < (j + 1) * (j + 1), 4 ^ (j / 6) < (j + 1) * (j + 1), 0 ≤ (j + 1) * (j + 1), 0 ≤ 4 ^ (j / 6), (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ (j ^ 2 / 2) / 3, 0 ≤ j / 6, 0 ≤ j, 2 * 1024 ≤ 2 * i, ¬ 36 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i / j; (s) j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) ⊦ 0 ≤ i * i; (s) ⊦ 0 < i ∧ 0 ≤ j → ((* j) ≤ (* i) * i0 ↔ (i + j - 1) / i ≤ 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) ⊦ 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 * 1024 ≤ 2 * i

Proof step 31 from proof pot-root-est (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 32:

  2 * i = j * j + j0, j = sqrt(2 * i), 4 ^ (j / 6) < (j + 1) * (j + 1), 2 * i < (j + 1) * (j + 1), 0 < i, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < j, 2 * 1024 ≤ 2 * i, 0 ≤ j, 0 ≤ j / 6, j / 6 * j ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), 0 ≤ 4 ^ (j / 6), 0 ≤ (j + 1) * (j + 1), sqrt(2 * 1024) ≤ sqrt(2 * i), ¬ 36 ≤ j ⊦

• Proof step 39:

  2 * i = j * j + j0, j = sqrt(2 * i), 4 ^ (j / 6) < (j + 1) * (j + 1), 2 * i < (j + 1) * (j + 1), 0 < i, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < j, 2 * 1024 ≤ 2 * i, 0 ≤ j, 0 ≤ j / 6, j / 6 * j ≤ (j ^ 2 / 2) / 3, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j0, j ^ 2 / 2 ≤ i, (j ^ 2 / 2) / 3 ≤ i / 3, (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), 0 ≤ 4 ^ (j / 6), 0 ≤ (j + 1) * (j + 1), ¬ sqrt(2 * 1024) ≤ sqrt(2 * i), ¬ 36 ≤ j ⊦

Rule argument

Additional information

Used formulas: sqrt(2 * 1024) ≤ sqrt(2 * i)

Proof step 32 from proof pot-root-est (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 33:

  2 * i = j * j + j0, 0 < j, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < i, 2 * i < (j + 1) * (j + 1), 4 ^ (j / 6) < (j + 1) * (j + 1), sqrt(2 * 1024) ≤ j, 0 ≤ (j + 1) * (j + 1), 0 ≤ 4 ^ (j / 6), (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ j, 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ (j ^ 2 / 2) / 3, 0 ≤ j / 6, 0 ≤ j, 2 * 1024 ≤ 2 * i, ¬ 36 ≤ j ⊦

Rule argument

Additional information

Proof step 33 from proof pot-root-est (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  2 * i = j * j + j0, sqrt(2048) < 36, 0 < (j + 1) * (j + 1), 4 ^ (i / 3) < ((j + 1) * (j + 1)) ^ j, j ^ 2 < (j + 1) * (j + 1), j < 36, 0 < j, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < i, 2 * i < (j + 1) * (j + 1), 4 ^ (j / 6) < (j + 1) * (j + 1), (4 ^ (j / 6)) ^ j < ((j + 1) * (j + 1)) ^ j, (4 ^ (j / 6)) ^ j ≤ (2 * i) ^ j, j / 6 * j ≤ i / 3, sqrt(2048) ≤ j, 0 ≤ 4 ^ (j / 6), (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), j ^ 2 / 6 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 4 ^ (i / 3) ≤ (2 * i) ^ j, 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ j ^ 2 / 6, 0 ≤ j, 1024 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) 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-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 0 ≤ i * i; (s) j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ 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 ∧ 0 ≤ j → ((* j) ≤ (* i) * i0 ↔ (i + j - 1) / i ≤ i0); (s)

Proof step 34 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ i ^2 ≤ j → ¬ sqrt(j) < i

• Proof step 36:

  2 * i = j * j + j0, (4 ^ (j / 6)) ^ j < ((j + 1) * (j + 1)) ^ j, 4 ^ (j / 6) < (j + 1) * (j + 1), 2 * i < (j + 1) * (j + 1), 0 < i, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < j, j < 36, j ^ 2 < (j + 1) * (j + 1), 4 ^ (i / 3) < ((j + 1) * (j + 1)) ^ j, 0 < (j + 1) * (j + 1), sqrt(2048) < 36, 1024 ≤ i, 0 ≤ j, j / 6 * j ≤ j ^ 2 / 6, j ^ 2 ≤ 2 * i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ j, j0 ≤ 2 * j, 0 ≤ j0, j ^ 2 / 2 ≤ i, j ^ 2 / 6 ≤ i / 3, (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), 0 ≤ 4 ^ (j / 6), sqrt(2048) ≤ j, j / 6 * j ≤ i / 3, (4 ^ (j / 6)) ^ j ≤ (2 * i) ^ j, ¬ 36 ^2 ≤ 2048 ⊦

Rule argument

Additional information

Used terms: 36, 2048

Proof step 35 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof pot-root-est (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  2 * i = j * j + j0, sqrt(2048) < 36, 0 < (j + 1) * (j + 1), 4 ^ (i / 3) < ((j + 1) * (j + 1)) ^ j, j ^ 2 < (j + 1) * (j + 1), j < 36, 0 < j, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < i, 2 * i < (j + 1) * (j + 1), 4 ^ (j / 6) < (j + 1) * (j + 1), (4 ^ (j / 6)) ^ j < ((j + 1) * (j + 1)) ^ j, 2048 < 36 ^2, 0 < 36 ^2, 1 < 36 ^2, (4 ^ (j / 6)) ^ j ≤ (2 * i) ^ j, j / 6 * j ≤ i / 3, sqrt(2048) ≤ j, 0 ≤ 4 ^ (j / 6), (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), j ^ 2 / 6 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 4 ^ (i / 3) ≤ (2 * i) ^ j, 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ j ^ 2 / 6, 0 ≤ j, 1024 ≤ i ⊦

Rule argument

Additional information

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

Proof step 37 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ i ^2 = i * i

Rule argument

Additional information

Used simplifier rules: associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 36

Proof step 38 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ i ≤ j ∧ 0 ≤ i ∧ 0 ≤ j → sqrt(i) ≤ sqrt(j)

Rule argument

Additional information

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

Proof step 40 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

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

• Proof step 43:

  2 * i = j * j + j0, j = sqrt(2 * i), (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 < i, 2 * i < (j + 1) ^ 2, 1 < 4, (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, j ^ 2 ≤ 2 * i, j * j / 6 ≤ (j ^ 2 / 2) / 3, 0 ≤ j * j / 6, ¬ j * j / 6 ≤ i / 3 ⊦

Rule argument

Additional information

Used simplifier rules: j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 0 ≤ i → (0 ≤ i * j ↔ i = 0 ∨ 0 ≤ j); (s) ⊦ 0 < i → sqrt(2 * i) ≠ 0; (s) ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i / j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i / 3, j * j / 6, 4

Proof step 42 from proof pot-root-est (previous step) (back to tree)

Lemma le-pos

Proof step 43 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ i → (0 ≤ i * j ↔ i = 0 ∨ 0 ≤ j); (s) ⊦ 0 < i → sqrt(2 * i) ≠ 0; (s) ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i / j; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 0 < j ∧ 0 ≤ i → (i / (* j) < j0 ↔ i < j * j0); (s) j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: (j ^ 2 / 2) / 3, i / 3, j * j / 6

Proof step 44 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ i ^ 2 = i * i

Rule argument

Additional information

Used simplifier rules: j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → i * i0 / j ≤ (i * i0) / j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j

Proof step 46 from proof pot-root-est (previous step) (back to tree)

Lemma pot-square-04

Proof step 47 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  0 < j0, 0 ≤ i, i ≤ j ⊦ i / j0 ≤ j / j0

Rule argument

Additional information

Used simplifier rules: notneg: ⊦ 0 ≤ i ∧ 0 ≤ j → ¬ i ^ j < 0; j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ 0 < j ∧ 0 ≤ i → (i / (* j) < j0 ↔ i < j * j0); (s) ⊦ 0 ≤ i / 2 ↔ ~1 ≤ i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 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-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs Used terms: i, 3, j ^ 2 / 2

Proof step 48 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

  ⊦ i ^ 2 = i * i

• Proof step 51:

  2 * i = j * j + j0, j = sqrt(2 * i), 2 * i < (j + 1) ^ 2, 0 < i, (2 * i) ^ j < ((j + 1) ^ 2) ^ j, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, ¬ j * j ≤ 2 * i ⊦

Rule argument

Additional information

Used terms: j

Proof step 50 from proof pot-root-est (previous step) (back to tree)

Lemma pot-square-04

Proof step 51 from proof pot-root-est (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 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

Proof step 52 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 53:

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

• Proof step 54:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < i, 2 * i < (j + 1) ^ 2, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, ¬ (2 * i) ^ j < ((j + 1) ^ 2) ^ j ⊦ 0 ≤ 2 * i ∧ 0 ≤ (j + 1) ^ 2 ∧ 0 < j

Rule argument

Additional information

Used terms: (j + 1) ^ 2, j, 2 * i

Proof step 53 from proof pot-root-est (previous step) (back to tree)

Lemma ls-pos-03

Proof step 54 from proof pot-root-est (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  2 * i = sqrt(2 * i) * sqrt(2 * i) + j0, (sqrt(2 * i) + 1) ^ 2 < 0, 0 < sqrt(2 * i), 2 * i < (sqrt(2 * i) + 1) ^ 2, 0 < i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * sqrt(2 * i), 0 ≤ sqrt(2 * i), 0 ≤ j0, ((sqrt(2 * i) + 1) ^ 2) ^ sqrt(2 * i) ≤ (2 * i) ^ sqrt(2 * i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-05: ⊦ 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 ↔ ¬ j < i; (ss) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → ¬ sqrt(2 * i) ≤ 0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs

Proof step 55 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ i ^ 2 = i * i

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ i * i < 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: sqrt(2 * i) + 1

Proof step 56 from proof pot-root-est (previous step) (back to tree)

Lemma pot-square-04

Proof step 57 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ i ^ 2 = i * i

• Proof step 59:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < i, 0 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 1024 ≤ i, j0 ≤ 2 * j, 0 ≤ j, 0 ≤ j0, ¬ 2 * i < (j + 1) * (j + 1) ⊦

Rule argument

Additional information

Used terms: j + 1

Proof step 58 from proof pot-root-est (previous step) (back to tree)

Lemma pot-square-04

Proof step 59 from proof pot-root-est (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

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

• Proof step 61:

  2 * i = j * j + j0, j = sqrt(2 * i), 0 < i, 0 ≤ j0, 0 ≤ j, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i), 0 ≤ i, ¬ 2 * i < j * (j + 1) + 1 * (j + 1) ⊦

Rule argument

Additional information

Used terms: j + 1, 1, j

Proof step 60 from proof pot-root-est (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof pot-root-est (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i * j + i0 < i * (j + j1) + j0 ↔ i0 < i * j1 + j0; (s) ⊦ 1 * i = i; (s) ⊦ i + i = 2 * i; (s) ⊦ i < j + 1 ↔ i ≤ j; (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 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2