Initial program 7.4
\[\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.im + \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.re
\]
Taylor expanded in x.re around 0 7.5
\[\leadsto \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.im + \color{blue}{2 \cdot \left({x.re}^{2} \cdot x.im\right)}
\]
Simplified7.5
\[\leadsto \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.im + \color{blue}{x.im \cdot \left(x.re \cdot \left(x.re \cdot 2\right)\right)}
\]
Proof
(*.f64 x.im (*.f64 x.re (*.f64 x.re 2))): 0 points increase in error, 0 points decrease in error
(*.f64 x.im (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x.re x.re) 2))): 0 points increase in error, 1 points decrease in error
(*.f64 x.im (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 x.re 2)) 2)): 0 points increase in error, 0 points decrease in error
(*.f64 x.im (Rewrite<= *-commutative_binary64 (*.f64 2 (pow.f64 x.re 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 (pow.f64 x.re 2)) x.im)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 (pow.f64 x.re 2) x.im))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.2
\[\leadsto \color{blue}{\mathsf{fma}\left(x.im + x.re, \left(x.re - x.im\right) \cdot x.im, \left(x.re + x.re\right) \cdot \left(x.im \cdot x.re\right)\right)}
\]
Final simplification0.2
\[\leadsto \mathsf{fma}\left(x.im + x.re, x.im \cdot \left(x.re - x.im\right), \left(x.re + x.re\right) \cdot \left(x.im \cdot x.re\right)\right)
\]