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

↓

\[\frac{x.re \cdot y.re + x.im \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 r1105750 = x_re;
        double r1105751 = y_re;
        double r1105752 = r1105750 * r1105751;
        double r1105753 = x_im;
        double r1105754 = y_im;
        double r1105755 = r1105753 * r1105754;
        double r1105756 = r1105752 + r1105755;
        double r1105757 = r1105751 * r1105751;
        double r1105758 = r1105754 * r1105754;
        double r1105759 = r1105757 + r1105758;
        double r1105760 = r1105756 / r1105759;
        return r1105760;
}

↓

double f(double x_re, double x_im, double y_re, double y_im) {
        double r1105761 = x_re;
        double r1105762 = y_re;
        double r1105763 = r1105761 * r1105762;
        double r1105764 = x_im;
        double r1105765 = y_im;
        double r1105766 = r1105764 * r1105765;
        double r1105767 = r1105763 + r1105766;
        double r1105768 = r1105762 * r1105762;
        double r1105769 = r1105765 * r1105765;
        double r1105770 = r1105768 + r1105769;
        double r1105771 = r1105767 / r1105770;
        return r1105771;
}

\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}

↓

\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}

Derivation

Initial program 1.1
\[\frac{\left(\frac{\left(x.re \cdot y.re\right)}{\left(x.im \cdot y.im\right)}\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
Final simplification1.1
\[\leadsto \frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]

Reproduce

herbie shell --seed 2019101 +o rules:numerics
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, real part"
  (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (*.p16 y.re y.re) (*.p16 y.im y.im))))

Error

Derivation

Reproduce