Statistics.Distribution.Beta:$cdensity from math-functions-0.1.5.2

Percentage Accurate: 89.3% → 99.8%
Time: 16.1s
Alternatives: 18
Speedup: 1.8×

Specification

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

\\
\left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \log \left(1 - y\right)\right) - t
\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 18 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: 89.3% accurate, 1.0× speedup?

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

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

Alternative 1: 99.8% accurate, 1.0× speedup?

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

\\
\mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \log y \cdot \left(x - 1\right) - t\right)
\end{array}
Derivation
  1. Initial program 86.2%

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

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

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

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

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

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

      \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
    7. lift-log.f64N/A

      \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
    8. lift--.f64N/A

      \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
    9. *-lft-identityN/A

      \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
    10. fp-cancel-sub-sign-invN/A

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

      \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
    12. *-lft-identityN/A

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

      \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
    14. lower-neg.f64N/A

      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
    15. lower--.f6499.8

      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
    16. lift-*.f64N/A

      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
    17. *-commutativeN/A

      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
    18. lower-*.f6499.8

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

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

Alternative 2: 66.0% accurate, 1.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -0.136 \lor \neg \left(x \leq 34000000000\right):\\ \;\;\;\;\log y \cdot x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\ \end{array} \end{array} \]
(FPCore (x y z t)
 :precision binary64
 (if (or (<= x -0.136) (not (<= x 34000000000.0)))
   (* (log y) x)
   (-
    (* (fma (- (* -0.5 y) 1.0) y (/ (* (* (+ (pow y -1.0) 0.5) y) y) z)) z)
    t)))
double code(double x, double y, double z, double t) {
	double tmp;
	if ((x <= -0.136) || !(x <= 34000000000.0)) {
		tmp = log(y) * x;
	} else {
		tmp = (fma(((-0.5 * y) - 1.0), y, ((((pow(y, -1.0) + 0.5) * y) * y) / z)) * z) - t;
	}
	return tmp;
}
function code(x, y, z, t)
	tmp = 0.0
	if ((x <= -0.136) || !(x <= 34000000000.0))
		tmp = Float64(log(y) * x);
	else
		tmp = Float64(Float64(fma(Float64(Float64(-0.5 * y) - 1.0), y, Float64(Float64(Float64(Float64((y ^ -1.0) + 0.5) * y) * y) / z)) * z) - t);
	end
	return tmp
