\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 r334755 = 1.0;
double r334756 = 5.0;
double r334757 = v;
double r334758 = r334757 * r334757;
double r334759 = r334756 * r334758;
double r334760 = r334755 - r334759;
double r334761 = r334758 - r334755;
double r334762 = r334760 / r334761;
double r334763 = acos(r334762);
return r334763;
}
double f(double v) {
double r334764 = 1.0;
double r334765 = 5.0;
double r334766 = v;
double r334767 = r334766 * r334766;
double r334768 = r334765 * r334767;
double r334769 = r334764 - r334768;
double r334770 = sqrt(r334769);
double r334771 = r334767 - r334764;
double r334772 = r334770 / r334771;
double r334773 = r334770 * r334772;
double r334774 = acos(r334773);
return r334774;
}



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))))