\sqrt{x - 1} \cdot \sqrt{x}x - \left(0.5 + 0.125 \cdot \frac{1}{x}\right)double f(double x) {
double r2491 = x;
double r2492 = 1.0;
double r2493 = r2491 - r2492;
double r2494 = sqrt(r2493);
double r2495 = sqrt(r2491);
double r2496 = r2494 * r2495;
return r2496;
}
double f(double x) {
double r2497 = x;
double r2498 = 0.5;
double r2499 = 0.125;
double r2500 = 1.0;
double r2501 = r2500 / r2497;
double r2502 = r2499 * r2501;
double r2503 = r2498 + r2502;
double r2504 = r2497 - r2503;
return r2504;
}



Bits error versus x
Results
Initial program 0.5
Taylor expanded around inf 0.4
Final simplification0.4
herbie shell --seed 2020027
(FPCore (x)
:name "sqrt times"
:precision binary64
(* (sqrt (- x 1)) (sqrt x)))