Initial program 26.7
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
\]
Applied egg-rr22.6
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)}, \frac{x.im \cdot y.re}{\mathsf{hypot}\left(y.re, y.im\right)}, -\frac{x.re \cdot y.im}{{\left(\mathsf{hypot}\left(y.re, y.im\right)\right)}^{2}}\right)}
\]
Simplified13.2
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)}, \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot y.re, \frac{x.re}{\frac{{\left(\mathsf{hypot}\left(y.re, y.im\right)\right)}^{2}}{-y.im}}\right)}
\]
Proof
(fma.f64 (/.f64 1 (hypot.f64 y.re y.im)) (*.f64 (/.f64 x.im (hypot.f64 y.re y.im)) y.re) (/.f64 x.re (/.f64 (pow.f64 (hypot.f64 y.re y.im) 2) (neg.f64 y.im)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 1 (hypot.f64 y.re y.im)) (Rewrite<= associate-/r/_binary64 (/.f64 x.im (/.f64 (hypot.f64 y.re y.im) y.re))) (/.f64 x.re (/.f64 (pow.f64 (hypot.f64 y.re y.im) 2) (neg.f64 y.im)))): 11 points increase in error, 6 points decrease in error
(fma.f64 (/.f64 1 (hypot.f64 y.re y.im)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x.im y.re) (hypot.f64 y.re y.im))) (/.f64 x.re (/.f64 (pow.f64 (hypot.f64 y.re y.im) 2) (neg.f64 y.im)))): 35 points increase in error, 7 points decrease in error
(fma.f64 (/.f64 1 (hypot.f64 y.re y.im)) (/.f64 (*.f64 x.im y.re) (hypot.f64 y.re y.im)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x.re (neg.f64 y.im)) (pow.f64 (hypot.f64 y.re y.im) 2)))): 41 points increase in error, 10 points decrease in error
(fma.f64 (/.f64 1 (hypot.f64 y.re y.im)) (/.f64 (*.f64 x.im y.re) (hypot.f64 y.re y.im)) (/.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 x.re y.im))) (pow.f64 (hypot.f64 y.re y.im) 2))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 1 (hypot.f64 y.re y.im)) (/.f64 (*.f64 x.im y.re) (hypot.f64 y.re y.im)) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (*.f64 x.re y.im) (pow.f64 (hypot.f64 y.re y.im) 2))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in y.re around 0 4.6
\[\leadsto \mathsf{fma}\left(\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)}, \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot y.re, \frac{x.re}{\color{blue}{-1 \cdot \frac{{y.re}^{2}}{y.im} + -1 \cdot y.im}}\right)
\]
Simplified2.5
\[\leadsto \mathsf{fma}\left(\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)}, \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot y.re, \frac{x.re}{\color{blue}{\left(-y.im\right) - \frac{y.re}{\frac{y.im}{y.re}}}}\right)
\]
Proof
(-.f64 (neg.f64 y.im) (/.f64 y.re (/.f64 y.im y.re))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 y.im)) (/.f64 y.re (/.f64 y.im y.re))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1 y.im) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y.re y.re) y.im))): 32 points increase in error, 13 points decrease in error
(-.f64 (*.f64 -1 y.im) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 y.re 2)) y.im)): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 y.im) (neg.f64 (/.f64 (pow.f64 y.re 2) y.im)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 y.im) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (pow.f64 y.re 2) y.im)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 y.re 2) y.im)) (*.f64 -1 y.im))): 0 points increase in error, 0 points decrease in error
Final simplification2.5
\[\leadsto \mathsf{fma}\left(\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)}, y.re \cdot \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)}, \frac{x.re}{\left(-y.im\right) - \frac{y.re}{\frac{y.im}{y.re}}}\right)
\]