\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)
\left(a2 \cdot \frac{a2}{\sqrt{2}} + a1 \cdot \frac{a1}{\sqrt{2}}\right) \cdot \cos th
(FPCore (a1 a2 th) :precision binary64 (+ (* (/ (cos th) (sqrt 2.0)) (* a1 a1)) (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))
(FPCore (a1 a2 th) :precision binary64 (* (+ (* a2 (/ a2 (sqrt 2.0))) (* a1 (/ a1 (sqrt 2.0)))) (cos th)))
double code(double a1, double a2, double th) {
return ((cos(th) / sqrt(2.0)) * (a1 * a1)) + ((cos(th) / sqrt(2.0)) * (a2 * a2));
}
double code(double a1, double a2, double th) {
return ((a2 * (a2 / sqrt(2.0))) + (a1 * (a1 / sqrt(2.0)))) * cos(th);
}



Bits error versus a1



Bits error versus a2



Bits error versus th
Results
Initial program 0.5
Simplified0.5
Proof
Taylor expanded in th around inf 0.5
Simplified0.5
Proof
Taylor expanded in a1 around 0 0.5
Simplified0.5
Proof
Applied associate-/r/_binary640.5
Final simplification0.5
herbie shell --seed 2022004
(FPCore (a1 a2 th)
:name "Migdal et al, Equation (64)"
:precision binary64
(+ (* (/ (cos th) (sqrt 2.0)) (* a1 a1)) (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))