Numeric.SpecFunctions:stirlingError from math-functions-0.1.5.2

Percentage Accurate: 99.8% → 99.9%
Time: 9.5s
Alternatives: 11
Speedup: 1.0×

Specification

?
\[\begin{array}{l} \\ \left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \end{array} \]
(FPCore (x y z) :precision binary64 (- (+ (- x (* (+ y 0.5) (log y))) y) z))
double code(double x, double y, double z) {
	return ((x - ((y + 0.5) * log(y))) + y) - z;
}
real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = ((x - ((y + 0.5d0) * log(y))) + y) - z
end function
public static double code(double x, double y, double z) {
	return ((x - ((y + 0.5) * Math.log(y))) + y) - z;
}
def code(x, y, z):
	return ((x - ((y + 0.5) * math.log(y))) + y) - z
function code(x, y, z)
	return Float64(Float64(Float64(x - Float64(Float64(y + 0.5) * log(y))) + y) - z)
end
function tmp = code(x, y, z)
	tmp = ((x - ((y + 0.5) * log(y))) + y) - z;
end
code[x_, y_, z_] := N[(N[(N[(x - N[(N[(y + 0.5), $MachinePrecision] * N[Log[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + y), $MachinePrecision] - z), $MachinePrecision]
\begin{array}{l}

\\
\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z
\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 11 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.8% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \end{array} \]
(FPCore (x y z) :precision binary64 (- (+ (- x (* (+ y 0.5) (log y))) y) z))
double code(double x, double y, double z) {
	return ((x - ((y + 0.5) * log(y))) + y) - z;
}
real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = ((x - ((y + 0.5d0) * log(y))) + y) - z
end function
public static double code(double x, double y, double z) {
	return ((x - ((y + 0.5) * Math.log(y))) + y) - z;
}
def code(x, y, z):
	return ((x - ((y + 0.5) * math.log(y))) + y) - z
function code(x, y, z)
	return Float64(Float64(Float64(x - Float64(Float64(y + 0.5) * log(y))) + y) - z)
end
function tmp = code(x, y, z)
	tmp = ((x - ((y + 0.5) * log(y))) + y) - z;
end
code[x_, y_, z_] := N[(N[(N[(x - N[(N[(y + 0.5), $MachinePrecision] * N[Log[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + y), $MachinePrecision] - z), $MachinePrecision]
\begin{array}{l}

\\
\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z
\end{array}

Alternative 1: 99.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \mathsf{fma}\left(-0.5 - y, \log y, \left(y - z\right) + x\right) \end{array} \]
(FPCore (x y z) :precision binary64 (fma (- -0.5 y) (log y) (+ (- y z) x)))
double code(double x, double y, double z) {
	return fma((-0.5 - y), log(y), ((y - z) + x));
}
function code(x, y, z)
	return fma(Float64(-0.5 - y), log(y), Float64(Float64(y - z) + x))
end
code[x_, y_, z_] := N[(N[(-0.5 - y), $MachinePrecision] * N[Log[y], $MachinePrecision] + N[(N[(y - z), $MachinePrecision] + x), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\mathsf{fma}\left(-0.5 - y, \log y, \left(y - z\right) + x\right)
\end{array}
Derivation
  1. Initial program 99.8%

    \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift--.f64N/A

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

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

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

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

      \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right)\right)} + \left(y - z\right) \]
    6. +-commutativeN/A

      \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + x\right)} + \left(y - z\right) \]
    7. associate-+l+N/A

      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + \left(x + \left(y - z\right)\right)} \]
    8. lift-*.f64N/A

      \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right) \cdot \log y}\right)\right) + \left(x + \left(y - z\right)\right) \]
    9. distribute-lft-neg-inN/A

      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right)\right) \cdot \log y} + \left(x + \left(y - z\right)\right) \]
    10. lower-fma.f64N/A

      \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right), \log y, x + \left(y - z\right)\right)} \]
    11. lift-+.f64N/A

      \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right)}\right), \log y, x + \left(y - z\right)\right) \]
    12. +-commutativeN/A

      \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right)}\right), \log y, x + \left(y - z\right)\right) \]
    13. distribute-neg-inN/A

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, x + \left(y - z\right)\right) \]
    14. unsub-negN/A

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
    15. lower--.f64N/A

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
    16. metadata-evalN/A

      \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} - y, \log y, x + \left(y - z\right)\right) \]
    17. lower-+.f64N/A

      \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + \left(y - z\right)}\right) \]
    18. lower--.f6499.9

      \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, x + \color{blue}{\left(y - z\right)}\right) \]
  4. Applied rewrites99.9%

    \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, x + \left(y - z\right)\right)} \]
  5. Final simplification99.9%

    \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \left(y - z\right) + x\right) \]
  6. Add Preprocessing

Alternative 2: 75.1% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left(-x\right) \cdot -1 + \left(-z\right)\\ t_1 := y - \left(\left(0.5 + y\right) \cdot \log y - x\right)\\ \mathbf{if}\;t\_1 \leq -5 \cdot 10^{+139}:\\ \;\;\;\;\left(1 - \log y\right) \cdot y\\ \mathbf{elif}\;t\_1 \leq -10000:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;t\_1 \leq 500:\\ \;\;\;\;\log y \cdot -0.5 - z\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (+ (* (- x) -1.0) (- z))) (t_1 (- y (- (* (+ 0.5 y) (log y)) x))))
   (if (<= t_1 -5e+139)
     (* (- 1.0 (log y)) y)
     (if (<= t_1 -10000.0)
       t_0
       (if (<= t_1 500.0) (- (* (log y) -0.5) z) t_0)))))
double code(double x, double y, double z) {
	double t_0 = (-x * -1.0) + -z;
	double t_1 = y - (((0.5 + y) * log(y)) - x);
	double tmp;
	if (t_1 <= -5e+139) {
		tmp = (1.0 - log(y)) * y;
	} else if (t_1 <= -10000.0) {
		tmp = t_0;
	} else if (t_1 <= 500.0) {
		tmp = (log(y) * -0.5) - z;
	} else {
		tmp = t_0;
	}
	return tmp;
}
real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8) :: t_0
    real(8) :: t_1
    real(8) :: tmp
    t_0 = (-x * (-1.0d0)) + -z
    t_1 = y - (((0.5d0 + y) * log(y)) - x)
    if (t_1 <= (-5d+139)) then
        tmp = (1.0d0 - log(y)) * y
    else if (t_1 <= (-10000.0d0)) then
        tmp = t_0
    else if (t_1 <= 500.0d0) then
        tmp = (log(y) * (-0.5d0)) - z
    else
        tmp = t_0
    end if
    code = tmp
end function
public static double code(double x, double y, double z) {
	double t_0 = (-x * -1.0) + -z;
	double t_1 = y - (((0.5 + y) * Math.log(y)) - x);
	double tmp;
	if (t_1 <= -5e+139) {
		tmp = (1.0 - Math.log(y)) * y;
	} else if (t_1 <= -10000.0) {
		tmp = t_0;
	} else if (t_1 <= 500.0) {
		tmp = (Math.log(y) * -0.5) - z;
	} else {
		tmp = t_0;
	}
	return tmp;
}
def code(x, y, z):
	t_0 = (-x * -1.0) + -z
	t_1 = y - (((0.5 + y) * math.log(y)) - x)
	tmp = 0
	if t_1 <= -5e+139:
		tmp = (1.0 - math.log(y)) * y
	elif t_1 <= -10000.0:
		tmp = t_0
	elif t_1 <= 500.0:
		tmp = (math.log(y) * -0.5) - z
	else:
		tmp = t_0
	return tmp
function code(x, y, z)
	t_0 = Float64(Float64(Float64(-x) * -1.0) + Float64(-z))
	t_1 = Float64(y - Float64(Float64(Float64(0.5 + y) * log(y)) - x))
	tmp = 0.0
	if (t_1 <= -5e+139)
		tmp = Float64(Float64(1.0 - log(y)) * y);
	elseif (t_1 <= -10000.0)
		tmp = t_0;
	elseif (t_1 <= 500.0)
		tmp = Float64(Float64(log(y) * -0.5) - z);
	else
		tmp = t_0;
	end
	return tmp
