Average Error: 19.6 → 19.5
Time: 40.3s
Precision: 64
Internal Precision: 1152
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \le 4.910961156792346 \cdot 10^{+97}:\\ \;\;\;\;\frac{\sqrt{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{\sqrt{x + 1}} - \sqrt{\sqrt{x \cdot x + \left(1 - x\right)}} \cdot \left(\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}\right)}{\sqrt{\sqrt{x \cdot x - \left(x - 1\right)}} \cdot \left(\sqrt{x + 1} \cdot \sqrt{x}\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{\left(\left(1 - \frac{\sqrt{\frac{1}{\sqrt{x + 1}}}}{\frac{\sqrt{\sqrt{x + 1}}}{\sqrt{x} \cdot \sqrt{1}}}\right) \cdot \left(1 - \frac{\sqrt{\frac{1}{\sqrt{x + 1}}}}{\frac{\sqrt{\sqrt{x + 1}}}{\sqrt{x} \cdot \sqrt{1}}}\right)\right) \cdot \frac{1 - \frac{\sqrt{\frac{1}{\sqrt{x + 1}}}}{\frac{\sqrt{\sqrt{x + 1}}}{\sqrt{x} \cdot \sqrt{1}}}}{x \cdot \sqrt{x}}}\\ \end{array}\]

Error

Bits error versus x

Target

Original19.6
Target0.6
Herbie19.5
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Split input into 2 regimes

  2. if x < 4.910961156792346e+97

    1. Initial program 13.4

      \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt13.3

      \[\leadsto \frac{1}{\sqrt{x}} - \color{blue}{\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}}\]
    4. Using strategy rm

    5. Applied sqrt-div13.3

      \[\leadsto \frac{1}{\sqrt{x}} - \sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \color{blue}{\frac{\sqrt{1}}{\sqrt{\sqrt{x + 1}}}}\]

    6. Applied associate-*r/13.3

      \[\leadsto \frac{1}{\sqrt{x}} - \color{blue}{\frac{\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{1}}{\sqrt{\sqrt{x + 1}}}}\]

    7. Applied frac-sub13.3

      \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{\sqrt{x + 1}} - \sqrt{x} \cdot \left(\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{1}\right)}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}}\]

    8. Applied simplify13.3

      \[\leadsto \frac{\color{blue}{\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]
    9. Using strategy rm

    10. Applied sqrt-div13.3

      \[\leadsto \frac{\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \color{blue}{\frac{\sqrt{1}}{\sqrt{\sqrt{x + 1}}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]

    11. Applied associate-*r/13.3

      \[\leadsto \frac{\sqrt{\sqrt{x + 1}} - \color{blue}{\frac{\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}}{\sqrt{\sqrt{x + 1}}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]

    12. Applied flip3-+13.3

      \[\leadsto \frac{\sqrt{\sqrt{\color{blue}{\frac{{x}^{3} + {1}^{3}}{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}}}} - \frac{\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}}{\sqrt{\sqrt{x + 1}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]

    13. Applied sqrt-div13.3

      \[\leadsto \frac{\sqrt{\color{blue}{\frac{\sqrt{{x}^{3} + {1}^{3}}}{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}}}} - \frac{\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}}{\sqrt{\sqrt{x + 1}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]

    14. Applied sqrt-div13.3

      \[\leadsto \frac{\color{blue}{\frac{\sqrt{\sqrt{{x}^{3} + {1}^{3}}}}{\sqrt{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}}}} - \frac{\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}}{\sqrt{\sqrt{x + 1}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]

    15. Applied frac-sub13.1

      \[\leadsto \frac{\color{blue}{\frac{\sqrt{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{\sqrt{x + 1}} - \sqrt{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}} \cdot \left(\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}\right)}{\sqrt{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}} \cdot \sqrt{\sqrt{x + 1}}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]

    16. Applied associate-/l/13.1

      \[\leadsto \color{blue}{\frac{\sqrt{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{\sqrt{x + 1}} - \sqrt{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}} \cdot \left(\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}\right)}{\left(\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \left(\sqrt{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}} \cdot \sqrt{\sqrt{x + 1}}\right)}}\]

    17. Applied simplify13.1

      \[\leadsto \frac{\sqrt{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{\sqrt{x + 1}} - \sqrt{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}} \cdot \left(\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}\right)}{\color{blue}{\sqrt{\sqrt{x \cdot x - \left(x - 1\right)}} \cdot \left(\sqrt{x + 1} \cdot \sqrt{x}\right)}}\]

    if 4.910961156792346e+97 < x

    1. Initial program 32.3

      \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt46.1

      \[\leadsto \frac{1}{\sqrt{x}} - \color{blue}{\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}}\]
    4. Using strategy rm

    5. Applied sqrt-div44.1

      \[\leadsto \frac{1}{\sqrt{x}} - \sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \color{blue}{\frac{\sqrt{1}}{\sqrt{\sqrt{x + 1}}}}\]

    6. Applied associate-*r/40.7

      \[\leadsto \frac{1}{\sqrt{x}} - \color{blue}{\frac{\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{1}}{\sqrt{\sqrt{x + 1}}}}\]

    7. Applied frac-sub40.9

      \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{\sqrt{x + 1}} - \sqrt{x} \cdot \left(\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{1}\right)}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}}\]

    8. Applied simplify40.9

      \[\leadsto \frac{\color{blue}{\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}}}{\sqrt{x} \cdot \sqrt{\sqrt{x + 1}}}\]
    9. Using strategy rm

    10. Applied add-cbrt-cube40.9

      \[\leadsto \frac{\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}}{\sqrt{x} \cdot \color{blue}{\sqrt[3]{\left(\sqrt{\sqrt{x + 1}} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \sqrt{\sqrt{x + 1}}}}}\]

    11. Applied add-cbrt-cube32.6

      \[\leadsto \frac{\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}}{\color{blue}{\sqrt[3]{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \sqrt{x}}} \cdot \sqrt[3]{\left(\sqrt{\sqrt{x + 1}} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \sqrt{\sqrt{x + 1}}}}\]

    12. Applied cbrt-unprod32.4

      \[\leadsto \frac{\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}}{\color{blue}{\sqrt[3]{\left(\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \sqrt{x}\right) \cdot \left(\left(\sqrt{\sqrt{x + 1}} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \sqrt{\sqrt{x + 1}}\right)}}}\]

    13. Applied add-cbrt-cube32.4

      \[\leadsto \frac{\color{blue}{\sqrt[3]{\left(\left(\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right) \cdot \left(\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)\right) \cdot \left(\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)}}}{\sqrt[3]{\left(\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \sqrt{x}\right) \cdot \left(\left(\sqrt{\sqrt{x + 1}} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \sqrt{\sqrt{x + 1}}\right)}}\]

    14. Applied cbrt-undiv32.4

      \[\leadsto \color{blue}{\sqrt[3]{\frac{\left(\left(\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right) \cdot \left(\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)\right) \cdot \left(\sqrt{\sqrt{x + 1}} - \left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)}{\left(\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \sqrt{x}\right) \cdot \left(\left(\sqrt{\sqrt{x + 1}} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \sqrt{\sqrt{x + 1}}\right)}}}\]

    15. Applied simplify32.5

      \[\leadsto \sqrt[3]{\color{blue}{\frac{1 - \frac{\sqrt{\frac{1}{\sqrt{1 + x}}}}{\frac{\sqrt{\sqrt{1 + x}}}{\sqrt{1} \cdot \sqrt{x}}}}{\sqrt{x} \cdot x} \cdot \left(\left(1 - \frac{\sqrt{\frac{1}{\sqrt{1 + x}}}}{\frac{\sqrt{\sqrt{1 + x}}}{\sqrt{1} \cdot \sqrt{x}}}\right) \cdot \left(1 - \frac{\sqrt{\frac{1}{\sqrt{1 + x}}}}{\frac{\sqrt{\sqrt{1 + x}}}{\sqrt{1} \cdot \sqrt{x}}}\right)\right)}}\]
  3. Recombined 2 regimes into one program.

  4. Applied simplify19.5

    \[\leadsto \color{blue}{\begin{array}{l} \mathbf{if}\;x \le 4.910961156792346 \cdot 10^{+97}:\\ \;\;\;\;\frac{\sqrt{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{\sqrt{x + 1}} - \sqrt{\sqrt{x \cdot x + \left(1 - x\right)}} \cdot \left(\left(\sqrt{x} \cdot \sqrt{1}\right) \cdot \sqrt{1}\right)}{\sqrt{\sqrt{x \cdot x - \left(x - 1\right)}} \cdot \left(\sqrt{x + 1} \cdot \sqrt{x}\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{\left(\left(1 - \frac{\sqrt{\frac{1}{\sqrt{x + 1}}}}{\frac{\sqrt{\sqrt{x + 1}}}{\sqrt{x} \cdot \sqrt{1}}}\right) \cdot \left(1 - \frac{\sqrt{\frac{1}{\sqrt{x + 1}}}}{\frac{\sqrt{\sqrt{x + 1}}}{\sqrt{x} \cdot \sqrt{1}}}\right)\right) \cdot \frac{1 - \frac{\sqrt{\frac{1}{\sqrt{x + 1}}}}{\frac{\sqrt{\sqrt{x + 1}}}{\sqrt{x} \cdot \sqrt{1}}}}{x \cdot \sqrt{x}}}\\ \end{array}}\]

Runtime

Time bar (total: 40.3s)Debug logProfile

herbie shell --seed '#(1070258749 1877548225 2229079127 1588002776 3179087814 1886870650)' 
(FPCore (x)
  :name "2isqrt (example 3.6)"

  :herbie-target
  (/ 1 (+ (* (+ x 1) (sqrt x)) (* x (sqrt (+ x 1)))))

  (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))