- Split input into 2 regimes
if (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) < 4.545311703826743e-21
Initial program 1.7
\[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\]
if 4.545311703826743e-21 < (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))))
Initial program 61.4
\[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\]
Initial simplification10.7
\[\leadsto \frac{\sin \left((y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*\right)}{\frac{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}}{{\left(\sqrt{x.re^2 + x.im^2}^*\right)}^{y.re}}}\]
- Using strategy
rm Applied add-cube-cbrt11.2
\[\leadsto \frac{\sin \color{blue}{\left(\left(\sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*} \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right) \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right)}}{\frac{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}}{{\left(\sqrt{x.re^2 + x.im^2}^*\right)}^{y.re}}}\]
- Using strategy
rm Applied pow-exp10.5
\[\leadsto \frac{\sin \left(\left(\sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*} \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right) \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right)}{\frac{\color{blue}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}}{{\left(\sqrt{x.re^2 + x.im^2}^*\right)}^{y.re}}}\]
- Using strategy
rm Applied add-cbrt-cube10.5
\[\leadsto \frac{\sin \left(\left(\sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*} \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right) \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right)}{\frac{e^{\color{blue}{\sqrt[3]{\left(\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot \left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot \left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}}}{{\left(\sqrt{x.re^2 + x.im^2}^*\right)}^{y.re}}}\]
- Using strategy
rm Applied log1p-expm1-u10.5
\[\leadsto \frac{\color{blue}{\log_* (1 + (e^{\sin \left(\left(\sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*} \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right) \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right)} - 1)^*)}}{\frac{e^{\sqrt[3]{\left(\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot \left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot \left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}}{{\left(\sqrt{x.re^2 + x.im^2}^*\right)}^{y.re}}}\]
- Recombined 2 regimes into one program.
Final simplification6.4
\[\leadsto \begin{array}{l}
\mathbf{if}\;\sin \left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{y.re \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \le 4.545311703826743 \cdot 10^{-21}:\\
\;\;\;\;\sin \left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{y.re \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}\\
\mathbf{else}:\\
\;\;\;\;\frac{\log_* (1 + (e^{\sin \left(\sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*} \cdot \left(\sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*} \cdot \sqrt[3]{(y.im \cdot \left(\log \left(\sqrt{x.re^2 + x.im^2}^*\right)\right) + \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right))_*}\right)\right)} - 1)^*)}{\frac{e^{\sqrt[3]{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right) \cdot \left(\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)\right)}}}{{\left(\sqrt{x.re^2 + x.im^2}^*\right)}^{y.re}}}\\
\end{array}\]