end
code[x_, y_, z_, t_] := If[Or[LessEqual[x, -0.136], N[Not[LessEqual[x, 34000000000.0]], $MachinePrecision]], N[(N[Log[y], $MachinePrecision] * x), $MachinePrecision], N[(N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * y + N[(N[(N[(N[(N[Power[y, -1.0], $MachinePrecision] + 0.5), $MachinePrecision] * y), $MachinePrecision] * y), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision] * z), $MachinePrecision] - t), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;x \leq -0.136 \lor \neg \left(x \leq 34000000000\right):\\
\;\;\;\;\log y \cdot x\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if x < -0.13600000000000001 or 3.4e10 < x

    1. Initial program 92.5%

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

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

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

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

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

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

        \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
      7. lift-log.f64N/A

        \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
      8. lift--.f64N/A

        \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
      9. *-lft-identityN/A

        \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
      10. fp-cancel-sub-sign-invN/A

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

        \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
      12. *-lft-identityN/A

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

        \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
      14. lower-neg.f64N/A

        \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
      15. lower--.f6499.6

        \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
      16. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
      17. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
      18. lower-*.f6499.6

        \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
    4. Applied rewrites99.6%

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

      \[\leadsto \color{blue}{x \cdot \log y} \]
    6. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \color{blue}{\log y \cdot x} \]
      2. lower-*.f64N/A

        \[\leadsto \color{blue}{\log y \cdot x} \]
      3. lower-log.f6474.9

        \[\leadsto \color{blue}{\log y} \cdot x \]
    7. Applied rewrites74.9%

      \[\leadsto \color{blue}{\log y \cdot x} \]

    if -0.13600000000000001 < x < 3.4e10

    1. Initial program 80.1%

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

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

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

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

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

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

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

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

      \[\leadsto z \cdot \color{blue}{\left(-1 \cdot \frac{y \cdot \left(\frac{-1}{2} \cdot y - 1\right)}{z} + \left(y \cdot \left(\frac{-1}{2} \cdot y - 1\right) + \frac{\log y \cdot \left(x - 1\right)}{z}\right)\right)} - t \]
    7. Step-by-step derivation
      1. Applied rewrites98.7%

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

        \[\leadsto \mathsf{fma}\left(\frac{-1}{2} \cdot y - 1, y, \frac{{y}^{2} \cdot \left(\frac{1}{2} + \frac{1}{y}\right)}{z}\right) \cdot z - t \]
      3. Step-by-step derivation
        1. Applied rewrites59.7%

          \[\leadsto \mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left(\frac{1}{y} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t \]
      4. Recombined 2 regimes into one program.
      5. Final simplification67.2%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -0.136 \lor \neg \left(x \leq 34000000000\right):\\ \;\;\;\;\log y \cdot x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\ \end{array} \]
      6. Add Preprocessing

      Alternative 3: 84.5% accurate, 1.4× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_1 := \log y \cdot x - t\\ \mathbf{if}\;x \leq -0.136:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \leq -1.22 \cdot 10^{-173}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\ \mathbf{elif}\;x \leq 1:\\ \;\;\;\;\left(-\log y\right) - t\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
      (FPCore (x y z t)
       :precision binary64
       (let* ((t_1 (- (* (log y) x) t)))
         (if (<= x -0.136)
           t_1
           (if (<= x -1.22e-173)
             (-
              (* (fma (- (* -0.5 y) 1.0) y (/ (* (* (+ (pow y -1.0) 0.5) y) y) z)) z)
              t)
             (if (<= x 1.0) (- (- (log y)) t) t_1)))))
      double code(double x, double y, double z, double t) {
      	double t_1 = (log(y) * x) - t;
      	double tmp;
      	if (x <= -0.136) {
      		tmp = t_1;
      	} else if (x <= -1.22e-173) {
      		tmp = (fma(((-0.5 * y) - 1.0), y, ((((pow(y, -1.0) + 0.5) * y) * y) / z)) * z) - t;
      	} else if (x <= 1.0) {
      		tmp = -log(y) - t;
      	} else {
      		tmp = t_1;
      	}
      	return tmp;
      }
      
      function code(x, y, z, t)
      	t_1 = Float64(Float64(log(y) * x) - t)
      	tmp = 0.0
      	if (x <= -0.136)
      		tmp = t_1;
      	elseif (x <= -1.22e-173)
      		tmp = Float64(Float64(fma(Float64(Float64(-0.5 * y) - 1.0), y, Float64(Float64(Float64(Float64((y ^ -1.0) + 0.5) * y) * y) / z)) * z) - t);
      	elseif (x <= 1.0)
      		tmp = Float64(Float64(-log(y)) - t);
      	else
      		tmp = t_1;
      	end
      	return tmp
      end
      
      code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[(N[Log[y], $MachinePrecision] * x), $MachinePrecision] - t), $MachinePrecision]}, If[LessEqual[x, -0.136], t$95$1, If[LessEqual[x, -1.22e-173], N[(N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * y + N[(N[(N[(N[(N[Power[y, -1.0], $MachinePrecision] + 0.5), $MachinePrecision] * y), $MachinePrecision] * y), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision] * z), $MachinePrecision] - t), $MachinePrecision], If[LessEqual[x, 1.0], N[((-N[Log[y], $MachinePrecision]) - t), $MachinePrecision], t$95$1]]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_1 := \log y \cdot x - t\\
      \mathbf{if}\;x \leq -0.136:\\
      \;\;\;\;t\_1\\
      
      \mathbf{elif}\;x \leq -1.22 \cdot 10^{-173}:\\
      \;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\
      
      \mathbf{elif}\;x \leq 1:\\
      \;\;\;\;\left(-\log y\right) - t\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_1\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if x < -0.13600000000000001 or 1 < x

        1. Initial program 92.5%

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

          \[\leadsto \color{blue}{x \cdot \log y} - t \]
        4. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto \color{blue}{\log y \cdot x} - t \]
          2. remove-double-negN/A

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

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

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

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

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

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

            \[\leadsto \color{blue}{\log y} \cdot x - t \]
          9. lower-log.f6490.3

            \[\leadsto \color{blue}{\log y} \cdot x - t \]
        5. Applied rewrites90.3%

          \[\leadsto \color{blue}{\log y \cdot x} - t \]

        if -0.13600000000000001 < x < -1.21999999999999993e-173

        1. Initial program 66.5%

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{-1 \cdot \left(\log \left(\frac{1}{y}\right) \cdot \left(x - 1\right)\right)} + y \cdot \left(-1 \cdot \left(z - 1\right) + \frac{-1}{2} \cdot \left(y \cdot \left(z - 1\right)\right)\right)\right) - t \]
        5. Applied rewrites96.7%

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

          \[\leadsto z \cdot \color{blue}{\left(-1 \cdot \frac{y \cdot \left(\frac{-1}{2} \cdot y - 1\right)}{z} + \left(y \cdot \left(\frac{-1}{2} \cdot y - 1\right) + \frac{\log y \cdot \left(x - 1\right)}{z}\right)\right)} - t \]
        7. Step-by-step derivation
          1. Applied rewrites96.6%

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

            \[\leadsto \mathsf{fma}\left(\frac{-1}{2} \cdot y - 1, y, \frac{{y}^{2} \cdot \left(\frac{1}{2} + \frac{1}{y}\right)}{z}\right) \cdot z - t \]
          3. Step-by-step derivation
            1. Applied rewrites73.6%

              \[\leadsto \mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left(\frac{1}{y} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t \]

            if -1.21999999999999993e-173 < x < 1

            1. Initial program 84.9%

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

              \[\leadsto \color{blue}{\log y \cdot \left(x - 1\right)} - t \]
            4. Step-by-step derivation
              1. remove-double-negN/A

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

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

                \[\leadsto \color{blue}{\left(-1 \cdot \log \left(\frac{1}{y}\right)\right)} \cdot \left(x - 1\right) - t \]
              4. distribute-rgt-out--N/A

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

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

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

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

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

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

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

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

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

                \[\leadsto \color{blue}{\left(-1 \cdot \log y + x \cdot \log y\right)} - t \]
              14. distribute-rgt-outN/A

                \[\leadsto \color{blue}{\log y \cdot \left(-1 + x\right)} - t \]
              15. remove-double-negN/A

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

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

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

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

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

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

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

                \[\leadsto \left(-1 + x\right) \cdot \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right) - t \]
            5. Applied rewrites84.4%

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

              \[\leadsto -1 \cdot \color{blue}{\log y} - t \]
            7. Step-by-step derivation
              1. Applied rewrites84.3%

                \[\leadsto \left(-\log y\right) - t \]
            8. Recombined 3 regimes into one program.
            9. Final simplification85.9%

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

            Alternative 4: 72.8% accurate, 1.4× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} t_1 := \log y \cdot x\\ \mathbf{if}\;x \leq -0.136:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \leq -1.22 \cdot 10^{-173}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\ \mathbf{elif}\;x \leq 215000:\\ \;\;\;\;\left(-\log y\right) - t\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
            (FPCore (x y z t)
             :precision binary64
             (let* ((t_1 (* (log y) x)))
               (if (<= x -0.136)
                 t_1
                 (if (<= x -1.22e-173)
                   (-
                    (* (fma (- (* -0.5 y) 1.0) y (/ (* (* (+ (pow y -1.0) 0.5) y) y) z)) z)
                    t)
                   (if (<= x 215000.0) (- (- (log y)) t) t_1)))))
            double code(double x, double y, double z, double t) {
            	double t_1 = log(y) * x;
            	double tmp;
            	if (x <= -0.136) {
            		tmp = t_1;
            	} else if (x <= -1.22e-173) {
            		tmp = (fma(((-0.5 * y) - 1.0), y, ((((pow(y, -1.0) + 0.5) * y) * y) / z)) * z) - t;
            	} else if (x <= 215000.0) {
            		tmp = -log(y) - t;
            	} else {
            		tmp = t_1;
            	}
            	return tmp;
            }
            
            function code(x, y, z, t)
            	t_1 = Float64(log(y) * x)
            	tmp = 0.0
            	if (x <= -0.136)
            		tmp = t_1;
            	elseif (x <= -1.22e-173)
            		tmp = Float64(Float64(fma(Float64(Float64(-0.5 * y) - 1.0), y, Float64(Float64(Float64(Float64((y ^ -1.0) + 0.5) * y) * y) / z)) * z) - t);
            	elseif (x <= 215000.0)
            		tmp = Float64(Float64(-log(y)) - t);
            	else
            		tmp = t_1;
            	end
            	return tmp
            end
            
            code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[Log[y], $MachinePrecision] * x), $MachinePrecision]}, If[LessEqual[x, -0.136], t$95$1, If[LessEqual[x, -1.22e-173], N[(N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * y + N[(N[(N[(N[(N[Power[y, -1.0], $MachinePrecision] + 0.5), $MachinePrecision] * y), $MachinePrecision] * y), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision] * z), $MachinePrecision] - t), $MachinePrecision], If[LessEqual[x, 215000.0], N[((-N[Log[y], $MachinePrecision]) - t), $MachinePrecision], t$95$1]]]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            t_1 := \log y \cdot x\\
            \mathbf{if}\;x \leq -0.136:\\
            \;\;\;\;t\_1\\
            
            \mathbf{elif}\;x \leq -1.22 \cdot 10^{-173}:\\
            \;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\
            
            \mathbf{elif}\;x \leq 215000:\\
            \;\;\;\;\left(-\log y\right) - t\\
            
            \mathbf{else}:\\
            \;\;\;\;t\_1\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 3 regimes
            2. if x < -0.13600000000000001 or 215000 < x

              1. Initial program 92.5%

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

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

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

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

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

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

                  \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
                7. lift-log.f64N/A

                  \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                8. lift--.f64N/A

                  \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                9. *-lft-identityN/A

                  \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                10. fp-cancel-sub-sign-invN/A

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

                  \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                12. *-lft-identityN/A

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

                  \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                14. lower-neg.f64N/A

                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                15. lower--.f6499.6

                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
                16. lift-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
                17. *-commutativeN/A

                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                18. lower-*.f6499.6

                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
              4. Applied rewrites99.6%

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

                \[\leadsto \color{blue}{x \cdot \log y} \]
              6. Step-by-step derivation
                1. *-commutativeN/A

                  \[\leadsto \color{blue}{\log y \cdot x} \]
                2. lower-*.f64N/A

                  \[\leadsto \color{blue}{\log y \cdot x} \]
                3. lower-log.f6474.3

                  \[\leadsto \color{blue}{\log y} \cdot x \]
              7. Applied rewrites74.3%

                \[\leadsto \color{blue}{\log y \cdot x} \]

              if -0.13600000000000001 < x < -1.21999999999999993e-173

              1. Initial program 66.5%

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

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

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

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

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

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

                  \[\leadsto \left(\color{blue}{-1 \cdot \left(\log \left(\frac{1}{y}\right) \cdot \left(x - 1\right)\right)} + y \cdot \left(-1 \cdot \left(z - 1\right) + \frac{-1}{2} \cdot \left(y \cdot \left(z - 1\right)\right)\right)\right) - t \]
              5. Applied rewrites96.7%

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

                \[\leadsto z \cdot \color{blue}{\left(-1 \cdot \frac{y \cdot \left(\frac{-1}{2} \cdot y - 1\right)}{z} + \left(y \cdot \left(\frac{-1}{2} \cdot y - 1\right) + \frac{\log y \cdot \left(x - 1\right)}{z}\right)\right)} - t \]
              7. Step-by-step derivation
                1. Applied rewrites96.6%

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

                  \[\leadsto \mathsf{fma}\left(\frac{-1}{2} \cdot y - 1, y, \frac{{y}^{2} \cdot \left(\frac{1}{2} + \frac{1}{y}\right)}{z}\right) \cdot z - t \]
                3. Step-by-step derivation
                  1. Applied rewrites73.6%

                    \[\leadsto \mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left(\frac{1}{y} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t \]

                  if -1.21999999999999993e-173 < x < 215000

                  1. Initial program 84.9%

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

                    \[\leadsto \color{blue}{\log y \cdot \left(x - 1\right)} - t \]
                  4. Step-by-step derivation
                    1. remove-double-negN/A

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

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

                      \[\leadsto \color{blue}{\left(-1 \cdot \log \left(\frac{1}{y}\right)\right)} \cdot \left(x - 1\right) - t \]
                    4. distribute-rgt-out--N/A

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

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

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

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

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

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

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

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

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

                      \[\leadsto \color{blue}{\left(-1 \cdot \log y + x \cdot \log y\right)} - t \]
                    14. distribute-rgt-outN/A

                      \[\leadsto \color{blue}{\log y \cdot \left(-1 + x\right)} - t \]
                    15. remove-double-negN/A

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

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

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

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

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

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

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

                      \[\leadsto \left(-1 + x\right) \cdot \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right) - t \]
                  5. Applied rewrites84.4%

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

                    \[\leadsto -1 \cdot \color{blue}{\log y} - t \]
                  7. Step-by-step derivation
                    1. Applied rewrites84.3%

                      \[\leadsto \left(-\log y\right) - t \]
                  8. Recombined 3 regimes into one program.
                  9. Final simplification77.9%

                    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -0.136:\\ \;\;\;\;\log y \cdot x\\ \mathbf{elif}\;x \leq -1.22 \cdot 10^{-173}:\\ \;\;\;\;\mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t\\ \mathbf{elif}\;x \leq 215000:\\ \;\;\;\;\left(-\log y\right) - t\\ \mathbf{else}:\\ \;\;\;\;\log y \cdot x\\ \end{array} \]
                  10. Add Preprocessing

                  Alternative 5: 99.5% accurate, 1.5× speedup?

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

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

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

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

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

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

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

                      \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
                    7. lift-log.f64N/A

                      \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                    8. lift--.f64N/A

                      \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                    9. *-lft-identityN/A

                      \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                    10. fp-cancel-sub-sign-invN/A

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

                      \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                    12. *-lft-identityN/A

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

                      \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                    14. lower-neg.f64N/A

                      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                    15. lower--.f6499.8

                      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
                    16. lift-*.f64N/A

                      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
                    17. *-commutativeN/A

                      \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                    18. lower-*.f6499.8

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

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

                    \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{y \cdot \left(y \cdot \left(y \cdot \left(\frac{-1}{4} \cdot y - \frac{1}{3}\right) - \frac{1}{2}\right) - 1\right)}, \log y \cdot \left(x - 1\right) - t\right) \]
                  6. Step-by-step derivation
                    1. *-commutativeN/A

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

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

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

                      \[\leadsto \mathsf{fma}\left(z - 1, \left(\color{blue}{\left(y \cdot \left(\frac{-1}{4} \cdot y - \frac{1}{3}\right) - \frac{1}{2}\right) \cdot y} - 1\right) \cdot y, \log y \cdot \left(x - 1\right) - t\right) \]
                    5. lower-*.f64N/A

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

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

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

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

                      \[\leadsto \mathsf{fma}\left(z - 1, \left(\left(\color{blue}{\left(\frac{-1}{4} \cdot y - \frac{1}{3}\right)} \cdot y - \frac{1}{2}\right) \cdot y - 1\right) \cdot y, \log y \cdot \left(x - 1\right) - t\right) \]
                    10. lower-*.f6499.5

                      \[\leadsto \mathsf{fma}\left(z - 1, \left(\left(\left(\color{blue}{-0.25 \cdot y} - 0.3333333333333333\right) \cdot y - 0.5\right) \cdot y - 1\right) \cdot y, \log y \cdot \left(x - 1\right) - t\right) \]
                  7. Applied rewrites99.5%

                    \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\left(\left(\left(-0.25 \cdot y - 0.3333333333333333\right) \cdot y - 0.5\right) \cdot y - 1\right) \cdot y}, \log y \cdot \left(x - 1\right) - t\right) \]
                  8. Add Preprocessing

                  Alternative 6: 46.8% accurate, 1.5× speedup?

                  \[\begin{array}{l} \\ \mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t \end{array} \]
                  (FPCore (x y z t)
                   :precision binary64
                   (- (* (fma (- (* -0.5 y) 1.0) y (/ (* (* (+ (pow y -1.0) 0.5) y) y) z)) z) t))
                  double code(double x, double y, double z, double t) {
                  	return (fma(((-0.5 * y) - 1.0), y, ((((pow(y, -1.0) + 0.5) * y) * y) / z)) * z) - t;
                  }
                  
                  function code(x, y, z, t)
                  	return Float64(Float64(fma(Float64(Float64(-0.5 * y) - 1.0), y, Float64(Float64(Float64(Float64((y ^ -1.0) + 0.5) * y) * y) / z)) * z) - t)
                  end
                  
                  code[x_, y_, z_, t_] := N[(N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * y + N[(N[(N[(N[(N[Power[y, -1.0], $MachinePrecision] + 0.5), $MachinePrecision] * y), $MachinePrecision] * y), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision] * z), $MachinePrecision] - t), $MachinePrecision]
                  
                  \begin{array}{l}
                  
                  \\
                  \mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t
                  \end{array}
                  
                  Derivation
                  1. Initial program 86.2%

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

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

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

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

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

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

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

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

                    \[\leadsto z \cdot \color{blue}{\left(-1 \cdot \frac{y \cdot \left(\frac{-1}{2} \cdot y - 1\right)}{z} + \left(y \cdot \left(\frac{-1}{2} \cdot y - 1\right) + \frac{\log y \cdot \left(x - 1\right)}{z}\right)\right)} - t \]
                  7. Step-by-step derivation
                    1. Applied rewrites90.0%

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

                      \[\leadsto \mathsf{fma}\left(\frac{-1}{2} \cdot y - 1, y, \frac{{y}^{2} \cdot \left(\frac{1}{2} + \frac{1}{y}\right)}{z}\right) \cdot z - t \]
                    3. Step-by-step derivation
                      1. Applied rewrites42.1%

                        \[\leadsto \mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left(\frac{1}{y} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t \]
                      2. Final simplification42.1%

                        \[\leadsto \mathsf{fma}\left(-0.5 \cdot y - 1, y, \frac{\left(\left({y}^{-1} + 0.5\right) \cdot y\right) \cdot y}{z}\right) \cdot z - t \]
                      3. Add Preprocessing

                      Alternative 7: 99.5% accurate, 1.6× speedup?

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

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

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

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

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

                      Alternative 8: 99.3% accurate, 1.7× speedup?

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

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

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

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

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

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

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

                        \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \color{blue}{\left(\left(-0.5 \cdot y - 1\right) \cdot y\right)}\right) - t \]
                      6. Final simplification99.2%

                        \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\left(-0.5 \cdot y - 1\right) \cdot y\right)\right) - t \]
                      7. Add Preprocessing

                      Alternative 9: 95.3% accurate, 1.7× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x - 1 \leq -1.1 \lor \neg \left(x - 1 \leq 200000000\right):\\ \;\;\;\;\left(-1 + x\right) \cdot \log y - t\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-y\right) \cdot \left(z - 1\right) - \log y\right) - t\\ \end{array} \end{array} \]
                      (FPCore (x y z t)
                       :precision binary64
                       (if (or (<= (- x 1.0) -1.1) (not (<= (- x 1.0) 200000000.0)))
                         (- (* (+ -1.0 x) (log y)) t)
                         (- (- (* (- y) (- z 1.0)) (log y)) t)))
                      double code(double x, double y, double z, double t) {
                      	double tmp;
                      	if (((x - 1.0) <= -1.1) || !((x - 1.0) <= 200000000.0)) {
                      		tmp = ((-1.0 + x) * log(y)) - t;
                      	} else {
                      		tmp = ((-y * (z - 1.0)) - log(y)) - t;
                      	}
                      	return tmp;
                      }
                      
                      real(8) function code(x, y, z, t)
                          real(8), intent (in) :: x
                          real(8), intent (in) :: y
                          real(8), intent (in) :: z
                          real(8), intent (in) :: t
                          real(8) :: tmp
                          if (((x - 1.0d0) <= (-1.1d0)) .or. (.not. ((x - 1.0d0) <= 200000000.0d0))) then
                              tmp = (((-1.0d0) + x) * log(y)) - t
                          else
                              tmp = ((-y * (z - 1.0d0)) - log(y)) - t
                          end if
                          code = tmp
                      end function
                      
                      public static double code(double x, double y, double z, double t) {
                      	double tmp;
                      	if (((x - 1.0) <= -1.1) || !((x - 1.0) <= 200000000.0)) {
                      		tmp = ((-1.0 + x) * Math.log(y)) - t;
                      	} else {
                      		tmp = ((-y * (z - 1.0)) - Math.log(y)) - t;
                      	}
                      	return tmp;
                      }
                      
                      def code(x, y, z, t):
                      	tmp = 0
                      	if ((x - 1.0) <= -1.1) or not ((x - 1.0) <= 200000000.0):
                      		tmp = ((-1.0 + x) * math.log(y)) - t
                      	else:
                      		tmp = ((-y * (z - 1.0)) - math.log(y)) - t
                      	return tmp
                      
                      function code(x, y, z, t)
                      	tmp = 0.0
                      	if ((Float64(x - 1.0) <= -1.1) || !(Float64(x - 1.0) <= 200000000.0))
                      		tmp = Float64(Float64(Float64(-1.0 + x) * log(y)) - t);
                      	else
                      		tmp = Float64(Float64(Float64(Float64(-y) * Float64(z - 1.0)) - log(y)) - t);
                      	end
                      	return tmp
                      end
                      
                      function tmp_2 = code(x, y, z, t)
                      	tmp = 0.0;
                      	if (((x - 1.0) <= -1.1) || ~(((x - 1.0) <= 200000000.0)))
                      		tmp = ((-1.0 + x) * log(y)) - t;
                      	else
                      		tmp = ((-y * (z - 1.0)) - log(y)) - t;
                      	end
                      	tmp_2 = tmp;
                      end
                      
                      code[x_, y_, z_, t_] := If[Or[LessEqual[N[(x - 1.0), $MachinePrecision], -1.1], N[Not[LessEqual[N[(x - 1.0), $MachinePrecision], 200000000.0]], $MachinePrecision]], N[(N[(N[(-1.0 + x), $MachinePrecision] * N[Log[y], $MachinePrecision]), $MachinePrecision] - t), $MachinePrecision], N[(N[(N[((-y) * N[(z - 1.0), $MachinePrecision]), $MachinePrecision] - N[Log[y], $MachinePrecision]), $MachinePrecision] - t), $MachinePrecision]]
                      
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      \mathbf{if}\;x - 1 \leq -1.1 \lor \neg \left(x - 1 \leq 200000000\right):\\
                      \;\;\;\;\left(-1 + x\right) \cdot \log y - t\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;\left(\left(-y\right) \cdot \left(z - 1\right) - \log y\right) - t\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if (-.f64 x #s(literal 1 binary64)) < -1.1000000000000001 or 2e8 < (-.f64 x #s(literal 1 binary64))

                        1. Initial program 92.5%

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

                          \[\leadsto \color{blue}{\log y \cdot \left(x - 1\right)} - t \]
                        4. Step-by-step derivation
                          1. remove-double-negN/A

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

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

                            \[\leadsto \color{blue}{\left(-1 \cdot \log \left(\frac{1}{y}\right)\right)} \cdot \left(x - 1\right) - t \]
                          4. distribute-rgt-out--N/A

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

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

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

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

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

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

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

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

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

                            \[\leadsto \color{blue}{\left(-1 \cdot \log y + x \cdot \log y\right)} - t \]
                          14. distribute-rgt-outN/A

                            \[\leadsto \color{blue}{\log y \cdot \left(-1 + x\right)} - t \]
                          15. remove-double-negN/A

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

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

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

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

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

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

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

                            \[\leadsto \left(-1 + x\right) \cdot \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right) - t \]
                        5. Applied rewrites92.1%

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

                        if -1.1000000000000001 < (-.f64 x #s(literal 1 binary64)) < 2e8

                        1. Initial program 80.1%

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

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

                            \[\leadsto \color{blue}{\left(\log \left(1 - y\right) \cdot \left(z - 1\right) + -1 \cdot \log y\right)} - t \]
                          2. distribute-rgt-out--N/A

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

                            \[\leadsto \left(\left(z \cdot \log \left(1 - y\right) - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot \log \left(1 - y\right)\right) + -1 \cdot \log y\right) - t \]
                          4. fp-cancel-sign-sub-invN/A

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

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

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

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

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

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

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

                            \[\leadsto \mathsf{fma}\left(-1 + z, \log \color{blue}{\left(1 - y\right)}, -1 \cdot \log y\right) - t \]
                          12. remove-double-negN/A

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

                            \[\leadsto \mathsf{fma}\left(-1 + z, \log \left(1 - y\right), \mathsf{neg}\left(\color{blue}{-1 \cdot \left(\mathsf{neg}\left(\log y\right)\right)}\right)\right) - t \]
                          14. log-recN/A

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

                            \[\leadsto \mathsf{fma}\left(-1 + z, \log \left(1 - y\right), \color{blue}{--1 \cdot \log \left(\frac{1}{y}\right)}\right) - t \]
                          16. mul-1-negN/A

                            \[\leadsto \mathsf{fma}\left(-1 + z, \log \left(1 - y\right), -\color{blue}{\left(\mathsf{neg}\left(\log \left(\frac{1}{y}\right)\right)\right)}\right) - t \]
                          17. log-recN/A

                            \[\leadsto \mathsf{fma}\left(-1 + z, \log \left(1 - y\right), -\left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right)\right) - t \]
                          18. remove-double-negN/A

                            \[\leadsto \mathsf{fma}\left(-1 + z, \log \left(1 - y\right), -\color{blue}{\log y}\right) - t \]
                          19. lower-log.f6480.0

                            \[\leadsto \mathsf{fma}\left(-1 + z, \log \left(1 - y\right), -\color{blue}{\log y}\right) - t \]
                        5. Applied rewrites80.0%

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

                          \[\leadsto \left(-1 \cdot \left(y \cdot \left(z - 1\right)\right) - \color{blue}{\log y}\right) - t \]
                        7. Step-by-step derivation
                          1. Applied rewrites98.2%

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

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

                        Alternative 10: 99.3% accurate, 1.7× speedup?

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

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

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

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

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

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

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

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

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

                        Alternative 11: 99.0% accurate, 1.8× speedup?

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

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

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

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

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

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

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

                            \[\leadsto \mathsf{fma}\left(\color{blue}{-y}, z - 1, \log y \cdot \left(x - 1\right) - t\right) \]
                          6. lower--.f64N/A

                            \[\leadsto \mathsf{fma}\left(-y, \color{blue}{z - 1}, \log y \cdot \left(x - 1\right) - t\right) \]
                          7. *-rgt-identityN/A

                            \[\leadsto \mathsf{fma}\left(-y, z - 1, \log y \cdot \left(x - 1\right) - \color{blue}{t \cdot 1}\right) \]
                          8. fp-cancel-sub-sign-invN/A

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

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

                        Alternative 12: 89.0% accurate, 1.9× speedup?

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

                          1. Initial program 34.2%

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

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

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

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

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

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

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

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

                            \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({y}^{2} \cdot \left(z - 1\right)\right)} - t \]
                          7. Step-by-step derivation
                            1. Applied rewrites28.6%

                              \[\leadsto \left(\left(-0.5 \cdot \left(z - 1\right)\right) \cdot y\right) \cdot \color{blue}{y} - t \]
                            2. Taylor expanded in z around inf

                              \[\leadsto y \cdot \color{blue}{\left(z \cdot \left(\frac{-1}{2} \cdot y - 1\right)\right)} - t \]
                            3. Step-by-step derivation
                              1. Applied rewrites86.8%

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

                              if -1.9999999999999998e250 < (-.f64 z #s(literal 1 binary64))

                              1. Initial program 88.8%

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

                                \[\leadsto \color{blue}{\log y \cdot \left(x - 1\right)} - t \]
                              4. Step-by-step derivation
                                1. remove-double-negN/A

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

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

                                  \[\leadsto \color{blue}{\left(-1 \cdot \log \left(\frac{1}{y}\right)\right)} \cdot \left(x - 1\right) - t \]
                                4. distribute-rgt-out--N/A

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

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

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

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

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

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

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

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

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

                                  \[\leadsto \color{blue}{\left(-1 \cdot \log y + x \cdot \log y\right)} - t \]
                                14. distribute-rgt-outN/A

                                  \[\leadsto \color{blue}{\log y \cdot \left(-1 + x\right)} - t \]
                                15. remove-double-negN/A

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

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

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

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

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

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

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

                                  \[\leadsto \left(-1 + x\right) \cdot \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right)\right) - t \]
                              5. Applied rewrites87.2%

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

                            Alternative 13: 42.8% accurate, 7.3× speedup?

                            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\ \;\;\;\;-t\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z\\ \end{array} \end{array} \]
                            (FPCore (x y z t)
                             :precision binary64
                             (if (or (<= t -3e+52) (not (<= t 14200.0)))
                               (- t)
                               (* (* (- (* -0.5 y) 1.0) y) z)))
                            double code(double x, double y, double z, double t) {
                            	double tmp;
                            	if ((t <= -3e+52) || !(t <= 14200.0)) {
                            		tmp = -t;
                            	} else {
                            		tmp = (((-0.5 * y) - 1.0) * y) * z;
                            	}
                            	return tmp;
                            }
                            
                            real(8) function code(x, y, z, t)
                                real(8), intent (in) :: x
                                real(8), intent (in) :: y
                                real(8), intent (in) :: z
                                real(8), intent (in) :: t
                                real(8) :: tmp
                                if ((t <= (-3d+52)) .or. (.not. (t <= 14200.0d0))) then
                                    tmp = -t
                                else
                                    tmp = ((((-0.5d0) * y) - 1.0d0) * y) * z
                                end if
                                code = tmp
                            end function
                            
                            public static double code(double x, double y, double z, double t) {
                            	double tmp;
                            	if ((t <= -3e+52) || !(t <= 14200.0)) {
                            		tmp = -t;
                            	} else {
                            		tmp = (((-0.5 * y) - 1.0) * y) * z;
                            	}
                            	return tmp;
                            }
                            
                            def code(x, y, z, t):
                            	tmp = 0
                            	if (t <= -3e+52) or not (t <= 14200.0):
                            		tmp = -t
                            	else:
                            		tmp = (((-0.5 * y) - 1.0) * y) * z
                            	return tmp
                            
                            function code(x, y, z, t)
                            	tmp = 0.0
                            	if ((t <= -3e+52) || !(t <= 14200.0))
                            		tmp = Float64(-t);
                            	else
                            		tmp = Float64(Float64(Float64(Float64(-0.5 * y) - 1.0) * y) * z);
                            	end
                            	return tmp
                            end
                            
                            function tmp_2 = code(x, y, z, t)
                            	tmp = 0.0;
                            	if ((t <= -3e+52) || ~((t <= 14200.0)))
                            		tmp = -t;
                            	else
                            		tmp = (((-0.5 * y) - 1.0) * y) * z;
                            	end
                            	tmp_2 = tmp;
                            end
                            
                            code[x_, y_, z_, t_] := If[Or[LessEqual[t, -3e+52], N[Not[LessEqual[t, 14200.0]], $MachinePrecision]], (-t), N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * y), $MachinePrecision] * z), $MachinePrecision]]
                            
                            \begin{array}{l}
                            
                            \\
                            \begin{array}{l}
                            \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\
                            \;\;\;\;-t\\
                            
                            \mathbf{else}:\\
                            \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z\\
                            
                            
                            \end{array}
                            \end{array}
                            
                            Derivation
                            1. Split input into 2 regimes
                            2. if t < -3e52 or 14200 < t

                              1. Initial program 94.8%

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

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

                                  \[\leadsto \color{blue}{\mathsf{neg}\left(t\right)} \]
                                2. lower-neg.f6468.8

                                  \[\leadsto \color{blue}{-t} \]
                              5. Applied rewrites68.8%

                                \[\leadsto \color{blue}{-t} \]

                              if -3e52 < t < 14200

                              1. Initial program 80.8%

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

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

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

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

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

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

                                  \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
                                7. lift-log.f64N/A

                                  \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                8. lift--.f64N/A

                                  \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                9. *-lft-identityN/A

                                  \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                10. fp-cancel-sub-sign-invN/A

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

                                  \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                12. *-lft-identityN/A

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

                                  \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                14. lower-neg.f64N/A

                                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                15. lower--.f6499.7

                                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
                                16. lift-*.f64N/A

                                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
                                17. *-commutativeN/A

                                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                                18. lower-*.f6499.7

                                  \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                              4. Applied rewrites99.7%

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

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

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

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

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

                                  \[\leadsto \log \color{blue}{\left(1 - y\right)} \cdot z \]
                              7. Applied rewrites3.7%

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

                                \[\leadsto \left(y \cdot \left(\frac{-1}{2} \cdot y - 1\right)\right) \cdot z \]
                              9. Step-by-step derivation
                                1. Applied rewrites20.7%

                                  \[\leadsto \left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z \]
                              10. Recombined 2 regimes into one program.
                              11. Final simplification39.1%

                                \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\ \;\;\;\;-t\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z\\ \end{array} \]
                              12. Add Preprocessing

                              Alternative 14: 42.8% accurate, 7.3× speedup?

                              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52}:\\ \;\;\;\;-t\\ \mathbf{elif}\;t \leq 14200:\\ \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z\\ \mathbf{else}:\\ \;\;\;\;\left(\left(y \cdot y\right) \cdot z\right) \cdot -0.5 - t\\ \end{array} \end{array} \]
                              (FPCore (x y z t)
                               :precision binary64
                               (if (<= t -3e+52)
                                 (- t)
                                 (if (<= t 14200.0)
                                   (* (* (- (* -0.5 y) 1.0) y) z)
                                   (- (* (* (* y y) z) -0.5) t))))
                              double code(double x, double y, double z, double t) {
                              	double tmp;
                              	if (t <= -3e+52) {
                              		tmp = -t;
                              	} else if (t <= 14200.0) {
                              		tmp = (((-0.5 * y) - 1.0) * y) * z;
                              	} else {
                              		tmp = (((y * y) * z) * -0.5) - t;
                              	}
                              	return tmp;
                              }
                              
                              real(8) function code(x, y, z, t)
                                  real(8), intent (in) :: x
                                  real(8), intent (in) :: y
                                  real(8), intent (in) :: z
                                  real(8), intent (in) :: t
                                  real(8) :: tmp
                                  if (t <= (-3d+52)) then
                                      tmp = -t
                                  else if (t <= 14200.0d0) then
                                      tmp = ((((-0.5d0) * y) - 1.0d0) * y) * z
                                  else
                                      tmp = (((y * y) * z) * (-0.5d0)) - t
                                  end if
                                  code = tmp
                              end function
                              
                              public static double code(double x, double y, double z, double t) {
                              	double tmp;
                              	if (t <= -3e+52) {
                              		tmp = -t;
                              	} else if (t <= 14200.0) {
                              		tmp = (((-0.5 * y) - 1.0) * y) * z;
                              	} else {
                              		tmp = (((y * y) * z) * -0.5) - t;
                              	}
                              	return tmp;
                              }
                              
                              def code(x, y, z, t):
                              	tmp = 0
                              	if t <= -3e+52:
                              		tmp = -t
                              	elif t <= 14200.0:
                              		tmp = (((-0.5 * y) - 1.0) * y) * z
                              	else:
                              		tmp = (((y * y) * z) * -0.5) - t
                              	return tmp
                              
                              function code(x, y, z, t)
                              	tmp = 0.0
                              	if (t <= -3e+52)
                              		tmp = Float64(-t);
                              	elseif (t <= 14200.0)
                              		tmp = Float64(Float64(Float64(Float64(-0.5 * y) - 1.0) * y) * z);
                              	else
                              		tmp = Float64(Float64(Float64(Float64(y * y) * z) * -0.5) - t);
                              	end
                              	return tmp
                              end
                              
                              function tmp_2 = code(x, y, z, t)
                              	tmp = 0.0;
                              	if (t <= -3e+52)
                              		tmp = -t;
                              	elseif (t <= 14200.0)
                              		tmp = (((-0.5 * y) - 1.0) * y) * z;
                              	else
                              		tmp = (((y * y) * z) * -0.5) - t;
                              	end
                              	tmp_2 = tmp;
                              end
                              
                              code[x_, y_, z_, t_] := If[LessEqual[t, -3e+52], (-t), If[LessEqual[t, 14200.0], N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * y), $MachinePrecision] * z), $MachinePrecision], N[(N[(N[(N[(y * y), $MachinePrecision] * z), $MachinePrecision] * -0.5), $MachinePrecision] - t), $MachinePrecision]]]
                              
                              \begin{array}{l}
                              
                              \\
                              \begin{array}{l}
                              \mathbf{if}\;t \leq -3 \cdot 10^{+52}:\\
                              \;\;\;\;-t\\
                              
                              \mathbf{elif}\;t \leq 14200:\\
                              \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z\\
                              
                              \mathbf{else}:\\
                              \;\;\;\;\left(\left(y \cdot y\right) \cdot z\right) \cdot -0.5 - t\\
                              
                              
                              \end{array}
                              \end{array}
                              
                              Derivation
                              1. Split input into 3 regimes
                              2. if t < -3e52

                                1. Initial program 97.7%

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

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

                                    \[\leadsto \color{blue}{\mathsf{neg}\left(t\right)} \]
                                  2. lower-neg.f6473.7

                                    \[\leadsto \color{blue}{-t} \]
                                5. Applied rewrites73.7%

                                  \[\leadsto \color{blue}{-t} \]

                                if -3e52 < t < 14200

                                1. Initial program 80.8%

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

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

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

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

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

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

                                    \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
                                  7. lift-log.f64N/A

                                    \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                  8. lift--.f64N/A

                                    \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                  9. *-lft-identityN/A

                                    \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                  10. fp-cancel-sub-sign-invN/A

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

                                    \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                  12. *-lft-identityN/A

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

                                    \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                  14. lower-neg.f64N/A

                                    \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                  15. lower--.f6499.7

                                    \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
                                  16. lift-*.f64N/A

                                    \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
                                  17. *-commutativeN/A

                                    \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                                  18. lower-*.f6499.7

                                    \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                                4. Applied rewrites99.7%

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

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

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

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

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

                                    \[\leadsto \log \color{blue}{\left(1 - y\right)} \cdot z \]
                                7. Applied rewrites3.7%

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

                                  \[\leadsto \left(y \cdot \left(\frac{-1}{2} \cdot y - 1\right)\right) \cdot z \]
                                9. Step-by-step derivation
                                  1. Applied rewrites20.7%

                                    \[\leadsto \left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z \]

                                  if 14200 < t

                                  1. Initial program 92.9%

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

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

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

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

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

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

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

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

                                    \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({y}^{2} \cdot \left(z - 1\right)\right)} - t \]
                                  7. Step-by-step derivation
                                    1. Applied rewrites65.8%

                                      \[\leadsto \left(\left(-0.5 \cdot \left(z - 1\right)\right) \cdot y\right) \cdot \color{blue}{y} - t \]
                                    2. Taylor expanded in z around inf

                                      \[\leadsto \frac{-1}{2} \cdot \left({y}^{2} \cdot \color{blue}{z}\right) - t \]
                                    3. Step-by-step derivation
                                      1. Applied rewrites65.8%

                                        \[\leadsto \left(\left(y \cdot y\right) \cdot z\right) \cdot -0.5 - t \]
                                    4. Recombined 3 regimes into one program.
                                    5. Final simplification39.2%

                                      \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52}:\\ \;\;\;\;-t\\ \mathbf{elif}\;t \leq 14200:\\ \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot z\\ \mathbf{else}:\\ \;\;\;\;\left(\left(y \cdot y\right) \cdot z\right) \cdot -0.5 - t\\ \end{array} \]
                                    6. Add Preprocessing

                                    Alternative 15: 42.8% accurate, 7.8× speedup?

                                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\ \;\;\;\;-t\\ \mathbf{else}:\\ \;\;\;\;\left(z \cdot \mathsf{fma}\left(-0.5, y, -1\right)\right) \cdot y\\ \end{array} \end{array} \]
                                    (FPCore (x y z t)
                                     :precision binary64
                                     (if (or (<= t -3e+52) (not (<= t 14200.0)))
                                       (- t)
                                       (* (* z (fma -0.5 y -1.0)) y)))
                                    double code(double x, double y, double z, double t) {
                                    	double tmp;
                                    	if ((t <= -3e+52) || !(t <= 14200.0)) {
                                    		tmp = -t;
                                    	} else {
                                    		tmp = (z * fma(-0.5, y, -1.0)) * y;
                                    	}
                                    	return tmp;
                                    }
                                    
                                    function code(x, y, z, t)
                                    	tmp = 0.0
                                    	if ((t <= -3e+52) || !(t <= 14200.0))
                                    		tmp = Float64(-t);
                                    	else
                                    		tmp = Float64(Float64(z * fma(-0.5, y, -1.0)) * y);
                                    	end
                                    	return tmp
                                    end
                                    
                                    code[x_, y_, z_, t_] := If[Or[LessEqual[t, -3e+52], N[Not[LessEqual[t, 14200.0]], $MachinePrecision]], (-t), N[(N[(z * N[(-0.5 * y + -1.0), $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision]]
                                    
                                    \begin{array}{l}
                                    
                                    \\
                                    \begin{array}{l}
                                    \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\
                                    \;\;\;\;-t\\
                                    
                                    \mathbf{else}:\\
                                    \;\;\;\;\left(z \cdot \mathsf{fma}\left(-0.5, y, -1\right)\right) \cdot y\\
                                    
                                    
                                    \end{array}
                                    \end{array}
                                    
                                    Derivation
                                    1. Split input into 2 regimes
                                    2. if t < -3e52 or 14200 < t

                                      1. Initial program 94.8%

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

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

                                          \[\leadsto \color{blue}{\mathsf{neg}\left(t\right)} \]
                                        2. lower-neg.f6468.8

                                          \[\leadsto \color{blue}{-t} \]
                                      5. Applied rewrites68.8%

                                        \[\leadsto \color{blue}{-t} \]

                                      if -3e52 < t < 14200

                                      1. Initial program 80.8%

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

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

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

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

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

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

                                          \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
                                        7. lift-log.f64N/A

                                          \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                        8. lift--.f64N/A

                                          \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                        9. *-lft-identityN/A

                                          \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                        10. fp-cancel-sub-sign-invN/A

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

                                          \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                        12. *-lft-identityN/A

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

                                          \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                        14. lower-neg.f64N/A

                                          \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                        15. lower--.f6499.7

                                          \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
                                        16. lift-*.f64N/A

                                          \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
                                        17. *-commutativeN/A

                                          \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                                        18. lower-*.f6499.7

                                          \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                                      4. Applied rewrites99.7%

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

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

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

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

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

                                          \[\leadsto \log \color{blue}{\left(1 - y\right)} \cdot z \]
                                      7. Applied rewrites3.7%

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

                                        \[\leadsto y \cdot \color{blue}{\left(-1 \cdot z + \frac{-1}{2} \cdot \left(y \cdot z\right)\right)} \]
                                      9. Step-by-step derivation
                                        1. Applied rewrites20.7%

                                          \[\leadsto \left(z \cdot \mathsf{fma}\left(-0.5, y, -1\right)\right) \cdot \color{blue}{y} \]
                                      10. Recombined 2 regimes into one program.
                                      11. Final simplification39.1%

                                        \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\ \;\;\;\;-t\\ \mathbf{else}:\\ \;\;\;\;\left(z \cdot \mathsf{fma}\left(-0.5, y, -1\right)\right) \cdot y\\ \end{array} \]
                                      12. Add Preprocessing

                                      Alternative 16: 46.6% accurate, 10.3× speedup?

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

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

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

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

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

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

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

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

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

                                        \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({y}^{2} \cdot \left(z - 1\right)\right)} - t \]
                                      7. Step-by-step derivation
                                        1. Applied rewrites29.7%

                                          \[\leadsto \left(\left(-0.5 \cdot \left(z - 1\right)\right) \cdot y\right) \cdot \color{blue}{y} - t \]
                                        2. Taylor expanded in z around inf

                                          \[\leadsto y \cdot \color{blue}{\left(z \cdot \left(\frac{-1}{2} \cdot y - 1\right)\right)} - t \]
                                        3. Step-by-step derivation
                                          1. Applied rewrites41.6%

                                            \[\leadsto \left(\left(-0.5 \cdot y - 1\right) \cdot y\right) \cdot \color{blue}{z} - t \]
                                          2. Add Preprocessing

                                          Alternative 17: 42.6% accurate, 11.3× speedup?

                                          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\ \;\;\;\;-t\\ \mathbf{else}:\\ \;\;\;\;\left(-y\right) \cdot z\\ \end{array} \end{array} \]
                                          (FPCore (x y z t)
                                           :precision binary64
                                           (if (or (<= t -3e+52) (not (<= t 14200.0))) (- t) (* (- y) z)))
                                          double code(double x, double y, double z, double t) {
                                          	double tmp;
                                          	if ((t <= -3e+52) || !(t <= 14200.0)) {
                                          		tmp = -t;
                                          	} else {
                                          		tmp = -y * z;
                                          	}
                                          	return tmp;
                                          }
                                          
                                          real(8) function code(x, y, z, t)
                                              real(8), intent (in) :: x
                                              real(8), intent (in) :: y
                                              real(8), intent (in) :: z
                                              real(8), intent (in) :: t
                                              real(8) :: tmp
                                              if ((t <= (-3d+52)) .or. (.not. (t <= 14200.0d0))) then
                                                  tmp = -t
                                              else
                                                  tmp = -y * z
                                              end if
                                              code = tmp
                                          end function
                                          
                                          public static double code(double x, double y, double z, double t) {
                                          	double tmp;
                                          	if ((t <= -3e+52) || !(t <= 14200.0)) {
                                          		tmp = -t;
                                          	} else {
                                          		tmp = -y * z;
                                          	}
                                          	return tmp;
                                          }
                                          
                                          def code(x, y, z, t):
                                          	tmp = 0
                                          	if (t <= -3e+52) or not (t <= 14200.0):
                                          		tmp = -t
                                          	else:
                                          		tmp = -y * z
                                          	return tmp
                                          
                                          function code(x, y, z, t)
                                          	tmp = 0.0
                                          	if ((t <= -3e+52) || !(t <= 14200.0))
                                          		tmp = Float64(-t);
                                          	else
                                          		tmp = Float64(Float64(-y) * z);
                                          	end
                                          	return tmp
                                          end
                                          
                                          function tmp_2 = code(x, y, z, t)
                                          	tmp = 0.0;
                                          	if ((t <= -3e+52) || ~((t <= 14200.0)))
                                          		tmp = -t;
                                          	else
                                          		tmp = -y * z;
                                          	end
                                          	tmp_2 = tmp;
                                          end
                                          
                                          code[x_, y_, z_, t_] := If[Or[LessEqual[t, -3e+52], N[Not[LessEqual[t, 14200.0]], $MachinePrecision]], (-t), N[((-y) * z), $MachinePrecision]]
                                          
                                          \begin{array}{l}
                                          
                                          \\
                                          \begin{array}{l}
                                          \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\
                                          \;\;\;\;-t\\
                                          
                                          \mathbf{else}:\\
                                          \;\;\;\;\left(-y\right) \cdot z\\
                                          
                                          
                                          \end{array}
                                          \end{array}
                                          
                                          Derivation
                                          1. Split input into 2 regimes
                                          2. if t < -3e52 or 14200 < t

                                            1. Initial program 94.8%

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

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

                                                \[\leadsto \color{blue}{\mathsf{neg}\left(t\right)} \]
                                              2. lower-neg.f6468.8

                                                \[\leadsto \color{blue}{-t} \]
                                            5. Applied rewrites68.8%

                                              \[\leadsto \color{blue}{-t} \]

                                            if -3e52 < t < 14200

                                            1. Initial program 80.8%

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

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

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

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

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

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

                                                \[\leadsto \color{blue}{\mathsf{fma}\left(z - 1, \log \left(1 - y\right), \left(x - 1\right) \cdot \log y - t\right)} \]
                                              7. lift-log.f64N/A

                                                \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\log \left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                              8. lift--.f64N/A

                                                \[\leadsto \mathsf{fma}\left(z - 1, \log \color{blue}{\left(1 - y\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                              9. *-lft-identityN/A

                                                \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 - \color{blue}{1 \cdot y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                              10. fp-cancel-sub-sign-invN/A

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

                                                \[\leadsto \mathsf{fma}\left(z - 1, \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot y\right)\right)}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                              12. *-lft-identityN/A

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

                                                \[\leadsto \mathsf{fma}\left(z - 1, \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(y\right)\right)}, \left(x - 1\right) \cdot \log y - t\right) \]
                                              14. lower-neg.f64N/A

                                                \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(\color{blue}{-y}\right), \left(x - 1\right) \cdot \log y - t\right) \]
                                              15. lower--.f6499.7

                                                \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y - t}\right) \]
                                              16. lift-*.f64N/A

                                                \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\left(x - 1\right) \cdot \log y} - t\right) \]
                                              17. *-commutativeN/A

                                                \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                                              18. lower-*.f6499.7

                                                \[\leadsto \mathsf{fma}\left(z - 1, \mathsf{log1p}\left(-y\right), \color{blue}{\log y \cdot \left(x - 1\right)} - t\right) \]
                                            4. Applied rewrites99.7%

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

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

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

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

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

                                                \[\leadsto \log \color{blue}{\left(1 - y\right)} \cdot z \]
                                            7. Applied rewrites3.7%

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

                                              \[\leadsto \left(-1 \cdot y\right) \cdot z \]
                                            9. Step-by-step derivation
                                              1. Applied rewrites20.5%

                                                \[\leadsto \left(-y\right) \cdot z \]
                                            10. Recombined 2 regimes into one program.
                                            11. Final simplification39.0%

                                              \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq -3 \cdot 10^{+52} \lor \neg \left(t \leq 14200\right):\\ \;\;\;\;-t\\ \mathbf{else}:\\ \;\;\;\;\left(-y\right) \cdot z\\ \end{array} \]
                                            12. Add Preprocessing

                                            Alternative 18: 36.2% accurate, 75.3× speedup?

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

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

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

                                                \[\leadsto \color{blue}{\mathsf{neg}\left(t\right)} \]
                                              2. lower-neg.f6428.9

                                                \[\leadsto \color{blue}{-t} \]
                                            5. Applied rewrites28.9%

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

                                            Reproduce

                                            ?
                                            herbie shell --seed 2024329 
                                            (FPCore (x y z t)
                                              :name "Statistics.Distribution.Beta:$cdensity from math-functions-0.1.5.2"
                                              :precision binary64
                                              (- (+ (* (- x 1.0) (log y)) (* (- z 1.0) (log (- 1.0 y)))) t))