\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)double f(double v) {
double r274129 = 1.0;
double r274130 = 5.0;
double r274131 = v;
double r274132 = r274131 * r274131;
double r274133 = r274130 * r274132;
double r274134 = r274129 - r274133;
double r274135 = r274132 - r274129;
double r274136 = r274134 / r274135;
double r274137 = acos(r274136);
return r274137;
}
double f(double v) {
double r274138 = 1.0;
double r274139 = 5.0;
double r274140 = v;
double r274141 = r274140 * r274140;
double r274142 = r274139 * r274141;
double r274143 = r274138 - r274142;
double r274144 = r274141 - r274138;
double r274145 = r274143 / r274144;
double r274146 = acos(r274145);
return r274146;
}



Bits error versus v
Results
Initial program 0.5
Final simplification0.5
herbie shell --seed 2020001 +o rules:numerics
(FPCore (v)
:name "Falkner and Boettcher, Appendix B, 1"
:precision binary64
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))