\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)double f(double v) {
double r358877 = 1.0;
double r358878 = 5.0;
double r358879 = v;
double r358880 = r358879 * r358879;
double r358881 = r358878 * r358880;
double r358882 = r358877 - r358881;
double r358883 = r358880 - r358877;
double r358884 = r358882 / r358883;
double r358885 = acos(r358884);
return r358885;
}
double f(double v) {
double r358886 = atan2(1.0, 0.0);
double r358887 = 2.0;
double r358888 = r358886 / r358887;
double r358889 = 1.0;
double r358890 = 5.0;
double r358891 = v;
double r358892 = r358891 * r358891;
double r358893 = r358890 * r358892;
double r358894 = r358889 - r358893;
double r358895 = r358892 - r358889;
double r358896 = r358894 / r358895;
double r358897 = asin(r358896);
double r358898 = r358888 - r358897;
return r358898;
}



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