Simplified24.1
\[\leadsto \color{blue}{\frac{y.re \cdot x.im}{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)} - \frac{x.re}{\frac{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)}{y.im}}}
\]
Proof
(-.f64 (/.f64 (*.f64 y.re x.im) (fma.f64 y.im y.im (*.f64 y.re y.re))) (/.f64 x.re (/.f64 (fma.f64 y.im y.im (*.f64 y.re y.re)) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 y.im y.im) (*.f64 y.re y.re)))) (/.f64 x.re (/.f64 (fma.f64 y.im y.im (*.f64 y.re y.re)) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y.re y.re) (*.f64 y.im y.im)))) (/.f64 x.re (/.f64 (fma.f64 y.im y.im (*.f64 y.re y.re)) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 y.re 2)) (*.f64 y.im y.im))) (/.f64 x.re (/.f64 (fma.f64 y.im y.im (*.f64 y.re y.re)) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (Rewrite<= unpow2_binary64 (pow.f64 y.im 2)))) (/.f64 x.re (/.f64 (fma.f64 y.im y.im (*.f64 y.re y.re)) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))) (/.f64 x.re (/.f64 (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 y.im y.im) (*.f64 y.re y.re))) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))) (/.f64 x.re (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y.re y.re) (*.f64 y.im y.im))) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))) (/.f64 x.re (/.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 y.re 2)) (*.f64 y.im y.im)) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))) (/.f64 x.re (/.f64 (+.f64 (pow.f64 y.re 2) (Rewrite<= unpow2_binary64 (pow.f64 y.im 2))) y.im))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x.re y.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))))): 42 points increase in error, 7 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))) (neg.f64 (/.f64 (*.f64 x.re y.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y.re x.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 x.re y.im) (+.f64 (pow.f64 y.re 2) (pow.f64 y.im 2)))))): 0 points increase in error, 0 points decrease in error
Simplified23.9
\[\leadsto \frac{y.re \cdot x.im}{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)} - \frac{x.re}{\color{blue}{y.im + \frac{y.re}{\frac{y.im}{y.re}}}}
\]
Proof
(+.f64 y.im (/.f64 y.re (/.f64 y.im y.re))): 0 points increase in error, 0 points decrease in error
(+.f64 y.im (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y.re y.re) y.im))): 19 points increase in error, 14 points decrease in error
(+.f64 y.im (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 y.re 2)) y.im)): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (pow.f64 y.re 2) y.im) y.im)): 0 points increase in error, 0 points decrease in error