Average Error: 25.9 → 22.1
Time: 3.4s
Precision: 64
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{x.im \cdot \frac{y.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} - \frac{x.re}{\frac{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}{y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{x.im \cdot \frac{y.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} - \frac{x.re}{\frac{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}{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 r51166 = x_im;
        double r51167 = y_re;
        double r51168 = r51166 * r51167;
        double r51169 = x_re;
        double r51170 = y_im;
        double r51171 = r51169 * r51170;
        double r51172 = r51168 - r51171;
        double r51173 = r51167 * r51167;
        double r51174 = r51170 * r51170;
        double r51175 = r51173 + r51174;
        double r51176 = r51172 / r51175;
        return r51176;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r51177 = x_im;
        double r51178 = y_re;
        double r51179 = r51178 * r51178;
        double r51180 = y_im;
        double r51181 = r51180 * r51180;
        double r51182 = r51179 + r51181;
        double r51183 = sqrt(r51182);
        double r51184 = r51178 / r51183;
        double r51185 = r51177 * r51184;
        double r51186 = x_re;
        double r51187 = r51183 / r51180;
        double r51188 = r51186 / r51187;
        double r51189 = r51185 - r51188;
        double r51190 = r51189 / r51183;
        return r51190;
}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 25.9

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

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

    \[\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. Using strategy rm

  6. Applied div-sub25.8

    \[\leadsto \frac{\color{blue}{\frac{x.im \cdot y.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} - \frac{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}}\]
  7. Using strategy rm

  8. Applied associate-/l*24.0

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

  10. Applied *-un-lft-identity24.0

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

  11. Applied sqrt-prod24.0

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

  12. Applied times-frac22.1

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

  13. Simplified22.1

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

  14. Final simplification22.1

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

Reproduce

herbie shell --seed 2020001 
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, imaginary part"
  :precision binary64
  (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))))