Initial program 0.5
\[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)
\]
Simplified0.5
\[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}
\]
Proof
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 2)) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 2)) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 2)) (*.f64 a2 a2)))): 0 points increase in error, 2 points decrease in error
Applied egg-rr0.5
\[\leadsto \color{blue}{\mathsf{fma}\left(\cos th, {2}^{-0.5} \cdot \left(a2 \cdot a2\right), \frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right)\right)}
\]
Simplified0.6
\[\leadsto \color{blue}{\mathsf{fma}\left(\cos th, a2 \cdot \left(a2 \cdot {2}^{-0.5}\right), \frac{\cos th}{\frac{\sqrt{2}}{a1 \cdot a1}}\right)}
\]
Proof
(fma.f64 (cos.f64 th) (*.f64 a2 (*.f64 a2 (pow.f64 2 -1/2))) (/.f64 (cos.f64 th) (/.f64 (sqrt.f64 2) (*.f64 a1 a1)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 th) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a2 a2) (pow.f64 2 -1/2))) (/.f64 (cos.f64 th) (/.f64 (sqrt.f64 2) (*.f64 a1 a1)))): 21 points increase in error, 11 points decrease in error
(fma.f64 (cos.f64 th) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 2 -1/2) (*.f64 a2 a2))) (/.f64 (cos.f64 th) (/.f64 (sqrt.f64 2) (*.f64 a1 a1)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 th) (*.f64 (pow.f64 2 -1/2) (*.f64 a2 a2)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (cos.f64 th) (*.f64 a1 a1)) (sqrt.f64 2)))): 15 points increase in error, 18 points decrease in error
(fma.f64 (cos.f64 th) (*.f64 (pow.f64 2 -1/2) (*.f64 a2 a2)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 2)) (*.f64 a1 a1)))): 18 points increase in error, 8 points decrease in error
Final simplification0.6
\[\leadsto \mathsf{fma}\left(\cos th, a2 \cdot \left(a2 \cdot {2}^{-0.5}\right), \frac{\cos th}{\frac{\sqrt{2}}{a1 \cdot a1}}\right)
\]