- Split input into 2 regimes
if x.re < -7.337353623269386e+26 or 1.9108902209969745e+25 < x.re
Initial program 32.1
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification32.1
\[\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-sqrt32.1
\[\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-identity32.1
\[\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-frac32.1
\[\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))_*}}}\]
Simplified32.1
\[\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))_*}}\]
Simplified23.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/23.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}^*}}\]
Simplified23.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}^*}\]
- Using strategy
rm Applied div-sub23.7
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*} - \frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
Applied div-sub23.7
\[\leadsto \color{blue}{\frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied associate-/l*9.0
\[\leadsto \frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\color{blue}{\frac{x.re}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.im}}}}{\sqrt{y.im^2 + y.re^2}^*}\]
if -7.337353623269386e+26 < x.re < 1.9108902209969745e+25
Initial program 20.2
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification20.2
\[\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.2
\[\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.2
\[\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.2
\[\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.2
\[\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))_*}}\]
Simplified10.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/10.0
\[\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}^*}}\]
Simplified10.0
\[\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 div-sub10.0
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*} - \frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
Applied div-sub10.0
\[\leadsto \color{blue}{\frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied add-sqr-sqrt10.2
\[\leadsto \frac{\frac{y.re \cdot x.im}{\color{blue}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\]
Applied times-frac1.6
\[\leadsto \frac{\color{blue}{\frac{y.re}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{x.im}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\]
- Recombined 2 regimes into one program.
Final simplification4.9
\[\leadsto \begin{array}{l}
\mathbf{if}\;x.re \le -7.337353623269386 \cdot 10^{+26} \lor \neg \left(x.re \le 1.9108902209969745 \cdot 10^{+25}\right):\\
\;\;\;\;\frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.im}}}{\sqrt{y.im^2 + y.re^2}^*}\\
\mathbf{else}:\\
\;\;\;\;\frac{\frac{x.im}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{y.re}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\\
\end{array}\]