\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\cos^{-1} \left(\sqrt{1 - 5 \cdot \left(v \cdot v\right)} \cdot \frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{v \cdot v - 1}\right)double f(double v) {
double r212427 = 1.0;
double r212428 = 5.0;
double r212429 = v;
double r212430 = r212429 * r212429;
double r212431 = r212428 * r212430;
double r212432 = r212427 - r212431;
double r212433 = r212430 - r212427;
double r212434 = r212432 / r212433;
double r212435 = acos(r212434);
return r212435;
}
double f(double v) {
double r212436 = 1.0;
double r212437 = 5.0;
double r212438 = v;
double r212439 = r212438 * r212438;
double r212440 = r212437 * r212439;
double r212441 = r212436 - r212440;
double r212442 = sqrt(r212441);
double r212443 = r212439 - r212436;
double r212444 = r212442 / r212443;
double r212445 = r212442 * r212444;
double r212446 = acos(r212445);
return r212446;
}



Bits error versus v
Results
Initial program 0.5
rmApplied *-un-lft-identity0.5
Applied add-sqr-sqrt0.6
Applied times-frac0.6
Simplified0.6
Final simplification0.6
herbie shell --seed 2020047 +o rules:numerics
(FPCore (v)
:name "Falkner and Boettcher, Appendix B, 1"
:precision binary64
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))