end
function tmp_2 = code(x, y, z)
	t_0 = (-x * -1.0) + -z;
	t_1 = y - (((0.5 + y) * log(y)) - x);
	tmp = 0.0;
	if (t_1 <= -5e+139)
		tmp = (1.0 - log(y)) * y;
	elseif (t_1 <= -10000.0)
		tmp = t_0;
	elseif (t_1 <= 500.0)
		tmp = (log(y) * -0.5) - z;
	else
		tmp = t_0;
	end
	tmp_2 = tmp;
end
code[x_, y_, z_] := Block[{t$95$0 = N[(N[((-x) * -1.0), $MachinePrecision] + (-z)), $MachinePrecision]}, Block[{t$95$1 = N[(y - N[(N[(N[(0.5 + y), $MachinePrecision] * N[Log[y], $MachinePrecision]), $MachinePrecision] - x), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -5e+139], N[(N[(1.0 - N[Log[y], $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision], If[LessEqual[t$95$1, -10000.0], t$95$0, If[LessEqual[t$95$1, 500.0], N[(N[(N[Log[y], $MachinePrecision] * -0.5), $MachinePrecision] - z), $MachinePrecision], t$95$0]]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \left(-x\right) \cdot -1 + \left(-z\right)\\
t_1 := y - \left(\left(0.5 + y\right) \cdot \log y - x\right)\\
\mathbf{if}\;t\_1 \leq -5 \cdot 10^{+139}:\\
\;\;\;\;\left(1 - \log y\right) \cdot y\\

\mathbf{elif}\;t\_1 \leq -10000:\\
\;\;\;\;t\_0\\

\mathbf{elif}\;t\_1 \leq 500:\\
\;\;\;\;\log y \cdot -0.5 - z\\

\mathbf{else}:\\
\;\;\;\;t\_0\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (+.f64 (-.f64 x (*.f64 (+.f64 y #s(literal 1/2 binary64)) (log.f64 y))) y) < -5.0000000000000003e139

    1. Initial program 99.6%

      \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
    2. Add Preprocessing
    3. Taylor expanded in y around inf

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

        \[\leadsto \color{blue}{\left(1 - -1 \cdot \log \left(\frac{1}{y}\right)\right) \cdot y} \]
      2. mul-1-negN/A

        \[\leadsto \left(1 - \color{blue}{\left(\mathsf{neg}\left(\log \left(\frac{1}{y}\right)\right)\right)}\right) \cdot y \]
      3. log-recN/A

        \[\leadsto \left(1 - \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right)\right) \cdot y \]
      4. remove-double-negN/A

        \[\leadsto \left(1 - \color{blue}{\log y}\right) \cdot y \]
      5. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(1 - \log y\right) \cdot y} \]
      6. lower--.f64N/A

        \[\leadsto \color{blue}{\left(1 - \log y\right)} \cdot y \]
      7. lower-log.f6458.0

        \[\leadsto \left(1 - \color{blue}{\log y}\right) \cdot y \]
    5. Applied rewrites58.0%

      \[\leadsto \color{blue}{\left(1 - \log y\right) \cdot y} \]

    if -5.0000000000000003e139 < (+.f64 (-.f64 x (*.f64 (+.f64 y #s(literal 1/2 binary64)) (log.f64 y))) y) < -1e4 or 500 < (+.f64 (-.f64 x (*.f64 (+.f64 y #s(literal 1/2 binary64)) (log.f64 y))) y)

    1. Initial program 99.9%

      \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
    2. Add Preprocessing
    3. Taylor expanded in x around inf

      \[\leadsto \left(\color{blue}{x \cdot \left(1 + -1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
    4. Step-by-step derivation
      1. distribute-rgt-inN/A

        \[\leadsto \left(\color{blue}{\left(1 \cdot x + \left(-1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right) \cdot x\right)} + y\right) - z \]
      2. metadata-evalN/A

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

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

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

        \[\leadsto \left(\left(-1 \cdot \left(-1 \cdot x\right) + \color{blue}{\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} \cdot \left(-1 \cdot x\right)}\right) + y\right) - z \]
      6. distribute-rgt-inN/A

        \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(-1 + \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
      7. +-commutativeN/A

        \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + -1\right)} + y\right) - z \]
      8. metadata-evalN/A

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

        \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
      10. lower-*.f64N/A

        \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
      11. mul-1-negN/A

        \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right) + y\right) - z \]
      12. lower-neg.f64N/A

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

        \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + \left(\mathsf{neg}\left(1\right)\right)\right)} + y\right) - z \]
      14. *-commutativeN/A

        \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\color{blue}{\left(\frac{1}{2} + y\right) \cdot \log y}}{x} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
      15. associate-/l*N/A

        \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\left(\frac{1}{2} + y\right) \cdot \frac{\log y}{x}} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
      16. *-commutativeN/A

        \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right)} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
      17. metadata-evalN/A

        \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right) + \color{blue}{-1}\right) + y\right) - z \]
      18. lower-fma.f64N/A

        \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{\log y}{x}, \frac{1}{2} + y, -1\right)} + y\right) - z \]
    5. Applied rewrites91.9%

      \[\leadsto \left(\color{blue}{\left(-x\right) \cdot \mathsf{fma}\left(\frac{\log y}{x}, y - -0.5, -1\right)} + y\right) - z \]
    6. Taylor expanded in x around inf

      \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
    7. Step-by-step derivation
      1. Applied rewrites81.2%

        \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
      2. Step-by-step derivation
        1. lift--.f64N/A

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

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

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

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

          \[\leadsto \color{blue}{\left(y - z\right) + \left(-x\right) \cdot -1} \]
        6. lower--.f6481.2

          \[\leadsto \color{blue}{\left(y - z\right)} + \left(-x\right) \cdot -1 \]
      3. Applied rewrites81.2%

        \[\leadsto \color{blue}{\left(y - z\right) + -1 \cdot \left(-x\right)} \]
      4. Taylor expanded in y around 0

        \[\leadsto \color{blue}{-1 \cdot z} + -1 \cdot \left(-x\right) \]
      5. Step-by-step derivation
        1. mul-1-negN/A

          \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z\right)\right)} + -1 \cdot \left(-x\right) \]
        2. lower-neg.f6481.7

          \[\leadsto \color{blue}{\left(-z\right)} + -1 \cdot \left(-x\right) \]
      6. Applied rewrites81.7%

        \[\leadsto \color{blue}{\left(-z\right)} + -1 \cdot \left(-x\right) \]

      if -1e4 < (+.f64 (-.f64 x (*.f64 (+.f64 y #s(literal 1/2 binary64)) (log.f64 y))) y) < 500

      1. Initial program 100.0%

        \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
      2. Add Preprocessing
      3. Taylor expanded in y around 0

        \[\leadsto \color{blue}{x - \left(z + \frac{1}{2} \cdot \log y\right)} \]
      4. Step-by-step derivation
        1. +-commutativeN/A

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

          \[\leadsto \color{blue}{\left(x - \frac{1}{2} \cdot \log y\right) - z} \]
        3. lower--.f64N/A

          \[\leadsto \color{blue}{\left(x - \frac{1}{2} \cdot \log y\right) - z} \]
        4. *-commutativeN/A

          \[\leadsto \left(x - \color{blue}{\log y \cdot \frac{1}{2}}\right) - z \]
        5. cancel-sub-sign-invN/A

          \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\log y\right)\right) \cdot \frac{1}{2}\right)} - z \]
        6. +-commutativeN/A

          \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\log y\right)\right) \cdot \frac{1}{2} + x\right)} - z \]
        7. distribute-lft-neg-inN/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\log y \cdot \frac{1}{2}\right)\right)} + x\right) - z \]
        8. *-commutativeN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\frac{1}{2} \cdot \log y}\right)\right) + x\right) - z \]
        9. distribute-lft-neg-inN/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) \cdot \log y} + x\right) - z \]
        10. metadata-evalN/A

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{-1}{2}, \log y, x\right)} - z \]
        12. lower-log.f6496.7

          \[\leadsto \mathsf{fma}\left(-0.5, \color{blue}{\log y}, x\right) - z \]
      5. Applied rewrites96.7%

        \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5, \log y, x\right) - z} \]
      6. Taylor expanded in x around 0

        \[\leadsto \frac{-1}{2} \cdot \log y - z \]
      7. Step-by-step derivation
        1. Applied rewrites95.0%

          \[\leadsto -0.5 \cdot \log y - z \]
      8. Recombined 3 regimes into one program.
      9. Final simplification76.7%

        \[\leadsto \begin{array}{l} \mathbf{if}\;y - \left(\left(0.5 + y\right) \cdot \log y - x\right) \leq -5 \cdot 10^{+139}:\\ \;\;\;\;\left(1 - \log y\right) \cdot y\\ \mathbf{elif}\;y - \left(\left(0.5 + y\right) \cdot \log y - x\right) \leq -10000:\\ \;\;\;\;\left(-x\right) \cdot -1 + \left(-z\right)\\ \mathbf{elif}\;y - \left(\left(0.5 + y\right) \cdot \log y - x\right) \leq 500:\\ \;\;\;\;\log y \cdot -0.5 - z\\ \mathbf{else}:\\ \;\;\;\;\left(-x\right) \cdot -1 + \left(-z\right)\\ \end{array} \]
      10. Add Preprocessing

      Alternative 3: 92.1% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{fma}\left(-0.5 - y, \log y, x - z\right)\\ \mathbf{if}\;z \leq -1.9 \cdot 10^{+24}:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;z \leq 4.4 \cdot 10^{+33}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x + y\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
      (FPCore (x y z)
       :precision binary64
       (let* ((t_0 (fma (- -0.5 y) (log y) (- x z))))
         (if (<= z -1.9e+24)
           t_0
           (if (<= z 4.4e+33) (fma (- -0.5 y) (log y) (+ x y)) t_0))))
      double code(double x, double y, double z) {
      	double t_0 = fma((-0.5 - y), log(y), (x - z));
      	double tmp;
      	if (z <= -1.9e+24) {
      		tmp = t_0;
      	} else if (z <= 4.4e+33) {
      		tmp = fma((-0.5 - y), log(y), (x + y));
      	} else {
      		tmp = t_0;
      	}
      	return tmp;
      }
      
      function code(x, y, z)
      	t_0 = fma(Float64(-0.5 - y), log(y), Float64(x - z))
      	tmp = 0.0
      	if (z <= -1.9e+24)
      		tmp = t_0;
      	elseif (z <= 4.4e+33)
      		tmp = fma(Float64(-0.5 - y), log(y), Float64(x + y));
      	else
      		tmp = t_0;
      	end
      	return tmp
      end
      
      code[x_, y_, z_] := Block[{t$95$0 = N[(N[(-0.5 - y), $MachinePrecision] * N[Log[y], $MachinePrecision] + N[(x - z), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z, -1.9e+24], t$95$0, If[LessEqual[z, 4.4e+33], N[(N[(-0.5 - y), $MachinePrecision] * N[Log[y], $MachinePrecision] + N[(x + y), $MachinePrecision]), $MachinePrecision], t$95$0]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := \mathsf{fma}\left(-0.5 - y, \log y, x - z\right)\\
      \mathbf{if}\;z \leq -1.9 \cdot 10^{+24}:\\
      \;\;\;\;t\_0\\
      
      \mathbf{elif}\;z \leq 4.4 \cdot 10^{+33}:\\
      \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x + y\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_0\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if z < -1.90000000000000008e24 or 4.39999999999999988e33 < z

        1. Initial program 99.9%

          \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift--.f64N/A

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

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

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

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

            \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right)\right)} + \left(y - z\right) \]
          6. +-commutativeN/A

            \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + x\right)} + \left(y - z\right) \]
          7. associate-+l+N/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + \left(x + \left(y - z\right)\right)} \]
          8. lift-*.f64N/A

            \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right) \cdot \log y}\right)\right) + \left(x + \left(y - z\right)\right) \]
          9. distribute-lft-neg-inN/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right)\right) \cdot \log y} + \left(x + \left(y - z\right)\right) \]
          10. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right), \log y, x + \left(y - z\right)\right)} \]
          11. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right)}\right), \log y, x + \left(y - z\right)\right) \]
          12. +-commutativeN/A

            \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right)}\right), \log y, x + \left(y - z\right)\right) \]
          13. distribute-neg-inN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, x + \left(y - z\right)\right) \]
          14. unsub-negN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
          15. lower--.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
          16. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} - y, \log y, x + \left(y - z\right)\right) \]
          17. lower-+.f64N/A

            \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + \left(y - z\right)}\right) \]
          18. lower--.f6499.9

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, x + \color{blue}{\left(y - z\right)}\right) \]
        4. Applied rewrites99.9%

          \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, x + \left(y - z\right)\right)} \]
        5. Taylor expanded in y around 0

          \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x - z}\right) \]
        6. Step-by-step derivation
          1. lower--.f6486.9

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x - z}\right) \]
        7. Applied rewrites86.9%

          \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x - z}\right) \]

        if -1.90000000000000008e24 < z < 4.39999999999999988e33

        1. Initial program 99.8%

          \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift--.f64N/A

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

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

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

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

            \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right)\right)} + \left(y - z\right) \]
          6. +-commutativeN/A

            \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + x\right)} + \left(y - z\right) \]
          7. associate-+l+N/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + \left(x + \left(y - z\right)\right)} \]
          8. lift-*.f64N/A

            \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right) \cdot \log y}\right)\right) + \left(x + \left(y - z\right)\right) \]
          9. distribute-lft-neg-inN/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right)\right) \cdot \log y} + \left(x + \left(y - z\right)\right) \]
          10. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right), \log y, x + \left(y - z\right)\right)} \]
          11. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right)}\right), \log y, x + \left(y - z\right)\right) \]
          12. +-commutativeN/A

            \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right)}\right), \log y, x + \left(y - z\right)\right) \]
          13. distribute-neg-inN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, x + \left(y - z\right)\right) \]
          14. unsub-negN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
          15. lower--.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
          16. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} - y, \log y, x + \left(y - z\right)\right) \]
          17. lower-+.f64N/A

            \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + \left(y - z\right)}\right) \]
          18. lower--.f6499.9

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, x + \color{blue}{\left(y - z\right)}\right) \]
        4. Applied rewrites99.9%

          \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, x + \left(y - z\right)\right)} \]
        5. Taylor expanded in z around 0

          \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + y}\right) \]
        6. Step-by-step derivation
          1. lower-+.f6499.5

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x + y}\right) \]
        7. Applied rewrites99.5%

          \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x + y}\right) \]
      3. Recombined 2 regimes into one program.
      4. Add Preprocessing

      Alternative 4: 89.0% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z \leq -2.3 \cdot 10^{+24}:\\ \;\;\;\;\left(-x\right) \cdot -1 + \left(-z\right)\\ \mathbf{elif}\;z \leq 3.1 \cdot 10^{+33}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x + y\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, y\right) - z\\ \end{array} \end{array} \]
      (FPCore (x y z)
       :precision binary64
       (if (<= z -2.3e+24)
         (+ (* (- x) -1.0) (- z))
         (if (<= z 3.1e+33)
           (fma (- -0.5 y) (log y) (+ x y))
           (- (fma (- -0.5 y) (log y) y) z))))
      double code(double x, double y, double z) {
      	double tmp;
      	if (z <= -2.3e+24) {
      		tmp = (-x * -1.0) + -z;
      	} else if (z <= 3.1e+33) {
      		tmp = fma((-0.5 - y), log(y), (x + y));
      	} else {
      		tmp = fma((-0.5 - y), log(y), y) - z;
      	}
      	return tmp;
      }
      
      function code(x, y, z)
      	tmp = 0.0
      	if (z <= -2.3e+24)
      		tmp = Float64(Float64(Float64(-x) * -1.0) + Float64(-z));
      	elseif (z <= 3.1e+33)
      		tmp = fma(Float64(-0.5 - y), log(y), Float64(x + y));
      	else
      		tmp = Float64(fma(Float64(-0.5 - y), log(y), y) - z);
      	end
      	return tmp
      end
      
      code[x_, y_, z_] := If[LessEqual[z, -2.3e+24], N[(N[((-x) * -1.0), $MachinePrecision] + (-z)), $MachinePrecision], If[LessEqual[z, 3.1e+33], N[(N[(-0.5 - y), $MachinePrecision] * N[Log[y], $MachinePrecision] + N[(x + y), $MachinePrecision]), $MachinePrecision], N[(N[(N[(-0.5 - y), $MachinePrecision] * N[Log[y], $MachinePrecision] + y), $MachinePrecision] - z), $MachinePrecision]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;z \leq -2.3 \cdot 10^{+24}:\\
      \;\;\;\;\left(-x\right) \cdot -1 + \left(-z\right)\\
      
      \mathbf{elif}\;z \leq 3.1 \cdot 10^{+33}:\\
      \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x + y\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, y\right) - z\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if z < -2.2999999999999999e24

        1. Initial program 99.9%

          \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
        2. Add Preprocessing
        3. Taylor expanded in x around inf

          \[\leadsto \left(\color{blue}{x \cdot \left(1 + -1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
        4. Step-by-step derivation
          1. distribute-rgt-inN/A

            \[\leadsto \left(\color{blue}{\left(1 \cdot x + \left(-1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right) \cdot x\right)} + y\right) - z \]
          2. metadata-evalN/A

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

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

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

            \[\leadsto \left(\left(-1 \cdot \left(-1 \cdot x\right) + \color{blue}{\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} \cdot \left(-1 \cdot x\right)}\right) + y\right) - z \]
          6. distribute-rgt-inN/A

            \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(-1 + \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
          7. +-commutativeN/A

            \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + -1\right)} + y\right) - z \]
          8. metadata-evalN/A

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

            \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
          10. lower-*.f64N/A

            \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
          11. mul-1-negN/A

            \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right) + y\right) - z \]
          12. lower-neg.f64N/A

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

            \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + \left(\mathsf{neg}\left(1\right)\right)\right)} + y\right) - z \]
          14. *-commutativeN/A

            \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\color{blue}{\left(\frac{1}{2} + y\right) \cdot \log y}}{x} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
          15. associate-/l*N/A

            \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\left(\frac{1}{2} + y\right) \cdot \frac{\log y}{x}} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
          16. *-commutativeN/A

            \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right)} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
          17. metadata-evalN/A

            \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right) + \color{blue}{-1}\right) + y\right) - z \]
          18. lower-fma.f64N/A

            \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{\log y}{x}, \frac{1}{2} + y, -1\right)} + y\right) - z \]
        5. Applied rewrites90.9%

          \[\leadsto \left(\color{blue}{\left(-x\right) \cdot \mathsf{fma}\left(\frac{\log y}{x}, y - -0.5, -1\right)} + y\right) - z \]
        6. Taylor expanded in x around inf

          \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
        7. Step-by-step derivation
          1. Applied rewrites84.6%

            \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
          2. Step-by-step derivation
            1. lift--.f64N/A

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

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

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

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

              \[\leadsto \color{blue}{\left(y - z\right) + \left(-x\right) \cdot -1} \]
            6. lower--.f6484.6

              \[\leadsto \color{blue}{\left(y - z\right)} + \left(-x\right) \cdot -1 \]
          3. Applied rewrites84.6%

            \[\leadsto \color{blue}{\left(y - z\right) + -1 \cdot \left(-x\right)} \]
          4. Taylor expanded in y around 0

            \[\leadsto \color{blue}{-1 \cdot z} + -1 \cdot \left(-x\right) \]
          5. Step-by-step derivation
            1. mul-1-negN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z\right)\right)} + -1 \cdot \left(-x\right) \]
            2. lower-neg.f6484.8

              \[\leadsto \color{blue}{\left(-z\right)} + -1 \cdot \left(-x\right) \]
          6. Applied rewrites84.8%

            \[\leadsto \color{blue}{\left(-z\right)} + -1 \cdot \left(-x\right) \]

          if -2.2999999999999999e24 < z < 3.1e33

          1. Initial program 99.8%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

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

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

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

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

              \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right)\right)} + \left(y - z\right) \]
            6. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + x\right)} + \left(y - z\right) \]
            7. associate-+l+N/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + \left(x + \left(y - z\right)\right)} \]
            8. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right) \cdot \log y}\right)\right) + \left(x + \left(y - z\right)\right) \]
            9. distribute-lft-neg-inN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right)\right) \cdot \log y} + \left(x + \left(y - z\right)\right) \]
            10. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right), \log y, x + \left(y - z\right)\right)} \]
            11. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right)}\right), \log y, x + \left(y - z\right)\right) \]
            12. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right)}\right), \log y, x + \left(y - z\right)\right) \]
            13. distribute-neg-inN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, x + \left(y - z\right)\right) \]
            14. unsub-negN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
            15. lower--.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
            16. metadata-evalN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} - y, \log y, x + \left(y - z\right)\right) \]
            17. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + \left(y - z\right)}\right) \]
            18. lower--.f6499.9

              \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, x + \color{blue}{\left(y - z\right)}\right) \]
          4. Applied rewrites99.9%

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, x + \left(y - z\right)\right)} \]
          5. Taylor expanded in z around 0

            \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + y}\right) \]
          6. Step-by-step derivation
            1. lower-+.f6499.5

              \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x + y}\right) \]
          7. Applied rewrites99.5%

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x + y}\right) \]

          if 3.1e33 < z

          1. Initial program 99.8%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Taylor expanded in y around inf

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

              \[\leadsto \left(\left(x - -1 \cdot \color{blue}{\left(\log \left(\frac{1}{y}\right) \cdot y\right)}\right) + y\right) - z \]
            2. associate-*r*N/A

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

              \[\leadsto \left(\left(x - \color{blue}{\left(\mathsf{neg}\left(\log \left(\frac{1}{y}\right)\right)\right)} \cdot y\right) + y\right) - z \]
            4. log-recN/A

              \[\leadsto \left(\left(x - \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right) \cdot y\right) + y\right) - z \]
            5. remove-double-negN/A

              \[\leadsto \left(\left(x - \color{blue}{\log y} \cdot y\right) + y\right) - z \]
            6. lower-*.f64N/A

              \[\leadsto \left(\left(x - \color{blue}{\log y \cdot y}\right) + y\right) - z \]
            7. lower-log.f6499.8

              \[\leadsto \left(\left(x - \color{blue}{\log y} \cdot y\right) + y\right) - z \]
          5. Applied rewrites99.8%

            \[\leadsto \left(\left(x - \color{blue}{\log y \cdot y}\right) + y\right) - z \]
          6. Taylor expanded in x around 0

            \[\leadsto \color{blue}{\left(y - \log y \cdot \left(\frac{1}{2} + y\right)\right)} - z \]
          7. Step-by-step derivation
            1. sub-negN/A

              \[\leadsto \color{blue}{\left(y + \left(\mathsf{neg}\left(\log y \cdot \left(\frac{1}{2} + y\right)\right)\right)\right)} - z \]
            2. +-commutativeN/A

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

              \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right) \cdot \log y}\right)\right) + y\right) - z \]
            4. distribute-lft-neg-inN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\left(\frac{1}{2} + y\right)\right)\right) \cdot \log y} + y\right) - z \]
            5. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(\frac{1}{2} + y\right)\right), \log y, y\right)} - z \]
            6. distribute-neg-inN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, y\right) - z \]
            7. metadata-evalN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} + \left(\mathsf{neg}\left(y\right)\right), \log y, y\right) - z \]
            8. unsub-negN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2} - y}, \log y, y\right) - z \]
            9. lower--.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2} - y}, \log y, y\right) - z \]
            10. lower-log.f6483.4

              \[\leadsto \mathsf{fma}\left(-0.5 - y, \color{blue}{\log y}, y\right) - z \]
          8. Applied rewrites83.4%

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, y\right)} - z \]
        8. Recombined 3 regimes into one program.
        9. Final simplification93.1%

          \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -2.3 \cdot 10^{+24}:\\ \;\;\;\;\left(-x\right) \cdot -1 + \left(-z\right)\\ \mathbf{elif}\;z \leq 3.1 \cdot 10^{+33}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x + y\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, y\right) - z\\ \end{array} \]
        10. Add Preprocessing

        Alternative 5: 99.3% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq 0.43:\\ \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x - z\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \log y \cdot y\right) - \left(z - y\right)\\ \end{array} \end{array} \]
        (FPCore (x y z)
         :precision binary64
         (if (<= y 0.43)
           (fma (- -0.5 y) (log y) (- x z))
           (- (- x (* (log y) y)) (- z y))))
        double code(double x, double y, double z) {
        	double tmp;
        	if (y <= 0.43) {
        		tmp = fma((-0.5 - y), log(y), (x - z));
        	} else {
        		tmp = (x - (log(y) * y)) - (z - y);
        	}
        	return tmp;
        }
        
        function code(x, y, z)
        	tmp = 0.0
        	if (y <= 0.43)
        		tmp = fma(Float64(-0.5 - y), log(y), Float64(x - z));
        	else
        		tmp = Float64(Float64(x - Float64(log(y) * y)) - Float64(z - y));
        	end
        	return tmp
        end
        
        code[x_, y_, z_] := If[LessEqual[y, 0.43], N[(N[(-0.5 - y), $MachinePrecision] * N[Log[y], $MachinePrecision] + N[(x - z), $MachinePrecision]), $MachinePrecision], N[(N[(x - N[(N[Log[y], $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision] - N[(z - y), $MachinePrecision]), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;y \leq 0.43:\\
        \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x - z\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(x - \log y \cdot y\right) - \left(z - y\right)\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if y < 0.429999999999999993

          1. Initial program 100.0%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

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

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

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

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

              \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right)\right)} + \left(y - z\right) \]
            6. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + x\right)} + \left(y - z\right) \]
            7. associate-+l+N/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + \left(x + \left(y - z\right)\right)} \]
            8. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right) \cdot \log y}\right)\right) + \left(x + \left(y - z\right)\right) \]
            9. distribute-lft-neg-inN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right)\right) \cdot \log y} + \left(x + \left(y - z\right)\right) \]
            10. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right), \log y, x + \left(y - z\right)\right)} \]
            11. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right)}\right), \log y, x + \left(y - z\right)\right) \]
            12. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right)}\right), \log y, x + \left(y - z\right)\right) \]
            13. distribute-neg-inN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, x + \left(y - z\right)\right) \]
            14. unsub-negN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
            15. lower--.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
            16. metadata-evalN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} - y, \log y, x + \left(y - z\right)\right) \]
            17. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + \left(y - z\right)}\right) \]
            18. lower--.f64100.0

              \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, x + \color{blue}{\left(y - z\right)}\right) \]
          4. Applied rewrites100.0%

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, x + \left(y - z\right)\right)} \]
          5. Taylor expanded in y around 0

            \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x - z}\right) \]
          6. Step-by-step derivation
            1. lower--.f6498.6

              \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x - z}\right) \]
          7. Applied rewrites98.6%

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x - z}\right) \]

          if 0.429999999999999993 < y

          1. Initial program 99.6%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Taylor expanded in y around inf

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

              \[\leadsto \left(\left(x - -1 \cdot \color{blue}{\left(\log \left(\frac{1}{y}\right) \cdot y\right)}\right) + y\right) - z \]
            2. associate-*r*N/A

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

              \[\leadsto \left(\left(x - \color{blue}{\left(\mathsf{neg}\left(\log \left(\frac{1}{y}\right)\right)\right)} \cdot y\right) + y\right) - z \]
            4. log-recN/A

              \[\leadsto \left(\left(x - \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right) \cdot y\right) + y\right) - z \]
            5. remove-double-negN/A

              \[\leadsto \left(\left(x - \color{blue}{\log y} \cdot y\right) + y\right) - z \]
            6. lower-*.f64N/A

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

              \[\leadsto \left(\left(x - \color{blue}{\log y} \cdot y\right) + y\right) - z \]
          5. Applied rewrites99.4%

            \[\leadsto \left(\left(x - \color{blue}{\log y \cdot y}\right) + y\right) - z \]
          6. Step-by-step derivation
            1. lift--.f64N/A

              \[\leadsto \color{blue}{\left(\left(x - \log y \cdot y\right) + y\right) - z} \]
            2. lift-+.f64N/A

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

              \[\leadsto \color{blue}{\left(x - \log y \cdot y\right) + \left(y - z\right)} \]
            4. lift--.f64N/A

              \[\leadsto \left(x - \log y \cdot y\right) + \color{blue}{\left(y - z\right)} \]
            5. +-commutativeN/A

              \[\leadsto \color{blue}{\left(y - z\right) + \left(x - \log y \cdot y\right)} \]
            6. lower-+.f6499.4

              \[\leadsto \color{blue}{\left(y - z\right) + \left(x - \log y \cdot y\right)} \]
          7. Applied rewrites99.4%

            \[\leadsto \color{blue}{\left(y - z\right) + \left(x - \log y \cdot y\right)} \]
        3. Recombined 2 regimes into one program.
        4. Final simplification99.0%

          \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq 0.43:\\ \;\;\;\;\mathsf{fma}\left(-0.5 - y, \log y, x - z\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \log y \cdot y\right) - \left(z - y\right)\\ \end{array} \]
        5. Add Preprocessing

        Alternative 6: 90.0% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq 9.2 \cdot 10^{+39}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, \log y, x\right) - z\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-y, \log y, x + y\right)\\ \end{array} \end{array} \]
        (FPCore (x y z)
         :precision binary64
         (if (<= y 9.2e+39) (- (fma -0.5 (log y) x) z) (fma (- y) (log y) (+ x y))))
        double code(double x, double y, double z) {
        	double tmp;
        	if (y <= 9.2e+39) {
        		tmp = fma(-0.5, log(y), x) - z;
        	} else {
        		tmp = fma(-y, log(y), (x + y));
        	}
        	return tmp;
        }
        
        function code(x, y, z)
        	tmp = 0.0
        	if (y <= 9.2e+39)
        		tmp = Float64(fma(-0.5, log(y), x) - z);
        	else
        		tmp = fma(Float64(-y), log(y), Float64(x + y));
        	end
        	return tmp
        end
        
        code[x_, y_, z_] := If[LessEqual[y, 9.2e+39], N[(N[(-0.5 * N[Log[y], $MachinePrecision] + x), $MachinePrecision] - z), $MachinePrecision], N[((-y) * N[Log[y], $MachinePrecision] + N[(x + y), $MachinePrecision]), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;y \leq 9.2 \cdot 10^{+39}:\\
        \;\;\;\;\mathsf{fma}\left(-0.5, \log y, x\right) - z\\
        
        \mathbf{else}:\\
        \;\;\;\;\mathsf{fma}\left(-y, \log y, x + y\right)\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if y < 9.20000000000000047e39

          1. Initial program 100.0%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Taylor expanded in y around 0

            \[\leadsto \color{blue}{x - \left(z + \frac{1}{2} \cdot \log y\right)} \]
          4. Step-by-step derivation
            1. +-commutativeN/A

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

              \[\leadsto \color{blue}{\left(x - \frac{1}{2} \cdot \log y\right) - z} \]
            3. lower--.f64N/A

              \[\leadsto \color{blue}{\left(x - \frac{1}{2} \cdot \log y\right) - z} \]
            4. *-commutativeN/A

              \[\leadsto \left(x - \color{blue}{\log y \cdot \frac{1}{2}}\right) - z \]
            5. cancel-sub-sign-invN/A

              \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\log y\right)\right) \cdot \frac{1}{2}\right)} - z \]
            6. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\log y\right)\right) \cdot \frac{1}{2} + x\right)} - z \]
            7. distribute-lft-neg-inN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\log y \cdot \frac{1}{2}\right)\right)} + x\right) - z \]
            8. *-commutativeN/A

              \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\frac{1}{2} \cdot \log y}\right)\right) + x\right) - z \]
            9. distribute-lft-neg-inN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) \cdot \log y} + x\right) - z \]
            10. metadata-evalN/A

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

              \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{-1}{2}, \log y, x\right)} - z \]
            12. lower-log.f6496.3

              \[\leadsto \mathsf{fma}\left(-0.5, \color{blue}{\log y}, x\right) - z \]
          5. Applied rewrites96.3%

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5, \log y, x\right) - z} \]

          if 9.20000000000000047e39 < y

          1. Initial program 99.6%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

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

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

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

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

              \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right)\right)} + \left(y - z\right) \]
            6. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + x\right)} + \left(y - z\right) \]
            7. associate-+l+N/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + \left(x + \left(y - z\right)\right)} \]
            8. lift-*.f64N/A

              \[\leadsto \left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right) \cdot \log y}\right)\right) + \left(x + \left(y - z\right)\right) \]
            9. distribute-lft-neg-inN/A

              \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right)\right) \cdot \log y} + \left(x + \left(y - z\right)\right) \]
            10. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right), \log y, x + \left(y - z\right)\right)} \]
            11. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right)}\right), \log y, x + \left(y - z\right)\right) \]
            12. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right)}\right), \log y, x + \left(y - z\right)\right) \]
            13. distribute-neg-inN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, x + \left(y - z\right)\right) \]
            14. unsub-negN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
            15. lower--.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + \left(y - z\right)\right) \]
            16. metadata-evalN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} - y, \log y, x + \left(y - z\right)\right) \]
            17. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + \left(y - z\right)}\right) \]
            18. lower--.f6499.8

              \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, x + \color{blue}{\left(y - z\right)}\right) \]
          4. Applied rewrites99.8%

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, x + \left(y - z\right)\right)} \]
          5. Taylor expanded in z around 0

            \[\leadsto \mathsf{fma}\left(\frac{-1}{2} - y, \log y, \color{blue}{x + y}\right) \]
          6. Step-by-step derivation
            1. lower-+.f6482.4

              \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x + y}\right) \]
          7. Applied rewrites82.4%

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x + y}\right) \]
          8. Taylor expanded in y around inf

            \[\leadsto \mathsf{fma}\left(\color{blue}{-1 \cdot y}, \log y, x + y\right) \]
          9. Step-by-step derivation
            1. mul-1-negN/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{neg}\left(y\right)}, \log y, x + y\right) \]
            2. lower-neg.f6482.4

              \[\leadsto \mathsf{fma}\left(\color{blue}{-y}, \log y, x + y\right) \]
          10. Applied rewrites82.4%

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

        Alternative 7: 84.3% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq 3.6 \cdot 10^{+136}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, \log y, x\right) - z\\ \mathbf{else}:\\ \;\;\;\;\left(1 - \log y\right) \cdot y\\ \end{array} \end{array} \]
        (FPCore (x y z)
         :precision binary64
         (if (<= y 3.6e+136) (- (fma -0.5 (log y) x) z) (* (- 1.0 (log y)) y)))
        double code(double x, double y, double z) {
        	double tmp;
        	if (y <= 3.6e+136) {
        		tmp = fma(-0.5, log(y), x) - z;
        	} else {
        		tmp = (1.0 - log(y)) * y;
        	}
        	return tmp;
        }
        
        function code(x, y, z)
        	tmp = 0.0
        	if (y <= 3.6e+136)
        		tmp = Float64(fma(-0.5, log(y), x) - z);
        	else
        		tmp = Float64(Float64(1.0 - log(y)) * y);
        	end
        	return tmp
        end
        
        code[x_, y_, z_] := If[LessEqual[y, 3.6e+136], N[(N[(-0.5 * N[Log[y], $MachinePrecision] + x), $MachinePrecision] - z), $MachinePrecision], N[(N[(1.0 - N[Log[y], $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;y \leq 3.6 \cdot 10^{+136}:\\
        \;\;\;\;\mathsf{fma}\left(-0.5, \log y, x\right) - z\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(1 - \log y\right) \cdot y\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if y < 3.60000000000000006e136

          1. Initial program 99.9%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Taylor expanded in y around 0

            \[\leadsto \color{blue}{x - \left(z + \frac{1}{2} \cdot \log y\right)} \]
          4. Step-by-step derivation
            1. +-commutativeN/A

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

              \[\leadsto \color{blue}{\left(x - \frac{1}{2} \cdot \log y\right) - z} \]
            3. lower--.f64N/A

              \[\leadsto \color{blue}{\left(x - \frac{1}{2} \cdot \log y\right) - z} \]
            4. *-commutativeN/A

              \[\leadsto \left(x - \color{blue}{\log y \cdot \frac{1}{2}}\right) - z \]
            5. cancel-sub-sign-invN/A

              \[\leadsto \color{blue}{\left(x + \left(\mathsf{neg}\left(\log y\right)\right) \cdot \frac{1}{2}\right)} - z \]
            6. +-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\log y\right)\right) \cdot \frac{1}{2} + x\right)} - z \]
            7. distribute-lft-neg-inN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\log y \cdot \frac{1}{2}\right)\right)} + x\right) - z \]
            8. *-commutativeN/A

              \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\frac{1}{2} \cdot \log y}\right)\right) + x\right) - z \]
            9. distribute-lft-neg-inN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) \cdot \log y} + x\right) - z \]
            10. metadata-evalN/A

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

              \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{-1}{2}, \log y, x\right)} - z \]
            12. lower-log.f6489.7

              \[\leadsto \mathsf{fma}\left(-0.5, \color{blue}{\log y}, x\right) - z \]
          5. Applied rewrites89.7%

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5, \log y, x\right) - z} \]

          if 3.60000000000000006e136 < y

          1. Initial program 99.5%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Taylor expanded in y around inf

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

              \[\leadsto \color{blue}{\left(1 - -1 \cdot \log \left(\frac{1}{y}\right)\right) \cdot y} \]
            2. mul-1-negN/A

              \[\leadsto \left(1 - \color{blue}{\left(\mathsf{neg}\left(\log \left(\frac{1}{y}\right)\right)\right)}\right) \cdot y \]
            3. log-recN/A

              \[\leadsto \left(1 - \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right)\right) \cdot y \]
            4. remove-double-negN/A

              \[\leadsto \left(1 - \color{blue}{\log y}\right) \cdot y \]
            5. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(1 - \log y\right) \cdot y} \]
            6. lower--.f64N/A

              \[\leadsto \color{blue}{\left(1 - \log y\right)} \cdot y \]
            7. lower-log.f6473.2

              \[\leadsto \left(1 - \color{blue}{\log y}\right) \cdot y \]
          5. Applied rewrites73.2%

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

        Alternative 8: 99.9% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ \mathsf{fma}\left(-0.5 - y, \log y, x + y\right) - z \end{array} \]
        (FPCore (x y z) :precision binary64 (- (fma (- -0.5 y) (log y) (+ x y)) z))
        double code(double x, double y, double z) {
        	return fma((-0.5 - y), log(y), (x + y)) - z;
        }
        
        function code(x, y, z)
        	return Float64(fma(Float64(-0.5 - y), log(y), Float64(x + y)) - z)
        end
        
        code[x_, y_, z_] := N[(N[(N[(-0.5 - y), $MachinePrecision] * N[Log[y], $MachinePrecision] + N[(x + y), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]
        
        \begin{array}{l}
        
        \\
        \mathsf{fma}\left(-0.5 - y, \log y, x + y\right) - z
        \end{array}
        
        Derivation
        1. Initial program 99.8%

          \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-+.f64N/A

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

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

            \[\leadsto \left(\color{blue}{\left(x + \left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right)\right)} + y\right) - z \]
          4. +-commutativeN/A

            \[\leadsto \left(\color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + x\right)} + y\right) - z \]
          5. associate-+l+N/A

            \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right) \cdot \log y\right)\right) + \left(x + y\right)\right)} - z \]
          6. lift-*.f64N/A

            \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right) \cdot \log y}\right)\right) + \left(x + y\right)\right) - z \]
          7. distribute-lft-neg-inN/A

            \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right)\right) \cdot \log y} + \left(x + y\right)\right) - z \]
          8. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\left(y + \frac{1}{2}\right)\right), \log y, x + y\right)} - z \]
          9. lift-+.f64N/A

            \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(y + \frac{1}{2}\right)}\right), \log y, x + y\right) - z \]
          10. +-commutativeN/A

            \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\left(\frac{1}{2} + y\right)}\right), \log y, x + y\right) - z \]
          11. distribute-neg-inN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}, \log y, x + y\right) - z \]
          12. unsub-negN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + y\right) - z \]
          13. lower--.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - y}, \log y, x + y\right) - z \]
          14. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{2}} - y, \log y, x + y\right) - z \]
          15. lower-+.f6499.9

            \[\leadsto \mathsf{fma}\left(-0.5 - y, \log y, \color{blue}{x + y}\right) - z \]
        4. Applied rewrites99.9%

          \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 - y, \log y, x + y\right) - z} \]
        5. Add Preprocessing

        Alternative 9: 71.4% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq 3.5 \cdot 10^{+136}:\\ \;\;\;\;\left(-x\right) \cdot -1 - \left(z - y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(1 - \log y\right) \cdot y\\ \end{array} \end{array} \]
        (FPCore (x y z)
         :precision binary64
         (if (<= y 3.5e+136) (- (* (- x) -1.0) (- z y)) (* (- 1.0 (log y)) y)))
        double code(double x, double y, double z) {
        	double tmp;
        	if (y <= 3.5e+136) {
        		tmp = (-x * -1.0) - (z - y);
        	} else {
        		tmp = (1.0 - log(y)) * y;
        	}
        	return tmp;
        }
        
        real(8) function code(x, y, z)
            real(8), intent (in) :: x
            real(8), intent (in) :: y
            real(8), intent (in) :: z
            real(8) :: tmp
            if (y <= 3.5d+136) then
                tmp = (-x * (-1.0d0)) - (z - y)
            else
                tmp = (1.0d0 - log(y)) * y
            end if
            code = tmp
        end function
        
        public static double code(double x, double y, double z) {
        	double tmp;
        	if (y <= 3.5e+136) {
        		tmp = (-x * -1.0) - (z - y);
        	} else {
        		tmp = (1.0 - Math.log(y)) * y;
        	}
        	return tmp;
        }
        
        def code(x, y, z):
        	tmp = 0
        	if y <= 3.5e+136:
        		tmp = (-x * -1.0) - (z - y)
        	else:
        		tmp = (1.0 - math.log(y)) * y
        	return tmp
        
        function code(x, y, z)
        	tmp = 0.0
        	if (y <= 3.5e+136)
        		tmp = Float64(Float64(Float64(-x) * -1.0) - Float64(z - y));
        	else
        		tmp = Float64(Float64(1.0 - log(y)) * y);
        	end
        	return tmp
        end
        
        function tmp_2 = code(x, y, z)
        	tmp = 0.0;
        	if (y <= 3.5e+136)
        		tmp = (-x * -1.0) - (z - y);
        	else
        		tmp = (1.0 - log(y)) * y;
        	end
        	tmp_2 = tmp;
        end
        
        code[x_, y_, z_] := If[LessEqual[y, 3.5e+136], N[(N[((-x) * -1.0), $MachinePrecision] - N[(z - y), $MachinePrecision]), $MachinePrecision], N[(N[(1.0 - N[Log[y], $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;y \leq 3.5 \cdot 10^{+136}:\\
        \;\;\;\;\left(-x\right) \cdot -1 - \left(z - y\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(1 - \log y\right) \cdot y\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if y < 3.50000000000000001e136

          1. Initial program 99.9%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Taylor expanded in x around inf

            \[\leadsto \left(\color{blue}{x \cdot \left(1 + -1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
          4. Step-by-step derivation
            1. distribute-rgt-inN/A

              \[\leadsto \left(\color{blue}{\left(1 \cdot x + \left(-1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right) \cdot x\right)} + y\right) - z \]
            2. metadata-evalN/A

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

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

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

              \[\leadsto \left(\left(-1 \cdot \left(-1 \cdot x\right) + \color{blue}{\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} \cdot \left(-1 \cdot x\right)}\right) + y\right) - z \]
            6. distribute-rgt-inN/A

              \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(-1 + \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
            7. +-commutativeN/A

              \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + -1\right)} + y\right) - z \]
            8. metadata-evalN/A

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

              \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
            10. lower-*.f64N/A

              \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
            11. mul-1-negN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right) + y\right) - z \]
            12. lower-neg.f64N/A

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

              \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + \left(\mathsf{neg}\left(1\right)\right)\right)} + y\right) - z \]
            14. *-commutativeN/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\color{blue}{\left(\frac{1}{2} + y\right) \cdot \log y}}{x} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
            15. associate-/l*N/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\left(\frac{1}{2} + y\right) \cdot \frac{\log y}{x}} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
            16. *-commutativeN/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right)} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
            17. metadata-evalN/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right) + \color{blue}{-1}\right) + y\right) - z \]
            18. lower-fma.f64N/A

              \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{\log y}{x}, \frac{1}{2} + y, -1\right)} + y\right) - z \]
          5. Applied rewrites95.3%

            \[\leadsto \left(\color{blue}{\left(-x\right) \cdot \mathsf{fma}\left(\frac{\log y}{x}, y - -0.5, -1\right)} + y\right) - z \]
          6. Taylor expanded in x around inf

            \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
          7. Step-by-step derivation
            1. Applied rewrites73.3%

              \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
            2. Step-by-step derivation
              1. lift--.f64N/A

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

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

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

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

                \[\leadsto \color{blue}{\left(y - z\right) + \left(-x\right) \cdot -1} \]
              6. lower--.f6473.3

                \[\leadsto \color{blue}{\left(y - z\right)} + \left(-x\right) \cdot -1 \]
            3. Applied rewrites73.3%

              \[\leadsto \color{blue}{\left(y - z\right) + -1 \cdot \left(-x\right)} \]

            if 3.50000000000000001e136 < y

            1. Initial program 99.5%

              \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
            2. Add Preprocessing
            3. Taylor expanded in y around inf

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

                \[\leadsto \color{blue}{\left(1 - -1 \cdot \log \left(\frac{1}{y}\right)\right) \cdot y} \]
              2. mul-1-negN/A

                \[\leadsto \left(1 - \color{blue}{\left(\mathsf{neg}\left(\log \left(\frac{1}{y}\right)\right)\right)}\right) \cdot y \]
              3. log-recN/A

                \[\leadsto \left(1 - \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right)\right) \cdot y \]
              4. remove-double-negN/A

                \[\leadsto \left(1 - \color{blue}{\log y}\right) \cdot y \]
              5. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(1 - \log y\right) \cdot y} \]
              6. lower--.f64N/A

                \[\leadsto \color{blue}{\left(1 - \log y\right)} \cdot y \]
              7. lower-log.f6473.2

                \[\leadsto \left(1 - \color{blue}{\log y}\right) \cdot y \]
            5. Applied rewrites73.2%

              \[\leadsto \color{blue}{\left(1 - \log y\right) \cdot y} \]
          8. Recombined 2 regimes into one program.
          9. Final simplification73.3%

            \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq 3.5 \cdot 10^{+136}:\\ \;\;\;\;\left(-x\right) \cdot -1 - \left(z - y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(1 - \log y\right) \cdot y\\ \end{array} \]
          10. Add Preprocessing

          Alternative 10: 57.9% accurate, 9.1× speedup?

          \[\begin{array}{l} \\ \left(-x\right) \cdot -1 + \left(-z\right) \end{array} \]
          (FPCore (x y z) :precision binary64 (+ (* (- x) -1.0) (- z)))
          double code(double x, double y, double z) {
          	return (-x * -1.0) + -z;
          }
          
          real(8) function code(x, y, z)
              real(8), intent (in) :: x
              real(8), intent (in) :: y
              real(8), intent (in) :: z
              code = (-x * (-1.0d0)) + -z
          end function
          
          public static double code(double x, double y, double z) {
          	return (-x * -1.0) + -z;
          }
          
          def code(x, y, z):
          	return (-x * -1.0) + -z
          
          function code(x, y, z)
          	return Float64(Float64(Float64(-x) * -1.0) + Float64(-z))
          end
          
          function tmp = code(x, y, z)
          	tmp = (-x * -1.0) + -z;
          end
          
          code[x_, y_, z_] := N[(N[((-x) * -1.0), $MachinePrecision] + (-z)), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          \left(-x\right) \cdot -1 + \left(-z\right)
          \end{array}
          
          Derivation
          1. Initial program 99.8%

            \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
          2. Add Preprocessing
          3. Taylor expanded in x around inf

            \[\leadsto \left(\color{blue}{x \cdot \left(1 + -1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
          4. Step-by-step derivation
            1. distribute-rgt-inN/A

              \[\leadsto \left(\color{blue}{\left(1 \cdot x + \left(-1 \cdot \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right) \cdot x\right)} + y\right) - z \]
            2. metadata-evalN/A

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

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

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

              \[\leadsto \left(\left(-1 \cdot \left(-1 \cdot x\right) + \color{blue}{\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} \cdot \left(-1 \cdot x\right)}\right) + y\right) - z \]
            6. distribute-rgt-inN/A

              \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(-1 + \frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x}\right)} + y\right) - z \]
            7. +-commutativeN/A

              \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + -1\right)} + y\right) - z \]
            8. metadata-evalN/A

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

              \[\leadsto \left(\left(-1 \cdot x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
            10. lower-*.f64N/A

              \[\leadsto \left(\color{blue}{\left(-1 \cdot x\right) \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right)} + y\right) - z \]
            11. mul-1-negN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} - 1\right) + y\right) - z \]
            12. lower-neg.f64N/A

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

              \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\left(\frac{\log y \cdot \left(\frac{1}{2} + y\right)}{x} + \left(\mathsf{neg}\left(1\right)\right)\right)} + y\right) - z \]
            14. *-commutativeN/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\color{blue}{\left(\frac{1}{2} + y\right) \cdot \log y}}{x} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
            15. associate-/l*N/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\left(\frac{1}{2} + y\right) \cdot \frac{\log y}{x}} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
            16. *-commutativeN/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\color{blue}{\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right)} + \left(\mathsf{neg}\left(1\right)\right)\right) + y\right) - z \]
            17. metadata-evalN/A

              \[\leadsto \left(\left(-x\right) \cdot \left(\frac{\log y}{x} \cdot \left(\frac{1}{2} + y\right) + \color{blue}{-1}\right) + y\right) - z \]
            18. lower-fma.f64N/A

              \[\leadsto \left(\left(-x\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{\log y}{x}, \frac{1}{2} + y, -1\right)} + y\right) - z \]
          5. Applied rewrites88.6%

            \[\leadsto \left(\color{blue}{\left(-x\right) \cdot \mathsf{fma}\left(\frac{\log y}{x}, y - -0.5, -1\right)} + y\right) - z \]
          6. Taylor expanded in x around inf

            \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
          7. Step-by-step derivation
            1. Applied rewrites60.3%

              \[\leadsto \left(\left(-x\right) \cdot -1 + y\right) - z \]
            2. Step-by-step derivation
              1. lift--.f64N/A

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

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

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

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

                \[\leadsto \color{blue}{\left(y - z\right) + \left(-x\right) \cdot -1} \]
              6. lower--.f6460.3

                \[\leadsto \color{blue}{\left(y - z\right)} + \left(-x\right) \cdot -1 \]
            3. Applied rewrites60.3%

              \[\leadsto \color{blue}{\left(y - z\right) + -1 \cdot \left(-x\right)} \]
            4. Taylor expanded in y around 0

              \[\leadsto \color{blue}{-1 \cdot z} + -1 \cdot \left(-x\right) \]
            5. Step-by-step derivation
              1. mul-1-negN/A

                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z\right)\right)} + -1 \cdot \left(-x\right) \]
              2. lower-neg.f6460.8

                \[\leadsto \color{blue}{\left(-z\right)} + -1 \cdot \left(-x\right) \]
            6. Applied rewrites60.8%

              \[\leadsto \color{blue}{\left(-z\right)} + -1 \cdot \left(-x\right) \]
            7. Final simplification60.8%

              \[\leadsto \left(-x\right) \cdot -1 + \left(-z\right) \]
            8. Add Preprocessing

            Alternative 11: 29.9% accurate, 39.3× speedup?

            \[\begin{array}{l} \\ -z \end{array} \]
            (FPCore (x y z) :precision binary64 (- z))
            double code(double x, double y, double z) {
            	return -z;
            }
            
            real(8) function code(x, y, z)
                real(8), intent (in) :: x
                real(8), intent (in) :: y
                real(8), intent (in) :: z
                code = -z
            end function
            
            public static double code(double x, double y, double z) {
            	return -z;
            }
            
            def code(x, y, z):
            	return -z
            
            function code(x, y, z)
            	return Float64(-z)
            end
            
            function tmp = code(x, y, z)
            	tmp = -z;
            end
            
            code[x_, y_, z_] := (-z)
            
            \begin{array}{l}
            
            \\
            -z
            \end{array}
            
            Derivation
            1. Initial program 99.8%

              \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z \]
            2. Add Preprocessing
            3. Taylor expanded in z around inf

              \[\leadsto \color{blue}{-1 \cdot z} \]
            4. Step-by-step derivation
              1. mul-1-negN/A

                \[\leadsto \color{blue}{\mathsf{neg}\left(z\right)} \]
              2. lower-neg.f6427.5

                \[\leadsto \color{blue}{-z} \]
            5. Applied rewrites27.5%

              \[\leadsto \color{blue}{-z} \]
            6. Add Preprocessing

            Developer Target 1: 99.8% accurate, 1.0× speedup?

            \[\begin{array}{l} \\ \left(\left(y + x\right) - z\right) - \left(y + 0.5\right) \cdot \log y \end{array} \]
            (FPCore (x y z) :precision binary64 (- (- (+ y x) z) (* (+ y 0.5) (log y))))
            double code(double x, double y, double z) {
            	return ((y + x) - z) - ((y + 0.5) * log(y));
            }
            
            real(8) function code(x, y, z)
                real(8), intent (in) :: x
                real(8), intent (in) :: y
                real(8), intent (in) :: z
                code = ((y + x) - z) - ((y + 0.5d0) * log(y))
            end function
            
            public static double code(double x, double y, double z) {
            	return ((y + x) - z) - ((y + 0.5) * Math.log(y));
            }
            
            def code(x, y, z):
            	return ((y + x) - z) - ((y + 0.5) * math.log(y))
            
            function code(x, y, z)
            	return Float64(Float64(Float64(y + x) - z) - Float64(Float64(y + 0.5) * log(y)))
            end
            
            function tmp = code(x, y, z)
            	tmp = ((y + x) - z) - ((y + 0.5) * log(y));
            end
            
            code[x_, y_, z_] := N[(N[(N[(y + x), $MachinePrecision] - z), $MachinePrecision] - N[(N[(y + 0.5), $MachinePrecision] * N[Log[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \left(\left(y + x\right) - z\right) - \left(y + 0.5\right) \cdot \log y
            \end{array}
            

            Reproduce

            ?
            herbie shell --seed 2024298 
            (FPCore (x y z)
              :name "Numeric.SpecFunctions:stirlingError from math-functions-0.1.5.2"
              :precision binary64
            
              :alt
              (! :herbie-platform default (- (- (+ y x) z) (* (+ y 1/2) (log y))))
            
              (- (+ (- x (* (+ y 0.5) (log y))) y) z))