Error

Derivation

1. Initial program 25.7

   \[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
2. Using strategy rm

3. Applied add-sqr-sqrt25.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}}}\]

4. Applied *-un-lft-identity25.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}}\]

5. Applied times-frac25.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}}}\]

6. Applied simplify25.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}}\]

7. Applied simplify16.6

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

9. Applied div-sub16.6

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

11. Applied add-cube-cbrt16.9

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

12. Applied add-sqr-sqrt17.0

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

13. Applied times-frac9.9

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

14. Applied prod-diff10.0

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

15. Applied distribute-lft-in10.0

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

16. Applied simplify9.9

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

17. Applied simplify1.2

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

Runtime

Time bar (total: 2.5m)Debug logProfile

herbie shell --seed '#(1070609872 3456127585 2380521889 2328837196 1765472538 734540918)' +o rules:numerics
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, imaginary part"
  (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))))