Initial program 0.0
\[x.re \cdot y.im + x.im \cdot y.re
\]
Taylor expanded in x.re around 0 0.0
\[\leadsto \color{blue}{x.re \cdot y.im + y.re \cdot x.im}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(y.re, x.im, x.re \cdot y.im\right)}
\]
Proof
(fma.f64 y.re x.im (*.f64 x.re y.im)): 0 points increase in error, 0 points decrease in error
(Rewrite=> fma-udef_binary64 (+.f64 (*.f64 y.re x.im) (*.f64 x.re y.im))): 1 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 x.im y.re)) (*.f64 x.re y.im)): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 (*.f64 x.re y.im) (*.f64 x.im y.re))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x.re y.im) (Rewrite=> *-commutative_binary64 (*.f64 y.re x.im))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{fma}\left(y.re, x.im, x.re \cdot y.im\right)
\]