\frac{1 - \cos x}{x \cdot x}\tan \left(\frac{x}{2}\right) \cdot \frac{\frac{\sin x}{x}}{x}double f(double x) {
double r3800538 = 1.0;
double r3800539 = x;
double r3800540 = cos(r3800539);
double r3800541 = r3800538 - r3800540;
double r3800542 = r3800539 * r3800539;
double r3800543 = r3800541 / r3800542;
return r3800543;
}
double f(double x) {
double r3800544 = x;
double r3800545 = 2.0;
double r3800546 = r3800544 / r3800545;
double r3800547 = tan(r3800546);
double r3800548 = sin(r3800544);
double r3800549 = r3800548 / r3800544;
double r3800550 = r3800549 / r3800544;
double r3800551 = r3800547 * r3800550;
return r3800551;
}



Bits error versus x
Results
Initial program 30.9
rmApplied flip--31.0
Applied associate-/l/31.0
Simplified14.7
Taylor expanded around -inf 14.7
Simplified0.3
rmApplied associate-*l/0.3
Applied associate-/l/0.3
rmApplied times-frac0.4
Simplified0.2
Final simplification0.2
herbie shell --seed 2019104 +o rules:numerics
(FPCore (x)
:name "cos2 (problem 3.4.1)"
(/ (- 1 (cos x)) (* x x)))