Bouland and Aaronson, Equation (26)

Percentage Accurate: 99.9% → 99.9%
Time: 7.3s
Alternatives: 9
Speedup: 1.0×

Specification

?
\[\begin{array}{l} \\ \left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(b \cdot b\right)\right) - 1 \end{array} \]
(FPCore (a b)
 :precision binary64
 (- (+ (pow (+ (* a a) (* b b)) 2.0) (* 4.0 (* b b))) 1.0))
double code(double a, double b) {
	return (pow(((a * a) + (b * b)), 2.0) + (4.0 * (b * b))) - 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 * (b * b))) - 1.0d0
end function
public static double code(double a, double b) {
	return (Math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (b * b))) - 1.0;
}
def code(a, b):
	return (math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (b * b))) - 1.0
function code(a, b)
	return Float64(Float64((Float64(Float64(a * a) + Float64(b * b)) ^ 2.0) + Float64(4.0 * Float64(b * b))) - 1.0)
end
function tmp = code(a, b)
	tmp = ((((a * a) + (b * b)) ^ 2.0) + (4.0 * (b * b))) - 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[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]
\begin{array}{l}

\\
\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(b \cdot b\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 9 alternatives:

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

Initial Program: 99.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(b \cdot b\right)\right) - 1 \end{array} \]
(FPCore (a b)
 :precision binary64
 (- (+ (pow (+ (* a a) (* b b)) 2.0) (* 4.0 (* b b))) 1.0))
double code(double a, double b) {
	return (pow(((a * a) + (b * b)), 2.0) + (4.0 * (b * b))) - 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 * (b * b))) - 1.0d0
end function
public static double code(double a, double b) {
	return (Math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (b * b))) - 1.0;
}
def code(a, b):
	return (math.pow(((a * a) + (b * b)), 2.0) + (4.0 * (b * b))) - 1.0
function code(a, b)
	return Float64(Float64((Float64(Float64(a * a) + Float64(b * b)) ^ 2.0) + Float64(4.0 * Float64(b * b))) - 1.0)
end
function tmp = code(a, b)
	tmp = ((((a * a) + (b * b)) ^ 2.0) + (4.0 * (b * b))) - 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[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]
\begin{array}{l}

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

Alternative 1: 99.9% accurate, 1.0× speedup?

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

\\
\left(4 \cdot \left(b \cdot b\right) + {\left(b \cdot b + a \cdot a\right)}^{2}\right) - 1
\end{array}
Derivation
  1. Initial program 99.9%

    \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(b \cdot b\right)\right) - 1 \]
  2. Add Preprocessing
  3. Final simplification99.9%

    \[\leadsto \left(4 \cdot \left(b \cdot b\right) + {\left(b \cdot b + a \cdot a\right)}^{2}\right) - 1 \]
  4. Add Preprocessing

Alternative 2: 97.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;a \cdot a \leq 2 \cdot 10^{+35}:\\ \;\;\;\;\mathsf{fma}\left(b \cdot b, 4, {b}^{4}\right) - 1\\ \mathbf{else}:\\ \;\;\;\;\left(\mathsf{fma}\left(b \cdot b, 2, a \cdot a\right) \cdot a\right) \cdot a - 1\\ \end{array} \end{array} \]
(FPCore (a b)
 :precision binary64
 (if (<= (* a a) 2e+35)
   (- (fma (* b b) 4.0 (pow b 4.0)) 1.0)
   (- (* (* (fma (* b b) 2.0 (* a a)) a) a) 1.0)))
double code(double a, double b) {
	double tmp;
	if ((a * a) <= 2e+35) {
		tmp = fma((b * b), 4.0, pow(b, 4.0)) - 1.0;
	} else {
		tmp = ((fma((b * b), 2.0, (a * a)) * a) * a) - 1.0;
	}
	return tmp;
}
function code(a, b)
	tmp = 0.0
	if (Float64(a * a) <= 2e+35)
		tmp = Float64(fma(Float64(b * b), 4.0, (b ^ 4.0)) - 1.0);
	else
		tmp = Float64(Float64(Float64(fma(Float64(b * b), 2.0, Float64(a * a)) * a) * a) - 1.0);
	end
	return tmp
