Simplified37.1
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(x.re, y.re, x.im \cdot y.im\right)}{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)}}
\]
Proof
(/.f64 (fma.f64 x.re y.re (*.f64 x.im y.im)) (fma.f64 y.re y.re (*.f64 y.im y.im))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x.re y.re) (*.f64 x.im y.im))) (fma.f64 y.re y.re (*.f64 y.im y.im))): 1 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 x.re y.re) (*.f64 x.im y.im)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y.re y.re) (*.f64 y.im y.im)))): 0 points increase in error, 0 points decrease in error
Simplified20.3
\[\leadsto \color{blue}{\frac{x.re}{y.re} + \frac{y.im}{y.re \cdot y.re} \cdot \left(x.im - \frac{y.im \cdot x.re}{y.re}\right)}
\]
Proof
(+.f64 (/.f64 x.re y.re) (*.f64 (/.f64 y.im (*.f64 y.re y.re)) (-.f64 x.im (/.f64 (*.f64 y.im x.re) y.re)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x.re y.re) (*.f64 (/.f64 y.im (Rewrite<= unpow2_binary64 (pow.f64 y.re 2))) (-.f64 x.im (/.f64 (*.f64 y.im x.re) y.re)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x.re y.re) (*.f64 (/.f64 y.im (pow.f64 y.re 2)) (-.f64 x.im (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 x.re y.im)) y.re)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x.re y.re) (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 x.im (/.f64 y.im (pow.f64 y.re 2))) (*.f64 (/.f64 (*.f64 x.re y.im) y.re) (/.f64 y.im (pow.f64 y.re 2)))))): 0 points increase in error, 2 points decrease in error
(+.f64 (/.f64 x.re y.re) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 y.im (pow.f64 y.re 2)) x.im)) (*.f64 (/.f64 (*.f64 x.re y.im) y.re) (/.f64 y.im (pow.f64 y.re 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x.re y.re) (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2))) (*.f64 (/.f64 (*.f64 x.re y.im) y.re) (/.f64 y.im (pow.f64 y.re 2))))): 19 points increase in error, 7 points decrease in error
(+.f64 (/.f64 x.re y.re) (-.f64 (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (*.f64 x.re y.im) y.im) (*.f64 y.re (pow.f64 y.re 2)))))): 17 points increase in error, 4 points decrease in error
(+.f64 (/.f64 x.re y.re) (-.f64 (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2)) (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 x.re (*.f64 y.im y.im))) (*.f64 y.re (pow.f64 y.re 2))))): 8 points increase in error, 2 points decrease in error
(+.f64 (/.f64 x.re y.re) (-.f64 (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2)) (/.f64 (*.f64 x.re (Rewrite<= unpow2_binary64 (pow.f64 y.im 2))) (*.f64 y.re (pow.f64 y.re 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x.re y.re) (-.f64 (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2)) (/.f64 (*.f64 x.re (pow.f64 y.im 2)) (*.f64 y.re (Rewrite=> unpow2_binary64 (*.f64 y.re y.re)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x.re y.re) (-.f64 (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2)) (/.f64 (*.f64 x.re (pow.f64 y.im 2)) (Rewrite<= cube-mult_binary64 (pow.f64 y.re 3))))): 0 points increase in error, 1 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 x.re y.re) (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2))) (/.f64 (*.f64 x.re (pow.f64 y.im 2)) (pow.f64 y.re 3)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (+.f64 (/.f64 x.re y.re) (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2))) (neg.f64 (/.f64 (*.f64 x.re (pow.f64 y.im 2)) (pow.f64 y.re 3))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 x.re y.re) (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 x.re (pow.f64 y.im 2)) (pow.f64 y.re 3))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 x.re (pow.f64 y.im 2)) (pow.f64 y.re 3))) (+.f64 (/.f64 x.re y.re) (/.f64 (*.f64 y.im x.im) (pow.f64 y.re 2))))): 0 points increase in error, 0 points decrease in error
Simplified16.0
\[\leadsto \frac{x.re}{y.re} + \color{blue}{\frac{x.im}{\frac{y.re}{\frac{y.im}{y.re}}}}
\]
Proof
(/.f64 x.im (/.f64 y.re (/.f64 y.im y.re))): 0 points increase in error, 0 points decrease in error
(/.f64 x.im (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y.re y.re) y.im))): 31 points increase in error, 12 points decrease in error
(/.f64 x.im (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 y.re 2)) y.im)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x.im y.im) (pow.f64 y.re 2))): 40 points increase in error, 25 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y.im x.im)) (pow.f64 y.re 2)): 0 points increase in error, 0 points decrease in error