Average Error: 20.2 → 0.2
Time: 1.4m
Precision: 64
Internal Precision: 1088
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\begin{array}{l} \mathbf{if}\;\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \le 0.0048865480386920505:\\ \;\;\;\;\frac{1}{(x \cdot \left(\frac{\frac{x + 1}{\sqrt{x}}}{x}\right) + \left(\frac{x}{\sqrt{x + 1}}\right))_*} \cdot \left(\frac{1}{\sqrt{x}} \cdot \frac{1}{\sqrt{x}} + \left(\frac{1}{\sqrt{x + 1}} \cdot \frac{1}{\sqrt{x + 1}} - \frac{1}{\sqrt{x}} \cdot \frac{1}{\sqrt{x + 1}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;{x}^{\left(-\frac{1}{2}\right)} - \frac{1}{\sqrt{x + 1}}\\ \end{array}\]

Error

Bits error versus x

Target

Original20.2
Target0.7
Herbie0.2
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Split input into 2 regimes

  2. if (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))) < 0.0048865480386920505

    1. Initial program 39.9

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

    3. Applied flip--39.9

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

    4. Applied simplify39.8

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

    6. Applied frac-sub38.4

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

    7. Applied simplify10.6

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

    8. Applied simplify10.6

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

    10. Applied associate-/l/10.6

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

    12. Applied flip3-+29.1

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

    13. Applied associate-*l/29.1

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

    14. Applied associate-/r/29.1

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

    15. Applied simplify0.5

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

    if 0.0048865480386920505 < (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))

    1. Initial program 0.3

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

    3. Applied pow1/20.3

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

    4. Applied pow-flip0.0

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

Runtime

Time bar (total: 1.4m)Debug logProfile

herbie shell --seed 2018199 +o rules:numerics
(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)))))