end
code[a_, b_] := If[LessEqual[N[(a * a), $MachinePrecision], 2e+35], N[(N[(N[(b * b), $MachinePrecision] * 4.0 + N[Power[b, 4.0], $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision], N[(N[(N[(N[(N[(b * b), $MachinePrecision] * 2.0 + N[(a * a), $MachinePrecision]), $MachinePrecision] * a), $MachinePrecision] * a), $MachinePrecision] - 1.0), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;a \cdot a \leq 2 \cdot 10^{+35}:\\
\;\;\;\;\mathsf{fma}\left(b \cdot b, 4, {b}^{4}\right) - 1\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 a a) < 1.9999999999999999e35

    1. Initial program 99.9%

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

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

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

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

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{b \cdot b}, 4, {b}^{4}\right) - 1 \]
      5. lower-pow.f6499.2

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

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

    if 1.9999999999999999e35 < (*.f64 a a)

    1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \left(\left(2 \cdot {b}^{2}\right) \cdot {a}^{2} + \color{blue}{{a}^{2} \cdot {a}^{2}}\right) - 1 \]
      14. distribute-rgt-inN/A

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

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

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

        \[\leadsto \color{blue}{\left(\left(2 \cdot {b}^{2} + {a}^{2}\right) \cdot a\right) \cdot a} - 1 \]
    5. Applied rewrites99.0%

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

Alternative 3: 97.5% accurate, 1.0× speedup?

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

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

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


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 a a) < 1.9999999999999999e35

    1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \mathsf{fma}\left(\left(\color{blue}{b \cdot b} + 4\right) \cdot b, b, -1\right) \]
      16. lower-fma.f6499.1

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

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

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(b, 4, {b}^{3}\right), b, -1\right) \]

      if 1.9999999999999999e35 < (*.f64 a a)

      1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \left(\left(2 \cdot {b}^{2}\right) \cdot {a}^{2} + \color{blue}{{a}^{2} \cdot {a}^{2}}\right) - 1 \]
        14. distribute-rgt-inN/A

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

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

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

          \[\leadsto \color{blue}{\left(\left(2 \cdot {b}^{2} + {a}^{2}\right) \cdot a\right) \cdot a} - 1 \]
      5. Applied rewrites99.0%

        \[\leadsto \color{blue}{\left(\mathsf{fma}\left(b \cdot b, 2, a \cdot a\right) \cdot a\right) \cdot a} - 1 \]
    10. Recombined 2 regimes into one program.
    11. Add Preprocessing

    Alternative 4: 97.4% accurate, 3.2× speedup?

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

      1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \mathsf{fma}\left(\left(\color{blue}{b \cdot b} + 4\right) \cdot b, b, -1\right) \]
        16. lower-fma.f6499.1

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

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

      if 1.9999999999999999e35 < (*.f64 a a)

      1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \left(\left(2 \cdot {b}^{2}\right) \cdot {a}^{2} + \color{blue}{{a}^{2} \cdot {a}^{2}}\right) - 1 \]
        14. distribute-rgt-inN/A

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

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

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

          \[\leadsto \color{blue}{\left(\left(2 \cdot {b}^{2} + {a}^{2}\right) \cdot a\right) \cdot a} - 1 \]
      5. Applied rewrites99.0%

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

    Alternative 5: 94.1% accurate, 4.4× speedup?

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

      1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \mathsf{fma}\left(\left(\color{blue}{b \cdot b} + 4\right) \cdot b, b, -1\right) \]
        16. lower-fma.f6499.1

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

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

      if 1.9999999999999999e35 < (*.f64 a a)

      1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \left(\left(2 \cdot {b}^{2}\right) \cdot {a}^{2} + \color{blue}{{a}^{2} \cdot {a}^{2}}\right) - 1 \]
        14. distribute-rgt-inN/A

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

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

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

          \[\leadsto \color{blue}{\left(\left(2 \cdot {b}^{2} + {a}^{2}\right) \cdot a\right) \cdot a} - 1 \]
      5. Applied rewrites99.0%

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

        \[\leadsto \left(\left(2 \cdot {b}^{2}\right) \cdot a\right) \cdot a - 1 \]
      7. Step-by-step derivation
        1. Applied rewrites50.8%

          \[\leadsto \left(\left(\left(b \cdot b\right) \cdot 2\right) \cdot a\right) \cdot a - 1 \]
        2. Taylor expanded in a around inf

          \[\leadsto \left({a}^{2} \cdot a\right) \cdot a - 1 \]
        3. Step-by-step derivation
          1. Applied rewrites95.6%

            \[\leadsto \left(\left(a \cdot a\right) \cdot a\right) \cdot a - 1 \]
        4. Recombined 2 regimes into one program.
        5. Add Preprocessing

        Alternative 6: 69.9% accurate, 7.3× speedup?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(\left(\color{blue}{b \cdot b} + 4\right) \cdot b, b, -1\right) \]
          16. lower-fma.f6471.9

            \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(b, b, 4\right)} \cdot b, b, -1\right) \]
        8. Applied rewrites71.9%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(b, b, 4\right) \cdot b, b, -1\right)} \]
        9. Add Preprocessing

        Alternative 7: 69.9% accurate, 7.3× speedup?

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{\mathsf{fma}\left(b, b, 4\right)}, \mathsf{neg}\left(1\right)\right) \]
          11. metadata-eval71.9

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(b \cdot b, \mathsf{fma}\left(b, b, 4\right), -1\right)} \]
        6. Add Preprocessing

        Alternative 8: 52.1% accurate, 10.9× speedup?

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{\mathsf{fma}\left(b, b, 4\right)}, \mathsf{neg}\left(1\right)\right) \]
          11. metadata-eval71.9

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

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

          \[\leadsto 4 \cdot {b}^{2} - \color{blue}{1} \]
        7. Step-by-step derivation
          1. Applied rewrites52.8%

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

          Alternative 9: 25.1% accurate, 131.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 99.9%

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

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

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

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

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

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

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

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

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

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

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

              \[\leadsto \mathsf{fma}\left(b \cdot b, \color{blue}{\mathsf{fma}\left(b, b, 4\right)}, \mathsf{neg}\left(1\right)\right) \]
            11. metadata-eval71.9

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

            \[\leadsto \color{blue}{\mathsf{fma}\left(b \cdot b, \mathsf{fma}\left(b, b, 4\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 2024332 
            (FPCore (a b)
              :name "Bouland and Aaronson, Equation (26)"
              :precision binary64
              (- (+ (pow (+ (* a a) (* b b)) 2.0) (* 4.0 (* b b))) 1.0))