Average Error: 20.1 → 0.4
Time: 14.2s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\frac{\frac{1}{1 \cdot \left(\sqrt{x + 1} + \sqrt{x}\right)}}{\sqrt{x} \cdot \sqrt{x + 1}}\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\frac{\frac{1}{1 \cdot \left(\sqrt{x + 1} + \sqrt{x}\right)}}{\sqrt{x} \cdot \sqrt{x + 1}}
double f(double x) {
        double r99807 = 1.0;
        double r99808 = x;
        double r99809 = sqrt(r99808);
        double r99810 = r99807 / r99809;
        double r99811 = r99808 + r99807;
        double r99812 = sqrt(r99811);
        double r99813 = r99807 / r99812;
        double r99814 = r99810 - r99813;
        return r99814;
}
↓
double f(double x) {
        double r99815 = 1.0;
        double r99816 = x;
        double r99817 = r99816 + r99815;
        double r99818 = sqrt(r99817);
        double r99819 = sqrt(r99816);
        double r99820 = r99818 + r99819;
        double r99821 = r99815 * r99820;
        double r99822 = r99815 / r99821;
        double r99823 = r99819 * r99818;
        double r99824 = r99822 / r99823;
        return r99824;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

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

Derivation

  1. Initial program 20.1

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

  3. Applied frac-sub20.1

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

  5. Applied flip--19.9

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

  6. Simplified19.5

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

  7. Simplified19.5

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

  8. Taylor expanded around 0 0.4

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

  9. Final simplification0.4

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

Reproduce

herbie shell --seed 2019347 +o rules:numerics
(FPCore (x)
  :name "2isqrt (example 3.6)"
  :precision binary64

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

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