\[\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\]

↓

\[\left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\]

double f(double x_re, double x_im) {
        double r273375 = x_re;
        double r273376 = r273375 * r273375;
        double r273377 = x_im;
        double r273378 = r273377 * r273377;
        double r273379 = r273376 - r273378;
        double r273380 = r273379 * r273375;
        double r273381 = r273375 * r273377;
        double r273382 = r273377 * r273375;
        double r273383 = r273381 + r273382;
        double r273384 = r273383 * r273377;
        double r273385 = r273380 - r273384;
        return r273385;
}

↓

double f(double x_re, double x_im) {
        double r273386 = x_re;
        double r273387 = x_im;
        double r273388 = r273386 + r273387;
        double r273389 = r273386 - r273387;
        double r273390 = r273389 * r273386;
        double r273391 = r273388 * r273390;
        double r273392 = r273386 * r273387;
        double r273393 = r273387 * r273386;
        double r273394 = r273392 + r273393;
        double r273395 = r273394 * r273387;
        double r273396 = r273391 - r273395;
        return r273396;
}

\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im

↓

\left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im

Derivation

Initial program 0.4
\[\left(\left(\left(x.re \cdot x.re\right) - \left(x.im \cdot x.im\right)\right) \cdot x.re\right) - \left(\left(\frac{\left(x.re \cdot x.im\right)}{\left(x.im \cdot x.re\right)}\right) \cdot x.im\right)\]
Using strategy rm
Applied difference-of-squares0.4
\[\leadsto \left(\color{blue}{\left(\left(\frac{x.re}{x.im}\right) \cdot \left(x.re - x.im\right)\right)} \cdot x.re\right) - \left(\left(\frac{\left(x.re \cdot x.im\right)}{\left(x.im \cdot x.re\right)}\right) \cdot x.im\right)\]
Applied associate-*l*0.4
\[\leadsto \color{blue}{\left(\left(\frac{x.re}{x.im}\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right)\right)} - \left(\left(\frac{\left(x.re \cdot x.im\right)}{\left(x.im \cdot x.re\right)}\right) \cdot x.im\right)\]
Final simplification0.4
\[\leadsto \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\]

Reproduce

herbie shell --seed 2019102 +o rules:numerics
(FPCore (x.re x.im)
  :name "math.cube on complex, real part"
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))

Error

Derivation

Reproduce