Average Error: 25.3 → 25.4
Time: 3.9m
Precision: 64
\[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{\frac{1}{\frac{1}{y.re \cdot x.re + x.im \cdot y.im}}}{y.im \cdot y.im + y.re \cdot y.re}\]
\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{\frac{1}{\frac{1}{y.re \cdot x.re + x.im \cdot y.im}}}{y.im \cdot y.im + y.re \cdot y.re}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r12738452 = x_re;
        double r12738453 = y_re;
        double r12738454 = r12738452 * r12738453;
        double r12738455 = x_im;
        double r12738456 = y_im;
        double r12738457 = r12738455 * r12738456;
        double r12738458 = r12738454 + r12738457;
        double r12738459 = r12738453 * r12738453;
        double r12738460 = r12738456 * r12738456;
        double r12738461 = r12738459 + r12738460;
        double r12738462 = r12738458 / r12738461;
        return r12738462;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r12738463 = 1.0;
        double r12738464 = y_re;
        double r12738465 = x_re;
        double r12738466 = r12738464 * r12738465;
        double r12738467 = x_im;
        double r12738468 = y_im;
        double r12738469 = r12738467 * r12738468;
        double r12738470 = r12738466 + r12738469;
        double r12738471 = r12738463 / r12738470;
        double r12738472 = r12738463 / r12738471;
        double r12738473 = r12738468 * r12738468;
        double r12738474 = r12738464 * r12738464;
        double r12738475 = r12738473 + r12738474;
        double r12738476 = r12738472 / r12738475;
        return r12738476;
}

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.3

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

  3. Applied add-sqr-sqrt25.3

    \[\leadsto \frac{x.re \cdot y.re + x.im \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.2

    \[\leadsto \color{blue}{\frac{\frac{x.re \cdot y.re + x.im \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 *-un-lft-identity25.2

    \[\leadsto \frac{\frac{x.re \cdot y.re + x.im \cdot y.im}{\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}}\]

  7. Applied *-un-lft-identity25.2

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

  8. Applied times-frac25.2

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

  9. Applied associate-/l*25.4

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

  10. Simplified25.4

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

  12. Applied div-inv25.4

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

  13. Applied *-un-lft-identity25.4

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

  14. Applied times-frac25.6

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

  15. Applied associate-/r*25.4

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

  16. Simplified25.4

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

  17. Final simplification25.4

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

Reproduce

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