Error

Derivation

1. Split input into 4 regimes

2. if y.im < -2.1203256376020936e+104

   1. Initial program 39.4

      \[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]

   2. Applied simplify39.4

      \[\leadsto \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
   3. Using strategy rm

   4. Applied add-sqr-sqrt39.4

      \[\leadsto \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\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))_*}}}\]

   5. Applied *-un-lft-identity39.4

      \[\leadsto \frac{\color{blue}{1 \cdot (x.im \cdot y.im + \left(y.re \cdot x.re\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))_*}}\]

   6. 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.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]

   7. Applied simplify39.4

      \[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]

   8. Applied simplify25.5

      \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{y.im^2 + y.re^2}^*}}\]

   9. Taylor expanded around -inf 17.1

      \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\left(-1 \cdot x.im\right)}\]

   10. Applied simplify17.0

       \[\leadsto \color{blue}{\frac{-x.im}{\sqrt{y.im^2 + y.re^2}^*}}\]

   if -2.1203256376020936e+104 < y.im < -1.5311629338677103e-192 or 2.2280832042887506e-81 < y.im < 5.302451626529533e+165

   1. Initial program 17.3

      \[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]

   2. Applied simplify17.3

      \[\leadsto \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
   3. Using strategy rm

   4. Applied add-sqr-sqrt17.3

      \[\leadsto \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\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))_*}}}\]

   5. Applied *-un-lft-identity17.3

      \[\leadsto \frac{\color{blue}{1 \cdot (x.im \cdot y.im + \left(y.re \cdot x.re\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))_*}}\]

   6. Applied times-frac17.3

      \[\leadsto \color{blue}{\frac{1}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]

   7. Applied simplify17.3

      \[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]

   8. Applied simplify12.1

      \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{y.im^2 + y.re^2}^*}}\]

   if -1.5311629338677103e-192 < y.im < 2.2280832042887506e-81

   1. Initial program 20.7

      \[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]

   2. Applied simplify20.7

      \[\leadsto \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
   3. Using strategy rm

   4. Applied add-sqr-sqrt20.7

      \[\leadsto \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\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))_*}}}\]

   5. Applied *-un-lft-identity20.7

      \[\leadsto \frac{\color{blue}{1 \cdot (x.im \cdot y.im + \left(y.re \cdot x.re\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))_*}}\]

   6. Applied times-frac20.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.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]

   7. Applied simplify20.7

      \[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]

   8. Applied simplify11.5

      \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{y.im^2 + y.re^2}^*}}\]
   9. Using strategy rm

   10. Applied add-sqr-sqrt11.7

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\color{blue}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}}\]

   11. Applied *-un-lft-identity11.7

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \frac{\color{blue}{1 \cdot (x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}\]

   12. Applied times-frac11.7

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\left(\frac{1}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right)}\]
   13. Using strategy rm

   14. Applied add-cube-cbrt11.9

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\frac{1}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{\color{blue}{\left(\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}\right) \cdot \sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}}}}\right)\]

   15. Applied sqrt-prod11.9

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\frac{1}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\color{blue}{\sqrt{\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt{\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}}}}\right)\]

   16. Applied *-un-lft-identity11.9

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\frac{1}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{\color{blue}{1 \cdot (x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}}{\sqrt{\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt{\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}}}\right)\]

   17. Applied times-frac11.9

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\frac{1}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \color{blue}{\left(\frac{1}{\sqrt{\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}}}\right)}\right)\]

   18. Applied simplify11.9

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\frac{1}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \left(\color{blue}{\frac{1}{\left|\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}\right|}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}}}\right)\right)\]

   19. Taylor expanded around 0 38.9

       \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\left({\left(\frac{1}{{y.re}^{2}}\right)}^{\frac{1}{3}} \cdot \frac{y.im \cdot x.im}{\left|\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}\right|} + \frac{x.re}{\left|\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}\right|} \cdot {y.re}^{\frac{1}{3}}\right)}\]

   20. Applied simplify10.9

       \[\leadsto \color{blue}{(\left(\frac{\sqrt[3]{\frac{1}{y.re \cdot y.re}}}{\sqrt{y.im^2 + y.re^2}^*}\right) \cdot \left(\frac{x.im \cdot y.im}{\left|\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}\right|}\right) + \left(\frac{\sqrt[3]{y.re} \cdot \frac{x.re}{\sqrt{y.im^2 + y.re^2}^*}}{\left|\sqrt[3]{\sqrt{y.im^2 + y.re^2}^*}\right|}\right))_*}\]

   if 5.302451626529533e+165 < y.im

   1. Initial program 45.2

      \[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]

   2. Applied simplify45.2

      \[\leadsto \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
   3. Using strategy rm

   4. Applied add-sqr-sqrt45.2

      \[\leadsto \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\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))_*}}}\]

   5. Applied *-un-lft-identity45.2

      \[\leadsto \frac{\color{blue}{1 \cdot (x.im \cdot y.im + \left(y.re \cdot x.re\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))_*}}\]

   6. Applied times-frac45.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.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]

   7. Applied simplify45.2

      \[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]

   8. Applied simplify30.4

      \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{(x.im \cdot y.im + \left(y.re \cdot x.re\right))_*}{\sqrt{y.im^2 + y.re^2}^*}}\]

   9. Taylor expanded around inf 14.5

      \[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{x.im}\]

   10. Applied simplify14.3

       \[\leadsto \color{blue}{\frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}}\]
3. Recombined 4 regimes into one program.

Runtime

Time bar (total: 1.8m)Debug logProfile

herbie shell --seed 2018206 +o rules:numerics
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, real part"
  (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im))))