\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 r321909 = 1.0;
double r321910 = 5.0;
double r321911 = v;
double r321912 = r321911 * r321911;
double r321913 = r321910 * r321912;
double r321914 = r321909 - r321913;
double r321915 = r321912 - r321909;
double r321916 = r321914 / r321915;
double r321917 = acos(r321916);
return r321917;
}
double f(double v) {
double r321918 = 1.0;
double r321919 = 5.0;
double r321920 = v;
double r321921 = r321920 * r321920;
double r321922 = r321919 * r321921;
double r321923 = r321918 - r321922;
double r321924 = sqrt(r321923);
double r321925 = r321921 - r321918;
double r321926 = r321924 / r321925;
double r321927 = r321924 * r321926;
double r321928 = acos(r321927);
return r321928;
}



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