Numeric.SpecFunctions:incompleteGamma from math-functions-0.1.5.2, B

Percentage Accurate: 99.4% → 99.5%
Time: 7.7s
Alternatives: 10
Speedup: 1.2×

Specification

?
\[\begin{array}{l} \\ \left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \end{array} \]
(FPCore (x y)
 :precision binary64
 (* (* 3.0 (sqrt x)) (- (+ y (/ 1.0 (* x 9.0))) 1.0)))
double code(double x, double y) {
	return (3.0 * sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0);
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    code = (3.0d0 * sqrt(x)) * ((y + (1.0d0 / (x * 9.0d0))) - 1.0d0)
end function
public static double code(double x, double y) {
	return (3.0 * Math.sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0);
}
def code(x, y):
	return (3.0 * math.sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0)
function code(x, y)
	return Float64(Float64(3.0 * sqrt(x)) * Float64(Float64(y + Float64(1.0 / Float64(x * 9.0))) - 1.0))
end
function tmp = code(x, y)
	tmp = (3.0 * sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0);
end
code[x_, y_] := N[(N[(3.0 * N[Sqrt[x], $MachinePrecision]), $MachinePrecision] * N[(N[(y + N[(1.0 / N[(x * 9.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)
\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 10 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.4% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \end{array} \]
(FPCore (x y)
 :precision binary64
 (* (* 3.0 (sqrt x)) (- (+ y (/ 1.0 (* x 9.0))) 1.0)))
double code(double x, double y) {
	return (3.0 * sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0);
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    code = (3.0d0 * sqrt(x)) * ((y + (1.0d0 / (x * 9.0d0))) - 1.0d0)
end function
public static double code(double x, double y) {
	return (3.0 * Math.sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0);
}
def code(x, y):
	return (3.0 * math.sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0)
function code(x, y)
	return Float64(Float64(3.0 * sqrt(x)) * Float64(Float64(y + Float64(1.0 / Float64(x * 9.0))) - 1.0))
end
function tmp = code(x, y)
	tmp = (3.0 * sqrt(x)) * ((y + (1.0 / (x * 9.0))) - 1.0);
end
code[x_, y_] := N[(N[(3.0 * N[Sqrt[x], $MachinePrecision]), $MachinePrecision] * N[(N[(y + N[(1.0 / N[(x * 9.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)
\end{array}

Alternative 1: 99.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \mathsf{fma}\left(\mathsf{fma}\left(3, y, -3\right), \sqrt{x}, \frac{0.3333333333333333}{\sqrt{x}}\right) \end{array} \]
(FPCore (x y)
 :precision binary64
 (fma (fma 3.0 y -3.0) (sqrt x) (/ 0.3333333333333333 (sqrt x))))
double code(double x, double y) {
	return fma(fma(3.0, y, -3.0), sqrt(x), (0.3333333333333333 / sqrt(x)));
}
function code(x, y)
	return fma(fma(3.0, y, -3.0), sqrt(x), Float64(0.3333333333333333 / sqrt(x)))
end
code[x_, y_] := N[(N[(3.0 * y + -3.0), $MachinePrecision] * N[Sqrt[x], $MachinePrecision] + N[(0.3333333333333333 / N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\mathsf{fma}\left(\mathsf{fma}\left(3, y, -3\right), \sqrt{x}, \frac{0.3333333333333333}{\sqrt{x}}\right)
\end{array}
Derivation
  1. Initial program 99.5%

    \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-*.f64N/A

      \[\leadsto \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)} \]
    2. lift--.f64N/A

      \[\leadsto \left(3 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)} \]
    3. sub-negN/A

      \[\leadsto \left(3 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) + \left(\mathsf{neg}\left(1\right)\right)\right)} \]
    4. metadata-evalN/A

      \[\leadsto \left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) + \color{blue}{-1}\right) \]
    5. +-commutativeN/A

      \[\leadsto \left(3 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(-1 + \left(y + \frac{1}{x \cdot 9}\right)\right)} \]
    6. distribute-lft-inN/A

      \[\leadsto \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot -1 + \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right)} \]
    7. lift-*.f64N/A

      \[\leadsto \color{blue}{\left(3 \cdot \sqrt{x}\right)} \cdot -1 + \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right) \]
    8. *-commutativeN/A

      \[\leadsto \color{blue}{\left(\sqrt{x} \cdot 3\right)} \cdot -1 + \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right) \]
    9. associate-*l*N/A

      \[\leadsto \color{blue}{\sqrt{x} \cdot \left(3 \cdot -1\right)} + \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right) \]
    10. metadata-evalN/A

      \[\leadsto \sqrt{x} \cdot \color{blue}{-3} + \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right) \]
    11. metadata-evalN/A

      \[\leadsto \sqrt{x} \cdot \color{blue}{\left(-1 \cdot 3\right)} + \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right) \]
    12. lower-fma.f64N/A

      \[\leadsto \color{blue}{\mathsf{fma}\left(\sqrt{x}, -1 \cdot 3, \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right)\right)} \]
    13. metadata-evalN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{x}, \color{blue}{-3}, \left(3 \cdot \sqrt{x}\right) \cdot \left(y + \frac{1}{x \cdot 9}\right)\right) \]
    14. *-commutativeN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{x}, -3, \color{blue}{\left(y + \frac{1}{x \cdot 9}\right) \cdot \left(3 \cdot \sqrt{x}\right)}\right) \]
    15. lift-*.f64N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{x}, -3, \left(y + \frac{1}{x \cdot 9}\right) \cdot \color{blue}{\left(3 \cdot \sqrt{x}\right)}\right) \]
    16. associate-*r*N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{x}, -3, \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) \cdot 3\right) \cdot \sqrt{x}}\right) \]
    17. lower-*.f64N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{x}, -3, \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) \cdot 3\right) \cdot \sqrt{x}}\right) \]
  4. Applied rewrites99.5%

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

    \[\leadsto \color{blue}{-3 \cdot \sqrt{x} + \left(\frac{1}{3} \cdot \sqrt{\frac{1}{x}} + 3 \cdot \left(\sqrt{x} \cdot y\right)\right)} \]
  6. Step-by-step derivation
    1. +-commutativeN/A

      \[\leadsto \color{blue}{\left(\frac{1}{3} \cdot \sqrt{\frac{1}{x}} + 3 \cdot \left(\sqrt{x} \cdot y\right)\right) + -3 \cdot \sqrt{x}} \]
    2. associate-+l+N/A

      \[\leadsto \color{blue}{\frac{1}{3} \cdot \sqrt{\frac{1}{x}} + \left(3 \cdot \left(\sqrt{x} \cdot y\right) + -3 \cdot \sqrt{x}\right)} \]
    3. *-commutativeN/A

      \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot \frac{1}{3}} + \left(3 \cdot \left(\sqrt{x} \cdot y\right) + -3 \cdot \sqrt{x}\right) \]
    4. +-commutativeN/A

      \[\leadsto \sqrt{\frac{1}{x}} \cdot \frac{1}{3} + \color{blue}{\left(-3 \cdot \sqrt{x} + 3 \cdot \left(\sqrt{x} \cdot y\right)\right)} \]
    5. lower-fma.f64N/A

      \[\leadsto \color{blue}{\mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, -3 \cdot \sqrt{x} + 3 \cdot \left(\sqrt{x} \cdot y\right)\right)} \]
    6. lower-sqrt.f64N/A

      \[\leadsto \mathsf{fma}\left(\color{blue}{\sqrt{\frac{1}{x}}}, \frac{1}{3}, -3 \cdot \sqrt{x} + 3 \cdot \left(\sqrt{x} \cdot y\right)\right) \]
    7. lower-/.f64N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\color{blue}{\frac{1}{x}}}, \frac{1}{3}, -3 \cdot \sqrt{x} + 3 \cdot \left(\sqrt{x} \cdot y\right)\right) \]
    8. +-commutativeN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{3 \cdot \left(\sqrt{x} \cdot y\right) + -3 \cdot \sqrt{x}}\right) \]
    9. metadata-evalN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, 3 \cdot \left(\sqrt{x} \cdot y\right) + \color{blue}{\left(\mathsf{neg}\left(3\right)\right)} \cdot \sqrt{x}\right) \]
    10. cancel-sign-sub-invN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{3 \cdot \left(\sqrt{x} \cdot y\right) - 3 \cdot \sqrt{x}}\right) \]
    11. *-commutativeN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, 3 \cdot \color{blue}{\left(y \cdot \sqrt{x}\right)} - 3 \cdot \sqrt{x}\right) \]
    12. associate-*r*N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{\left(3 \cdot y\right) \cdot \sqrt{x}} - 3 \cdot \sqrt{x}\right) \]
    13. distribute-rgt-out--N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{\sqrt{x} \cdot \left(3 \cdot y - 3\right)}\right) \]
    14. *-commutativeN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{\left(3 \cdot y - 3\right) \cdot \sqrt{x}}\right) \]
    15. lower-*.f64N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{\left(3 \cdot y - 3\right) \cdot \sqrt{x}}\right) \]
    16. sub-negN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{\left(3 \cdot y + \left(\mathsf{neg}\left(3\right)\right)\right)} \cdot \sqrt{x}\right) \]
    17. metadata-evalN/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \left(3 \cdot y + \color{blue}{-3}\right) \cdot \sqrt{x}\right) \]
    18. lower-fma.f64N/A

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, \frac{1}{3}, \color{blue}{\mathsf{fma}\left(3, y, -3\right)} \cdot \sqrt{x}\right) \]
    19. lower-sqrt.f6499.5

      \[\leadsto \mathsf{fma}\left(\sqrt{\frac{1}{x}}, 0.3333333333333333, \mathsf{fma}\left(3, y, -3\right) \cdot \color{blue}{\sqrt{x}}\right) \]
  7. Applied rewrites99.5%

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

      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(3, y, -3\right), \color{blue}{\sqrt{x}}, \frac{0.3333333333333333}{\sqrt{x}}\right) \]
    2. Add Preprocessing

    Alternative 2: 91.8% accurate, 0.1× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_0 := 3 \cdot \sqrt{x}\\ t_1 := t\_0 \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right)\\ \mathbf{if}\;t\_1 \leq -1:\\ \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\ \mathbf{elif}\;t\_1 \leq 10^{+153}:\\ \;\;\;\;\sqrt{{x}^{-1}} \cdot 0.3333333333333333\\ \mathbf{else}:\\ \;\;\;\;t\_0 \cdot y\\ \end{array} \end{array} \]
    (FPCore (x y)
     :precision binary64
     (let* ((t_0 (* 3.0 (sqrt x)))
            (t_1 (* t_0 (- (+ y (pow (* x 9.0) -1.0)) 1.0))))
       (if (<= t_1 -1.0)
         (* (fma 3.0 y -3.0) (sqrt x))
         (if (<= t_1 1e+153)
           (* (sqrt (pow x -1.0)) 0.3333333333333333)
           (* t_0 y)))))
    double code(double x, double y) {
    	double t_0 = 3.0 * sqrt(x);
    	double t_1 = t_0 * ((y + pow((x * 9.0), -1.0)) - 1.0);
    	double tmp;
    	if (t_1 <= -1.0) {
    		tmp = fma(3.0, y, -3.0) * sqrt(x);
    	} else if (t_1 <= 1e+153) {
    		tmp = sqrt(pow(x, -1.0)) * 0.3333333333333333;
    	} else {
    		tmp = t_0 * y;
    	}
    	return tmp;
    }
    
    function code(x, y)
    	t_0 = Float64(3.0 * sqrt(x))
    	t_1 = Float64(t_0 * Float64(Float64(y + (Float64(x * 9.0) ^ -1.0)) - 1.0))
    	tmp = 0.0
    	if (t_1 <= -1.0)
    		tmp = Float64(fma(3.0, y, -3.0) * sqrt(x));
    	elseif (t_1 <= 1e+153)
    		tmp = Float64(sqrt((x ^ -1.0)) * 0.3333333333333333);
    	else
    		tmp = Float64(t_0 * y);
    	end
    	return tmp
    end
    
    code[x_, y_] := Block[{t$95$0 = N[(3.0 * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 * N[(N[(y + N[Power[N[(x * 9.0), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -1.0], N[(N[(3.0 * y + -3.0), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 1e+153], N[(N[Sqrt[N[Power[x, -1.0], $MachinePrecision]], $MachinePrecision] * 0.3333333333333333), $MachinePrecision], N[(t$95$0 * y), $MachinePrecision]]]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_0 := 3 \cdot \sqrt{x}\\
    t_1 := t\_0 \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right)\\
    \mathbf{if}\;t\_1 \leq -1:\\
    \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\
    
    \mathbf{elif}\;t\_1 \leq 10^{+153}:\\
    \;\;\;\;\sqrt{{x}^{-1}} \cdot 0.3333333333333333\\
    
    \mathbf{else}:\\
    \;\;\;\;t\_0 \cdot y\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 3 regimes
    2. if (*.f64 (*.f64 #s(literal 3 binary64) (sqrt.f64 x)) (-.f64 (+.f64 y (/.f64 #s(literal 1 binary64) (*.f64 x #s(literal 9 binary64)))) #s(literal 1 binary64))) < -1

      1. Initial program 99.6%

        \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
      2. Add Preprocessing
      3. Taylor expanded in x around inf

        \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot \left(y - 1\right)\right)} \]
      4. Step-by-step derivation
        1. associate-*r*N/A

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

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

          \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
        4. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
        5. *-commutativeN/A

          \[\leadsto \color{blue}{\left(3 \cdot \left(y - 1\right)\right)} \cdot \sqrt{x} \]
        6. sub-negN/A

          \[\leadsto \left(3 \cdot \color{blue}{\left(y + \left(\mathsf{neg}\left(1\right)\right)\right)}\right) \cdot \sqrt{x} \]
        7. metadata-evalN/A

          \[\leadsto \left(3 \cdot \left(y + \color{blue}{-1}\right)\right) \cdot \sqrt{x} \]
        8. distribute-lft-inN/A

          \[\leadsto \color{blue}{\left(3 \cdot y + 3 \cdot -1\right)} \cdot \sqrt{x} \]
        9. metadata-evalN/A

          \[\leadsto \left(3 \cdot y + \color{blue}{-3}\right) \cdot \sqrt{x} \]
        10. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(3, y, -3\right)} \cdot \sqrt{x} \]
        11. lower-sqrt.f6497.2

          \[\leadsto \mathsf{fma}\left(3, y, -3\right) \cdot \color{blue}{\sqrt{x}} \]
      5. Applied rewrites97.2%

        \[\leadsto \color{blue}{\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}} \]

      if -1 < (*.f64 (*.f64 #s(literal 3 binary64) (sqrt.f64 x)) (-.f64 (+.f64 y (/.f64 #s(literal 1 binary64) (*.f64 x #s(literal 9 binary64)))) #s(literal 1 binary64))) < 1e153

      1. Initial program 99.3%

        \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

        \[\leadsto \color{blue}{\frac{1}{3} \cdot \sqrt{\frac{1}{x}}} \]
      4. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot \frac{1}{3}} \]
        2. lower-*.f64N/A

          \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot \frac{1}{3}} \]
        3. lower-sqrt.f64N/A

          \[\leadsto \color{blue}{\sqrt{\frac{1}{x}}} \cdot \frac{1}{3} \]
        4. lower-/.f6481.7

          \[\leadsto \sqrt{\color{blue}{\frac{1}{x}}} \cdot 0.3333333333333333 \]
      5. Applied rewrites81.7%

        \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot 0.3333333333333333} \]

      if 1e153 < (*.f64 (*.f64 #s(literal 3 binary64) (sqrt.f64 x)) (-.f64 (+.f64 y (/.f64 #s(literal 1 binary64) (*.f64 x #s(literal 9 binary64)))) #s(literal 1 binary64)))

      1. Initial program 99.8%

        \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
      2. Add Preprocessing
      3. Taylor expanded in y around inf

        \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot y\right)} \]
      4. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
        2. lower-*.f64N/A

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

          \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right)} \cdot 3 \]
        4. lower-sqrt.f6499.7

          \[\leadsto \left(\color{blue}{\sqrt{x}} \cdot y\right) \cdot 3 \]
      5. Applied rewrites99.7%

        \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
      6. Step-by-step derivation
        1. Applied rewrites99.8%

          \[\leadsto \left(3 \cdot \sqrt{x}\right) \cdot \color{blue}{y} \]
      7. Recombined 3 regimes into one program.
      8. Final simplification91.2%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right) \leq -1:\\ \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\ \mathbf{elif}\;\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right) \leq 10^{+153}:\\ \;\;\;\;\sqrt{{x}^{-1}} \cdot 0.3333333333333333\\ \mathbf{else}:\\ \;\;\;\;\left(3 \cdot \sqrt{x}\right) \cdot y\\ \end{array} \]
      9. Add Preprocessing

      Alternative 3: 92.7% accurate, 0.1× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := 3 \cdot \sqrt{x}\\ t_1 := t\_0 \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right)\\ \mathbf{if}\;t\_1 \leq -2000000:\\ \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\ \mathbf{elif}\;t\_1 \leq 10^{+153}:\\ \;\;\;\;\sqrt{x} \cdot \left(\frac{0.3333333333333333}{x} - 3\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0 \cdot y\\ \end{array} \end{array} \]
      (FPCore (x y)
       :precision binary64
       (let* ((t_0 (* 3.0 (sqrt x)))
              (t_1 (* t_0 (- (+ y (pow (* x 9.0) -1.0)) 1.0))))
         (if (<= t_1 -2000000.0)
           (* (fma 3.0 y -3.0) (sqrt x))
           (if (<= t_1 1e+153)
             (* (sqrt x) (- (/ 0.3333333333333333 x) 3.0))
             (* t_0 y)))))
      double code(double x, double y) {
      	double t_0 = 3.0 * sqrt(x);
      	double t_1 = t_0 * ((y + pow((x * 9.0), -1.0)) - 1.0);
      	double tmp;
      	if (t_1 <= -2000000.0) {
      		tmp = fma(3.0, y, -3.0) * sqrt(x);
      	} else if (t_1 <= 1e+153) {
      		tmp = sqrt(x) * ((0.3333333333333333 / x) - 3.0);
      	} else {
      		tmp = t_0 * y;
      	}
      	return tmp;
      }
      
      function code(x, y)
      	t_0 = Float64(3.0 * sqrt(x))
      	t_1 = Float64(t_0 * Float64(Float64(y + (Float64(x * 9.0) ^ -1.0)) - 1.0))
      	tmp = 0.0
      	if (t_1 <= -2000000.0)
      		tmp = Float64(fma(3.0, y, -3.0) * sqrt(x));
      	elseif (t_1 <= 1e+153)
      		tmp = Float64(sqrt(x) * Float64(Float64(0.3333333333333333 / x) - 3.0));
      	else
      		tmp = Float64(t_0 * y);
      	end
      	return tmp
      end
      
      code[x_, y_] := Block[{t$95$0 = N[(3.0 * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 * N[(N[(y + N[Power[N[(x * 9.0), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -2000000.0], N[(N[(3.0 * y + -3.0), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 1e+153], N[(N[Sqrt[x], $MachinePrecision] * N[(N[(0.3333333333333333 / x), $MachinePrecision] - 3.0), $MachinePrecision]), $MachinePrecision], N[(t$95$0 * y), $MachinePrecision]]]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := 3 \cdot \sqrt{x}\\
      t_1 := t\_0 \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right)\\
      \mathbf{if}\;t\_1 \leq -2000000:\\
      \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\
      
      \mathbf{elif}\;t\_1 \leq 10^{+153}:\\
      \;\;\;\;\sqrt{x} \cdot \left(\frac{0.3333333333333333}{x} - 3\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_0 \cdot y\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if (*.f64 (*.f64 #s(literal 3 binary64) (sqrt.f64 x)) (-.f64 (+.f64 y (/.f64 #s(literal 1 binary64) (*.f64 x #s(literal 9 binary64)))) #s(literal 1 binary64))) < -2e6

        1. Initial program 99.6%

          \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
        2. Add Preprocessing
        3. Taylor expanded in x around inf

          \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot \left(y - 1\right)\right)} \]
        4. Step-by-step derivation
          1. associate-*r*N/A

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

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

            \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
          4. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
          5. *-commutativeN/A

            \[\leadsto \color{blue}{\left(3 \cdot \left(y - 1\right)\right)} \cdot \sqrt{x} \]
          6. sub-negN/A

            \[\leadsto \left(3 \cdot \color{blue}{\left(y + \left(\mathsf{neg}\left(1\right)\right)\right)}\right) \cdot \sqrt{x} \]
          7. metadata-evalN/A

            \[\leadsto \left(3 \cdot \left(y + \color{blue}{-1}\right)\right) \cdot \sqrt{x} \]
          8. distribute-lft-inN/A

            \[\leadsto \color{blue}{\left(3 \cdot y + 3 \cdot -1\right)} \cdot \sqrt{x} \]
          9. metadata-evalN/A

            \[\leadsto \left(3 \cdot y + \color{blue}{-3}\right) \cdot \sqrt{x} \]
          10. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(3, y, -3\right)} \cdot \sqrt{x} \]
          11. lower-sqrt.f6498.3

            \[\leadsto \mathsf{fma}\left(3, y, -3\right) \cdot \color{blue}{\sqrt{x}} \]
        5. Applied rewrites98.3%

          \[\leadsto \color{blue}{\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}} \]

        if -2e6 < (*.f64 (*.f64 #s(literal 3 binary64) (sqrt.f64 x)) (-.f64 (+.f64 y (/.f64 #s(literal 1 binary64) (*.f64 x #s(literal 9 binary64)))) #s(literal 1 binary64))) < 1e153

        1. Initial program 99.3%

          \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
        2. Add Preprocessing
        3. Taylor expanded in y around 0

          \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot \left(\frac{1}{9} \cdot \frac{1}{x} - 1\right)\right)} \]
        4. Step-by-step derivation
          1. associate-*r*N/A

            \[\leadsto \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot \left(\frac{1}{9} \cdot \frac{1}{x} - 1\right)} \]
          2. distribute-lft-out--N/A

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

            \[\leadsto \color{blue}{\left(\sqrt{x} \cdot 3\right)} \cdot \left(\frac{1}{9} \cdot \frac{1}{x}\right) - \left(3 \cdot \sqrt{x}\right) \cdot 1 \]
          4. associate-*l*N/A

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

            \[\leadsto \sqrt{x} \cdot \left(3 \cdot \color{blue}{\frac{\frac{1}{9} \cdot 1}{x}}\right) - \left(3 \cdot \sqrt{x}\right) \cdot 1 \]
          6. metadata-evalN/A

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

            \[\leadsto \sqrt{x} \cdot \color{blue}{\frac{3 \cdot \frac{1}{9}}{x}} - \left(3 \cdot \sqrt{x}\right) \cdot 1 \]
          8. metadata-evalN/A

            \[\leadsto \sqrt{x} \cdot \frac{\color{blue}{\frac{1}{3}}}{x} - \left(3 \cdot \sqrt{x}\right) \cdot 1 \]
          9. metadata-evalN/A

            \[\leadsto \sqrt{x} \cdot \frac{\color{blue}{\frac{1}{9} \cdot 3}}{x} - \left(3 \cdot \sqrt{x}\right) \cdot 1 \]
          10. associate-*l/N/A

            \[\leadsto \sqrt{x} \cdot \color{blue}{\left(\frac{\frac{1}{9}}{x} \cdot 3\right)} - \left(3 \cdot \sqrt{x}\right) \cdot 1 \]
          11. metadata-evalN/A

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

            \[\leadsto \sqrt{x} \cdot \left(\color{blue}{\left(\frac{1}{9} \cdot \frac{1}{x}\right)} \cdot 3\right) - \left(3 \cdot \sqrt{x}\right) \cdot 1 \]
          13. *-rgt-identityN/A

            \[\leadsto \sqrt{x} \cdot \left(\left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot 3\right) - \color{blue}{3 \cdot \sqrt{x}} \]
          14. *-commutativeN/A

            \[\leadsto \sqrt{x} \cdot \left(\left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot 3\right) - \color{blue}{\sqrt{x} \cdot 3} \]
          15. distribute-lft-out--N/A

            \[\leadsto \color{blue}{\sqrt{x} \cdot \left(\left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot 3 - 3\right)} \]
          16. lower-*.f64N/A

            \[\leadsto \color{blue}{\sqrt{x} \cdot \left(\left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot 3 - 3\right)} \]
          17. lower-sqrt.f64N/A

            \[\leadsto \color{blue}{\sqrt{x}} \cdot \left(\left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot 3 - 3\right) \]
          18. lower--.f64N/A

            \[\leadsto \sqrt{x} \cdot \color{blue}{\left(\left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot 3 - 3\right)} \]
        5. Applied rewrites82.3%

          \[\leadsto \color{blue}{\sqrt{x} \cdot \left(\frac{0.3333333333333333}{x} - 3\right)} \]

        if 1e153 < (*.f64 (*.f64 #s(literal 3 binary64) (sqrt.f64 x)) (-.f64 (+.f64 y (/.f64 #s(literal 1 binary64) (*.f64 x #s(literal 9 binary64)))) #s(literal 1 binary64)))

        1. Initial program 99.8%

          \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
        2. Add Preprocessing
        3. Taylor expanded in y around inf

          \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot y\right)} \]
        4. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
          2. lower-*.f64N/A

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

            \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right)} \cdot 3 \]
          4. lower-sqrt.f6499.7

            \[\leadsto \left(\color{blue}{\sqrt{x}} \cdot y\right) \cdot 3 \]
        5. Applied rewrites99.7%

          \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
        6. Step-by-step derivation
          1. Applied rewrites99.8%

            \[\leadsto \left(3 \cdot \sqrt{x}\right) \cdot \color{blue}{y} \]
        7. Recombined 3 regimes into one program.
        8. Final simplification91.8%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right) \leq -2000000:\\ \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\ \mathbf{elif}\;\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + {\left(x \cdot 9\right)}^{-1}\right) - 1\right) \leq 10^{+153}:\\ \;\;\;\;\sqrt{x} \cdot \left(\frac{0.3333333333333333}{x} - 3\right)\\ \mathbf{else}:\\ \;\;\;\;\left(3 \cdot \sqrt{x}\right) \cdot y\\ \end{array} \]
        9. Add Preprocessing

        Alternative 4: 99.4% accurate, 0.3× speedup?

        \[\begin{array}{l} \\ \mathsf{fma}\left(1 - y, -3, {\left(x \cdot 3\right)}^{-1}\right) \cdot \sqrt{x} \end{array} \]
        (FPCore (x y)
         :precision binary64
         (* (fma (- 1.0 y) -3.0 (pow (* x 3.0) -1.0)) (sqrt x)))
        double code(double x, double y) {
        	return fma((1.0 - y), -3.0, pow((x * 3.0), -1.0)) * sqrt(x);
        }
        
        function code(x, y)
        	return Float64(fma(Float64(1.0 - y), -3.0, (Float64(x * 3.0) ^ -1.0)) * sqrt(x))
        end
        
        code[x_, y_] := N[(N[(N[(1.0 - y), $MachinePrecision] * -3.0 + N[Power[N[(x * 3.0), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]
        
        \begin{array}{l}
        
        \\
        \mathsf{fma}\left(1 - y, -3, {\left(x \cdot 3\right)}^{-1}\right) \cdot \sqrt{x}
        \end{array}
        
        Derivation
        1. Initial program 99.5%

          \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)} \]
          2. *-commutativeN/A

            \[\leadsto \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot \left(3 \cdot \sqrt{x}\right)} \]
          3. lift-*.f64N/A

            \[\leadsto \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot \color{blue}{\left(3 \cdot \sqrt{x}\right)} \]
          4. associate-*r*N/A

            \[\leadsto \color{blue}{\left(\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
          5. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
          6. *-commutativeN/A

            \[\leadsto \color{blue}{\left(3 \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)\right)} \cdot \sqrt{x} \]
          7. lift--.f64N/A

            \[\leadsto \left(3 \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)}\right) \cdot \sqrt{x} \]
          8. sub-negN/A

            \[\leadsto \left(3 \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) + \left(\mathsf{neg}\left(1\right)\right)\right)}\right) \cdot \sqrt{x} \]
          9. metadata-evalN/A

            \[\leadsto \left(3 \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) + \color{blue}{-1}\right)\right) \cdot \sqrt{x} \]
          10. distribute-rgt-inN/A

            \[\leadsto \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) \cdot 3 + -1 \cdot 3\right)} \cdot \sqrt{x} \]
          11. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(y + \frac{1}{x \cdot 9}, 3, -1 \cdot 3\right)} \cdot \sqrt{x} \]
          12. lift-/.f64N/A

            \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{1}{x \cdot 9}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          13. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(y + \frac{1}{\color{blue}{x \cdot 9}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          14. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left(y + \frac{1}{\color{blue}{9 \cdot x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          15. associate-/r*N/A

            \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{\frac{1}{9}}{x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          16. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{\frac{1}{9}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          17. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{{9}^{-1}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          18. lower-/.f64N/A

            \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{{9}^{-1}}{x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          19. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{\frac{1}{9}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
          20. metadata-eval99.4

            \[\leadsto \mathsf{fma}\left(y + \frac{0.1111111111111111}{x}, 3, \color{blue}{-3}\right) \cdot \sqrt{x} \]
        4. Applied rewrites99.4%

          \[\leadsto \color{blue}{\mathsf{fma}\left(y + \frac{0.1111111111111111}{x}, 3, -3\right) \cdot \sqrt{x}} \]
        5. Taylor expanded in x around inf

          \[\leadsto \color{blue}{\left(\left(3 \cdot y + \frac{1}{3} \cdot \frac{1}{x}\right) - 3\right)} \cdot \sqrt{x} \]
        6. Step-by-step derivation
          1. +-commutativeN/A

            \[\leadsto \left(\color{blue}{\left(\frac{1}{3} \cdot \frac{1}{x} + 3 \cdot y\right)} - 3\right) \cdot \sqrt{x} \]
          2. associate--l+N/A

            \[\leadsto \color{blue}{\left(\frac{1}{3} \cdot \frac{1}{x} + \left(3 \cdot y - 3\right)\right)} \cdot \sqrt{x} \]
          3. +-commutativeN/A

            \[\leadsto \color{blue}{\left(\left(3 \cdot y - 3\right) + \frac{1}{3} \cdot \frac{1}{x}\right)} \cdot \sqrt{x} \]
          4. sub-negN/A

            \[\leadsto \left(\color{blue}{\left(3 \cdot y + \left(\mathsf{neg}\left(3\right)\right)\right)} + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          5. metadata-evalN/A

            \[\leadsto \left(\left(\color{blue}{\left(\mathsf{neg}\left(-3\right)\right)} \cdot y + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          6. distribute-lft-neg-inN/A

            \[\leadsto \left(\left(\color{blue}{\left(\mathsf{neg}\left(-3 \cdot y\right)\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          7. distribute-rgt-neg-outN/A

            \[\leadsto \left(\left(\color{blue}{-3 \cdot \left(\mathsf{neg}\left(y\right)\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          8. mul-1-negN/A

            \[\leadsto \left(\left(-3 \cdot \color{blue}{\left(-1 \cdot y\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          9. rem-square-sqrtN/A

            \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)} \cdot y\right) + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          10. unpow2N/A

            \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{{\left(\sqrt{-1}\right)}^{2}} \cdot y\right) + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          11. *-commutativeN/A

            \[\leadsto \left(\left(-3 \cdot \color{blue}{\left(y \cdot {\left(\sqrt{-1}\right)}^{2}\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          12. metadata-evalN/A

            \[\leadsto \left(\left(-3 \cdot \left(y \cdot {\left(\sqrt{-1}\right)}^{2}\right) + \color{blue}{-3}\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          13. *-commutativeN/A

            \[\leadsto \left(\left(-3 \cdot \color{blue}{\left({\left(\sqrt{-1}\right)}^{2} \cdot y\right)} + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          14. unpow2N/A

            \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)} \cdot y\right) + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          15. rem-square-sqrtN/A

            \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{-1} \cdot y\right) + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          16. *-commutativeN/A

            \[\leadsto \left(\left(\color{blue}{\left(-1 \cdot y\right) \cdot -3} + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          17. distribute-lft1-inN/A

            \[\leadsto \left(\color{blue}{\left(-1 \cdot y + 1\right) \cdot -3} + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          18. +-commutativeN/A

            \[\leadsto \left(\color{blue}{\left(1 + -1 \cdot y\right)} \cdot -3 + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
          19. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(1 + -1 \cdot y, -3, \frac{1}{3} \cdot \frac{1}{x}\right)} \cdot \sqrt{x} \]
        7. Applied rewrites99.5%

          \[\leadsto \color{blue}{\mathsf{fma}\left(1 - y, -3, \frac{0.3333333333333333}{x}\right)} \cdot \sqrt{x} \]
        8. Step-by-step derivation
          1. Applied rewrites99.5%

            \[\leadsto \mathsf{fma}\left(1 - y, -3, \frac{1}{x \cdot 3}\right) \cdot \sqrt{x} \]
          2. Final simplification99.5%

            \[\leadsto \mathsf{fma}\left(1 - y, -3, {\left(x \cdot 3\right)}^{-1}\right) \cdot \sqrt{x} \]
          3. Add Preprocessing

          Alternative 5: 98.1% accurate, 1.0× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq 3 \cdot 10^{-8}:\\ \;\;\;\;\mathsf{fma}\left(-y, -3, \frac{0.3333333333333333}{x}\right) \cdot \sqrt{x}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\ \end{array} \end{array} \]
          (FPCore (x y)
           :precision binary64
           (if (<= x 3e-8)
             (* (fma (- y) -3.0 (/ 0.3333333333333333 x)) (sqrt x))
             (* (fma 3.0 y -3.0) (sqrt x))))
          double code(double x, double y) {
          	double tmp;
          	if (x <= 3e-8) {
          		tmp = fma(-y, -3.0, (0.3333333333333333 / x)) * sqrt(x);
          	} else {
          		tmp = fma(3.0, y, -3.0) * sqrt(x);
          	}
          	return tmp;
          }
          
          function code(x, y)
          	tmp = 0.0
          	if (x <= 3e-8)
          		tmp = Float64(fma(Float64(-y), -3.0, Float64(0.3333333333333333 / x)) * sqrt(x));
          	else
          		tmp = Float64(fma(3.0, y, -3.0) * sqrt(x));
          	end
          	return tmp
          end
          
          code[x_, y_] := If[LessEqual[x, 3e-8], N[(N[((-y) * -3.0 + N[(0.3333333333333333 / x), $MachinePrecision]), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision], N[(N[(3.0 * y + -3.0), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;x \leq 3 \cdot 10^{-8}:\\
          \;\;\;\;\mathsf{fma}\left(-y, -3, \frac{0.3333333333333333}{x}\right) \cdot \sqrt{x}\\
          
          \mathbf{else}:\\
          \;\;\;\;\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if x < 2.99999999999999973e-8

            1. Initial program 99.3%

              \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)} \]
              2. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot \left(3 \cdot \sqrt{x}\right)} \]
              3. lift-*.f64N/A

                \[\leadsto \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot \color{blue}{\left(3 \cdot \sqrt{x}\right)} \]
              4. associate-*r*N/A

                \[\leadsto \color{blue}{\left(\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
              5. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
              6. *-commutativeN/A

                \[\leadsto \color{blue}{\left(3 \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)\right)} \cdot \sqrt{x} \]
              7. lift--.f64N/A

                \[\leadsto \left(3 \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)}\right) \cdot \sqrt{x} \]
              8. sub-negN/A

                \[\leadsto \left(3 \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) + \left(\mathsf{neg}\left(1\right)\right)\right)}\right) \cdot \sqrt{x} \]
              9. metadata-evalN/A

                \[\leadsto \left(3 \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) + \color{blue}{-1}\right)\right) \cdot \sqrt{x} \]
              10. distribute-rgt-inN/A

                \[\leadsto \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) \cdot 3 + -1 \cdot 3\right)} \cdot \sqrt{x} \]
              11. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(y + \frac{1}{x \cdot 9}, 3, -1 \cdot 3\right)} \cdot \sqrt{x} \]
              12. lift-/.f64N/A

                \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{1}{x \cdot 9}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              13. lift-*.f64N/A

                \[\leadsto \mathsf{fma}\left(y + \frac{1}{\color{blue}{x \cdot 9}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              14. *-commutativeN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{1}{\color{blue}{9 \cdot x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              15. associate-/r*N/A

                \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{\frac{1}{9}}{x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              16. metadata-evalN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{\frac{1}{9}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              17. metadata-evalN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{{9}^{-1}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              18. lower-/.f64N/A

                \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{{9}^{-1}}{x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              19. metadata-evalN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{\frac{1}{9}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              20. metadata-eval99.1

                \[\leadsto \mathsf{fma}\left(y + \frac{0.1111111111111111}{x}, 3, \color{blue}{-3}\right) \cdot \sqrt{x} \]
            4. Applied rewrites99.1%

              \[\leadsto \color{blue}{\mathsf{fma}\left(y + \frac{0.1111111111111111}{x}, 3, -3\right) \cdot \sqrt{x}} \]
            5. Taylor expanded in x around inf

              \[\leadsto \color{blue}{\left(\left(3 \cdot y + \frac{1}{3} \cdot \frac{1}{x}\right) - 3\right)} \cdot \sqrt{x} \]
            6. Step-by-step derivation
              1. +-commutativeN/A

                \[\leadsto \left(\color{blue}{\left(\frac{1}{3} \cdot \frac{1}{x} + 3 \cdot y\right)} - 3\right) \cdot \sqrt{x} \]
              2. associate--l+N/A

                \[\leadsto \color{blue}{\left(\frac{1}{3} \cdot \frac{1}{x} + \left(3 \cdot y - 3\right)\right)} \cdot \sqrt{x} \]
              3. +-commutativeN/A

                \[\leadsto \color{blue}{\left(\left(3 \cdot y - 3\right) + \frac{1}{3} \cdot \frac{1}{x}\right)} \cdot \sqrt{x} \]
              4. sub-negN/A

                \[\leadsto \left(\color{blue}{\left(3 \cdot y + \left(\mathsf{neg}\left(3\right)\right)\right)} + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              5. metadata-evalN/A

                \[\leadsto \left(\left(\color{blue}{\left(\mathsf{neg}\left(-3\right)\right)} \cdot y + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              6. distribute-lft-neg-inN/A

                \[\leadsto \left(\left(\color{blue}{\left(\mathsf{neg}\left(-3 \cdot y\right)\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              7. distribute-rgt-neg-outN/A

                \[\leadsto \left(\left(\color{blue}{-3 \cdot \left(\mathsf{neg}\left(y\right)\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              8. mul-1-negN/A

                \[\leadsto \left(\left(-3 \cdot \color{blue}{\left(-1 \cdot y\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              9. rem-square-sqrtN/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)} \cdot y\right) + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              10. unpow2N/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{{\left(\sqrt{-1}\right)}^{2}} \cdot y\right) + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              11. *-commutativeN/A

                \[\leadsto \left(\left(-3 \cdot \color{blue}{\left(y \cdot {\left(\sqrt{-1}\right)}^{2}\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              12. metadata-evalN/A

                \[\leadsto \left(\left(-3 \cdot \left(y \cdot {\left(\sqrt{-1}\right)}^{2}\right) + \color{blue}{-3}\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              13. *-commutativeN/A

                \[\leadsto \left(\left(-3 \cdot \color{blue}{\left({\left(\sqrt{-1}\right)}^{2} \cdot y\right)} + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              14. unpow2N/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)} \cdot y\right) + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              15. rem-square-sqrtN/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{-1} \cdot y\right) + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              16. *-commutativeN/A

                \[\leadsto \left(\left(\color{blue}{\left(-1 \cdot y\right) \cdot -3} + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              17. distribute-lft1-inN/A

                \[\leadsto \left(\color{blue}{\left(-1 \cdot y + 1\right) \cdot -3} + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              18. +-commutativeN/A

                \[\leadsto \left(\color{blue}{\left(1 + -1 \cdot y\right)} \cdot -3 + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              19. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(1 + -1 \cdot y, -3, \frac{1}{3} \cdot \frac{1}{x}\right)} \cdot \sqrt{x} \]
            7. Applied rewrites99.3%

              \[\leadsto \color{blue}{\mathsf{fma}\left(1 - y, -3, \frac{0.3333333333333333}{x}\right)} \cdot \sqrt{x} \]
            8. Taylor expanded in y around inf

              \[\leadsto \mathsf{fma}\left(-1 \cdot y, -3, \frac{\frac{1}{3}}{x}\right) \cdot \sqrt{x} \]
            9. Step-by-step derivation
              1. Applied rewrites98.6%

                \[\leadsto \mathsf{fma}\left(-y, -3, \frac{0.3333333333333333}{x}\right) \cdot \sqrt{x} \]

              if 2.99999999999999973e-8 < x

              1. Initial program 99.6%

                \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
              2. Add Preprocessing
              3. Taylor expanded in x around inf

                \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot \left(y - 1\right)\right)} \]
              4. Step-by-step derivation
                1. associate-*r*N/A

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

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

                  \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
                4. lower-*.f64N/A

                  \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
                5. *-commutativeN/A

                  \[\leadsto \color{blue}{\left(3 \cdot \left(y - 1\right)\right)} \cdot \sqrt{x} \]
                6. sub-negN/A

                  \[\leadsto \left(3 \cdot \color{blue}{\left(y + \left(\mathsf{neg}\left(1\right)\right)\right)}\right) \cdot \sqrt{x} \]
                7. metadata-evalN/A

                  \[\leadsto \left(3 \cdot \left(y + \color{blue}{-1}\right)\right) \cdot \sqrt{x} \]
                8. distribute-lft-inN/A

                  \[\leadsto \color{blue}{\left(3 \cdot y + 3 \cdot -1\right)} \cdot \sqrt{x} \]
                9. metadata-evalN/A

                  \[\leadsto \left(3 \cdot y + \color{blue}{-3}\right) \cdot \sqrt{x} \]
                10. lower-fma.f64N/A

                  \[\leadsto \color{blue}{\mathsf{fma}\left(3, y, -3\right)} \cdot \sqrt{x} \]
                11. lower-sqrt.f6498.6

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

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

            Alternative 6: 99.4% accurate, 1.2× speedup?

            \[\begin{array}{l} \\ \mathsf{fma}\left(1 - y, -3, \frac{0.3333333333333333}{x}\right) \cdot \sqrt{x} \end{array} \]
            (FPCore (x y)
             :precision binary64
             (* (fma (- 1.0 y) -3.0 (/ 0.3333333333333333 x)) (sqrt x)))
            double code(double x, double y) {
            	return fma((1.0 - y), -3.0, (0.3333333333333333 / x)) * sqrt(x);
            }
            
            function code(x, y)
            	return Float64(fma(Float64(1.0 - y), -3.0, Float64(0.3333333333333333 / x)) * sqrt(x))
            end
            
            code[x_, y_] := N[(N[(N[(1.0 - y), $MachinePrecision] * -3.0 + N[(0.3333333333333333 / x), $MachinePrecision]), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \mathsf{fma}\left(1 - y, -3, \frac{0.3333333333333333}{x}\right) \cdot \sqrt{x}
            \end{array}
            
            Derivation
            1. Initial program 99.5%

              \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)} \]
              2. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot \left(3 \cdot \sqrt{x}\right)} \]
              3. lift-*.f64N/A

                \[\leadsto \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot \color{blue}{\left(3 \cdot \sqrt{x}\right)} \]
              4. associate-*r*N/A

                \[\leadsto \color{blue}{\left(\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
              5. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
              6. *-commutativeN/A

                \[\leadsto \color{blue}{\left(3 \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)\right)} \cdot \sqrt{x} \]
              7. lift--.f64N/A

                \[\leadsto \left(3 \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right)}\right) \cdot \sqrt{x} \]
              8. sub-negN/A

                \[\leadsto \left(3 \cdot \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) + \left(\mathsf{neg}\left(1\right)\right)\right)}\right) \cdot \sqrt{x} \]
              9. metadata-evalN/A

                \[\leadsto \left(3 \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) + \color{blue}{-1}\right)\right) \cdot \sqrt{x} \]
              10. distribute-rgt-inN/A

                \[\leadsto \color{blue}{\left(\left(y + \frac{1}{x \cdot 9}\right) \cdot 3 + -1 \cdot 3\right)} \cdot \sqrt{x} \]
              11. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(y + \frac{1}{x \cdot 9}, 3, -1 \cdot 3\right)} \cdot \sqrt{x} \]
              12. lift-/.f64N/A

                \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{1}{x \cdot 9}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              13. lift-*.f64N/A

                \[\leadsto \mathsf{fma}\left(y + \frac{1}{\color{blue}{x \cdot 9}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              14. *-commutativeN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{1}{\color{blue}{9 \cdot x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              15. associate-/r*N/A

                \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{\frac{1}{9}}{x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              16. metadata-evalN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{\frac{1}{9}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              17. metadata-evalN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{{9}^{-1}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              18. lower-/.f64N/A

                \[\leadsto \mathsf{fma}\left(y + \color{blue}{\frac{{9}^{-1}}{x}}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              19. metadata-evalN/A

                \[\leadsto \mathsf{fma}\left(y + \frac{\color{blue}{\frac{1}{9}}}{x}, 3, -1 \cdot 3\right) \cdot \sqrt{x} \]
              20. metadata-eval99.4

                \[\leadsto \mathsf{fma}\left(y + \frac{0.1111111111111111}{x}, 3, \color{blue}{-3}\right) \cdot \sqrt{x} \]
            4. Applied rewrites99.4%

              \[\leadsto \color{blue}{\mathsf{fma}\left(y + \frac{0.1111111111111111}{x}, 3, -3\right) \cdot \sqrt{x}} \]
            5. Taylor expanded in x around inf

              \[\leadsto \color{blue}{\left(\left(3 \cdot y + \frac{1}{3} \cdot \frac{1}{x}\right) - 3\right)} \cdot \sqrt{x} \]
            6. Step-by-step derivation
              1. +-commutativeN/A

                \[\leadsto \left(\color{blue}{\left(\frac{1}{3} \cdot \frac{1}{x} + 3 \cdot y\right)} - 3\right) \cdot \sqrt{x} \]
              2. associate--l+N/A

                \[\leadsto \color{blue}{\left(\frac{1}{3} \cdot \frac{1}{x} + \left(3 \cdot y - 3\right)\right)} \cdot \sqrt{x} \]
              3. +-commutativeN/A

                \[\leadsto \color{blue}{\left(\left(3 \cdot y - 3\right) + \frac{1}{3} \cdot \frac{1}{x}\right)} \cdot \sqrt{x} \]
              4. sub-negN/A

                \[\leadsto \left(\color{blue}{\left(3 \cdot y + \left(\mathsf{neg}\left(3\right)\right)\right)} + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              5. metadata-evalN/A

                \[\leadsto \left(\left(\color{blue}{\left(\mathsf{neg}\left(-3\right)\right)} \cdot y + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              6. distribute-lft-neg-inN/A

                \[\leadsto \left(\left(\color{blue}{\left(\mathsf{neg}\left(-3 \cdot y\right)\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              7. distribute-rgt-neg-outN/A

                \[\leadsto \left(\left(\color{blue}{-3 \cdot \left(\mathsf{neg}\left(y\right)\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              8. mul-1-negN/A

                \[\leadsto \left(\left(-3 \cdot \color{blue}{\left(-1 \cdot y\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              9. rem-square-sqrtN/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)} \cdot y\right) + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              10. unpow2N/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{{\left(\sqrt{-1}\right)}^{2}} \cdot y\right) + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              11. *-commutativeN/A

                \[\leadsto \left(\left(-3 \cdot \color{blue}{\left(y \cdot {\left(\sqrt{-1}\right)}^{2}\right)} + \left(\mathsf{neg}\left(3\right)\right)\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              12. metadata-evalN/A

                \[\leadsto \left(\left(-3 \cdot \left(y \cdot {\left(\sqrt{-1}\right)}^{2}\right) + \color{blue}{-3}\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              13. *-commutativeN/A

                \[\leadsto \left(\left(-3 \cdot \color{blue}{\left({\left(\sqrt{-1}\right)}^{2} \cdot y\right)} + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              14. unpow2N/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)} \cdot y\right) + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              15. rem-square-sqrtN/A

                \[\leadsto \left(\left(-3 \cdot \left(\color{blue}{-1} \cdot y\right) + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              16. *-commutativeN/A

                \[\leadsto \left(\left(\color{blue}{\left(-1 \cdot y\right) \cdot -3} + -3\right) + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              17. distribute-lft1-inN/A

                \[\leadsto \left(\color{blue}{\left(-1 \cdot y + 1\right) \cdot -3} + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              18. +-commutativeN/A

                \[\leadsto \left(\color{blue}{\left(1 + -1 \cdot y\right)} \cdot -3 + \frac{1}{3} \cdot \frac{1}{x}\right) \cdot \sqrt{x} \]
              19. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(1 + -1 \cdot y, -3, \frac{1}{3} \cdot \frac{1}{x}\right)} \cdot \sqrt{x} \]
            7. Applied rewrites99.5%

              \[\leadsto \color{blue}{\mathsf{fma}\left(1 - y, -3, \frac{0.3333333333333333}{x}\right)} \cdot \sqrt{x} \]
            8. Add Preprocessing

            Alternative 7: 99.4% accurate, 1.2× speedup?

            \[\begin{array}{l} \\ \sqrt{x} \cdot \left(\mathsf{fma}\left(3, y, \frac{0.3333333333333333}{x}\right) - 3\right) \end{array} \]
            (FPCore (x y)
             :precision binary64
             (* (sqrt x) (- (fma 3.0 y (/ 0.3333333333333333 x)) 3.0)))
            double code(double x, double y) {
            	return sqrt(x) * (fma(3.0, y, (0.3333333333333333 / x)) - 3.0);
            }
            
            function code(x, y)
            	return Float64(sqrt(x) * Float64(fma(3.0, y, Float64(0.3333333333333333 / x)) - 3.0))
            end
            
            code[x_, y_] := N[(N[Sqrt[x], $MachinePrecision] * N[(N[(3.0 * y + N[(0.3333333333333333 / x), $MachinePrecision]), $MachinePrecision] - 3.0), $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \sqrt{x} \cdot \left(\mathsf{fma}\left(3, y, \frac{0.3333333333333333}{x}\right) - 3\right)
            \end{array}
            
            Derivation
            1. Initial program 99.5%

              \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
            2. Add Preprocessing
            3. Taylor expanded in y around 0

              \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot y\right) + 3 \cdot \left(\sqrt{x} \cdot \left(\frac{1}{9} \cdot \frac{1}{x} - 1\right)\right)} \]
            4. Step-by-step derivation
              1. associate-*r*N/A

                \[\leadsto 3 \cdot \left(\sqrt{x} \cdot y\right) + \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot \left(\frac{1}{9} \cdot \frac{1}{x} - 1\right)} \]
              2. sub-negN/A

                \[\leadsto 3 \cdot \left(\sqrt{x} \cdot y\right) + \left(3 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\frac{1}{9} \cdot \frac{1}{x} + \left(\mathsf{neg}\left(1\right)\right)\right)} \]
              3. metadata-evalN/A

                \[\leadsto 3 \cdot \left(\sqrt{x} \cdot y\right) + \left(3 \cdot \sqrt{x}\right) \cdot \left(\frac{1}{9} \cdot \frac{1}{x} + \color{blue}{-1}\right) \]
              4. distribute-rgt-inN/A

                \[\leadsto 3 \cdot \left(\sqrt{x} \cdot y\right) + \color{blue}{\left(\left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot \left(3 \cdot \sqrt{x}\right) + -1 \cdot \left(3 \cdot \sqrt{x}\right)\right)} \]
              5. associate-+r+N/A

                \[\leadsto \color{blue}{\left(3 \cdot \left(\sqrt{x} \cdot y\right) + \left(\frac{1}{9} \cdot \frac{1}{x}\right) \cdot \left(3 \cdot \sqrt{x}\right)\right) + -1 \cdot \left(3 \cdot \sqrt{x}\right)} \]
              6. *-commutativeN/A

                \[\leadsto \left(3 \cdot \left(\sqrt{x} \cdot y\right) + \color{blue}{\left(3 \cdot \sqrt{x}\right) \cdot \left(\frac{1}{9} \cdot \frac{1}{x}\right)}\right) + -1 \cdot \left(3 \cdot \sqrt{x}\right) \]
              7. mul-1-negN/A

                \[\leadsto \left(3 \cdot \left(\sqrt{x} \cdot y\right) + \left(3 \cdot \sqrt{x}\right) \cdot \left(\frac{1}{9} \cdot \frac{1}{x}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(3 \cdot \sqrt{x}\right)\right)} \]
              8. unsub-negN/A

                \[\leadsto \color{blue}{\left(3 \cdot \left(\sqrt{x} \cdot y\right) + \left(3 \cdot \sqrt{x}\right) \cdot \left(\frac{1}{9} \cdot \frac{1}{x}\right)\right) - 3 \cdot \sqrt{x}} \]
            5. Applied rewrites99.5%

              \[\leadsto \color{blue}{\sqrt{x} \cdot \left(\mathsf{fma}\left(3, y, \frac{0.3333333333333333}{x}\right) - 3\right)} \]
            6. Add Preprocessing

            Alternative 8: 62.6% accurate, 2.0× speedup?

            \[\begin{array}{l} \\ \mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x} \end{array} \]
            (FPCore (x y) :precision binary64 (* (fma 3.0 y -3.0) (sqrt x)))
            double code(double x, double y) {
            	return fma(3.0, y, -3.0) * sqrt(x);
            }
            
            function code(x, y)
            	return Float64(fma(3.0, y, -3.0) * sqrt(x))
            end
            
            code[x_, y_] := N[(N[(3.0 * y + -3.0), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}
            \end{array}
            
            Derivation
            1. Initial program 99.5%

              \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
            2. Add Preprocessing
            3. Taylor expanded in x around inf

              \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot \left(y - 1\right)\right)} \]
            4. Step-by-step derivation
              1. associate-*r*N/A

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

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

                \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
              4. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(y - 1\right) \cdot 3\right) \cdot \sqrt{x}} \]
              5. *-commutativeN/A

                \[\leadsto \color{blue}{\left(3 \cdot \left(y - 1\right)\right)} \cdot \sqrt{x} \]
              6. sub-negN/A

                \[\leadsto \left(3 \cdot \color{blue}{\left(y + \left(\mathsf{neg}\left(1\right)\right)\right)}\right) \cdot \sqrt{x} \]
              7. metadata-evalN/A

                \[\leadsto \left(3 \cdot \left(y + \color{blue}{-1}\right)\right) \cdot \sqrt{x} \]
              8. distribute-lft-inN/A

                \[\leadsto \color{blue}{\left(3 \cdot y + 3 \cdot -1\right)} \cdot \sqrt{x} \]
              9. metadata-evalN/A

                \[\leadsto \left(3 \cdot y + \color{blue}{-3}\right) \cdot \sqrt{x} \]
              10. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(3, y, -3\right)} \cdot \sqrt{x} \]
              11. lower-sqrt.f6465.7

                \[\leadsto \mathsf{fma}\left(3, y, -3\right) \cdot \color{blue}{\sqrt{x}} \]
            5. Applied rewrites65.7%

              \[\leadsto \color{blue}{\mathsf{fma}\left(3, y, -3\right) \cdot \sqrt{x}} \]
            6. Add Preprocessing

            Alternative 9: 38.7% accurate, 2.0× speedup?

            \[\begin{array}{l} \\ \left(y \cdot 3\right) \cdot \sqrt{x} \end{array} \]
            (FPCore (x y) :precision binary64 (* (* y 3.0) (sqrt x)))
            double code(double x, double y) {
            	return (y * 3.0) * sqrt(x);
            }
            
            real(8) function code(x, y)
                real(8), intent (in) :: x
                real(8), intent (in) :: y
                code = (y * 3.0d0) * sqrt(x)
            end function
            
            public static double code(double x, double y) {
            	return (y * 3.0) * Math.sqrt(x);
            }
            
            def code(x, y):
            	return (y * 3.0) * math.sqrt(x)
            
            function code(x, y)
            	return Float64(Float64(y * 3.0) * sqrt(x))
            end
            
            function tmp = code(x, y)
            	tmp = (y * 3.0) * sqrt(x);
            end
            
            code[x_, y_] := N[(N[(y * 3.0), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \left(y \cdot 3\right) \cdot \sqrt{x}
            \end{array}
            
            Derivation
            1. Initial program 99.5%

              \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
            2. Add Preprocessing
            3. Taylor expanded in y around inf

              \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot y\right)} \]
            4. Step-by-step derivation
              1. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
              2. lower-*.f64N/A

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

                \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right)} \cdot 3 \]
              4. lower-sqrt.f6440.6

                \[\leadsto \left(\color{blue}{\sqrt{x}} \cdot y\right) \cdot 3 \]
            5. Applied rewrites40.6%

              \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
            6. Step-by-step derivation
              1. Applied rewrites40.6%

                \[\leadsto \color{blue}{\left(y \cdot 3\right) \cdot \sqrt{x}} \]
              2. Add Preprocessing

              Alternative 10: 38.7% accurate, 2.0× speedup?

              \[\begin{array}{l} \\ \left(3 \cdot \sqrt{x}\right) \cdot y \end{array} \]
              (FPCore (x y) :precision binary64 (* (* 3.0 (sqrt x)) y))
              double code(double x, double y) {
              	return (3.0 * sqrt(x)) * y;
              }
              
              real(8) function code(x, y)
                  real(8), intent (in) :: x
                  real(8), intent (in) :: y
                  code = (3.0d0 * sqrt(x)) * y
              end function
              
              public static double code(double x, double y) {
              	return (3.0 * Math.sqrt(x)) * y;
              }
              
              def code(x, y):
              	return (3.0 * math.sqrt(x)) * y
              
              function code(x, y)
              	return Float64(Float64(3.0 * sqrt(x)) * y)
              end
              
              function tmp = code(x, y)
              	tmp = (3.0 * sqrt(x)) * y;
              end
              
              code[x_, y_] := N[(N[(3.0 * N[Sqrt[x], $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision]
              
              \begin{array}{l}
              
              \\
              \left(3 \cdot \sqrt{x}\right) \cdot y
              \end{array}
              
              Derivation
              1. Initial program 99.5%

                \[\left(3 \cdot \sqrt{x}\right) \cdot \left(\left(y + \frac{1}{x \cdot 9}\right) - 1\right) \]
              2. Add Preprocessing
              3. Taylor expanded in y around inf

                \[\leadsto \color{blue}{3 \cdot \left(\sqrt{x} \cdot y\right)} \]
              4. Step-by-step derivation
                1. *-commutativeN/A

                  \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
                2. lower-*.f64N/A

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

                  \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right)} \cdot 3 \]
                4. lower-sqrt.f6440.6

                  \[\leadsto \left(\color{blue}{\sqrt{x}} \cdot y\right) \cdot 3 \]
              5. Applied rewrites40.6%

                \[\leadsto \color{blue}{\left(\sqrt{x} \cdot y\right) \cdot 3} \]
              6. Step-by-step derivation
                1. Applied rewrites40.6%

                  \[\leadsto \left(3 \cdot \sqrt{x}\right) \cdot \color{blue}{y} \]
                2. Add Preprocessing

                Developer Target 1: 99.4% accurate, 0.7× speedup?

                \[\begin{array}{l} \\ 3 \cdot \left(y \cdot \sqrt{x} + \left(\frac{1}{x \cdot 9} - 1\right) \cdot \sqrt{x}\right) \end{array} \]
                (FPCore (x y)
                 :precision binary64
                 (* 3.0 (+ (* y (sqrt x)) (* (- (/ 1.0 (* x 9.0)) 1.0) (sqrt x)))))
                double code(double x, double y) {
                	return 3.0 * ((y * sqrt(x)) + (((1.0 / (x * 9.0)) - 1.0) * sqrt(x)));
                }
                
                real(8) function code(x, y)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    code = 3.0d0 * ((y * sqrt(x)) + (((1.0d0 / (x * 9.0d0)) - 1.0d0) * sqrt(x)))
                end function
                
                public static double code(double x, double y) {
                	return 3.0 * ((y * Math.sqrt(x)) + (((1.0 / (x * 9.0)) - 1.0) * Math.sqrt(x)));
                }
                
                def code(x, y):
                	return 3.0 * ((y * math.sqrt(x)) + (((1.0 / (x * 9.0)) - 1.0) * math.sqrt(x)))
                
                function code(x, y)
                	return Float64(3.0 * Float64(Float64(y * sqrt(x)) + Float64(Float64(Float64(1.0 / Float64(x * 9.0)) - 1.0) * sqrt(x))))
                end
                
                function tmp = code(x, y)
                	tmp = 3.0 * ((y * sqrt(x)) + (((1.0 / (x * 9.0)) - 1.0) * sqrt(x)));
                end
                
                code[x_, y_] := N[(3.0 * N[(N[(y * N[Sqrt[x], $MachinePrecision]), $MachinePrecision] + N[(N[(N[(1.0 / N[(x * 9.0), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision] * N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
                
                \begin{array}{l}
                
                \\
                3 \cdot \left(y \cdot \sqrt{x} + \left(\frac{1}{x \cdot 9} - 1\right) \cdot \sqrt{x}\right)
                \end{array}
                

                Reproduce

                ?
                herbie shell --seed 2024313 
                (FPCore (x y)
                  :name "Numeric.SpecFunctions:incompleteGamma from math-functions-0.1.5.2, B"
                  :precision binary64
                
                  :alt
                  (! :herbie-platform default (* 3 (+ (* y (sqrt x)) (* (- (/ 1 (* x 9)) 1) (sqrt x)))))
                
                  (* (* 3.0 (sqrt x)) (- (+ y (/ 1.0 (* x 9.0))) 1.0)))