- Split input into 3 regimes
if y.re < -3.704346594137205e+198
Initial program 41.7
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification41.7
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}\]
- Using strategy
rm Applied add-sqr-sqrt41.7
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Applied *-un-lft-identity41.7
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Applied times-frac41.7
\[\leadsto \color{blue}{\frac{1}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Simplified41.7
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Simplified28.9
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied associate-*l/28.8
\[\leadsto \color{blue}{\frac{1 \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
Simplified28.8
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
Taylor expanded around -inf 11.0
\[\leadsto \frac{\color{blue}{-1 \cdot x.im}}{\sqrt{y.im^2 + y.re^2}^*}\]
Simplified11.0
\[\leadsto \frac{\color{blue}{-x.im}}{\sqrt{y.im^2 + y.re^2}^*}\]
if -3.704346594137205e+198 < y.re < 3.7016953149313007e+136
Initial program 20.0
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification20.0
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}\]
- Using strategy
rm Applied add-sqr-sqrt20.0
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Applied *-un-lft-identity20.0
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Applied times-frac20.0
\[\leadsto \color{blue}{\frac{1}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Simplified20.0
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Simplified12.2
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied associate-*l/12.1
\[\leadsto \color{blue}{\frac{1 \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
Simplified12.1
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
if 3.7016953149313007e+136 < y.re
Initial program 41.6
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification41.6
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}\]
- Using strategy
rm Applied add-sqr-sqrt41.6
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Applied *-un-lft-identity41.6
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Applied times-frac41.6
\[\leadsto \color{blue}{\frac{1}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Simplified41.6
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Simplified25.8
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied associate-*l/25.8
\[\leadsto \color{blue}{\frac{1 \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
Simplified25.8
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
Taylor expanded around inf 14.2
\[\leadsto \frac{\color{blue}{x.im}}{\sqrt{y.im^2 + y.re^2}^*}\]
- Recombined 3 regimes into one program.
Final simplification12.3
\[\leadsto \begin{array}{l}
\mathbf{if}\;y.re \le -3.704346594137205 \cdot 10^{+198}:\\
\;\;\;\;\frac{-x.im}{\sqrt{y.im^2 + y.re^2}^*}\\
\mathbf{elif}\;y.re \le 3.7016953149313007 \cdot 10^{+136}:\\
\;\;\;\;\frac{\frac{x.im \cdot y.re - y.im \cdot x.re}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\\
\mathbf{else}:\\
\;\;\;\;\frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}\\
\end{array}\]