Initial program 25.8
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Simplified25.8
\[\leadsto \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)}}\]
- Using strategy
rm Applied add-sqr-sqrt25.8
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)} \cdot \sqrt{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)}}}\]
Applied *-un-lft-identity25.8
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)} \cdot \sqrt{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)}}\]
Applied times-frac25.8
\[\leadsto \color{blue}{\frac{1}{\sqrt{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)}}}\]
Simplified25.8
\[\leadsto \color{blue}{\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{\mathsf{fma}\left(y.re, y.re, y.im \cdot y.im\right)}}\]
Simplified17.2
\[\leadsto \frac{1}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\mathsf{hypot}\left(y.re, y.im\right)}}\]
- Using strategy
rm Applied pow117.2
\[\leadsto \frac{1}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot \color{blue}{{\left(\frac{x.im \cdot y.re - x.re \cdot y.im}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}}\]
Applied pow117.2
\[\leadsto \color{blue}{{\left(\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}} \cdot {\left(\frac{x.im \cdot y.re - x.re \cdot y.im}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
Applied pow-prod-down17.2
\[\leadsto \color{blue}{{\left(\frac{1}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}}\]
Simplified17.1
\[\leadsto {\color{blue}{\left(\frac{\frac{x.im \cdot y.re - x.re \cdot y.im}{\mathsf{hypot}\left(y.re, y.im\right)}}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}}^{1}\]
- Using strategy
rm Applied div-sub17.1
\[\leadsto {\left(\frac{\color{blue}{\frac{x.im \cdot y.re}{\mathsf{hypot}\left(y.re, y.im\right)} - \frac{x.re \cdot y.im}{\mathsf{hypot}\left(y.re, y.im\right)}}}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
Simplified17.1
\[\leadsto {\left(\frac{\color{blue}{\frac{y.re \cdot x.im}{\mathsf{hypot}\left(y.re, y.im\right)}} - \frac{x.re \cdot y.im}{\mathsf{hypot}\left(y.re, y.im\right)}}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
Simplified9.9
\[\leadsto {\left(\frac{\frac{y.re \cdot x.im}{\mathsf{hypot}\left(y.re, y.im\right)} - \color{blue}{y.im \cdot \frac{x.re}{\mathsf{hypot}\left(y.re, y.im\right)}}}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
- Using strategy
rm Applied *-un-lft-identity9.9
\[\leadsto {\left(\frac{\frac{y.re \cdot x.im}{\color{blue}{1 \cdot \mathsf{hypot}\left(y.re, y.im\right)}} - y.im \cdot \frac{x.re}{\mathsf{hypot}\left(y.re, y.im\right)}}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
Applied times-frac1.2
\[\leadsto {\left(\frac{\color{blue}{\frac{y.re}{1} \cdot \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)}} - y.im \cdot \frac{x.re}{\mathsf{hypot}\left(y.re, y.im\right)}}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
Applied fma-neg1.2
\[\leadsto {\left(\frac{\color{blue}{\mathsf{fma}\left(\frac{y.re}{1}, \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)}, -y.im \cdot \frac{x.re}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
Simplified1.2
\[\leadsto {\left(\frac{\mathsf{fma}\left(\frac{y.re}{1}, \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)}, \color{blue}{-\frac{x.re}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot y.im}\right)}{\mathsf{hypot}\left(y.re, y.im\right)}\right)}^{1}\]
Final simplification1.2
\[\leadsto \frac{\mathsf{fma}\left(y.re, \frac{x.im}{\mathsf{hypot}\left(y.re, y.im\right)}, -\frac{x.re}{\mathsf{hypot}\left(y.re, y.im\right)} \cdot y.im\right)}{\mathsf{hypot}\left(y.re, y.im\right)}\]