Average Error: 25.5 → 24.1
Time: 24.6s
Precision: 64
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{\frac{y.re \cdot x.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} - y.im \cdot \frac{x.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
double f(double x_re, double x_im, double y_re, double y_im) {
        double r5780733 = x_im;
        double r5780734 = y_re;
        double r5780735 = r5780733 * r5780734;
        double r5780736 = x_re;
        double r5780737 = y_im;
        double r5780738 = r5780736 * r5780737;
        double r5780739 = r5780735 - r5780738;
        double r5780740 = r5780734 * r5780734;
        double r5780741 = r5780737 * r5780737;
        double r5780742 = r5780740 + r5780741;
        double r5780743 = r5780739 / r5780742;
        return r5780743;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r5780744 = y_re;
        double r5780745 = x_im;
        double r5780746 = r5780744 * r5780745;
        double r5780747 = r5780744 * r5780744;
        double r5780748 = y_im;
        double r5780749 = r5780748 * r5780748;
        double r5780750 = r5780747 + r5780749;
        double r5780751 = sqrt(r5780750);
        double r5780752 = r5780746 / r5780751;
        double r5780753 = x_re;
        double r5780754 = r5780753 / r5780751;
        double r5780755 = r5780748 * r5780754;
        double r5780756 = r5780752 - r5780755;
        double r5780757 = r5780756 / r5780751;
        return r5780757;
}


\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{\frac{y.re \cdot x.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} - y.im \cdot \frac{x.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Derivation

  1. Initial program 25.5

    \[\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.5

    \[\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 associate-/r*25.5

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

  5. Taylor expanded around -inf 25.5

    \[\leadsto \frac{\frac{\color{blue}{y.re \cdot x.im - y.im \cdot x.re}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
  6. Using strategy rm

  7. Applied div-sub25.5

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

  9. Applied *-un-lft-identity25.5

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

  10. Applied times-frac24.1

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

  11. Simplified24.1

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

  12. Final simplification24.1

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

Reproduce

herbie shell --seed 2019102 
(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))))