\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 r310084 = 1.0;
double r310085 = 5.0;
double r310086 = v;
double r310087 = r310086 * r310086;
double r310088 = r310085 * r310087;
double r310089 = r310084 - r310088;
double r310090 = r310087 - r310084;
double r310091 = r310089 / r310090;
double r310092 = acos(r310091);
return r310092;
}
double f(double v) {
double r310093 = 1.0;
double r310094 = 5.0;
double r310095 = v;
double r310096 = r310095 * r310095;
double r310097 = r310094 * r310096;
double r310098 = r310093 - r310097;
double r310099 = sqrt(r310098);
double r310100 = r310096 - r310093;
double r310101 = r310099 / r310100;
double r310102 = r310099 * r310101;
double r310103 = acos(r310102);
return r310103;
}



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
(FPCore (v)
:name "Falkner and Boettcher, Appendix B, 1"
:precision binary64
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))