- Split input into 3 regimes
if y.re < -3.297785523352951e+180
Initial program 42.7
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
- Using strategy
rm Applied add-sqr-sqrt42.7
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]
Applied *-un-lft-identity42.7
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
Applied times-frac42.7
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]
Simplified42.7
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.re^2 + y.im^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
Simplified29.9
\[\leadsto \frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re^2 + y.im^2}^*}}\]
- Using strategy
rm Applied associate-*r/29.9
\[\leadsto \color{blue}{\frac{\frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}{\sqrt{y.re^2 + y.im^2}^*}}\]
Taylor expanded around -inf 12.6
\[\leadsto \frac{\color{blue}{-1 \cdot x.im}}{\sqrt{y.re^2 + y.im^2}^*}\]
Simplified12.6
\[\leadsto \frac{\color{blue}{-x.im}}{\sqrt{y.re^2 + y.im^2}^*}\]
if -3.297785523352951e+180 < y.re < 4.7704829791947515e+204
Initial program 22.0
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
- Using strategy
rm Applied add-sqr-sqrt22.0
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]
Applied *-un-lft-identity22.0
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
Applied times-frac22.0
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]
Simplified22.0
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.re^2 + y.im^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
Simplified13.2
\[\leadsto \frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re^2 + y.im^2}^*}}\]
- Using strategy
rm Applied associate-*r/13.2
\[\leadsto \color{blue}{\frac{\frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}{\sqrt{y.re^2 + y.im^2}^*}}\]
- Using strategy
rm Applied sub-neg13.2
\[\leadsto \frac{\frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \color{blue}{\left(x.im \cdot y.re + \left(-x.re \cdot y.im\right)\right)}}{\sqrt{y.re^2 + y.im^2}^*}\]
Applied distribute-rgt-in13.2
\[\leadsto \frac{\color{blue}{\left(x.im \cdot y.re\right) \cdot \frac{1}{\sqrt{y.re^2 + y.im^2}^*} + \left(-x.re \cdot y.im\right) \cdot \frac{1}{\sqrt{y.re^2 + y.im^2}^*}}}{\sqrt{y.re^2 + y.im^2}^*}\]
Simplified5.1
\[\leadsto \frac{\left(x.im \cdot y.re\right) \cdot \frac{1}{\sqrt{y.re^2 + y.im^2}^*} + \color{blue}{x.re \cdot \frac{-y.im}{\sqrt{y.re^2 + y.im^2}^*}}}{\sqrt{y.re^2 + y.im^2}^*}\]
if 4.7704829791947515e+204 < y.re
Initial program 41.3
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
- Using strategy
rm Applied add-sqr-sqrt41.3
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]
Applied *-un-lft-identity41.3
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
Applied times-frac41.3
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]
Simplified41.3
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.re^2 + y.im^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
Simplified30.0
\[\leadsto \frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re^2 + y.im^2}^*}}\]
- Using strategy
rm Applied associate-*r/30.0
\[\leadsto \color{blue}{\frac{\frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}{\sqrt{y.re^2 + y.im^2}^*}}\]
Taylor expanded around inf 10.5
\[\leadsto \frac{\color{blue}{x.im}}{\sqrt{y.re^2 + y.im^2}^*}\]
- Recombined 3 regimes into one program.
Final simplification6.4
\[\leadsto \begin{array}{l}
\mathbf{if}\;y.re \le -3.297785523352951 \cdot 10^{+180}:\\
\;\;\;\;\frac{-x.im}{\sqrt{y.re^2 + y.im^2}^*}\\
\mathbf{elif}\;y.re \le 4.7704829791947515 \cdot 10^{+204}:\\
\;\;\;\;\frac{x.re \cdot \frac{-y.im}{\sqrt{y.re^2 + y.im^2}^*} + \frac{1}{\sqrt{y.re^2 + y.im^2}^*} \cdot \left(x.im \cdot y.re\right)}{\sqrt{y.re^2 + y.im^2}^*}\\
\mathbf{else}:\\
\;\;\;\;\frac{x.im}{\sqrt{y.re^2 + y.im^2}^*}\\
\end{array}\]