Initial program 16.7
\[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U
\]
Simplified16.7
\[\leadsto \color{blue}{\mathsf{fma}\left(J \cdot \left(e^{\ell} - e^{-\ell}\right), \cos \left(\frac{K}{2}\right), U\right)}
\]
Proof
(fma.f64 (*.f64 J (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l)))) (cos.f64 (/.f64 K 2)) U): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 J (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l)))) (cos.f64 (/.f64 K 2))) U)): 1 points increase in error, 0 points decrease in error
Applied egg-rr0.1
\[\leadsto \color{blue}{\left(J \cdot \left(2 \cdot \sinh \ell\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U}
\]
Simplified0.1
\[\leadsto \color{blue}{\mathsf{fma}\left(J, \left(2 \cdot \sinh \ell\right) \cdot \cos \left(\frac{K}{2}\right), U\right)}
\]
Proof
(fma.f64 J (*.f64 (*.f64 2 (sinh.f64 l)) (cos.f64 (/.f64 K 2))) U): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 J (*.f64 (*.f64 2 (sinh.f64 l)) (cos.f64 (/.f64 K 2)))) U)): 2 points increase in error, 1 points decrease in error
(+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 J (*.f64 2 (sinh.f64 l))) (cos.f64 (/.f64 K 2)))) U): 7 points increase in error, 6 points decrease in error
Final simplification0.1
\[\leadsto \mathsf{fma}\left(J, \left(2 \cdot \sinh \ell\right) \cdot \cos \left(\frac{K}{2}\right), U\right)
\]