\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 r215706 = 1.0;
double r215707 = 5.0;
double r215708 = v;
double r215709 = r215708 * r215708;
double r215710 = r215707 * r215709;
double r215711 = r215706 - r215710;
double r215712 = r215709 - r215706;
double r215713 = r215711 / r215712;
double r215714 = acos(r215713);
return r215714;
}
double f(double v) {
double r215715 = 1.0;
double r215716 = 5.0;
double r215717 = v;
double r215718 = r215717 * r215717;
double r215719 = r215716 * r215718;
double r215720 = r215715 - r215719;
double r215721 = sqrt(r215720);
double r215722 = r215718 - r215715;
double r215723 = r215721 / r215722;
double r215724 = r215721 * r215723;
double r215725 = acos(r215724);
return r215725;
}



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
(FPCore (v)
:name "Falkner and Boettcher, Appendix B, 1"
:precision binary64
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))