Bouland and Aaronson, Equation (24)

Percentage Accurate: 74.3% → 98.3%
Time: 10.2s
Alternatives: 12
Speedup: 5.7×

Specification

?
\[\begin{array}{l} \\ \left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \end{array} \]
(FPCore (a b)
 :precision binary64
 (-
  (+
   (pow (+ (* a a) (* b b)) 2.0)
   (* 4.0 (+ (* (* a a) (- 1.0 a)) (* (* b b) (+ 3.0 a)))))
  1.0))
double code(double a, double b) {
	return (pow(((a * a) + (b * b)), 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0;
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = ((((a * a) + (b * b)) ** 2.0d0) + (4.0d0 * (((a * a) * (1.0d0 - a)) + ((b * b) * (3.0d0 + a))))) - 1.0d0
end function
public static double code(double a, double b) {
	return (Math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0;
}
def code(a, b):
	return (math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0
function code(a, b)
	return Float64(Float64((Float64(Float64(a * a) + Float64(b * b)) ^ 2.0) + Float64(4.0 * Float64(Float64(Float64(a * a) * Float64(1.0 - a)) + Float64(Float64(b * b) * Float64(3.0 + a))))) - 1.0)
end
function tmp = code(a, b)
	tmp = ((((a * a) + (b * b)) ^ 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0;
end
code[a_, b_] := N[(N[(N[Power[N[(N[(a * a), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision] + N[(4.0 * N[(N[(N[(a * a), $MachinePrecision] * N[(1.0 - a), $MachinePrecision]), $MachinePrecision] + N[(N[(b * b), $MachinePrecision] * N[(3.0 + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]
\begin{array}{l}

\\
\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1
\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 12 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: 74.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \end{array} \]
(FPCore (a b)
 :precision binary64
 (-
  (+
   (pow (+ (* a a) (* b b)) 2.0)
   (* 4.0 (+ (* (* a a) (- 1.0 a)) (* (* b b) (+ 3.0 a)))))
  1.0))
double code(double a, double b) {
	return (pow(((a * a) + (b * b)), 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0;
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = ((((a * a) + (b * b)) ** 2.0d0) + (4.0d0 * (((a * a) * (1.0d0 - a)) + ((b * b) * (3.0d0 + a))))) - 1.0d0
end function
public static double code(double a, double b) {
	return (Math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0;
}
def code(a, b):
	return (math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0
function code(a, b)
	return Float64(Float64((Float64(Float64(a * a) + Float64(b * b)) ^ 2.0) + Float64(4.0 * Float64(Float64(Float64(a * a) * Float64(1.0 - a)) + Float64(Float64(b * b) * Float64(3.0 + a))))) - 1.0)
end
function tmp = code(a, b)
	tmp = ((((a * a) + (b * b)) ^ 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (3.0 + a))))) - 1.0;
end
code[a_, b_] := N[(N[(N[Power[N[(N[(a * a), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision] + N[(4.0 * N[(N[(N[(a * a), $MachinePrecision] * N[(1.0 - a), $MachinePrecision]), $MachinePrecision] + N[(N[(b * b), $MachinePrecision] * N[(3.0 + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]
\begin{array}{l}

\\
\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1
\end{array}

Alternative 1: 98.3% accurate, 0.7× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{fma}\left(a, a, b \cdot b\right)\\ \mathbf{if}\;{\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(a + 3\right)\right) \leq \infty:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(a, a \cdot \left(1 - a\right), b \cdot \left(b \cdot \left(a + 3\right)\right)\right), 4, \mathsf{fma}\left(t\_0, t\_0, -1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a + -4, 4\right), -1\right)\\ \end{array} \end{array} \]
(FPCore (a b)
 :precision binary64
 (let* ((t_0 (fma a a (* b b))))
   (if (<=
        (+
         (pow (+ (* a a) (* b b)) 2.0)
         (* 4.0 (+ (* (* a a) (- 1.0 a)) (* (* b b) (+ a 3.0)))))
        INFINITY)
     (fma (fma a (* a (- 1.0 a)) (* b (* b (+ a 3.0)))) 4.0 (fma t_0 t_0 -1.0))
     (fma (* a a) (fma a (+ a -4.0) 4.0) -1.0))))
double code(double a, double b) {
	double t_0 = fma(a, a, (b * b));
	double tmp;
	if ((pow(((a * a) + (b * b)), 2.0) + (4.0 * (((a * a) * (1.0 - a)) + ((b * b) * (a + 3.0))))) <= ((double) INFINITY)) {
		tmp = fma(fma(a, (a * (1.0 - a)), (b * (b * (a + 3.0)))), 4.0, fma(t_0, t_0, -1.0));
	} else {
		tmp = fma((a * a), fma(a, (a + -4.0), 4.0), -1.0);
	}
	return tmp;
}
function code(a, b)
	t_0 = fma(a, a, Float64(b * b))
	tmp = 0.0
	if (Float64((Float64(Float64(a * a) + Float64(b * b)) ^ 2.0) + Float64(4.0 * Float64(Float64(Float64(a * a) * Float64(1.0 - a)) + Float64(Float64(b * b) * Float64(a + 3.0))))) <= Inf)
		tmp = fma(fma(a, Float64(a * Float64(1.0 - a)), Float64(b * Float64(b * Float64(a + 3.0)))), 4.0, fma(t_0, t_0, -1.0));
	else
		tmp = fma(Float64(a * a), fma(a, Float64(a + -4.0), 4.0), -1.0);
	end
	return tmp
end
code[a_, b_] := Block[{t$95$0 = N[(a * a + N[(b * b), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[Power[N[(N[(a * a), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision] + N[(4.0 * N[(N[(N[(a * a), $MachinePrecision] * N[(1.0 - a), $MachinePrecision]), $MachinePrecision] + N[(N[(b * b), $MachinePrecision] * N[(a + 3.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(N[(a * N[(a * N[(1.0 - a), $MachinePrecision]), $MachinePrecision] + N[(b * N[(b * N[(a + 3.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(t$95$0 * t$95$0 + -1.0), $MachinePrecision]), $MachinePrecision], N[(N[(a * a), $MachinePrecision] * N[(a * N[(a + -4.0), $MachinePrecision] + 4.0), $MachinePrecision] + -1.0), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \mathsf{fma}\left(a, a, b \cdot b\right)\\
\mathbf{if}\;{\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(a + 3\right)\right) \leq \infty:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(a, a \cdot \left(1 - a\right), b \cdot \left(b \cdot \left(a + 3\right)\right)\right), 4, \mathsf{fma}\left(t\_0, t\_0, -1\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a + -4, 4\right), -1\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (+.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) #s(literal 2 binary64)) (*.f64 #s(literal 4 binary64) (+.f64 (*.f64 (*.f64 a a) (-.f64 #s(literal 1 binary64) a)) (*.f64 (*.f64 b b) (+.f64 #s(literal 3 binary64) a))))) < +inf.0

    1. Initial program 99.9%

      \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto \color{blue}{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1} \]
      2. lift-+.f64N/A

        \[\leadsto \color{blue}{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right)} - 1 \]
      3. +-commutativeN/A

        \[\leadsto \color{blue}{\left(4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right) + {\left(a \cdot a + b \cdot b\right)}^{2}\right)} - 1 \]
      4. associate--l+N/A

        \[\leadsto \color{blue}{4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right) + \left({\left(a \cdot a + b \cdot b\right)}^{2} - 1\right)} \]
      5. lift-*.f64N/A

        \[\leadsto \color{blue}{4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)} + \left({\left(a \cdot a + b \cdot b\right)}^{2} - 1\right) \]
      6. *-commutativeN/A

        \[\leadsto \color{blue}{\left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right) \cdot 4} + \left({\left(a \cdot a + b \cdot b\right)}^{2} - 1\right) \]
      7. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right), 4, {\left(a \cdot a + b \cdot b\right)}^{2} - 1\right)} \]
    4. Applied rewrites99.9%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(a, a \cdot \left(1 - a\right), b \cdot \left(b \cdot \left(a + 3\right)\right)\right), 4, \mathsf{fma}\left(\mathsf{fma}\left(a, a, b \cdot b\right), \mathsf{fma}\left(a, a, b \cdot b\right), -1\right)\right)} \]

    if +inf.0 < (+.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) #s(literal 2 binary64)) (*.f64 #s(literal 4 binary64) (+.f64 (*.f64 (*.f64 a a) (-.f64 #s(literal 1 binary64) a)) (*.f64 (*.f64 b b) (+.f64 #s(literal 3 binary64) a)))))

    1. Initial program 0.0%

      \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
    2. Add Preprocessing
    3. Taylor expanded in b around 0

      \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
    4. Step-by-step derivation
      1. sub-negN/A

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

        \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
      3. metadata-evalN/A

        \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
      4. pow-sqrN/A

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

        \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
      6. associate-*r*N/A

        \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
      7. distribute-rgt-outN/A

        \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
      8. metadata-evalN/A

        \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
      9. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
      10. unpow2N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
      11. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
      12. unpow2N/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
      13. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
      14. sub-negN/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
      15. mul-1-negN/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
      16. +-commutativeN/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
      17. distribute-lft-inN/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
      18. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
      19. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
      20. mul-1-negN/A

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
      21. lower-neg.f6489.3

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
    5. Applied rewrites89.3%

      \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
    6. Taylor expanded in a around 0

      \[\leadsto \mathsf{fma}\left(a \cdot a, 4 + \color{blue}{a \cdot \left(a - 4\right)}, -1\right) \]
    7. Step-by-step derivation
      1. Applied rewrites90.8%

        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, \color{blue}{a + -4}, 4\right), -1\right) \]
    8. Recombined 2 regimes into one program.
    9. Final simplification97.7%

      \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(a + 3\right)\right) \leq \infty:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(a, a \cdot \left(1 - a\right), b \cdot \left(b \cdot \left(a + 3\right)\right)\right), 4, \mathsf{fma}\left(\mathsf{fma}\left(a, a, b \cdot b\right), \mathsf{fma}\left(a, a, b \cdot b\right), -1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a + -4, 4\right), -1\right)\\ \end{array} \]
    10. Add Preprocessing

    Alternative 2: 94.6% accurate, 3.7× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a + -4, a \cdot \left(a \cdot a\right), \mathsf{fma}\left(a, a \cdot 4, -1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \end{array} \]
    (FPCore (a b)
     :precision binary64
     (if (<= (* b b) 5e+23)
       (fma (+ a -4.0) (* a (* a a)) (fma a (* a 4.0) -1.0))
       (* b (* b (* b b)))))
    double code(double a, double b) {
    	double tmp;
    	if ((b * b) <= 5e+23) {
    		tmp = fma((a + -4.0), (a * (a * a)), fma(a, (a * 4.0), -1.0));
    	} else {
    		tmp = b * (b * (b * b));
    	}
    	return tmp;
    }
    
    function code(a, b)
    	tmp = 0.0
    	if (Float64(b * b) <= 5e+23)
    		tmp = fma(Float64(a + -4.0), Float64(a * Float64(a * a)), fma(a, Float64(a * 4.0), -1.0));
    	else
    		tmp = Float64(b * Float64(b * Float64(b * b)));
    	end
    	return tmp
    end
    
    code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5e+23], N[(N[(a + -4.0), $MachinePrecision] * N[(a * N[(a * a), $MachinePrecision]), $MachinePrecision] + N[(a * N[(a * 4.0), $MachinePrecision] + -1.0), $MachinePrecision]), $MachinePrecision], N[(b * N[(b * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\
    \;\;\;\;\mathsf{fma}\left(a + -4, a \cdot \left(a \cdot a\right), \mathsf{fma}\left(a, a \cdot 4, -1\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (*.f64 b b) < 4.9999999999999999e23

      1. Initial program 88.4%

        \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift--.f64N/A

          \[\leadsto \color{blue}{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1} \]
        2. flip--N/A

          \[\leadsto \color{blue}{\frac{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) \cdot \left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \cdot 1}{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) + 1}} \]
        3. clear-numN/A

          \[\leadsto \color{blue}{\frac{1}{\frac{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) + 1}{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) \cdot \left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \cdot 1}}} \]
        4. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{1}{\frac{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) + 1}{\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) \cdot \left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \cdot 1}}} \]
      4. Applied rewrites88.4%

        \[\leadsto \color{blue}{\frac{1}{\frac{1}{\mathsf{fma}\left(4, \mathsf{fma}\left(a, a \cdot \left(1 - a\right), b \cdot \left(b \cdot \left(a + 3\right)\right)\right), \mathsf{fma}\left(\mathsf{fma}\left(a, a, b \cdot b\right), \mathsf{fma}\left(a, a, b \cdot b\right), -1\right)\right)}}} \]
      5. Taylor expanded in b around inf

        \[\leadsto \color{blue}{{b}^{4}} \]
      6. Step-by-step derivation
        1. metadata-evalN/A

          \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
        2. pow-sqrN/A

          \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
        3. unpow2N/A

          \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
        4. associate-*l*N/A

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

          \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
        6. lower-*.f64N/A

          \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
        7. unpow2N/A

          \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
        8. lower-*.f642.8

          \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
      7. Applied rewrites2.8%

        \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
      8. Taylor expanded in b around 0

        \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
      9. Applied rewrites98.8%

        \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, -4 + a, 4\right), -1\right)} \]
      10. Step-by-step derivation
        1. Applied rewrites98.9%

          \[\leadsto \mathsf{fma}\left(a + -4, \color{blue}{a \cdot \left(a \cdot a\right)}, \mathsf{fma}\left(a, a \cdot 4, -1\right)\right) \]

        if 4.9999999999999999e23 < (*.f64 b b)

        1. Initial program 59.7%

          \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
        2. Add Preprocessing
        3. Taylor expanded in b around inf

          \[\leadsto \color{blue}{{b}^{4}} \]
        4. Step-by-step derivation
          1. metadata-evalN/A

            \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
          2. pow-sqrN/A

            \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
          3. unpow2N/A

            \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
          4. associate-*l*N/A

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

            \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
          6. lower-*.f64N/A

            \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
          7. unpow2N/A

            \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
          8. lower-*.f6494.4

            \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
        5. Applied rewrites94.4%

          \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
      11. Recombined 2 regimes into one program.
      12. Add Preprocessing

      Alternative 3: 94.6% accurate, 4.4× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, -4, \mathsf{fma}\left(a, a, 4\right)\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \end{array} \]
      (FPCore (a b)
       :precision binary64
       (if (<= (* b b) 5e+23)
         (fma (* a a) (fma a -4.0 (fma a a 4.0)) -1.0)
         (* b (* b (* b b)))))
      double code(double a, double b) {
      	double tmp;
      	if ((b * b) <= 5e+23) {
      		tmp = fma((a * a), fma(a, -4.0, fma(a, a, 4.0)), -1.0);
      	} else {
      		tmp = b * (b * (b * b));
      	}
      	return tmp;
      }
      
      function code(a, b)
      	tmp = 0.0
      	if (Float64(b * b) <= 5e+23)
      		tmp = fma(Float64(a * a), fma(a, -4.0, fma(a, a, 4.0)), -1.0);
      	else
      		tmp = Float64(b * Float64(b * Float64(b * b)));
      	end
      	return tmp
      end
      
      code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5e+23], N[(N[(a * a), $MachinePrecision] * N[(a * -4.0 + N[(a * a + 4.0), $MachinePrecision]), $MachinePrecision] + -1.0), $MachinePrecision], N[(b * N[(b * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\
      \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, -4, \mathsf{fma}\left(a, a, 4\right)\right), -1\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (*.f64 b b) < 4.9999999999999999e23

        1. Initial program 88.4%

          \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
        2. Add Preprocessing
        3. Taylor expanded in b around 0

          \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
        4. Step-by-step derivation
          1. sub-negN/A

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

            \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
          3. metadata-evalN/A

            \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
          4. pow-sqrN/A

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

            \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
          6. associate-*r*N/A

            \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
          7. distribute-rgt-outN/A

            \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
          8. metadata-evalN/A

            \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
          9. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
          10. unpow2N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
          11. lower-*.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
          12. unpow2N/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
          13. lower-fma.f64N/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
          14. sub-negN/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
          15. mul-1-negN/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
          16. +-commutativeN/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
          17. distribute-lft-inN/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
          18. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
          19. lower-fma.f64N/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
          20. mul-1-negN/A

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
          21. lower-neg.f6498.8

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
        5. Applied rewrites98.8%

          \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
        6. Step-by-step derivation
          1. Applied rewrites98.8%

            \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(-4, \color{blue}{a}, 4 + a \cdot a\right), -1\right) \]
          2. Step-by-step derivation
            1. Applied rewrites98.8%

              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, \color{blue}{-4}, \mathsf{fma}\left(a, a, 4\right)\right), -1\right) \]

            if 4.9999999999999999e23 < (*.f64 b b)

            1. Initial program 59.7%

              \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
            2. Add Preprocessing
            3. Taylor expanded in b around inf

              \[\leadsto \color{blue}{{b}^{4}} \]
            4. Step-by-step derivation
              1. metadata-evalN/A

                \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
              2. pow-sqrN/A

                \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
              3. unpow2N/A

                \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
              4. associate-*l*N/A

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

                \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
              6. lower-*.f64N/A

                \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
              7. unpow2N/A

                \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
              8. lower-*.f6494.4

                \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
            5. Applied rewrites94.4%

              \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
          3. Recombined 2 regimes into one program.
          4. Add Preprocessing

          Alternative 4: 94.6% accurate, 4.8× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot \mathsf{fma}\left(a, a + -4, 4\right), a, -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \end{array} \]
          (FPCore (a b)
           :precision binary64
           (if (<= (* b b) 5e+23)
             (fma (* a (fma a (+ a -4.0) 4.0)) a -1.0)
             (* b (* b (* b b)))))
          double code(double a, double b) {
          	double tmp;
          	if ((b * b) <= 5e+23) {
          		tmp = fma((a * fma(a, (a + -4.0), 4.0)), a, -1.0);
          	} else {
          		tmp = b * (b * (b * b));
          	}
          	return tmp;
          }
          
          function code(a, b)
          	tmp = 0.0
          	if (Float64(b * b) <= 5e+23)
          		tmp = fma(Float64(a * fma(a, Float64(a + -4.0), 4.0)), a, -1.0);
          	else
          		tmp = Float64(b * Float64(b * Float64(b * b)));
          	end
          	return tmp
          end
          
          code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5e+23], N[(N[(a * N[(a * N[(a + -4.0), $MachinePrecision] + 4.0), $MachinePrecision]), $MachinePrecision] * a + -1.0), $MachinePrecision], N[(b * N[(b * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\
          \;\;\;\;\mathsf{fma}\left(a \cdot \mathsf{fma}\left(a, a + -4, 4\right), a, -1\right)\\
          
          \mathbf{else}:\\
          \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if (*.f64 b b) < 4.9999999999999999e23

            1. Initial program 88.4%

              \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
            2. Add Preprocessing
            3. Taylor expanded in b around 0

              \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
            4. Step-by-step derivation
              1. sub-negN/A

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

                \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
              3. metadata-evalN/A

                \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
              4. pow-sqrN/A

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

                \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
              6. associate-*r*N/A

                \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
              7. distribute-rgt-outN/A

                \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
              8. metadata-evalN/A

                \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
              9. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
              10. unpow2N/A

                \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
              11. lower-*.f64N/A

                \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
              12. unpow2N/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
              13. lower-fma.f64N/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
              14. sub-negN/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
              15. mul-1-negN/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
              16. +-commutativeN/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
              17. distribute-lft-inN/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
              18. metadata-evalN/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
              19. lower-fma.f64N/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
              20. mul-1-negN/A

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
              21. lower-neg.f6498.8

                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
            5. Applied rewrites98.8%

              \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
            6. Step-by-step derivation
              1. Applied rewrites98.8%

                \[\leadsto \mathsf{fma}\left(a \cdot \mathsf{fma}\left(a, a, \mathsf{fma}\left(-4, a, 4\right)\right), \color{blue}{a}, -1\right) \]
              2. Step-by-step derivation
                1. Applied rewrites98.8%

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a, a + -4, 4\right) \cdot a, a, -1\right) \]

                if 4.9999999999999999e23 < (*.f64 b b)

                1. Initial program 59.7%

                  \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                2. Add Preprocessing
                3. Taylor expanded in b around inf

                  \[\leadsto \color{blue}{{b}^{4}} \]
                4. Step-by-step derivation
                  1. metadata-evalN/A

                    \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
                  2. pow-sqrN/A

                    \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
                  3. unpow2N/A

                    \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
                  4. associate-*l*N/A

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

                    \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
                  6. lower-*.f64N/A

                    \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
                  7. unpow2N/A

                    \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                  8. lower-*.f6494.4

                    \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                5. Applied rewrites94.4%

                  \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
              3. Recombined 2 regimes into one program.
              4. Final simplification96.8%

                \[\leadsto \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot \mathsf{fma}\left(a, a + -4, 4\right), a, -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \]
              5. Add Preprocessing

              Alternative 5: 94.6% accurate, 4.8× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a + -4, 4\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \end{array} \]
              (FPCore (a b)
               :precision binary64
               (if (<= (* b b) 5e+23)
                 (fma (* a a) (fma a (+ a -4.0) 4.0) -1.0)
                 (* b (* b (* b b)))))
              double code(double a, double b) {
              	double tmp;
              	if ((b * b) <= 5e+23) {
              		tmp = fma((a * a), fma(a, (a + -4.0), 4.0), -1.0);
              	} else {
              		tmp = b * (b * (b * b));
              	}
              	return tmp;
              }
              
              function code(a, b)
              	tmp = 0.0
              	if (Float64(b * b) <= 5e+23)
              		tmp = fma(Float64(a * a), fma(a, Float64(a + -4.0), 4.0), -1.0);
              	else
              		tmp = Float64(b * Float64(b * Float64(b * b)));
              	end
              	return tmp
              end
              
              code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5e+23], N[(N[(a * a), $MachinePrecision] * N[(a * N[(a + -4.0), $MachinePrecision] + 4.0), $MachinePrecision] + -1.0), $MachinePrecision], N[(b * N[(b * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\
              \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a + -4, 4\right), -1\right)\\
              
              \mathbf{else}:\\
              \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 2 regimes
              2. if (*.f64 b b) < 4.9999999999999999e23

                1. Initial program 88.4%

                  \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                2. Add Preprocessing
                3. Taylor expanded in b around 0

                  \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
                4. Step-by-step derivation
                  1. sub-negN/A

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

                    \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                  3. metadata-evalN/A

                    \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                  4. pow-sqrN/A

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

                    \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                  6. associate-*r*N/A

                    \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                  7. distribute-rgt-outN/A

                    \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                  8. metadata-evalN/A

                    \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
                  9. lower-fma.f64N/A

                    \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
                  10. unpow2N/A

                    \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                  11. lower-*.f64N/A

                    \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                  12. unpow2N/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
                  13. lower-fma.f64N/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
                  14. sub-negN/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
                  15. mul-1-negN/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
                  16. +-commutativeN/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
                  17. distribute-lft-inN/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
                  18. metadata-evalN/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
                  19. lower-fma.f64N/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
                  20. mul-1-negN/A

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
                  21. lower-neg.f6498.8

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
                5. Applied rewrites98.8%

                  \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
                6. Taylor expanded in a around 0

                  \[\leadsto \mathsf{fma}\left(a \cdot a, 4 + \color{blue}{a \cdot \left(a - 4\right)}, -1\right) \]
                7. Step-by-step derivation
                  1. Applied rewrites98.8%

                    \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, \color{blue}{a + -4}, 4\right), -1\right) \]

                  if 4.9999999999999999e23 < (*.f64 b b)

                  1. Initial program 59.7%

                    \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                  2. Add Preprocessing
                  3. Taylor expanded in b around inf

                    \[\leadsto \color{blue}{{b}^{4}} \]
                  4. Step-by-step derivation
                    1. metadata-evalN/A

                      \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
                    2. pow-sqrN/A

                      \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
                    3. unpow2N/A

                      \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
                    4. associate-*l*N/A

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

                      \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
                    6. lower-*.f64N/A

                      \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
                    7. unpow2N/A

                      \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                    8. lower-*.f6494.4

                      \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                  5. Applied rewrites94.4%

                    \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
                8. Recombined 2 regimes into one program.
                9. Add Preprocessing

                Alternative 6: 94.0% accurate, 5.0× speedup?

                \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot \left(a \cdot \left(a + -4\right)\right), a, -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \end{array} \]
                (FPCore (a b)
                 :precision binary64
                 (if (<= (* b b) 5e+23)
                   (fma (* a (* a (+ a -4.0))) a -1.0)
                   (* b (* b (* b b)))))
                double code(double a, double b) {
                	double tmp;
                	if ((b * b) <= 5e+23) {
                		tmp = fma((a * (a * (a + -4.0))), a, -1.0);
                	} else {
                		tmp = b * (b * (b * b));
                	}
                	return tmp;
                }
                
                function code(a, b)
                	tmp = 0.0
                	if (Float64(b * b) <= 5e+23)
                		tmp = fma(Float64(a * Float64(a * Float64(a + -4.0))), a, -1.0);
                	else
                		tmp = Float64(b * Float64(b * Float64(b * b)));
                	end
                	return tmp
                end
                
                code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5e+23], N[(N[(a * N[(a * N[(a + -4.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * a + -1.0), $MachinePrecision], N[(b * N[(b * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
                
                \begin{array}{l}
                
                \\
                \begin{array}{l}
                \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\
                \;\;\;\;\mathsf{fma}\left(a \cdot \left(a \cdot \left(a + -4\right)\right), a, -1\right)\\
                
                \mathbf{else}:\\
                \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\
                
                
                \end{array}
                \end{array}
                
                Derivation
                1. Split input into 2 regimes
                2. if (*.f64 b b) < 4.9999999999999999e23

                  1. Initial program 88.4%

                    \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                  2. Add Preprocessing
                  3. Taylor expanded in b around 0

                    \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
                  4. Step-by-step derivation
                    1. sub-negN/A

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

                      \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                    3. metadata-evalN/A

                      \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                    4. pow-sqrN/A

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

                      \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                    6. associate-*r*N/A

                      \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                    7. distribute-rgt-outN/A

                      \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                    8. metadata-evalN/A

                      \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
                    9. lower-fma.f64N/A

                      \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
                    10. unpow2N/A

                      \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                    11. lower-*.f64N/A

                      \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                    12. unpow2N/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
                    13. lower-fma.f64N/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
                    14. sub-negN/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
                    15. mul-1-negN/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
                    16. +-commutativeN/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
                    17. distribute-lft-inN/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
                    18. metadata-evalN/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
                    19. lower-fma.f64N/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
                    20. mul-1-negN/A

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
                    21. lower-neg.f6498.8

                      \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
                  5. Applied rewrites98.8%

                    \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
                  6. Step-by-step derivation
                    1. Applied rewrites98.8%

                      \[\leadsto \mathsf{fma}\left(a \cdot \mathsf{fma}\left(a, a, \mathsf{fma}\left(-4, a, 4\right)\right), \color{blue}{a}, -1\right) \]
                    2. Taylor expanded in a around inf

                      \[\leadsto \mathsf{fma}\left(a \cdot \left({a}^{2} \cdot \left(1 - 4 \cdot \frac{1}{a}\right)\right), a, -1\right) \]
                    3. Step-by-step derivation
                      1. Applied rewrites97.7%

                        \[\leadsto \mathsf{fma}\left(a \cdot \left(a \cdot \left(-4 + a\right)\right), a, -1\right) \]

                      if 4.9999999999999999e23 < (*.f64 b b)

                      1. Initial program 59.7%

                        \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                      2. Add Preprocessing
                      3. Taylor expanded in b around inf

                        \[\leadsto \color{blue}{{b}^{4}} \]
                      4. Step-by-step derivation
                        1. metadata-evalN/A

                          \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
                        2. pow-sqrN/A

                          \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
                        3. unpow2N/A

                          \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
                        4. associate-*l*N/A

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

                          \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
                        6. lower-*.f64N/A

                          \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
                        7. unpow2N/A

                          \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                        8. lower-*.f6494.4

                          \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                      5. Applied rewrites94.4%

                        \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
                    4. Recombined 2 regimes into one program.
                    5. Final simplification96.2%

                      \[\leadsto \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot \left(a \cdot \left(a + -4\right)\right), a, -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \]
                    6. Add Preprocessing

                    Alternative 7: 93.8% accurate, 5.3× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \end{array} \]
                    (FPCore (a b)
                     :precision binary64
                     (if (<= (* b b) 5e+23) (fma (* a a) (fma a a 4.0) -1.0) (* b (* b (* b b)))))
                    double code(double a, double b) {
                    	double tmp;
                    	if ((b * b) <= 5e+23) {
                    		tmp = fma((a * a), fma(a, a, 4.0), -1.0);
                    	} else {
                    		tmp = b * (b * (b * b));
                    	}
                    	return tmp;
                    }
                    
                    function code(a, b)
                    	tmp = 0.0
                    	if (Float64(b * b) <= 5e+23)
                    		tmp = fma(Float64(a * a), fma(a, a, 4.0), -1.0);
                    	else
                    		tmp = Float64(b * Float64(b * Float64(b * b)));
                    	end
                    	return tmp
                    end
                    
                    code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5e+23], N[(N[(a * a), $MachinePrecision] * N[(a * a + 4.0), $MachinePrecision] + -1.0), $MachinePrecision], N[(b * N[(b * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\
                    \;\;\;\;\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4\right), -1\right)\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 2 regimes
                    2. if (*.f64 b b) < 4.9999999999999999e23

                      1. Initial program 88.4%

                        \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                      2. Add Preprocessing
                      3. Taylor expanded in b around 0

                        \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
                      4. Step-by-step derivation
                        1. sub-negN/A

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

                          \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                        3. metadata-evalN/A

                          \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                        4. pow-sqrN/A

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

                          \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                        6. associate-*r*N/A

                          \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                        7. distribute-rgt-outN/A

                          \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                        8. metadata-evalN/A

                          \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
                        9. lower-fma.f64N/A

                          \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
                        10. unpow2N/A

                          \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                        11. lower-*.f64N/A

                          \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                        12. unpow2N/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
                        13. lower-fma.f64N/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
                        14. sub-negN/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
                        15. mul-1-negN/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
                        16. +-commutativeN/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
                        17. distribute-lft-inN/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
                        18. metadata-evalN/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
                        19. lower-fma.f64N/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
                        20. mul-1-negN/A

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
                        21. lower-neg.f6498.8

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
                      5. Applied rewrites98.8%

                        \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
                      6. Taylor expanded in a around 0

                        \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4\right), -1\right) \]
                      7. Step-by-step derivation
                        1. Applied rewrites97.5%

                          \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4\right), -1\right) \]

                        if 4.9999999999999999e23 < (*.f64 b b)

                        1. Initial program 59.7%

                          \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                        2. Add Preprocessing
                        3. Taylor expanded in b around inf

                          \[\leadsto \color{blue}{{b}^{4}} \]
                        4. Step-by-step derivation
                          1. metadata-evalN/A

                            \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
                          2. pow-sqrN/A

                            \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
                          3. unpow2N/A

                            \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
                          4. associate-*l*N/A

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

                            \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
                          6. lower-*.f64N/A

                            \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
                          7. unpow2N/A

                            \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                          8. lower-*.f6494.4

                            \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                        5. Applied rewrites94.4%

                          \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
                      8. Recombined 2 regimes into one program.
                      9. Add Preprocessing

                      Alternative 8: 81.8% accurate, 5.5× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} t_0 := a \cdot \left(a \cdot \left(a \cdot a\right)\right)\\ \mathbf{if}\;a \leq -1.95 \cdot 10^{+24}:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;a \leq 5.1 \cdot 10^{+28}:\\ \;\;\;\;\mathsf{fma}\left(b \cdot b, 12, -1\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
                      (FPCore (a b)
                       :precision binary64
                       (let* ((t_0 (* a (* a (* a a)))))
                         (if (<= a -1.95e+24) t_0 (if (<= a 5.1e+28) (fma (* b b) 12.0 -1.0) t_0))))
                      double code(double a, double b) {
                      	double t_0 = a * (a * (a * a));
                      	double tmp;
                      	if (a <= -1.95e+24) {
                      		tmp = t_0;
                      	} else if (a <= 5.1e+28) {
                      		tmp = fma((b * b), 12.0, -1.0);
                      	} else {
                      		tmp = t_0;
                      	}
                      	return tmp;
                      }
                      
                      function code(a, b)
                      	t_0 = Float64(a * Float64(a * Float64(a * a)))
                      	tmp = 0.0
                      	if (a <= -1.95e+24)
                      		tmp = t_0;
                      	elseif (a <= 5.1e+28)
                      		tmp = fma(Float64(b * b), 12.0, -1.0);
                      	else
                      		tmp = t_0;
                      	end
                      	return tmp
                      end
                      
                      code[a_, b_] := Block[{t$95$0 = N[(a * N[(a * N[(a * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[a, -1.95e+24], t$95$0, If[LessEqual[a, 5.1e+28], N[(N[(b * b), $MachinePrecision] * 12.0 + -1.0), $MachinePrecision], t$95$0]]]
                      
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      t_0 := a \cdot \left(a \cdot \left(a \cdot a\right)\right)\\
                      \mathbf{if}\;a \leq -1.95 \cdot 10^{+24}:\\
                      \;\;\;\;t\_0\\
                      
                      \mathbf{elif}\;a \leq 5.1 \cdot 10^{+28}:\\
                      \;\;\;\;\mathsf{fma}\left(b \cdot b, 12, -1\right)\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;t\_0\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if a < -1.9499999999999999e24 or 5.1000000000000004e28 < a

                        1. Initial program 47.2%

                          \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                        2. Add Preprocessing
                        3. Taylor expanded in a around inf

                          \[\leadsto \color{blue}{{a}^{4}} \]
                        4. Step-by-step derivation
                          1. metadata-evalN/A

                            \[\leadsto {a}^{\color{blue}{\left(3 + 1\right)}} \]
                          2. pow-plusN/A

                            \[\leadsto \color{blue}{{a}^{3} \cdot a} \]
                          3. *-commutativeN/A

                            \[\leadsto \color{blue}{a \cdot {a}^{3}} \]
                          4. lower-*.f64N/A

                            \[\leadsto \color{blue}{a \cdot {a}^{3}} \]
                          5. cube-multN/A

                            \[\leadsto a \cdot \color{blue}{\left(a \cdot \left(a \cdot a\right)\right)} \]
                          6. unpow2N/A

                            \[\leadsto a \cdot \left(a \cdot \color{blue}{{a}^{2}}\right) \]
                          7. lower-*.f64N/A

                            \[\leadsto a \cdot \color{blue}{\left(a \cdot {a}^{2}\right)} \]
                          8. unpow2N/A

                            \[\leadsto a \cdot \left(a \cdot \color{blue}{\left(a \cdot a\right)}\right) \]
                          9. lower-*.f6496.5

                            \[\leadsto a \cdot \left(a \cdot \color{blue}{\left(a \cdot a\right)}\right) \]
                        5. Applied rewrites96.5%

                          \[\leadsto \color{blue}{a \cdot \left(a \cdot \left(a \cdot a\right)\right)} \]

                        if -1.9499999999999999e24 < a < 5.1000000000000004e28

                        1. Initial program 96.5%

                          \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                        2. Add Preprocessing
                        3. Taylor expanded in a around 0

                          \[\leadsto \color{blue}{\left(12 \cdot {b}^{2} + {b}^{4}\right) - 1} \]
                        4. Step-by-step derivation
                          1. sub-negN/A

                            \[\leadsto \color{blue}{\left(12 \cdot {b}^{2} + {b}^{4}\right) + \left(\mathsf{neg}\left(1\right)\right)} \]
                          2. metadata-evalN/A

                            \[\leadsto \left(12 \cdot {b}^{2} + {b}^{\color{blue}{\left(2 \cdot 2\right)}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                          3. pow-sqrN/A

                            \[\leadsto \left(12 \cdot {b}^{2} + \color{blue}{{b}^{2} \cdot {b}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                          4. distribute-rgt-outN/A

                            \[\leadsto \color{blue}{{b}^{2} \cdot \left(12 + {b}^{2}\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                          5. +-commutativeN/A

                            \[\leadsto {b}^{2} \cdot \color{blue}{\left({b}^{2} + 12\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                          6. metadata-evalN/A

                            \[\leadsto {b}^{2} \cdot \left({b}^{2} + 12\right) + \color{blue}{-1} \]
                          7. lower-fma.f64N/A

                            \[\leadsto \color{blue}{\mathsf{fma}\left({b}^{2}, {b}^{2} + 12, -1\right)} \]
                          8. unpow2N/A

                            \[\leadsto \mathsf{fma}\left(\color{blue}{b \cdot b}, {b}^{2} + 12, -1\right) \]
                          9. lower-*.f64N/A

                            \[\leadsto \mathsf{fma}\left(\color{blue}{b \cdot b}, {b}^{2} + 12, -1\right) \]
                          10. unpow2N/A

                            \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{b \cdot b} + 12, -1\right) \]
                          11. lower-fma.f6497.0

                            \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{\mathsf{fma}\left(b, b, 12\right)}, -1\right) \]
                        5. Applied rewrites97.0%

                          \[\leadsto \color{blue}{\mathsf{fma}\left(b \cdot b, \mathsf{fma}\left(b, b, 12\right), -1\right)} \]
                        6. Taylor expanded in b around 0

                          \[\leadsto \mathsf{fma}\left(b \cdot b, 12, -1\right) \]
                        7. Step-by-step derivation
                          1. Applied rewrites72.1%

                            \[\leadsto \mathsf{fma}\left(b \cdot b, 12, -1\right) \]
                        8. Recombined 2 regimes into one program.
                        9. Add Preprocessing

                        Alternative 9: 81.7% accurate, 5.7× speedup?

                        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot a, 4, -1\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\ \end{array} \end{array} \]
                        (FPCore (a b)
                         :precision binary64
                         (if (<= (* b b) 5e+23) (fma (* a a) 4.0 -1.0) (* b (* b (* b b)))))
                        double code(double a, double b) {
                        	double tmp;
                        	if ((b * b) <= 5e+23) {
                        		tmp = fma((a * a), 4.0, -1.0);
                        	} else {
                        		tmp = b * (b * (b * b));
                        	}
                        	return tmp;
                        }
                        
                        function code(a, b)
                        	tmp = 0.0
                        	if (Float64(b * b) <= 5e+23)
                        		tmp = fma(Float64(a * a), 4.0, -1.0);
                        	else
                        		tmp = Float64(b * Float64(b * Float64(b * b)));
                        	end
                        	return tmp
                        end
                        
                        code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5e+23], N[(N[(a * a), $MachinePrecision] * 4.0 + -1.0), $MachinePrecision], N[(b * N[(b * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
                        
                        \begin{array}{l}
                        
                        \\
                        \begin{array}{l}
                        \mathbf{if}\;b \cdot b \leq 5 \cdot 10^{+23}:\\
                        \;\;\;\;\mathsf{fma}\left(a \cdot a, 4, -1\right)\\
                        
                        \mathbf{else}:\\
                        \;\;\;\;b \cdot \left(b \cdot \left(b \cdot b\right)\right)\\
                        
                        
                        \end{array}
                        \end{array}
                        
                        Derivation
                        1. Split input into 2 regimes
                        2. if (*.f64 b b) < 4.9999999999999999e23

                          1. Initial program 88.4%

                            \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                          2. Add Preprocessing
                          3. Taylor expanded in b around 0

                            \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
                          4. Step-by-step derivation
                            1. sub-negN/A

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

                              \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                            3. metadata-evalN/A

                              \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                            4. pow-sqrN/A

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

                              \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                            6. associate-*r*N/A

                              \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                            7. distribute-rgt-outN/A

                              \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                            8. metadata-evalN/A

                              \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
                            9. lower-fma.f64N/A

                              \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
                            10. unpow2N/A

                              \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                            11. lower-*.f64N/A

                              \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                            12. unpow2N/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
                            13. lower-fma.f64N/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
                            14. sub-negN/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
                            15. mul-1-negN/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
                            16. +-commutativeN/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
                            17. distribute-lft-inN/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
                            18. metadata-evalN/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
                            19. lower-fma.f64N/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
                            20. mul-1-negN/A

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
                            21. lower-neg.f6498.8

                              \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
                          5. Applied rewrites98.8%

                            \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
                          6. Taylor expanded in a around 0

                            \[\leadsto \mathsf{fma}\left(a \cdot a, 4, -1\right) \]
                          7. Step-by-step derivation
                            1. Applied rewrites74.0%

                              \[\leadsto \mathsf{fma}\left(a \cdot a, 4, -1\right) \]

                            if 4.9999999999999999e23 < (*.f64 b b)

                            1. Initial program 59.7%

                              \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                            2. Add Preprocessing
                            3. Taylor expanded in b around inf

                              \[\leadsto \color{blue}{{b}^{4}} \]
                            4. Step-by-step derivation
                              1. metadata-evalN/A

                                \[\leadsto {b}^{\color{blue}{\left(2 \cdot 2\right)}} \]
                              2. pow-sqrN/A

                                \[\leadsto \color{blue}{{b}^{2} \cdot {b}^{2}} \]
                              3. unpow2N/A

                                \[\leadsto \color{blue}{\left(b \cdot b\right)} \cdot {b}^{2} \]
                              4. associate-*l*N/A

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

                                \[\leadsto \color{blue}{b \cdot \left(b \cdot {b}^{2}\right)} \]
                              6. lower-*.f64N/A

                                \[\leadsto b \cdot \color{blue}{\left(b \cdot {b}^{2}\right)} \]
                              7. unpow2N/A

                                \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                              8. lower-*.f6494.4

                                \[\leadsto b \cdot \left(b \cdot \color{blue}{\left(b \cdot b\right)}\right) \]
                            5. Applied rewrites94.4%

                              \[\leadsto \color{blue}{b \cdot \left(b \cdot \left(b \cdot b\right)\right)} \]
                          8. Recombined 2 regimes into one program.
                          9. Add Preprocessing

                          Alternative 10: 69.4% accurate, 6.7× speedup?

                          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot b \leq 5.2 \cdot 10^{+296}:\\ \;\;\;\;\mathsf{fma}\left(a \cdot a, 4, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(b \cdot b, 12, -1\right)\\ \end{array} \end{array} \]
                          (FPCore (a b)
                           :precision binary64
                           (if (<= (* b b) 5.2e+296) (fma (* a a) 4.0 -1.0) (fma (* b b) 12.0 -1.0)))
                          double code(double a, double b) {
                          	double tmp;
                          	if ((b * b) <= 5.2e+296) {
                          		tmp = fma((a * a), 4.0, -1.0);
                          	} else {
                          		tmp = fma((b * b), 12.0, -1.0);
                          	}
                          	return tmp;
                          }
                          
                          function code(a, b)
                          	tmp = 0.0
                          	if (Float64(b * b) <= 5.2e+296)
                          		tmp = fma(Float64(a * a), 4.0, -1.0);
                          	else
                          		tmp = fma(Float64(b * b), 12.0, -1.0);
                          	end
                          	return tmp
                          end
                          
                          code[a_, b_] := If[LessEqual[N[(b * b), $MachinePrecision], 5.2e+296], N[(N[(a * a), $MachinePrecision] * 4.0 + -1.0), $MachinePrecision], N[(N[(b * b), $MachinePrecision] * 12.0 + -1.0), $MachinePrecision]]
                          
                          \begin{array}{l}
                          
                          \\
                          \begin{array}{l}
                          \mathbf{if}\;b \cdot b \leq 5.2 \cdot 10^{+296}:\\
                          \;\;\;\;\mathsf{fma}\left(a \cdot a, 4, -1\right)\\
                          
                          \mathbf{else}:\\
                          \;\;\;\;\mathsf{fma}\left(b \cdot b, 12, -1\right)\\
                          
                          
                          \end{array}
                          \end{array}
                          
                          Derivation
                          1. Split input into 2 regimes
                          2. if (*.f64 b b) < 5.2000000000000003e296

                            1. Initial program 84.5%

                              \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                            2. Add Preprocessing
                            3. Taylor expanded in b around 0

                              \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
                            4. Step-by-step derivation
                              1. sub-negN/A

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

                                \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                              3. metadata-evalN/A

                                \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                              4. pow-sqrN/A

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

                                \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                              6. associate-*r*N/A

                                \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                              7. distribute-rgt-outN/A

                                \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                              8. metadata-evalN/A

                                \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
                              9. lower-fma.f64N/A

                                \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
                              10. unpow2N/A

                                \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                              11. lower-*.f64N/A

                                \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                              12. unpow2N/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
                              13. lower-fma.f64N/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
                              14. sub-negN/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
                              15. mul-1-negN/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
                              16. +-commutativeN/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
                              17. distribute-lft-inN/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
                              18. metadata-evalN/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
                              19. lower-fma.f64N/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
                              20. mul-1-negN/A

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
                              21. lower-neg.f6480.3

                                \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
                            5. Applied rewrites80.3%

                              \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
                            6. Taylor expanded in a around 0

                              \[\leadsto \mathsf{fma}\left(a \cdot a, 4, -1\right) \]
                            7. Step-by-step derivation
                              1. Applied rewrites61.1%

                                \[\leadsto \mathsf{fma}\left(a \cdot a, 4, -1\right) \]

                              if 5.2000000000000003e296 < (*.f64 b b)

                              1. Initial program 49.3%

                                \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                              2. Add Preprocessing
                              3. Taylor expanded in a around 0

                                \[\leadsto \color{blue}{\left(12 \cdot {b}^{2} + {b}^{4}\right) - 1} \]
                              4. Step-by-step derivation
                                1. sub-negN/A

                                  \[\leadsto \color{blue}{\left(12 \cdot {b}^{2} + {b}^{4}\right) + \left(\mathsf{neg}\left(1\right)\right)} \]
                                2. metadata-evalN/A

                                  \[\leadsto \left(12 \cdot {b}^{2} + {b}^{\color{blue}{\left(2 \cdot 2\right)}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                                3. pow-sqrN/A

                                  \[\leadsto \left(12 \cdot {b}^{2} + \color{blue}{{b}^{2} \cdot {b}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                                4. distribute-rgt-outN/A

                                  \[\leadsto \color{blue}{{b}^{2} \cdot \left(12 + {b}^{2}\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                                5. +-commutativeN/A

                                  \[\leadsto {b}^{2} \cdot \color{blue}{\left({b}^{2} + 12\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                                6. metadata-evalN/A

                                  \[\leadsto {b}^{2} \cdot \left({b}^{2} + 12\right) + \color{blue}{-1} \]
                                7. lower-fma.f64N/A

                                  \[\leadsto \color{blue}{\mathsf{fma}\left({b}^{2}, {b}^{2} + 12, -1\right)} \]
                                8. unpow2N/A

                                  \[\leadsto \mathsf{fma}\left(\color{blue}{b \cdot b}, {b}^{2} + 12, -1\right) \]
                                9. lower-*.f64N/A

                                  \[\leadsto \mathsf{fma}\left(\color{blue}{b \cdot b}, {b}^{2} + 12, -1\right) \]
                                10. unpow2N/A

                                  \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{b \cdot b} + 12, -1\right) \]
                                11. lower-fma.f64100.0

                                  \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{\mathsf{fma}\left(b, b, 12\right)}, -1\right) \]
                              5. Applied rewrites100.0%

                                \[\leadsto \color{blue}{\mathsf{fma}\left(b \cdot b, \mathsf{fma}\left(b, b, 12\right), -1\right)} \]
                              6. Taylor expanded in b around 0

                                \[\leadsto \mathsf{fma}\left(b \cdot b, 12, -1\right) \]
                              7. Step-by-step derivation
                                1. Applied rewrites93.4%

                                  \[\leadsto \mathsf{fma}\left(b \cdot b, 12, -1\right) \]
                              8. Recombined 2 regimes into one program.
                              9. Add Preprocessing

                              Alternative 11: 51.5% accurate, 12.9× speedup?

                              \[\begin{array}{l} \\ \mathsf{fma}\left(a \cdot a, 4, -1\right) \end{array} \]
                              (FPCore (a b) :precision binary64 (fma (* a a) 4.0 -1.0))
                              double code(double a, double b) {
                              	return fma((a * a), 4.0, -1.0);
                              }
                              
                              function code(a, b)
                              	return fma(Float64(a * a), 4.0, -1.0)
                              end
                              
                              code[a_, b_] := N[(N[(a * a), $MachinePrecision] * 4.0 + -1.0), $MachinePrecision]
                              
                              \begin{array}{l}
                              
                              \\
                              \mathsf{fma}\left(a \cdot a, 4, -1\right)
                              \end{array}
                              
                              Derivation
                              1. Initial program 75.3%

                                \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                              2. Add Preprocessing
                              3. Taylor expanded in b around 0

                                \[\leadsto \color{blue}{\left(4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right) + {a}^{4}\right) - 1} \]
                              4. Step-by-step derivation
                                1. sub-negN/A

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

                                  \[\leadsto \color{blue}{\left({a}^{4} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                                3. metadata-evalN/A

                                  \[\leadsto \left({a}^{\color{blue}{\left(2 \cdot 2\right)}} + 4 \cdot \left({a}^{2} \cdot \left(1 - a\right)\right)\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                                4. pow-sqrN/A

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

                                  \[\leadsto \left({a}^{2} \cdot {a}^{2} + 4 \cdot \color{blue}{\left(\left(1 - a\right) \cdot {a}^{2}\right)}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                                6. associate-*r*N/A

                                  \[\leadsto \left({a}^{2} \cdot {a}^{2} + \color{blue}{\left(4 \cdot \left(1 - a\right)\right) \cdot {a}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                                7. distribute-rgt-outN/A

                                  \[\leadsto \color{blue}{{a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                                8. metadata-evalN/A

                                  \[\leadsto {a}^{2} \cdot \left({a}^{2} + 4 \cdot \left(1 - a\right)\right) + \color{blue}{-1} \]
                                9. lower-fma.f64N/A

                                  \[\leadsto \color{blue}{\mathsf{fma}\left({a}^{2}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right)} \]
                                10. unpow2N/A

                                  \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                                11. lower-*.f64N/A

                                  \[\leadsto \mathsf{fma}\left(\color{blue}{a \cdot a}, {a}^{2} + 4 \cdot \left(1 - a\right), -1\right) \]
                                12. unpow2N/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{a \cdot a} + 4 \cdot \left(1 - a\right), -1\right) \]
                                13. lower-fma.f64N/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \color{blue}{\mathsf{fma}\left(a, a, 4 \cdot \left(1 - a\right)\right)}, -1\right) \]
                                14. sub-negN/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(a\right)\right)\right)}\right), -1\right) \]
                                15. mul-1-negN/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(1 + \color{blue}{-1 \cdot a}\right)\right), -1\right) \]
                                16. +-commutativeN/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \color{blue}{\left(-1 \cdot a + 1\right)}\right), -1\right) \]
                                17. distribute-lft-inN/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{4 \cdot \left(-1 \cdot a\right) + 4 \cdot 1}\right), -1\right) \]
                                18. metadata-evalN/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, 4 \cdot \left(-1 \cdot a\right) + \color{blue}{4}\right), -1\right) \]
                                19. lower-fma.f64N/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \color{blue}{\mathsf{fma}\left(4, -1 \cdot a, 4\right)}\right), -1\right) \]
                                20. mul-1-negN/A

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{\mathsf{neg}\left(a\right)}, 4\right)\right), -1\right) \]
                                21. lower-neg.f6470.5

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, \color{blue}{-a}, 4\right)\right), -1\right) \]
                              5. Applied rewrites70.5%

                                \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot a, \mathsf{fma}\left(a, a, \mathsf{fma}\left(4, -a, 4\right)\right), -1\right)} \]
                              6. Taylor expanded in a around 0

                                \[\leadsto \mathsf{fma}\left(a \cdot a, 4, -1\right) \]
                              7. Step-by-step derivation
                                1. Applied rewrites53.4%

                                  \[\leadsto \mathsf{fma}\left(a \cdot a, 4, -1\right) \]
                                2. Add Preprocessing

                                Alternative 12: 25.6% accurate, 155.0× speedup?

                                \[\begin{array}{l} \\ -1 \end{array} \]
                                (FPCore (a b) :precision binary64 -1.0)
                                double code(double a, double b) {
                                	return -1.0;
                                }
                                
                                real(8) function code(a, b)
                                    real(8), intent (in) :: a
                                    real(8), intent (in) :: b
                                    code = -1.0d0
                                end function
                                
                                public static double code(double a, double b) {
                                	return -1.0;
                                }
                                
                                def code(a, b):
                                	return -1.0
                                
                                function code(a, b)
                                	return -1.0
                                end
                                
                                function tmp = code(a, b)
                                	tmp = -1.0;
                                end
                                
                                code[a_, b_] := -1.0
                                
                                \begin{array}{l}
                                
                                \\
                                -1
                                \end{array}
                                
                                Derivation
                                1. Initial program 75.3%

                                  \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1 \]
                                2. Add Preprocessing
                                3. Taylor expanded in a around 0

                                  \[\leadsto \color{blue}{\left(12 \cdot {b}^{2} + {b}^{4}\right) - 1} \]
                                4. Step-by-step derivation
                                  1. sub-negN/A

                                    \[\leadsto \color{blue}{\left(12 \cdot {b}^{2} + {b}^{4}\right) + \left(\mathsf{neg}\left(1\right)\right)} \]
                                  2. metadata-evalN/A

                                    \[\leadsto \left(12 \cdot {b}^{2} + {b}^{\color{blue}{\left(2 \cdot 2\right)}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                                  3. pow-sqrN/A

                                    \[\leadsto \left(12 \cdot {b}^{2} + \color{blue}{{b}^{2} \cdot {b}^{2}}\right) + \left(\mathsf{neg}\left(1\right)\right) \]
                                  4. distribute-rgt-outN/A

                                    \[\leadsto \color{blue}{{b}^{2} \cdot \left(12 + {b}^{2}\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                                  5. +-commutativeN/A

                                    \[\leadsto {b}^{2} \cdot \color{blue}{\left({b}^{2} + 12\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
                                  6. metadata-evalN/A

                                    \[\leadsto {b}^{2} \cdot \left({b}^{2} + 12\right) + \color{blue}{-1} \]
                                  7. lower-fma.f64N/A

                                    \[\leadsto \color{blue}{\mathsf{fma}\left({b}^{2}, {b}^{2} + 12, -1\right)} \]
                                  8. unpow2N/A

                                    \[\leadsto \mathsf{fma}\left(\color{blue}{b \cdot b}, {b}^{2} + 12, -1\right) \]
                                  9. lower-*.f64N/A

                                    \[\leadsto \mathsf{fma}\left(\color{blue}{b \cdot b}, {b}^{2} + 12, -1\right) \]
                                  10. unpow2N/A

                                    \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{b \cdot b} + 12, -1\right) \]
                                  11. lower-fma.f6471.3

                                    \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{\mathsf{fma}\left(b, b, 12\right)}, -1\right) \]
                                5. Applied rewrites71.3%

                                  \[\leadsto \color{blue}{\mathsf{fma}\left(b \cdot b, \mathsf{fma}\left(b, b, 12\right), -1\right)} \]
                                6. Taylor expanded in b around 0

                                  \[\leadsto -1 \]
                                7. Step-by-step derivation
                                  1. Applied rewrites27.9%

                                    \[\leadsto -1 \]
                                  2. Add Preprocessing

                                  Reproduce

                                  ?
                                  herbie shell --seed 2024233 
                                  (FPCore (a b)
                                    :name "Bouland and Aaronson, Equation (24)"
                                    :precision binary64
                                    (- (+ (pow (+ (* a a) (* b b)) 2.0) (* 4.0 (+ (* (* a a) (- 1.0 a)) (* (* b b) (+ 3.0 a))))) 1.0))