Average Error: 25.1 → 25.1
Time: 11.8s
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 y.re - 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{x.im \cdot y.re - 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 r2975204 = x_im;
        double r2975205 = y_re;
        double r2975206 = r2975204 * r2975205;
        double r2975207 = x_re;
        double r2975208 = y_im;
        double r2975209 = r2975207 * r2975208;
        double r2975210 = r2975206 - r2975209;
        double r2975211 = r2975205 * r2975205;
        double r2975212 = r2975208 * r2975208;
        double r2975213 = r2975211 + r2975212;
        double r2975214 = r2975210 / r2975213;
        return r2975214;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r2975215 = x_im;
        double r2975216 = y_re;
        double r2975217 = r2975215 * r2975216;
        double r2975218 = x_re;
        double r2975219 = y_im;
        double r2975220 = r2975218 * r2975219;
        double r2975221 = r2975217 - r2975220;
        double r2975222 = r2975216 * r2975216;
        double r2975223 = r2975219 * r2975219;
        double r2975224 = r2975222 + r2975223;
        double r2975225 = r2975221 / r2975224;
        return r2975225;
}

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

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

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

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

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

  7. Applied frac-times25.1

    \[\leadsto \color{blue}{\frac{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}}}\]

  8. Simplified25.1

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

  9. Simplified25.1

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

  10. Final simplification25.1

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

Reproduce

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