- Split input into 3 regimes
if y.re < -2.753704486803755e+110
Initial program 39.4
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification39.4
\[\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-sqrt39.4
\[\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-identity39.4
\[\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-frac39.4
\[\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))_*}}}\]
Simplified39.4
\[\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.7
\[\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.6
\[\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.6
\[\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.5
\[\leadsto \frac{\color{blue}{-1 \cdot x.im}}{\sqrt{y.im^2 + y.re^2}^*}\]
Simplified14.5
\[\leadsto \frac{\color{blue}{-x.im}}{\sqrt{y.im^2 + y.re^2}^*}\]
if -2.753704486803755e+110 < y.re < 1.0039535823854329e+149
Initial program 18.6
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification18.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-sqrt18.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-identity18.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-frac18.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))_*}}}\]
Simplified18.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))_*}}\]
Simplified11.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/11.7
\[\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}^*}}\]
Simplified11.7
\[\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 1.0039535823854329e+149 < y.re
Initial program 43.6
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification43.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-sqrt43.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-identity43.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-frac43.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))_*}}}\]
Simplified43.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))_*}}\]
Simplified27.5
\[\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/27.5
\[\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}^*}}\]
Simplified27.5
\[\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}^*}\]
- Using strategy
rm Applied *-un-lft-identity27.5
\[\leadsto \frac{\frac{\color{blue}{1 \cdot \left(y.re \cdot x.im - x.re \cdot y.im\right)}}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\]
Applied associate-/l*27.5
\[\leadsto \frac{\color{blue}{\frac{1}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.re \cdot x.im - x.re \cdot y.im}}}}{\sqrt{y.im^2 + y.re^2}^*}\]
Taylor expanded around 0 13.9
\[\leadsto \frac{\color{blue}{x.im}}{\sqrt{y.im^2 + y.re^2}^*}\]
- Recombined 3 regimes into one program.
Final simplification12.5
\[\leadsto \begin{array}{l}
\mathbf{if}\;y.re \le -2.753704486803755 \cdot 10^{+110}:\\
\;\;\;\;\frac{-x.im}{\sqrt{y.im^2 + y.re^2}^*}\\
\mathbf{elif}\;y.re \le 1.0039535823854329 \cdot 10^{+149}:\\
\;\;\;\;\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}\]