Average Error: 26.5 → 26.5
Time: 34.2s
Precision: 64
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{y.re \cdot x.im - x.re \cdot y.im}{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{y.re \cdot x.im - x.re \cdot y.im}{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 r3478356 = x_im;
        double r3478357 = y_re;
        double r3478358 = r3478356 * r3478357;
        double r3478359 = x_re;
        double r3478360 = y_im;
        double r3478361 = r3478359 * r3478360;
        double r3478362 = r3478358 - r3478361;
        double r3478363 = r3478357 * r3478357;
        double r3478364 = r3478360 * r3478360;
        double r3478365 = r3478363 + r3478364;
        double r3478366 = r3478362 / r3478365;
        return r3478366;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r3478367 = y_re;
        double r3478368 = x_im;
        double r3478369 = r3478367 * r3478368;
        double r3478370 = x_re;
        double r3478371 = y_im;
        double r3478372 = r3478370 * r3478371;
        double r3478373 = r3478369 - r3478372;
        double r3478374 = r3478367 * r3478367;
        double r3478375 = r3478371 * r3478371;
        double r3478376 = r3478374 + r3478375;
        double r3478377 = r3478373 / r3478376;
        return r3478377;
}

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 26.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 clear-num26.7

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

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

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

  6. Applied *-un-lft-identity26.7

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

  7. Applied times-frac26.7

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

  8. Applied *-un-lft-identity26.7

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

  9. Applied times-frac26.7

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

  10. Simplified26.7

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

  11. Simplified26.5

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

  12. Final simplification26.5

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

Reproduce

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