math.cube on complex, real part

Percentage Accurate: 83.1% → 99.7%
Time: 10.8s
Alternatives: 9
Speedup: 0.7×

Specification

?
\[\begin{array}{l} \\ \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 \end{array} \]
(FPCore (x.re x.im)
 :precision binary64
 (-
  (* (- (* x.re x.re) (* x.im x.im)) x.re)
  (* (+ (* x.re x.im) (* x.im x.re)) x.im)))
double code(double x_46_re, double x_46_im) {
	return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
}
real(8) function code(x_46re, x_46im)
    real(8), intent (in) :: x_46re
    real(8), intent (in) :: x_46im
    code = (((x_46re * x_46re) - (x_46im * x_46im)) * x_46re) - (((x_46re * x_46im) + (x_46im * x_46re)) * x_46im)
end function
public static double code(double x_46_re, double x_46_im) {
	return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
}
def code(x_46_re, x_46_im):
	return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im)
function code(x_46_re, x_46_im)
	return Float64(Float64(Float64(Float64(x_46_re * x_46_re) - Float64(x_46_im * x_46_im)) * x_46_re) - Float64(Float64(Float64(x_46_re * x_46_im) + Float64(x_46_im * x_46_re)) * x_46_im))
end
function tmp = code(x_46_re, x_46_im)
	tmp = (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
end
code[x$46$re_, x$46$im_] := N[(N[(N[(N[(x$46$re * x$46$re), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re), $MachinePrecision] - N[(N[(N[(x$46$re * x$46$im), $MachinePrecision] + N[(x$46$im * x$46$re), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\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
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 9 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 83.1% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \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 \end{array} \]
(FPCore (x.re x.im)
 :precision binary64
 (-
  (* (- (* x.re x.re) (* x.im x.im)) x.re)
  (* (+ (* x.re x.im) (* x.im x.re)) x.im)))
double code(double x_46_re, double x_46_im) {
	return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
}
real(8) function code(x_46re, x_46im)
    real(8), intent (in) :: x_46re
    real(8), intent (in) :: x_46im
    code = (((x_46re * x_46re) - (x_46im * x_46im)) * x_46re) - (((x_46re * x_46im) + (x_46im * x_46re)) * x_46im)
end function
public static double code(double x_46_re, double x_46_im) {
	return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
}
def code(x_46_re, x_46_im):
	return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im)
function code(x_46_re, x_46_im)
	return Float64(Float64(Float64(Float64(x_46_re * x_46_re) - Float64(x_46_im * x_46_im)) * x_46_re) - Float64(Float64(Float64(x_46_re * x_46_im) + Float64(x_46_im * x_46_re)) * x_46_im))
end
function tmp = code(x_46_re, x_46_im)
	tmp = (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
end
code[x$46$re_, x$46$im_] := N[(N[(N[(N[(x$46$re * x$46$re), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re), $MachinePrecision] - N[(N[(N[(x$46$re * x$46$im), $MachinePrecision] + N[(x$46$im * x$46$re), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\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
\end{array}

Alternative 1: 99.7% accurate, 0.4× speedup?

\[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(\left(x.re\_m + x.re\_m\right) \cdot x.im, -x.im, \left(x.re\_m - x.im\right) \cdot \left(\mathsf{fma}\left(x.re\_m, \frac{x.re\_m}{x.im}, x.re\_m\right) \cdot x.im\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\ \end{array} \end{array} \]
x.re\_m = (fabs.f64 x.re)
x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
(FPCore (x.re_s x.re_m x.im)
 :precision binary64
 (*
  x.re_s
  (if (<=
       (-
        (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
        (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))
       5e+20)
    (fma
     (* (+ x.re_m x.re_m) x.im)
     (- x.im)
     (* (- x.re_m x.im) (* (fma x.re_m (/ x.re_m x.im) x.re_m) x.im)))
    (fma (- x.re_m x.im) (* (+ x.im x.re_m) x.re_m) (+ x.re_m x.re_m)))))
x.re\_m = fabs(x_46_re);
x.re\_s = copysign(1.0, x_46_re);
double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
	double tmp;
	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= 5e+20) {
		tmp = fma(((x_46_re_m + x_46_re_m) * x_46_im), -x_46_im, ((x_46_re_m - x_46_im) * (fma(x_46_re_m, (x_46_re_m / x_46_im), x_46_re_m) * x_46_im)));
	} else {
		tmp = fma((x_46_re_m - x_46_im), ((x_46_im + x_46_re_m) * x_46_re_m), (x_46_re_m + x_46_re_m));
	}
	return x_46_re_s * tmp;
}
x.re\_m = abs(x_46_re)
x.re\_s = copysign(1.0, x_46_re)
function code(x_46_re_s, x_46_re_m, x_46_im)
	tmp = 0.0
	if (Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im)) <= 5e+20)
		tmp = fma(Float64(Float64(x_46_re_m + x_46_re_m) * x_46_im), Float64(-x_46_im), Float64(Float64(x_46_re_m - x_46_im) * Float64(fma(x_46_re_m, Float64(x_46_re_m / x_46_im), x_46_re_m) * x_46_im)));
	else
		tmp = fma(Float64(x_46_re_m - x_46_im), Float64(Float64(x_46_im + x_46_re_m) * x_46_re_m), Float64(x_46_re_m + x_46_re_m));
	end
	return Float64(x_46_re_s * tmp)
end
x.re\_m = N[Abs[x$46$re], $MachinePrecision]
x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := N[(x$46$re$95$s * If[LessEqual[N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision], 5e+20], N[(N[(N[(x$46$re$95$m + x$46$re$95$m), $MachinePrecision] * x$46$im), $MachinePrecision] * (-x$46$im) + N[(N[(x$46$re$95$m - x$46$im), $MachinePrecision] * N[(N[(x$46$re$95$m * N[(x$46$re$95$m / x$46$im), $MachinePrecision] + x$46$re$95$m), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$46$re$95$m - x$46$im), $MachinePrecision] * N[(N[(x$46$im + x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] + N[(x$46$re$95$m + x$46$re$95$m), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]
\begin{array}{l}
x.re\_m = \left|x.re\right|
\\
x.re\_s = \mathsf{copysign}\left(1, x.re\right)

\\
x.re\_s \cdot \begin{array}{l}
\mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\
\;\;\;\;\mathsf{fma}\left(\left(x.re\_m + x.re\_m\right) \cdot x.im, -x.im, \left(x.re\_m - x.im\right) \cdot \left(\mathsf{fma}\left(x.re\_m, \frac{x.re\_m}{x.im}, x.re\_m\right) \cdot x.im\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < 5e20

    1. Initial program 92.9%

      \[\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 \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto \color{blue}{\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} \]
      2. sub-negN/A

        \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
      3. +-commutativeN/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
      4. lift-*.f64N/A

        \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
      5. distribute-rgt-neg-inN/A

        \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
      6. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
      7. lift-+.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      8. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      9. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      10. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      11. distribute-lft-outN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      12. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      13. lower-+.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      14. lower-neg.f6493.0

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      15. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
      16. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
      17. lift--.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
      18. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
      19. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
      20. difference-of-squaresN/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
      21. associate-*r*N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
      22. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
    4. Applied rewrites99.8%

      \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]
    5. Taylor expanded in x.im around inf

      \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.im \cdot \left(x.re + \frac{{x.re}^{2}}{x.im}\right)\right)} \cdot \left(x.re - x.im\right)\right) \]
    6. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(\left(x.re + \frac{{x.re}^{2}}{x.im}\right) \cdot x.im\right)} \cdot \left(x.re - x.im\right)\right) \]
      2. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(\left(x.re + \frac{{x.re}^{2}}{x.im}\right) \cdot x.im\right)} \cdot \left(x.re - x.im\right)\right) \]
      3. +-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \left(\color{blue}{\left(\frac{{x.re}^{2}}{x.im} + x.re\right)} \cdot x.im\right) \cdot \left(x.re - x.im\right)\right) \]
      4. unpow2N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \left(\left(\frac{\color{blue}{x.re \cdot x.re}}{x.im} + x.re\right) \cdot x.im\right) \cdot \left(x.re - x.im\right)\right) \]
      5. associate-/l*N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \left(\left(\color{blue}{x.re \cdot \frac{x.re}{x.im}} + x.re\right) \cdot x.im\right) \cdot \left(x.re - x.im\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \left(\color{blue}{\mathsf{fma}\left(x.re, \frac{x.re}{x.im}, x.re\right)} \cdot x.im\right) \cdot \left(x.re - x.im\right)\right) \]
      7. lower-/.f6497.5

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(\mathsf{fma}\left(x.re, \color{blue}{\frac{x.re}{x.im}}, x.re\right) \cdot x.im\right) \cdot \left(x.re - x.im\right)\right) \]
    7. Applied rewrites97.5%

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

    if 5e20 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

    1. Initial program 59.0%

      \[\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 \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto \color{blue}{\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} \]
      2. sub-negN/A

        \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
      3. +-commutativeN/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
      4. lift-*.f64N/A

        \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
      5. distribute-rgt-neg-inN/A

        \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
      6. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
      7. lift-+.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      8. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      9. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      10. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      11. distribute-lft-outN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      12. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      13. lower-+.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      14. lower-neg.f6467.8

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
      15. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
      16. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
      17. lift--.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
      18. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
      19. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
      20. difference-of-squaresN/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
      21. associate-*r*N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
      22. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
    4. Applied rewrites82.3%

      \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]
    5. Step-by-step derivation
      1. lift-fma.f64N/A

        \[\leadsto \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) + \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} \]
      2. +-commutativeN/A

        \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right) + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} \]
      3. lift-*.f64N/A

        \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
      4. *-commutativeN/A

        \[\leadsto \color{blue}{\left(x.re - x.im\right) \cdot \left(x.re \cdot \left(x.im + x.re\right)\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
      5. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, x.re \cdot \left(x.im + x.re\right), \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{x.re \cdot \left(x.im + x.re\right)}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      7. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      8. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      9. lift-+.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      10. +-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      11. lower-+.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      12. lift-neg.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(x.im\right)\right)}\right) \]
      13. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      14. lift-+.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      15. distribute-lft-inN/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      16. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      17. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      18. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      19. lift-+.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
      20. distribute-rgt-neg-inN/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)}\right) \]
      21. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(\color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
      22. lift-+.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
      23. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right)\right)\right) \]
      24. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
      25. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
    6. Applied rewrites87.3%

      \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, x.re + x.re\right)} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification93.9%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(\left(x.re + x.re\right) \cdot x.im, -x.im, \left(x.re - x.im\right) \cdot \left(\mathsf{fma}\left(x.re, \frac{x.re}{x.im}, x.re\right) \cdot x.im\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re - x.im, \left(x.im + x.re\right) \cdot x.re, x.re + x.re\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 2: 99.7% accurate, 0.3× speedup?

\[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ \begin{array}{l} t_0 := \left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im\\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;t\_0 \leq -\infty:\\ \;\;\;\;\left(\left(-3 \cdot x.im\right) \cdot x.re\_m\right) \cdot x.im\\ \mathbf{elif}\;t\_0 \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(-3 \cdot \left(x.im \cdot x.im\right), x.re\_m, \left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\ \end{array} \end{array} \end{array} \]
x.re\_m = (fabs.f64 x.re)
x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
(FPCore (x.re_s x.re_m x.im)
 :precision binary64
 (let* ((t_0
         (-
          (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
          (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))))
   (*
    x.re_s
    (if (<= t_0 (- INFINITY))
      (* (* (* -3.0 x.im) x.re_m) x.im)
      (if (<= t_0 5e+20)
        (fma (* -3.0 (* x.im x.im)) x.re_m (* (* x.re_m x.re_m) x.re_m))
        (fma (- x.re_m x.im) (* (+ x.im x.re_m) x.re_m) (+ x.re_m x.re_m)))))))
x.re\_m = fabs(x_46_re);
x.re\_s = copysign(1.0, x_46_re);
double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
	double t_0 = (((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im);
	double tmp;
	if (t_0 <= -((double) INFINITY)) {
		tmp = ((-3.0 * x_46_im) * x_46_re_m) * x_46_im;
	} else if (t_0 <= 5e+20) {
		tmp = fma((-3.0 * (x_46_im * x_46_im)), x_46_re_m, ((x_46_re_m * x_46_re_m) * x_46_re_m));
	} else {
		tmp = fma((x_46_re_m - x_46_im), ((x_46_im + x_46_re_m) * x_46_re_m), (x_46_re_m + x_46_re_m));
	}
	return x_46_re_s * tmp;
}
x.re\_m = abs(x_46_re)
x.re\_s = copysign(1.0, x_46_re)
function code(x_46_re_s, x_46_re_m, x_46_im)
	t_0 = Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im))
	tmp = 0.0
	if (t_0 <= Float64(-Inf))
		tmp = Float64(Float64(Float64(-3.0 * x_46_im) * x_46_re_m) * x_46_im);
	elseif (t_0 <= 5e+20)
		tmp = fma(Float64(-3.0 * Float64(x_46_im * x_46_im)), x_46_re_m, Float64(Float64(x_46_re_m * x_46_re_m) * x_46_re_m));
	else
		tmp = fma(Float64(x_46_re_m - x_46_im), Float64(Float64(x_46_im + x_46_re_m) * x_46_re_m), Float64(x_46_re_m + x_46_re_m));
	end
	return Float64(x_46_re_s * tmp)
end
x.re\_m = N[Abs[x$46$re], $MachinePrecision]
x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := Block[{t$95$0 = N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision]}, N[(x$46$re$95$s * If[LessEqual[t$95$0, (-Infinity)], N[(N[(N[(-3.0 * x$46$im), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] * x$46$im), $MachinePrecision], If[LessEqual[t$95$0, 5e+20], N[(N[(-3.0 * N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m + N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision]), $MachinePrecision], N[(N[(x$46$re$95$m - x$46$im), $MachinePrecision] * N[(N[(x$46$im + x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] + N[(x$46$re$95$m + x$46$re$95$m), $MachinePrecision]), $MachinePrecision]]]), $MachinePrecision]]
\begin{array}{l}
x.re\_m = \left|x.re\right|
\\
x.re\_s = \mathsf{copysign}\left(1, x.re\right)

\\
\begin{array}{l}
t_0 := \left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im\\
x.re\_s \cdot \begin{array}{l}
\mathbf{if}\;t\_0 \leq -\infty:\\
\;\;\;\;\left(\left(-3 \cdot x.im\right) \cdot x.re\_m\right) \cdot x.im\\

\mathbf{elif}\;t\_0 \leq 5 \cdot 10^{+20}:\\
\;\;\;\;\mathsf{fma}\left(-3 \cdot \left(x.im \cdot x.im\right), x.re\_m, \left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\


\end{array}
\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < -inf.0

    1. Initial program 83.4%

      \[\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 \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\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 \]
      2. lift--.f64N/A

        \[\leadsto \color{blue}{\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 \]
      3. flip3--N/A

        \[\leadsto \color{blue}{\frac{{\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
      4. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
      5. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
    4. Applied rewrites0.0%

      \[\leadsto \color{blue}{\frac{\left(\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right) \cdot \left(\left(x.re - x.im\right) \cdot \left(x.im + x.re\right)\right)\right) \cdot x.re}{\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
    5. Taylor expanded in x.re around 0

      \[\leadsto \color{blue}{x.re \cdot \left(-1 \cdot {x.im}^{2} - 2 \cdot {x.im}^{2}\right)} \]
    6. Step-by-step derivation
      1. distribute-rgt-out--N/A

        \[\leadsto x.re \cdot \color{blue}{\left({x.im}^{2} \cdot \left(-1 - 2\right)\right)} \]
      2. metadata-evalN/A

        \[\leadsto x.re \cdot \left({x.im}^{2} \cdot \color{blue}{-3}\right) \]
      3. *-commutativeN/A

        \[\leadsto x.re \cdot \color{blue}{\left(-3 \cdot {x.im}^{2}\right)} \]
      4. associate-*r*N/A

        \[\leadsto \color{blue}{\left(x.re \cdot -3\right) \cdot {x.im}^{2}} \]
      5. metadata-evalN/A

        \[\leadsto \left(x.re \cdot \color{blue}{\left(-1 - 2\right)}\right) \cdot {x.im}^{2} \]
      6. distribute-rgt-out--N/A

        \[\leadsto \color{blue}{\left(-1 \cdot x.re - 2 \cdot x.re\right)} \cdot {x.im}^{2} \]
      7. unpow2N/A

        \[\leadsto \left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot \color{blue}{\left(x.im \cdot x.im\right)} \]
      8. associate-*r*N/A

        \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right) \cdot x.im} \]
      9. *-commutativeN/A

        \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right)} \cdot x.im \]
      10. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right) \cdot x.im} \]
      11. *-commutativeN/A

        \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right)} \cdot x.im \]
      12. distribute-rgt-out--N/A

        \[\leadsto \left(\color{blue}{\left(x.re \cdot \left(-1 - 2\right)\right)} \cdot x.im\right) \cdot x.im \]
      13. metadata-evalN/A

        \[\leadsto \left(\left(x.re \cdot \color{blue}{-3}\right) \cdot x.im\right) \cdot x.im \]
      14. *-commutativeN/A

        \[\leadsto \left(\color{blue}{\left(-3 \cdot x.re\right)} \cdot x.im\right) \cdot x.im \]
      15. associate-*l*N/A

        \[\leadsto \color{blue}{\left(-3 \cdot \left(x.re \cdot x.im\right)\right)} \cdot x.im \]
      16. *-commutativeN/A

        \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
      17. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right)} \cdot x.im \]
      18. lower-*.f6445.9

        \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
    7. Applied rewrites45.9%

      \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im} \]
    8. Step-by-step derivation
      1. Applied rewrites45.9%

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

      if -inf.0 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < 5e20

      1. Initial program 99.6%

        \[\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 \]
      2. Add Preprocessing
      3. Taylor expanded in x.re around 0

        \[\leadsto \color{blue}{x.re \cdot \left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) - 2 \cdot {x.im}^{2}\right)} \]
      4. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \color{blue}{\left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) - 2 \cdot {x.im}^{2}\right) \cdot x.re} \]
        2. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) - 2 \cdot {x.im}^{2}\right) \cdot x.re} \]
        3. cancel-sign-sub-invN/A

          \[\leadsto \color{blue}{\left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) + \left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2}\right)} \cdot x.re \]
        4. +-commutativeN/A

          \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2} + \left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right)\right)} \cdot x.re \]
        5. associate-+r+N/A

          \[\leadsto \color{blue}{\left(\left(\left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2} + -1 \cdot {x.im}^{2}\right) + {x.re}^{2}\right)} \cdot x.re \]
        6. +-commutativeN/A

          \[\leadsto \left(\color{blue}{\left(-1 \cdot {x.im}^{2} + \left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2}\right)} + {x.re}^{2}\right) \cdot x.re \]
        7. cancel-sign-sub-invN/A

          \[\leadsto \left(\color{blue}{\left(-1 \cdot {x.im}^{2} - 2 \cdot {x.im}^{2}\right)} + {x.re}^{2}\right) \cdot x.re \]
        8. distribute-rgt-out--N/A

          \[\leadsto \left(\color{blue}{{x.im}^{2} \cdot \left(-1 - 2\right)} + {x.re}^{2}\right) \cdot x.re \]
        9. *-commutativeN/A

          \[\leadsto \left(\color{blue}{\left(-1 - 2\right) \cdot {x.im}^{2}} + {x.re}^{2}\right) \cdot x.re \]
        10. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(-1 - 2, {x.im}^{2}, {x.re}^{2}\right)} \cdot x.re \]
        11. metadata-evalN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{-3}, {x.im}^{2}, {x.re}^{2}\right) \cdot x.re \]
        12. unpow2N/A

          \[\leadsto \mathsf{fma}\left(-3, \color{blue}{x.im \cdot x.im}, {x.re}^{2}\right) \cdot x.re \]
        13. lower-*.f64N/A

          \[\leadsto \mathsf{fma}\left(-3, \color{blue}{x.im \cdot x.im}, {x.re}^{2}\right) \cdot x.re \]
        14. unpow2N/A

          \[\leadsto \mathsf{fma}\left(-3, x.im \cdot x.im, \color{blue}{x.re \cdot x.re}\right) \cdot x.re \]
        15. lower-*.f6499.6

          \[\leadsto \mathsf{fma}\left(-3, x.im \cdot x.im, \color{blue}{x.re \cdot x.re}\right) \cdot x.re \]
      5. Applied rewrites99.6%

        \[\leadsto \color{blue}{\mathsf{fma}\left(-3, x.im \cdot x.im, x.re \cdot x.re\right) \cdot x.re} \]
      6. Step-by-step derivation
        1. Applied rewrites99.6%

          \[\leadsto \mathsf{fma}\left(\left(x.im \cdot x.im\right) \cdot -3, \color{blue}{x.re}, \left(x.re \cdot x.re\right) \cdot x.re\right) \]

        if 5e20 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

        1. Initial program 59.0%

          \[\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 \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift--.f64N/A

            \[\leadsto \color{blue}{\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} \]
          2. sub-negN/A

            \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
          3. +-commutativeN/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
          4. lift-*.f64N/A

            \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
          5. distribute-rgt-neg-inN/A

            \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
          6. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
          7. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          8. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          9. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          10. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          11. distribute-lft-outN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          12. lower-*.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          13. lower-+.f64N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          14. lower-neg.f6467.8

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
          15. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
          16. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
          17. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
          18. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
          19. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
          20. difference-of-squaresN/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
          21. associate-*r*N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
          22. lower-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
        4. Applied rewrites82.3%

          \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]
        5. Step-by-step derivation
          1. lift-fma.f64N/A

            \[\leadsto \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) + \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right) + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} \]
          3. lift-*.f64N/A

            \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
          4. *-commutativeN/A

            \[\leadsto \color{blue}{\left(x.re - x.im\right) \cdot \left(x.re \cdot \left(x.im + x.re\right)\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, x.re \cdot \left(x.im + x.re\right), \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right)} \]
          6. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{x.re \cdot \left(x.im + x.re\right)}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          7. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          8. lower-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          9. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          10. +-commutativeN/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          11. lower-+.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          12. lift-neg.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(x.im\right)\right)}\right) \]
          13. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          14. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          15. distribute-lft-inN/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          16. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          17. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          18. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          19. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
          20. distribute-rgt-neg-inN/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)}\right) \]
          21. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(\color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
          22. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
          23. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right)\right)\right) \]
          24. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
          25. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
        6. Applied rewrites87.3%

          \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, x.re + x.re\right)} \]
      7. Recombined 3 regimes into one program.
      8. Final simplification81.0%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq -\infty:\\ \;\;\;\;\left(\left(-3 \cdot x.im\right) \cdot x.re\right) \cdot x.im\\ \mathbf{elif}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(-3 \cdot \left(x.im \cdot x.im\right), x.re, \left(x.re \cdot x.re\right) \cdot x.re\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re - x.im, \left(x.im + x.re\right) \cdot x.re, x.re + x.re\right)\\ \end{array} \]
      9. Add Preprocessing

      Alternative 3: 99.7% accurate, 0.4× speedup?

      \[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ \begin{array}{l} t_0 := \left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im\\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;t\_0 \leq -\infty:\\ \;\;\;\;\left(\left(-3 \cdot x.im\right) \cdot x.re\_m\right) \cdot x.im\\ \mathbf{elif}\;t\_0 \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(-3, x.im \cdot x.im, x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\ \end{array} \end{array} \end{array} \]
      x.re\_m = (fabs.f64 x.re)
      x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
      (FPCore (x.re_s x.re_m x.im)
       :precision binary64
       (let* ((t_0
               (-
                (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
                (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))))
         (*
          x.re_s
          (if (<= t_0 (- INFINITY))
            (* (* (* -3.0 x.im) x.re_m) x.im)
            (if (<= t_0 5e+20)
              (* (fma -3.0 (* x.im x.im) (* x.re_m x.re_m)) x.re_m)
              (fma (- x.re_m x.im) (* (+ x.im x.re_m) x.re_m) (+ x.re_m x.re_m)))))))
      x.re\_m = fabs(x_46_re);
      x.re\_s = copysign(1.0, x_46_re);
      double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
      	double t_0 = (((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im);
      	double tmp;
      	if (t_0 <= -((double) INFINITY)) {
      		tmp = ((-3.0 * x_46_im) * x_46_re_m) * x_46_im;
      	} else if (t_0 <= 5e+20) {
      		tmp = fma(-3.0, (x_46_im * x_46_im), (x_46_re_m * x_46_re_m)) * x_46_re_m;
      	} else {
      		tmp = fma((x_46_re_m - x_46_im), ((x_46_im + x_46_re_m) * x_46_re_m), (x_46_re_m + x_46_re_m));
      	}
      	return x_46_re_s * tmp;
      }
      
      x.re\_m = abs(x_46_re)
      x.re\_s = copysign(1.0, x_46_re)
      function code(x_46_re_s, x_46_re_m, x_46_im)
      	t_0 = Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im))
      	tmp = 0.0
      	if (t_0 <= Float64(-Inf))
      		tmp = Float64(Float64(Float64(-3.0 * x_46_im) * x_46_re_m) * x_46_im);
      	elseif (t_0 <= 5e+20)
      		tmp = Float64(fma(-3.0, Float64(x_46_im * x_46_im), Float64(x_46_re_m * x_46_re_m)) * x_46_re_m);
      	else
      		tmp = fma(Float64(x_46_re_m - x_46_im), Float64(Float64(x_46_im + x_46_re_m) * x_46_re_m), Float64(x_46_re_m + x_46_re_m));
      	end
      	return Float64(x_46_re_s * tmp)
      end
      
      x.re\_m = N[Abs[x$46$re], $MachinePrecision]
      x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := Block[{t$95$0 = N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision]}, N[(x$46$re$95$s * If[LessEqual[t$95$0, (-Infinity)], N[(N[(N[(-3.0 * x$46$im), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] * x$46$im), $MachinePrecision], If[LessEqual[t$95$0, 5e+20], N[(N[(-3.0 * N[(x$46$im * x$46$im), $MachinePrecision] + N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision], N[(N[(x$46$re$95$m - x$46$im), $MachinePrecision] * N[(N[(x$46$im + x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] + N[(x$46$re$95$m + x$46$re$95$m), $MachinePrecision]), $MachinePrecision]]]), $MachinePrecision]]
      
      \begin{array}{l}
      x.re\_m = \left|x.re\right|
      \\
      x.re\_s = \mathsf{copysign}\left(1, x.re\right)
      
      \\
      \begin{array}{l}
      t_0 := \left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im\\
      x.re\_s \cdot \begin{array}{l}
      \mathbf{if}\;t\_0 \leq -\infty:\\
      \;\;\;\;\left(\left(-3 \cdot x.im\right) \cdot x.re\_m\right) \cdot x.im\\
      
      \mathbf{elif}\;t\_0 \leq 5 \cdot 10^{+20}:\\
      \;\;\;\;\mathsf{fma}\left(-3, x.im \cdot x.im, x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\
      
      \mathbf{else}:\\
      \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\
      
      
      \end{array}
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < -inf.0

        1. Initial program 83.4%

          \[\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 \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \color{blue}{\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 \]
          2. lift--.f64N/A

            \[\leadsto \color{blue}{\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 \]
          3. flip3--N/A

            \[\leadsto \color{blue}{\frac{{\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
          4. associate-*l/N/A

            \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
          5. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
        4. Applied rewrites0.0%

          \[\leadsto \color{blue}{\frac{\left(\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right) \cdot \left(\left(x.re - x.im\right) \cdot \left(x.im + x.re\right)\right)\right) \cdot x.re}{\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
        5. Taylor expanded in x.re around 0

          \[\leadsto \color{blue}{x.re \cdot \left(-1 \cdot {x.im}^{2} - 2 \cdot {x.im}^{2}\right)} \]
        6. Step-by-step derivation
          1. distribute-rgt-out--N/A

            \[\leadsto x.re \cdot \color{blue}{\left({x.im}^{2} \cdot \left(-1 - 2\right)\right)} \]
          2. metadata-evalN/A

            \[\leadsto x.re \cdot \left({x.im}^{2} \cdot \color{blue}{-3}\right) \]
          3. *-commutativeN/A

            \[\leadsto x.re \cdot \color{blue}{\left(-3 \cdot {x.im}^{2}\right)} \]
          4. associate-*r*N/A

            \[\leadsto \color{blue}{\left(x.re \cdot -3\right) \cdot {x.im}^{2}} \]
          5. metadata-evalN/A

            \[\leadsto \left(x.re \cdot \color{blue}{\left(-1 - 2\right)}\right) \cdot {x.im}^{2} \]
          6. distribute-rgt-out--N/A

            \[\leadsto \color{blue}{\left(-1 \cdot x.re - 2 \cdot x.re\right)} \cdot {x.im}^{2} \]
          7. unpow2N/A

            \[\leadsto \left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot \color{blue}{\left(x.im \cdot x.im\right)} \]
          8. associate-*r*N/A

            \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right) \cdot x.im} \]
          9. *-commutativeN/A

            \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right)} \cdot x.im \]
          10. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right) \cdot x.im} \]
          11. *-commutativeN/A

            \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right)} \cdot x.im \]
          12. distribute-rgt-out--N/A

            \[\leadsto \left(\color{blue}{\left(x.re \cdot \left(-1 - 2\right)\right)} \cdot x.im\right) \cdot x.im \]
          13. metadata-evalN/A

            \[\leadsto \left(\left(x.re \cdot \color{blue}{-3}\right) \cdot x.im\right) \cdot x.im \]
          14. *-commutativeN/A

            \[\leadsto \left(\color{blue}{\left(-3 \cdot x.re\right)} \cdot x.im\right) \cdot x.im \]
          15. associate-*l*N/A

            \[\leadsto \color{blue}{\left(-3 \cdot \left(x.re \cdot x.im\right)\right)} \cdot x.im \]
          16. *-commutativeN/A

            \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
          17. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right)} \cdot x.im \]
          18. lower-*.f6445.9

            \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
        7. Applied rewrites45.9%

          \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im} \]
        8. Step-by-step derivation
          1. Applied rewrites45.9%

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

          if -inf.0 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < 5e20

          1. Initial program 99.6%

            \[\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 \]
          2. Add Preprocessing
          3. Taylor expanded in x.re around 0

            \[\leadsto \color{blue}{x.re \cdot \left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) - 2 \cdot {x.im}^{2}\right)} \]
          4. Step-by-step derivation
            1. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) - 2 \cdot {x.im}^{2}\right) \cdot x.re} \]
            2. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) - 2 \cdot {x.im}^{2}\right) \cdot x.re} \]
            3. cancel-sign-sub-invN/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right) + \left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2}\right)} \cdot x.re \]
            4. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2} + \left(-1 \cdot {x.im}^{2} + {x.re}^{2}\right)\right)} \cdot x.re \]
            5. associate-+r+N/A

              \[\leadsto \color{blue}{\left(\left(\left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2} + -1 \cdot {x.im}^{2}\right) + {x.re}^{2}\right)} \cdot x.re \]
            6. +-commutativeN/A

              \[\leadsto \left(\color{blue}{\left(-1 \cdot {x.im}^{2} + \left(\mathsf{neg}\left(2\right)\right) \cdot {x.im}^{2}\right)} + {x.re}^{2}\right) \cdot x.re \]
            7. cancel-sign-sub-invN/A

              \[\leadsto \left(\color{blue}{\left(-1 \cdot {x.im}^{2} - 2 \cdot {x.im}^{2}\right)} + {x.re}^{2}\right) \cdot x.re \]
            8. distribute-rgt-out--N/A

              \[\leadsto \left(\color{blue}{{x.im}^{2} \cdot \left(-1 - 2\right)} + {x.re}^{2}\right) \cdot x.re \]
            9. *-commutativeN/A

              \[\leadsto \left(\color{blue}{\left(-1 - 2\right) \cdot {x.im}^{2}} + {x.re}^{2}\right) \cdot x.re \]
            10. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(-1 - 2, {x.im}^{2}, {x.re}^{2}\right)} \cdot x.re \]
            11. metadata-evalN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{-3}, {x.im}^{2}, {x.re}^{2}\right) \cdot x.re \]
            12. unpow2N/A

              \[\leadsto \mathsf{fma}\left(-3, \color{blue}{x.im \cdot x.im}, {x.re}^{2}\right) \cdot x.re \]
            13. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(-3, \color{blue}{x.im \cdot x.im}, {x.re}^{2}\right) \cdot x.re \]
            14. unpow2N/A

              \[\leadsto \mathsf{fma}\left(-3, x.im \cdot x.im, \color{blue}{x.re \cdot x.re}\right) \cdot x.re \]
            15. lower-*.f6499.6

              \[\leadsto \mathsf{fma}\left(-3, x.im \cdot x.im, \color{blue}{x.re \cdot x.re}\right) \cdot x.re \]
          5. Applied rewrites99.6%

            \[\leadsto \color{blue}{\mathsf{fma}\left(-3, x.im \cdot x.im, x.re \cdot x.re\right) \cdot x.re} \]

          if 5e20 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

          1. Initial program 59.0%

            \[\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 \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

              \[\leadsto \color{blue}{\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} \]
            2. sub-negN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
            3. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
            4. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            5. distribute-rgt-neg-inN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            6. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
            7. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            8. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            9. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            10. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            11. distribute-lft-outN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            12. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            13. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            14. lower-neg.f6467.8

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            15. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            17. lift--.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
            19. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
            20. difference-of-squaresN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
            21. associate-*r*N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
            22. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
          4. Applied rewrites82.3%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]
          5. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) + \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right) + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} \]
            3. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            4. *-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re - x.im\right) \cdot \left(x.re \cdot \left(x.im + x.re\right)\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            5. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, x.re \cdot \left(x.im + x.re\right), \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right)} \]
            6. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{x.re \cdot \left(x.im + x.re\right)}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            7. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            8. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            9. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            10. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            11. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            12. lift-neg.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(x.im\right)\right)}\right) \]
            13. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            14. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            15. distribute-lft-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            17. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            19. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            20. distribute-rgt-neg-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)}\right) \]
            21. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(\color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            22. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            23. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right)\right)\right) \]
            24. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
            25. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
          6. Applied rewrites87.3%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, x.re + x.re\right)} \]
        9. Recombined 3 regimes into one program.
        10. Final simplification81.0%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq -\infty:\\ \;\;\;\;\left(\left(-3 \cdot x.im\right) \cdot x.re\right) \cdot x.im\\ \mathbf{elif}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(-3, x.im \cdot x.im, x.re \cdot x.re\right) \cdot x.re\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re - x.im, \left(x.im + x.re\right) \cdot x.re, x.re + x.re\right)\\ \end{array} \]
        11. Add Preprocessing

        Alternative 4: 99.0% accurate, 0.4× speedup?

        \[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ \begin{array}{l} t_0 := \left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im\\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;t\_0 \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(-3 \cdot \left(x.im \cdot x.re\_m\right)\right) \cdot x.im\\ \mathbf{elif}\;t\_0 \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\ \end{array} \end{array} \end{array} \]
        x.re\_m = (fabs.f64 x.re)
        x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
        (FPCore (x.re_s x.re_m x.im)
         :precision binary64
         (let* ((t_0
                 (-
                  (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
                  (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))))
           (*
            x.re_s
            (if (<= t_0 -4e-298)
              (* (* -3.0 (* x.im x.re_m)) x.im)
              (if (<= t_0 5e+20)
                (* (* x.re_m x.re_m) x.re_m)
                (fma (- x.re_m x.im) (* (+ x.im x.re_m) x.re_m) (+ x.re_m x.re_m)))))))
        x.re\_m = fabs(x_46_re);
        x.re\_s = copysign(1.0, x_46_re);
        double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double t_0 = (((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im);
        	double tmp;
        	if (t_0 <= -4e-298) {
        		tmp = (-3.0 * (x_46_im * x_46_re_m)) * x_46_im;
        	} else if (t_0 <= 5e+20) {
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	} else {
        		tmp = fma((x_46_re_m - x_46_im), ((x_46_im + x_46_re_m) * x_46_re_m), (x_46_re_m + x_46_re_m));
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = abs(x_46_re)
        x.re\_s = copysign(1.0, x_46_re)
        function code(x_46_re_s, x_46_re_m, x_46_im)
        	t_0 = Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im))
        	tmp = 0.0
        	if (t_0 <= -4e-298)
        		tmp = Float64(Float64(-3.0 * Float64(x_46_im * x_46_re_m)) * x_46_im);
        	elseif (t_0 <= 5e+20)
        		tmp = Float64(Float64(x_46_re_m * x_46_re_m) * x_46_re_m);
        	else
        		tmp = fma(Float64(x_46_re_m - x_46_im), Float64(Float64(x_46_im + x_46_re_m) * x_46_re_m), Float64(x_46_re_m + x_46_re_m));
        	end
        	return Float64(x_46_re_s * tmp)
        end
        
        x.re\_m = N[Abs[x$46$re], $MachinePrecision]
        x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := Block[{t$95$0 = N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision]}, N[(x$46$re$95$s * If[LessEqual[t$95$0, -4e-298], N[(N[(-3.0 * N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision], If[LessEqual[t$95$0, 5e+20], N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision], N[(N[(x$46$re$95$m - x$46$im), $MachinePrecision] * N[(N[(x$46$im + x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] + N[(x$46$re$95$m + x$46$re$95$m), $MachinePrecision]), $MachinePrecision]]]), $MachinePrecision]]
        
        \begin{array}{l}
        x.re\_m = \left|x.re\right|
        \\
        x.re\_s = \mathsf{copysign}\left(1, x.re\right)
        
        \\
        \begin{array}{l}
        t_0 := \left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im\\
        x.re\_s \cdot \begin{array}{l}
        \mathbf{if}\;t\_0 \leq -4 \cdot 10^{-298}:\\
        \;\;\;\;\left(-3 \cdot \left(x.im \cdot x.re\_m\right)\right) \cdot x.im\\
        
        \mathbf{elif}\;t\_0 \leq 5 \cdot 10^{+20}:\\
        \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\
        
        \mathbf{else}:\\
        \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, \left(x.im + x.re\_m\right) \cdot x.re\_m, x.re\_m + x.re\_m\right)\\
        
        
        \end{array}
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 3 regimes
        2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < -3.99999999999999965e-298

          1. Initial program 89.8%

            \[\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 \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\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 \]
            2. lift--.f64N/A

              \[\leadsto \color{blue}{\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 \]
            3. flip3--N/A

              \[\leadsto \color{blue}{\frac{{\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
            4. associate-*l/N/A

              \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
            5. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
          4. Applied rewrites13.9%

            \[\leadsto \color{blue}{\frac{\left(\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right) \cdot \left(\left(x.re - x.im\right) \cdot \left(x.im + x.re\right)\right)\right) \cdot x.re}{\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
          5. Taylor expanded in x.re around 0

            \[\leadsto \color{blue}{x.re \cdot \left(-1 \cdot {x.im}^{2} - 2 \cdot {x.im}^{2}\right)} \]
          6. Step-by-step derivation
            1. distribute-rgt-out--N/A

              \[\leadsto x.re \cdot \color{blue}{\left({x.im}^{2} \cdot \left(-1 - 2\right)\right)} \]
            2. metadata-evalN/A

              \[\leadsto x.re \cdot \left({x.im}^{2} \cdot \color{blue}{-3}\right) \]
            3. *-commutativeN/A

              \[\leadsto x.re \cdot \color{blue}{\left(-3 \cdot {x.im}^{2}\right)} \]
            4. associate-*r*N/A

              \[\leadsto \color{blue}{\left(x.re \cdot -3\right) \cdot {x.im}^{2}} \]
            5. metadata-evalN/A

              \[\leadsto \left(x.re \cdot \color{blue}{\left(-1 - 2\right)}\right) \cdot {x.im}^{2} \]
            6. distribute-rgt-out--N/A

              \[\leadsto \color{blue}{\left(-1 \cdot x.re - 2 \cdot x.re\right)} \cdot {x.im}^{2} \]
            7. unpow2N/A

              \[\leadsto \left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot \color{blue}{\left(x.im \cdot x.im\right)} \]
            8. associate-*r*N/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right) \cdot x.im} \]
            9. *-commutativeN/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right)} \cdot x.im \]
            10. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right) \cdot x.im} \]
            11. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right)} \cdot x.im \]
            12. distribute-rgt-out--N/A

              \[\leadsto \left(\color{blue}{\left(x.re \cdot \left(-1 - 2\right)\right)} \cdot x.im\right) \cdot x.im \]
            13. metadata-evalN/A

              \[\leadsto \left(\left(x.re \cdot \color{blue}{-3}\right) \cdot x.im\right) \cdot x.im \]
            14. *-commutativeN/A

              \[\leadsto \left(\color{blue}{\left(-3 \cdot x.re\right)} \cdot x.im\right) \cdot x.im \]
            15. associate-*l*N/A

              \[\leadsto \color{blue}{\left(-3 \cdot \left(x.re \cdot x.im\right)\right)} \cdot x.im \]
            16. *-commutativeN/A

              \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
            17. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right)} \cdot x.im \]
            18. lower-*.f6450.6

              \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
          7. Applied rewrites50.6%

            \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im} \]

          if -3.99999999999999965e-298 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < 5e20

          1. Initial program 99.8%

            \[\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 \]
          2. Add Preprocessing
          3. Taylor expanded in x.re around inf

            \[\leadsto \color{blue}{{x.re}^{3}} \]
          4. Step-by-step derivation
            1. unpow3N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
            2. unpow2N/A

              \[\leadsto \color{blue}{{x.re}^{2}} \cdot x.re \]
            3. lower-*.f64N/A

              \[\leadsto \color{blue}{{x.re}^{2} \cdot x.re} \]
            4. unpow2N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
            5. lower-*.f6474.2

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
          5. Applied rewrites74.2%

            \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]

          if 5e20 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

          1. Initial program 59.0%

            \[\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 \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

              \[\leadsto \color{blue}{\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} \]
            2. sub-negN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
            3. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
            4. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            5. distribute-rgt-neg-inN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            6. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
            7. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            8. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            9. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            10. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            11. distribute-lft-outN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            12. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            13. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            14. lower-neg.f6467.8

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            15. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            17. lift--.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
            19. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
            20. difference-of-squaresN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
            21. associate-*r*N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
            22. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
          4. Applied rewrites82.3%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]
          5. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) + \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right) + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} \]
            3. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            4. *-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re - x.im\right) \cdot \left(x.re \cdot \left(x.im + x.re\right)\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            5. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, x.re \cdot \left(x.im + x.re\right), \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right)} \]
            6. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{x.re \cdot \left(x.im + x.re\right)}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            7. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            8. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            9. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            10. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            11. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            12. lift-neg.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(x.im\right)\right)}\right) \]
            13. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            14. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            15. distribute-lft-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            17. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            19. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            20. distribute-rgt-neg-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)}\right) \]
            21. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(\color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            22. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            23. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right)\right)\right) \]
            24. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
            25. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
          6. Applied rewrites87.3%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, x.re + x.re\right)} \]
        3. Recombined 3 regimes into one program.
        4. Final simplification68.5%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(-3 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im\\ \mathbf{elif}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\left(x.re \cdot x.re\right) \cdot x.re\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re - x.im, \left(x.im + x.re\right) \cdot x.re, x.re + x.re\right)\\ \end{array} \]
        5. Add Preprocessing

        Alternative 5: 99.7% accurate, 0.5× speedup?

        \[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ \begin{array}{l} t_0 := \left(x.im + x.re\_m\right) \cdot x.re\_m\\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(\left(x.re\_m + x.re\_m\right) \cdot x.im, -x.im, t\_0 \cdot \left(x.re\_m - x.im\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, t\_0, x.re\_m + x.re\_m\right)\\ \end{array} \end{array} \end{array} \]
        x.re\_m = (fabs.f64 x.re)
        x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
        (FPCore (x.re_s x.re_m x.im)
         :precision binary64
         (let* ((t_0 (* (+ x.im x.re_m) x.re_m)))
           (*
            x.re_s
            (if (<=
                 (-
                  (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
                  (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))
                 5e+20)
              (fma (* (+ x.re_m x.re_m) x.im) (- x.im) (* t_0 (- x.re_m x.im)))
              (fma (- x.re_m x.im) t_0 (+ x.re_m x.re_m))))))
        x.re\_m = fabs(x_46_re);
        x.re\_s = copysign(1.0, x_46_re);
        double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double t_0 = (x_46_im + x_46_re_m) * x_46_re_m;
        	double tmp;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= 5e+20) {
        		tmp = fma(((x_46_re_m + x_46_re_m) * x_46_im), -x_46_im, (t_0 * (x_46_re_m - x_46_im)));
        	} else {
        		tmp = fma((x_46_re_m - x_46_im), t_0, (x_46_re_m + x_46_re_m));
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = abs(x_46_re)
        x.re\_s = copysign(1.0, x_46_re)
        function code(x_46_re_s, x_46_re_m, x_46_im)
        	t_0 = Float64(Float64(x_46_im + x_46_re_m) * x_46_re_m)
        	tmp = 0.0
        	if (Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im)) <= 5e+20)
        		tmp = fma(Float64(Float64(x_46_re_m + x_46_re_m) * x_46_im), Float64(-x_46_im), Float64(t_0 * Float64(x_46_re_m - x_46_im)));
        	else
        		tmp = fma(Float64(x_46_re_m - x_46_im), t_0, Float64(x_46_re_m + x_46_re_m));
        	end
        	return Float64(x_46_re_s * tmp)
        end
        
        x.re\_m = N[Abs[x$46$re], $MachinePrecision]
        x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := Block[{t$95$0 = N[(N[(x$46$im + x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision]}, N[(x$46$re$95$s * If[LessEqual[N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision], 5e+20], N[(N[(N[(x$46$re$95$m + x$46$re$95$m), $MachinePrecision] * x$46$im), $MachinePrecision] * (-x$46$im) + N[(t$95$0 * N[(x$46$re$95$m - x$46$im), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$46$re$95$m - x$46$im), $MachinePrecision] * t$95$0 + N[(x$46$re$95$m + x$46$re$95$m), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]]
        
        \begin{array}{l}
        x.re\_m = \left|x.re\right|
        \\
        x.re\_s = \mathsf{copysign}\left(1, x.re\right)
        
        \\
        \begin{array}{l}
        t_0 := \left(x.im + x.re\_m\right) \cdot x.re\_m\\
        x.re\_s \cdot \begin{array}{l}
        \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\
        \;\;\;\;\mathsf{fma}\left(\left(x.re\_m + x.re\_m\right) \cdot x.im, -x.im, t\_0 \cdot \left(x.re\_m - x.im\right)\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;\mathsf{fma}\left(x.re\_m - x.im, t\_0, x.re\_m + x.re\_m\right)\\
        
        
        \end{array}
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < 5e20

          1. Initial program 92.9%

            \[\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 \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

              \[\leadsto \color{blue}{\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} \]
            2. sub-negN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
            3. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
            4. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            5. distribute-rgt-neg-inN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            6. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
            7. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            8. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            9. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            10. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            11. distribute-lft-outN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            12. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            13. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            14. lower-neg.f6493.0

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            15. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            17. lift--.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
            19. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
            20. difference-of-squaresN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
            21. associate-*r*N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
            22. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
          4. Applied rewrites99.8%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]

          if 5e20 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

          1. Initial program 59.0%

            \[\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 \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

              \[\leadsto \color{blue}{\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} \]
            2. sub-negN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
            3. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
            4. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            5. distribute-rgt-neg-inN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            6. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
            7. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            8. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            9. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            10. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            11. distribute-lft-outN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            12. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            13. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            14. lower-neg.f6467.8

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            15. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            17. lift--.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
            19. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
            20. difference-of-squaresN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
            21. associate-*r*N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
            22. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
          4. Applied rewrites82.3%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]
          5. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) + \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right) + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} \]
            3. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            4. *-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re - x.im\right) \cdot \left(x.re \cdot \left(x.im + x.re\right)\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            5. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, x.re \cdot \left(x.im + x.re\right), \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right)} \]
            6. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{x.re \cdot \left(x.im + x.re\right)}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            7. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            8. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            9. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            10. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            11. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            12. lift-neg.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(x.im\right)\right)}\right) \]
            13. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            14. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            15. distribute-lft-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            17. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            19. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            20. distribute-rgt-neg-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)}\right) \]
            21. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(\color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            22. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            23. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right)\right)\right) \]
            24. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
            25. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
          6. Applied rewrites87.3%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, x.re + x.re\right)} \]
        3. Recombined 2 regimes into one program.
        4. Final simplification95.3%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq 5 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(\left(x.re + x.re\right) \cdot x.im, -x.im, \left(\left(x.im + x.re\right) \cdot x.re\right) \cdot \left(x.re - x.im\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x.re - x.im, \left(x.im + x.re\right) \cdot x.re, x.re + x.re\right)\\ \end{array} \]
        5. Add Preprocessing

        Alternative 6: 96.4% accurate, 0.7× speedup?

        \[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(-3 \cdot \left(x.im \cdot x.re\_m\right)\right) \cdot x.im\\ \mathbf{else}:\\ \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\ \end{array} \end{array} \]
        x.re\_m = (fabs.f64 x.re)
        x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
        (FPCore (x.re_s x.re_m x.im)
         :precision binary64
         (*
          x.re_s
          (if (<=
               (-
                (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
                (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))
               -4e-298)
            (* (* -3.0 (* x.im x.re_m)) x.im)
            (* (* x.re_m x.re_m) x.re_m))))
        x.re\_m = fabs(x_46_re);
        x.re\_s = copysign(1.0, x_46_re);
        double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double tmp;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298) {
        		tmp = (-3.0 * (x_46_im * x_46_re_m)) * x_46_im;
        	} else {
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = abs(x_46re)
        x.re\_s = copysign(1.0d0, x_46re)
        real(8) function code(x_46re_s, x_46re_m, x_46im)
            real(8), intent (in) :: x_46re_s
            real(8), intent (in) :: x_46re_m
            real(8), intent (in) :: x_46im
            real(8) :: tmp
            if (((((x_46re_m * x_46re_m) - (x_46im * x_46im)) * x_46re_m) - (((x_46im * x_46re_m) + (x_46im * x_46re_m)) * x_46im)) <= (-4d-298)) then
                tmp = ((-3.0d0) * (x_46im * x_46re_m)) * x_46im
            else
                tmp = (x_46re_m * x_46re_m) * x_46re_m
            end if
            code = x_46re_s * tmp
        end function
        
        x.re\_m = Math.abs(x_46_re);
        x.re\_s = Math.copySign(1.0, x_46_re);
        public static double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double tmp;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298) {
        		tmp = (-3.0 * (x_46_im * x_46_re_m)) * x_46_im;
        	} else {
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = math.fabs(x_46_re)
        x.re\_s = math.copysign(1.0, x_46_re)
        def code(x_46_re_s, x_46_re_m, x_46_im):
        	tmp = 0
        	if ((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298:
        		tmp = (-3.0 * (x_46_im * x_46_re_m)) * x_46_im
        	else:
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m
        	return x_46_re_s * tmp
        
        x.re\_m = abs(x_46_re)
        x.re\_s = copysign(1.0, x_46_re)
        function code(x_46_re_s, x_46_re_m, x_46_im)
        	tmp = 0.0
        	if (Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298)
        		tmp = Float64(Float64(-3.0 * Float64(x_46_im * x_46_re_m)) * x_46_im);
        	else
        		tmp = Float64(Float64(x_46_re_m * x_46_re_m) * x_46_re_m);
        	end
        	return Float64(x_46_re_s * tmp)
        end
        
        x.re\_m = abs(x_46_re);
        x.re\_s = sign(x_46_re) * abs(1.0);
        function tmp_2 = code(x_46_re_s, x_46_re_m, x_46_im)
        	tmp = 0.0;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298)
        		tmp = (-3.0 * (x_46_im * x_46_re_m)) * x_46_im;
        	else
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	end
        	tmp_2 = x_46_re_s * tmp;
        end
        
        x.re\_m = N[Abs[x$46$re], $MachinePrecision]
        x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := N[(x$46$re$95$s * If[LessEqual[N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision], -4e-298], N[(N[(-3.0 * N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision], N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision]]), $MachinePrecision]
        
        \begin{array}{l}
        x.re\_m = \left|x.re\right|
        \\
        x.re\_s = \mathsf{copysign}\left(1, x.re\right)
        
        \\
        x.re\_s \cdot \begin{array}{l}
        \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\
        \;\;\;\;\left(-3 \cdot \left(x.im \cdot x.re\_m\right)\right) \cdot x.im\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < -3.99999999999999965e-298

          1. Initial program 89.8%

            \[\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 \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\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 \]
            2. lift--.f64N/A

              \[\leadsto \color{blue}{\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 \]
            3. flip3--N/A

              \[\leadsto \color{blue}{\frac{{\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
            4. associate-*l/N/A

              \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
            5. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left({\left(x.re \cdot x.re\right)}^{3} - {\left(x.im \cdot x.im\right)}^{3}\right) \cdot x.re}{\left(x.re \cdot x.re\right) \cdot \left(x.re \cdot x.re\right) + \left(\left(x.im \cdot x.im\right) \cdot \left(x.im \cdot x.im\right) + \left(x.re \cdot x.re\right) \cdot \left(x.im \cdot x.im\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
          4. Applied rewrites13.9%

            \[\leadsto \color{blue}{\frac{\left(\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right) \cdot \left(\left(x.re - x.im\right) \cdot \left(x.im + x.re\right)\right)\right) \cdot x.re}{\mathsf{fma}\left(\left(x.re \cdot x.re\right) \cdot x.re, x.re, \left(x.im \cdot x.im\right) \cdot \mathsf{fma}\left(x.im, x.im, x.re \cdot x.re\right)\right)}} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im \]
          5. Taylor expanded in x.re around 0

            \[\leadsto \color{blue}{x.re \cdot \left(-1 \cdot {x.im}^{2} - 2 \cdot {x.im}^{2}\right)} \]
          6. Step-by-step derivation
            1. distribute-rgt-out--N/A

              \[\leadsto x.re \cdot \color{blue}{\left({x.im}^{2} \cdot \left(-1 - 2\right)\right)} \]
            2. metadata-evalN/A

              \[\leadsto x.re \cdot \left({x.im}^{2} \cdot \color{blue}{-3}\right) \]
            3. *-commutativeN/A

              \[\leadsto x.re \cdot \color{blue}{\left(-3 \cdot {x.im}^{2}\right)} \]
            4. associate-*r*N/A

              \[\leadsto \color{blue}{\left(x.re \cdot -3\right) \cdot {x.im}^{2}} \]
            5. metadata-evalN/A

              \[\leadsto \left(x.re \cdot \color{blue}{\left(-1 - 2\right)}\right) \cdot {x.im}^{2} \]
            6. distribute-rgt-out--N/A

              \[\leadsto \color{blue}{\left(-1 \cdot x.re - 2 \cdot x.re\right)} \cdot {x.im}^{2} \]
            7. unpow2N/A

              \[\leadsto \left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot \color{blue}{\left(x.im \cdot x.im\right)} \]
            8. associate-*r*N/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right) \cdot x.im} \]
            9. *-commutativeN/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right)} \cdot x.im \]
            10. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(-1 \cdot x.re - 2 \cdot x.re\right)\right) \cdot x.im} \]
            11. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re - 2 \cdot x.re\right) \cdot x.im\right)} \cdot x.im \]
            12. distribute-rgt-out--N/A

              \[\leadsto \left(\color{blue}{\left(x.re \cdot \left(-1 - 2\right)\right)} \cdot x.im\right) \cdot x.im \]
            13. metadata-evalN/A

              \[\leadsto \left(\left(x.re \cdot \color{blue}{-3}\right) \cdot x.im\right) \cdot x.im \]
            14. *-commutativeN/A

              \[\leadsto \left(\color{blue}{\left(-3 \cdot x.re\right)} \cdot x.im\right) \cdot x.im \]
            15. associate-*l*N/A

              \[\leadsto \color{blue}{\left(-3 \cdot \left(x.re \cdot x.im\right)\right)} \cdot x.im \]
            16. *-commutativeN/A

              \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
            17. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right)} \cdot x.im \]
            18. lower-*.f6450.6

              \[\leadsto \left(-3 \cdot \color{blue}{\left(x.im \cdot x.re\right)}\right) \cdot x.im \]
          7. Applied rewrites50.6%

            \[\leadsto \color{blue}{\left(-3 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im} \]

          if -3.99999999999999965e-298 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

          1. Initial program 73.8%

            \[\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 \]
          2. Add Preprocessing
          3. Taylor expanded in x.re around inf

            \[\leadsto \color{blue}{{x.re}^{3}} \]
          4. Step-by-step derivation
            1. unpow3N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
            2. unpow2N/A

              \[\leadsto \color{blue}{{x.re}^{2}} \cdot x.re \]
            3. lower-*.f64N/A

              \[\leadsto \color{blue}{{x.re}^{2} \cdot x.re} \]
            4. unpow2N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
            5. lower-*.f6469.1

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
          5. Applied rewrites69.1%

            \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
        3. Recombined 2 regimes into one program.
        4. Final simplification61.0%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(-3 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im\\ \mathbf{else}:\\ \;\;\;\;\left(x.re \cdot x.re\right) \cdot x.re\\ \end{array} \]
        5. Add Preprocessing

        Alternative 7: 96.4% accurate, 0.7× speedup?

        \[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(\left(x.im \cdot x.re\_m\right) \cdot x.im\right) \cdot -3\\ \mathbf{else}:\\ \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\ \end{array} \end{array} \]
        x.re\_m = (fabs.f64 x.re)
        x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
        (FPCore (x.re_s x.re_m x.im)
         :precision binary64
         (*
          x.re_s
          (if (<=
               (-
                (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
                (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))
               -4e-298)
            (* (* (* x.im x.re_m) x.im) -3.0)
            (* (* x.re_m x.re_m) x.re_m))))
        x.re\_m = fabs(x_46_re);
        x.re\_s = copysign(1.0, x_46_re);
        double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double tmp;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298) {
        		tmp = ((x_46_im * x_46_re_m) * x_46_im) * -3.0;
        	} else {
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = abs(x_46re)
        x.re\_s = copysign(1.0d0, x_46re)
        real(8) function code(x_46re_s, x_46re_m, x_46im)
            real(8), intent (in) :: x_46re_s
            real(8), intent (in) :: x_46re_m
            real(8), intent (in) :: x_46im
            real(8) :: tmp
            if (((((x_46re_m * x_46re_m) - (x_46im * x_46im)) * x_46re_m) - (((x_46im * x_46re_m) + (x_46im * x_46re_m)) * x_46im)) <= (-4d-298)) then
                tmp = ((x_46im * x_46re_m) * x_46im) * (-3.0d0)
            else
                tmp = (x_46re_m * x_46re_m) * x_46re_m
            end if
            code = x_46re_s * tmp
        end function
        
        x.re\_m = Math.abs(x_46_re);
        x.re\_s = Math.copySign(1.0, x_46_re);
        public static double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double tmp;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298) {
        		tmp = ((x_46_im * x_46_re_m) * x_46_im) * -3.0;
        	} else {
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = math.fabs(x_46_re)
        x.re\_s = math.copysign(1.0, x_46_re)
        def code(x_46_re_s, x_46_re_m, x_46_im):
        	tmp = 0
        	if ((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298:
        		tmp = ((x_46_im * x_46_re_m) * x_46_im) * -3.0
        	else:
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m
        	return x_46_re_s * tmp
        
        x.re\_m = abs(x_46_re)
        x.re\_s = copysign(1.0, x_46_re)
        function code(x_46_re_s, x_46_re_m, x_46_im)
        	tmp = 0.0
        	if (Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298)
        		tmp = Float64(Float64(Float64(x_46_im * x_46_re_m) * x_46_im) * -3.0);
        	else
        		tmp = Float64(Float64(x_46_re_m * x_46_re_m) * x_46_re_m);
        	end
        	return Float64(x_46_re_s * tmp)
        end
        
        x.re\_m = abs(x_46_re);
        x.re\_s = sign(x_46_re) * abs(1.0);
        function tmp_2 = code(x_46_re_s, x_46_re_m, x_46_im)
        	tmp = 0.0;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298)
        		tmp = ((x_46_im * x_46_re_m) * x_46_im) * -3.0;
        	else
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	end
        	tmp_2 = x_46_re_s * tmp;
        end
        
        x.re\_m = N[Abs[x$46$re], $MachinePrecision]
        x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := N[(x$46$re$95$s * If[LessEqual[N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision], -4e-298], N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] * x$46$im), $MachinePrecision] * -3.0), $MachinePrecision], N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision]]), $MachinePrecision]
        
        \begin{array}{l}
        x.re\_m = \left|x.re\right|
        \\
        x.re\_s = \mathsf{copysign}\left(1, x.re\right)
        
        \\
        x.re\_s \cdot \begin{array}{l}
        \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\
        \;\;\;\;\left(\left(x.im \cdot x.re\_m\right) \cdot x.im\right) \cdot -3\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < -3.99999999999999965e-298

          1. Initial program 89.8%

            \[\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 \]
          2. Add Preprocessing
          3. Taylor expanded in x.re around 0

            \[\leadsto \color{blue}{x.re \cdot \left(-1 \cdot {x.im}^{2} - 2 \cdot {x.im}^{2}\right)} \]
          4. Step-by-step derivation
            1. distribute-rgt-out--N/A

              \[\leadsto x.re \cdot \color{blue}{\left({x.im}^{2} \cdot \left(-1 - 2\right)\right)} \]
            2. associate-*r*N/A

              \[\leadsto \color{blue}{\left(x.re \cdot {x.im}^{2}\right) \cdot \left(-1 - 2\right)} \]
            3. *-commutativeN/A

              \[\leadsto \color{blue}{\left({x.im}^{2} \cdot x.re\right)} \cdot \left(-1 - 2\right) \]
            4. *-commutativeN/A

              \[\leadsto \color{blue}{\left(-1 - 2\right) \cdot \left({x.im}^{2} \cdot x.re\right)} \]
            5. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(-1 - 2\right) \cdot \left({x.im}^{2} \cdot x.re\right)} \]
            6. metadata-evalN/A

              \[\leadsto \color{blue}{-3} \cdot \left({x.im}^{2} \cdot x.re\right) \]
            7. unpow2N/A

              \[\leadsto -3 \cdot \left(\color{blue}{\left(x.im \cdot x.im\right)} \cdot x.re\right) \]
            8. associate-*l*N/A

              \[\leadsto -3 \cdot \color{blue}{\left(x.im \cdot \left(x.im \cdot x.re\right)\right)} \]
            9. *-commutativeN/A

              \[\leadsto -3 \cdot \color{blue}{\left(\left(x.im \cdot x.re\right) \cdot x.im\right)} \]
            10. lower-*.f64N/A

              \[\leadsto -3 \cdot \color{blue}{\left(\left(x.im \cdot x.re\right) \cdot x.im\right)} \]
            11. lower-*.f6450.6

              \[\leadsto -3 \cdot \left(\color{blue}{\left(x.im \cdot x.re\right)} \cdot x.im\right) \]
          5. Applied rewrites50.6%

            \[\leadsto \color{blue}{-3 \cdot \left(\left(x.im \cdot x.re\right) \cdot x.im\right)} \]

          if -3.99999999999999965e-298 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

          1. Initial program 73.8%

            \[\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 \]
          2. Add Preprocessing
          3. Taylor expanded in x.re around inf

            \[\leadsto \color{blue}{{x.re}^{3}} \]
          4. Step-by-step derivation
            1. unpow3N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
            2. unpow2N/A

              \[\leadsto \color{blue}{{x.re}^{2}} \cdot x.re \]
            3. lower-*.f64N/A

              \[\leadsto \color{blue}{{x.re}^{2} \cdot x.re} \]
            4. unpow2N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
            5. lower-*.f6469.1

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
          5. Applied rewrites69.1%

            \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
        3. Recombined 2 regimes into one program.
        4. Final simplification61.0%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(\left(x.im \cdot x.re\right) \cdot x.im\right) \cdot -3\\ \mathbf{else}:\\ \;\;\;\;\left(x.re \cdot x.re\right) \cdot x.re\\ \end{array} \]
        5. Add Preprocessing

        Alternative 8: 75.6% accurate, 0.7× speedup?

        \[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ x.re\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(\left(-x.re\_m\right) \cdot x.im\right) \cdot x.im\\ \mathbf{else}:\\ \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\ \end{array} \end{array} \]
        x.re\_m = (fabs.f64 x.re)
        x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
        (FPCore (x.re_s x.re_m x.im)
         :precision binary64
         (*
          x.re_s
          (if (<=
               (-
                (* (- (* x.re_m x.re_m) (* x.im x.im)) x.re_m)
                (* (+ (* x.im x.re_m) (* x.im x.re_m)) x.im))
               -4e-298)
            (* (* (- x.re_m) x.im) x.im)
            (* (* x.re_m x.re_m) x.re_m))))
        x.re\_m = fabs(x_46_re);
        x.re\_s = copysign(1.0, x_46_re);
        double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double tmp;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298) {
        		tmp = (-x_46_re_m * x_46_im) * x_46_im;
        	} else {
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = abs(x_46re)
        x.re\_s = copysign(1.0d0, x_46re)
        real(8) function code(x_46re_s, x_46re_m, x_46im)
            real(8), intent (in) :: x_46re_s
            real(8), intent (in) :: x_46re_m
            real(8), intent (in) :: x_46im
            real(8) :: tmp
            if (((((x_46re_m * x_46re_m) - (x_46im * x_46im)) * x_46re_m) - (((x_46im * x_46re_m) + (x_46im * x_46re_m)) * x_46im)) <= (-4d-298)) then
                tmp = (-x_46re_m * x_46im) * x_46im
            else
                tmp = (x_46re_m * x_46re_m) * x_46re_m
            end if
            code = x_46re_s * tmp
        end function
        
        x.re\_m = Math.abs(x_46_re);
        x.re\_s = Math.copySign(1.0, x_46_re);
        public static double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	double tmp;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298) {
        		tmp = (-x_46_re_m * x_46_im) * x_46_im;
        	} else {
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	}
        	return x_46_re_s * tmp;
        }
        
        x.re\_m = math.fabs(x_46_re)
        x.re\_s = math.copysign(1.0, x_46_re)
        def code(x_46_re_s, x_46_re_m, x_46_im):
        	tmp = 0
        	if ((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298:
        		tmp = (-x_46_re_m * x_46_im) * x_46_im
        	else:
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m
        	return x_46_re_s * tmp
        
        x.re\_m = abs(x_46_re)
        x.re\_s = copysign(1.0, x_46_re)
        function code(x_46_re_s, x_46_re_m, x_46_im)
        	tmp = 0.0
        	if (Float64(Float64(Float64(Float64(x_46_re_m * x_46_re_m) - Float64(x_46_im * x_46_im)) * x_46_re_m) - Float64(Float64(Float64(x_46_im * x_46_re_m) + Float64(x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298)
        		tmp = Float64(Float64(Float64(-x_46_re_m) * x_46_im) * x_46_im);
        	else
        		tmp = Float64(Float64(x_46_re_m * x_46_re_m) * x_46_re_m);
        	end
        	return Float64(x_46_re_s * tmp)
        end
        
        x.re\_m = abs(x_46_re);
        x.re\_s = sign(x_46_re) * abs(1.0);
        function tmp_2 = code(x_46_re_s, x_46_re_m, x_46_im)
        	tmp = 0.0;
        	if (((((x_46_re_m * x_46_re_m) - (x_46_im * x_46_im)) * x_46_re_m) - (((x_46_im * x_46_re_m) + (x_46_im * x_46_re_m)) * x_46_im)) <= -4e-298)
        		tmp = (-x_46_re_m * x_46_im) * x_46_im;
        	else
        		tmp = (x_46_re_m * x_46_re_m) * x_46_re_m;
        	end
        	tmp_2 = x_46_re_s * tmp;
        end
        
        x.re\_m = N[Abs[x$46$re], $MachinePrecision]
        x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := N[(x$46$re$95$s * If[LessEqual[N[(N[(N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re$95$m), $MachinePrecision] - N[(N[(N[(x$46$im * x$46$re$95$m), $MachinePrecision] + N[(x$46$im * x$46$re$95$m), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision], -4e-298], N[(N[((-x$46$re$95$m) * x$46$im), $MachinePrecision] * x$46$im), $MachinePrecision], N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision]]), $MachinePrecision]
        
        \begin{array}{l}
        x.re\_m = \left|x.re\right|
        \\
        x.re\_s = \mathsf{copysign}\left(1, x.re\right)
        
        \\
        x.re\_s \cdot \begin{array}{l}
        \mathbf{if}\;\left(x.re\_m \cdot x.re\_m - x.im \cdot x.im\right) \cdot x.re\_m - \left(x.im \cdot x.re\_m + x.im \cdot x.re\_m\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\
        \;\;\;\;\left(\left(-x.re\_m\right) \cdot x.im\right) \cdot x.im\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < -3.99999999999999965e-298

          1. Initial program 89.8%

            \[\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 \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

              \[\leadsto \color{blue}{\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} \]
            2. sub-negN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right)} \]
            3. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} \]
            4. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im}\right)\right) + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            5. distribute-rgt-neg-inN/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} + \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re \]
            6. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re \cdot x.im + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right)} \]
            7. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im + x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            8. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            9. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot x.re} + x.im \cdot x.re, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            10. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot x.re + \color{blue}{x.im \cdot x.re}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            11. distribute-lft-outN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            12. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{x.im \cdot \left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            13. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}, \mathsf{neg}\left(x.im\right), \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            14. lower-neg.f6489.8

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \color{blue}{-x.im}, \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re\right) \]
            15. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re}\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            17. lift--.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right)}\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(\color{blue}{x.re \cdot x.re} - x.im \cdot x.im\right)\right) \]
            19. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \left(x.re \cdot x.re - \color{blue}{x.im \cdot x.im}\right)\right) \]
            20. difference-of-squaresN/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), x.re \cdot \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)}\right) \]
            21. associate-*r*N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
            22. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), \mathsf{neg}\left(x.im\right), \color{blue}{\left(x.re \cdot \left(x.re + x.im\right)\right) \cdot \left(x.re - x.im\right)}\right) \]
          4. Applied rewrites99.7%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.im \cdot \left(x.re + x.re\right), -x.im, \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)\right)} \]
          5. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) + \left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right) + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)} \]
            3. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(x.re \cdot \left(x.im + x.re\right)\right) \cdot \left(x.re - x.im\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            4. *-commutativeN/A

              \[\leadsto \color{blue}{\left(x.re - x.im\right) \cdot \left(x.re \cdot \left(x.im + x.re\right)\right)} + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right) \]
            5. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, x.re \cdot \left(x.im + x.re\right), \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right)} \]
            6. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{x.re \cdot \left(x.im + x.re\right)}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            7. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            8. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right) \cdot x.re}, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            9. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.im + x.re\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            10. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            11. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \color{blue}{\left(x.re + x.im\right)} \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            12. lift-neg.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(x.im\right)\right)}\right) \]
            13. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            14. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.im \cdot \color{blue}{\left(x.re + x.re\right)}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            15. distribute-lft-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            17. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(\color{blue}{x.re \cdot x.im} + x.im \cdot x.re\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            18. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right) \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            19. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)} \cdot \left(\mathsf{neg}\left(x.im\right)\right)\right) \]
            20. distribute-rgt-neg-inN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \color{blue}{\mathsf{neg}\left(\left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\right)}\right) \]
            21. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(\color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            22. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \color{blue}{\left(x.re \cdot x.im + x.im \cdot x.re\right)}\right)\right) \]
            23. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.im \cdot x.re}\right)\right)\right) \]
            24. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
            25. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, \mathsf{neg}\left(x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)\right)\right) \]
          6. Applied rewrites66.0%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x.re - x.im, \left(x.re + x.im\right) \cdot x.re, x.re + x.re\right)} \]
          7. Taylor expanded in x.im around inf

            \[\leadsto \color{blue}{-1 \cdot \left({x.im}^{2} \cdot x.re\right)} \]
          8. Step-by-step derivation
            1. *-commutativeN/A

              \[\leadsto -1 \cdot \color{blue}{\left(x.re \cdot {x.im}^{2}\right)} \]
            2. unpow2N/A

              \[\leadsto -1 \cdot \left(x.re \cdot \color{blue}{\left(x.im \cdot x.im\right)}\right) \]
            3. associate-*r*N/A

              \[\leadsto -1 \cdot \color{blue}{\left(\left(x.re \cdot x.im\right) \cdot x.im\right)} \]
            4. *-commutativeN/A

              \[\leadsto -1 \cdot \left(\color{blue}{\left(x.im \cdot x.re\right)} \cdot x.im\right) \]
            5. associate-*l*N/A

              \[\leadsto \color{blue}{\left(-1 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im} \]
            6. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(-1 \cdot \left(x.im \cdot x.re\right)\right) \cdot x.im} \]
            7. *-commutativeN/A

              \[\leadsto \left(-1 \cdot \color{blue}{\left(x.re \cdot x.im\right)}\right) \cdot x.im \]
            8. associate-*r*N/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re\right) \cdot x.im\right)} \cdot x.im \]
            9. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\left(-1 \cdot x.re\right) \cdot x.im\right)} \cdot x.im \]
            10. mul-1-negN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(x.re\right)\right)} \cdot x.im\right) \cdot x.im \]
            11. lower-neg.f6423.5

              \[\leadsto \left(\color{blue}{\left(-x.re\right)} \cdot x.im\right) \cdot x.im \]
          9. Applied rewrites23.5%

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

          if -3.99999999999999965e-298 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im))

          1. Initial program 73.8%

            \[\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 \]
          2. Add Preprocessing
          3. Taylor expanded in x.re around inf

            \[\leadsto \color{blue}{{x.re}^{3}} \]
          4. Step-by-step derivation
            1. unpow3N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
            2. unpow2N/A

              \[\leadsto \color{blue}{{x.re}^{2}} \cdot x.re \]
            3. lower-*.f64N/A

              \[\leadsto \color{blue}{{x.re}^{2} \cdot x.re} \]
            4. unpow2N/A

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
            5. lower-*.f6469.1

              \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
          5. Applied rewrites69.1%

            \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
        3. Recombined 2 regimes into one program.
        4. Final simplification49.0%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.im \cdot x.re + x.im \cdot x.re\right) \cdot x.im \leq -4 \cdot 10^{-298}:\\ \;\;\;\;\left(\left(-x.re\right) \cdot x.im\right) \cdot x.im\\ \mathbf{else}:\\ \;\;\;\;\left(x.re \cdot x.re\right) \cdot x.re\\ \end{array} \]
        5. Add Preprocessing

        Alternative 9: 58.0% accurate, 3.6× speedup?

        \[\begin{array}{l} x.re\_m = \left|x.re\right| \\ x.re\_s = \mathsf{copysign}\left(1, x.re\right) \\ x.re\_s \cdot \left(\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\right) \end{array} \]
        x.re\_m = (fabs.f64 x.re)
        x.re\_s = (copysign.f64 #s(literal 1 binary64) x.re)
        (FPCore (x.re_s x.re_m x.im)
         :precision binary64
         (* x.re_s (* (* x.re_m x.re_m) x.re_m)))
        x.re\_m = fabs(x_46_re);
        x.re\_s = copysign(1.0, x_46_re);
        double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	return x_46_re_s * ((x_46_re_m * x_46_re_m) * x_46_re_m);
        }
        
        x.re\_m = abs(x_46re)
        x.re\_s = copysign(1.0d0, x_46re)
        real(8) function code(x_46re_s, x_46re_m, x_46im)
            real(8), intent (in) :: x_46re_s
            real(8), intent (in) :: x_46re_m
            real(8), intent (in) :: x_46im
            code = x_46re_s * ((x_46re_m * x_46re_m) * x_46re_m)
        end function
        
        x.re\_m = Math.abs(x_46_re);
        x.re\_s = Math.copySign(1.0, x_46_re);
        public static double code(double x_46_re_s, double x_46_re_m, double x_46_im) {
        	return x_46_re_s * ((x_46_re_m * x_46_re_m) * x_46_re_m);
        }
        
        x.re\_m = math.fabs(x_46_re)
        x.re\_s = math.copysign(1.0, x_46_re)
        def code(x_46_re_s, x_46_re_m, x_46_im):
        	return x_46_re_s * ((x_46_re_m * x_46_re_m) * x_46_re_m)
        
        x.re\_m = abs(x_46_re)
        x.re\_s = copysign(1.0, x_46_re)
        function code(x_46_re_s, x_46_re_m, x_46_im)
        	return Float64(x_46_re_s * Float64(Float64(x_46_re_m * x_46_re_m) * x_46_re_m))
        end
        
        x.re\_m = abs(x_46_re);
        x.re\_s = sign(x_46_re) * abs(1.0);
        function tmp = code(x_46_re_s, x_46_re_m, x_46_im)
        	tmp = x_46_re_s * ((x_46_re_m * x_46_re_m) * x_46_re_m);
        end
        
        x.re\_m = N[Abs[x$46$re], $MachinePrecision]
        x.re\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x$46$re]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$46$re$95$s_, x$46$re$95$m_, x$46$im_] := N[(x$46$re$95$s * N[(N[(x$46$re$95$m * x$46$re$95$m), $MachinePrecision] * x$46$re$95$m), $MachinePrecision]), $MachinePrecision]
        
        \begin{array}{l}
        x.re\_m = \left|x.re\right|
        \\
        x.re\_s = \mathsf{copysign}\left(1, x.re\right)
        
        \\
        x.re\_s \cdot \left(\left(x.re\_m \cdot x.re\_m\right) \cdot x.re\_m\right)
        \end{array}
        
        Derivation
        1. Initial program 80.9%

          \[\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 \]
        2. Add Preprocessing
        3. Taylor expanded in x.re around inf

          \[\leadsto \color{blue}{{x.re}^{3}} \]
        4. Step-by-step derivation
          1. unpow3N/A

            \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
          2. unpow2N/A

            \[\leadsto \color{blue}{{x.re}^{2}} \cdot x.re \]
          3. lower-*.f64N/A

            \[\leadsto \color{blue}{{x.re}^{2} \cdot x.re} \]
          4. unpow2N/A

            \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
          5. lower-*.f6460.9

            \[\leadsto \color{blue}{\left(x.re \cdot x.re\right)} \cdot x.re \]
        5. Applied rewrites60.9%

          \[\leadsto \color{blue}{\left(x.re \cdot x.re\right) \cdot x.re} \]
        6. Add Preprocessing

        Developer Target 1: 88.0% accurate, 1.1× speedup?

        \[\begin{array}{l} \\ \left(x.re \cdot x.re\right) \cdot \left(x.re - x.im\right) + \left(x.re \cdot x.im\right) \cdot \left(x.re - 3 \cdot x.im\right) \end{array} \]
        (FPCore (x.re x.im)
         :precision binary64
         (+ (* (* x.re x.re) (- x.re x.im)) (* (* x.re x.im) (- x.re (* 3.0 x.im)))))
        double code(double x_46_re, double x_46_im) {
        	return ((x_46_re * x_46_re) * (x_46_re - x_46_im)) + ((x_46_re * x_46_im) * (x_46_re - (3.0 * x_46_im)));
        }
        
        real(8) function code(x_46re, x_46im)
            real(8), intent (in) :: x_46re
            real(8), intent (in) :: x_46im
            code = ((x_46re * x_46re) * (x_46re - x_46im)) + ((x_46re * x_46im) * (x_46re - (3.0d0 * x_46im)))
        end function
        
        public static double code(double x_46_re, double x_46_im) {
        	return ((x_46_re * x_46_re) * (x_46_re - x_46_im)) + ((x_46_re * x_46_im) * (x_46_re - (3.0 * x_46_im)));
        }
        
        def code(x_46_re, x_46_im):
        	return ((x_46_re * x_46_re) * (x_46_re - x_46_im)) + ((x_46_re * x_46_im) * (x_46_re - (3.0 * x_46_im)))
        
        function code(x_46_re, x_46_im)
        	return Float64(Float64(Float64(x_46_re * x_46_re) * Float64(x_46_re - x_46_im)) + Float64(Float64(x_46_re * x_46_im) * Float64(x_46_re - Float64(3.0 * x_46_im))))
        end
        
        function tmp = code(x_46_re, x_46_im)
        	tmp = ((x_46_re * x_46_re) * (x_46_re - x_46_im)) + ((x_46_re * x_46_im) * (x_46_re - (3.0 * x_46_im)));
        end
        
        code[x$46$re_, x$46$im_] := N[(N[(N[(x$46$re * x$46$re), $MachinePrecision] * N[(x$46$re - x$46$im), $MachinePrecision]), $MachinePrecision] + N[(N[(x$46$re * x$46$im), $MachinePrecision] * N[(x$46$re - N[(3.0 * x$46$im), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
        
        \begin{array}{l}
        
        \\
        \left(x.re \cdot x.re\right) \cdot \left(x.re - x.im\right) + \left(x.re \cdot x.im\right) \cdot \left(x.re - 3 \cdot x.im\right)
        \end{array}
        

        Reproduce

        ?
        herbie shell --seed 2024235 
        (FPCore (x.re x.im)
          :name "math.cube on complex, real part"
          :precision binary64
        
          :alt
          (! :herbie-platform default (+ (* (* x.re x.re) (- x.re x.im)) (* (* x.re x.im) (- x.re (* 3 x.im)))))
        
          (- (* (- (* x.re x.re) (* x.im x.im)) x.re) (* (+ (* x.re x.im) (* x.im x.re)) x.im)))