\sqrt{x - 1} \cdot \sqrt{x}x - \left(\frac{0.125}{x} + 0.5\right)double f(double x) {
double r9863 = x;
double r9864 = 1.0;
double r9865 = r9863 - r9864;
double r9866 = sqrt(r9865);
double r9867 = sqrt(r9863);
double r9868 = r9866 * r9867;
return r9868;
}
double f(double x) {
double r9869 = x;
double r9870 = 0.125;
double r9871 = r9870 / r9869;
double r9872 = 0.5;
double r9873 = r9871 + r9872;
double r9874 = r9869 - r9873;
return r9874;
}



Bits error versus x
Results
Initial program 0.5
Taylor expanded around inf 0.3
Simplified0.3
Final simplification0.3
herbie shell --seed 2020045 +o rules:numerics
(FPCore (x)
:name "sqrt times"
:precision binary64
(* (sqrt (- x 1)) (sqrt x)))