\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)(FPCore (v) :precision binary64 (acos (/ (- 1.0 (* 5.0 (* v v))) (- (* v v) 1.0))))
(FPCore (v) :precision binary64 (- (/ PI 2.0) (asin (/ (- 1.0 (* 5.0 (* v v))) (- (* v v) 1.0)))))
double code(double v) {
return ((double) acos((((double) (1.0 - ((double) (5.0 * ((double) (v * v)))))) / ((double) (((double) (v * v)) - 1.0)))));
}
double code(double v) {
return ((double) ((((double) M_PI) / 2.0) - ((double) asin((((double) (1.0 - ((double) (5.0 * ((double) (v * v)))))) / ((double) (((double) (v * v)) - 1.0)))))));
}



Bits error versus v
Results
Initial program Error: 0.6 bits
rmApplied acos-asinError: 0.6 bits
Final simplificationError: 0.6 bits
herbie shell --seed 2020204
(FPCore (v)
:name "Falkner and Boettcher, Appendix B, 1"
:precision binary64
(acos (/ (- 1.0 (* 5.0 (* v v))) (- (* v v) 1.0))))