\[re \cdot re - im \cdot im\]

↓

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

double f(double re, double im) {
        double r34132 = re;
        double r34133 = r34132 * r34132;
        double r34134 = im;
        double r34135 = r34134 * r34134;
        double r34136 = r34133 - r34135;
        return r34136;
}

↓

double f(double re, double im) {
        double r34137 = im;
        double r34138 = re;
        double r34139 = r34137 + r34138;
        double r34140 = r34138 - r34137;
        double r34141 = r34139 * r34140;
        return r34141;
}

re \cdot re - im \cdot im

↓

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

Derivation

Initial program 0.0
\[re \cdot re - im \cdot im\]
Using strategy rm
Applied difference-of-squares0.0
\[\leadsto \color{blue}{\left(re + im\right) \cdot \left(re - im\right)}\]
Final simplification0.0
\[\leadsto \left(im + re\right) \cdot \left(re - im\right)\]

Reproduce

herbie shell --seed 2019101 
(FPCore (re im)
  :name "math.square on complex, real part"
  (- (* re re) (* im im)))

Error

Derivation

Reproduce