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

Percentage Accurate: 89.6% → 99.8%
Time: 12.3s
Alternatives: 19
Speedup: 1.9×

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;
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z, t)
use fmin_fmax_functions
    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 19 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.6% 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;
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z, t)
use fmin_fmax_functions
    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, 0.7× speedup?

\[\begin{array}{l} \\ \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\left(-y\right) \cdot y\right) - \mathsf{log1p}\left(y\right)\right)\right) - t \end{array} \]
(FPCore (x y z t)
 :precision binary64
 (-
  (+ (* (- x 1.0) (log y)) (* (- z 1.0) (- (log1p (* (- y) y)) (log1p y))))
  t))
double code(double x, double y, double z, double t) {
	return (((x - 1.0) * log(y)) + ((z - 1.0) * (log1p((-y * y)) - log1p(y)))) - t;
}
public static double code(double x, double y, double z, double t) {
	return (((x - 1.0) * Math.log(y)) + ((z - 1.0) * (Math.log1p((-y * y)) - Math.log1p(y)))) - t;
}
def code(x, y, z, t):
	return (((x - 1.0) * math.log(y)) + ((z - 1.0) * (math.log1p((-y * y)) - math.log1p(y)))) - t
function code(x, y, z, t)
	return Float64(Float64(Float64(Float64(x - 1.0) * log(y)) + Float64(Float64(z - 1.0) * Float64(log1p(Float64(Float64(-y) * y)) - log1p(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[Log[1 + N[((-y) * y), $MachinePrecision]], $MachinePrecision] - N[Log[1 + y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - t), $MachinePrecision]
\begin{array}{l}

\\
\left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\left(-y\right) \cdot y\right) - \mathsf{log1p}\left(y\right)\right)\right) - t
\end{array}
Derivation
  1. Initial program 90.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-log.f64N/A

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

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

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

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

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

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

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

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

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

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

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

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

Alternative 2: 85.5% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \log y \cdot x - t\\ t_2 := \left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \log \left(1 - y\right)\\ \mathbf{if}\;t\_2 \leq -1 \cdot 10^{+48}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t\_2 \leq 150:\\ \;\;\;\;\mathsf{fma}\left(-y, z, y\right) - t\\ \mathbf{elif}\;t\_2 \leq 665:\\ \;\;\;\;\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))
        (t_2 (+ (* (- x 1.0) (log y)) (* (- z 1.0) (log (- 1.0 y))))))
   (if (<= t_2 -1e+48)
     t_1
     (if (<= t_2 150.0)
       (- (fma (- y) z y) t)
       (if (<= t_2 665.0) (- (- (log y)) t) t_1)))))
double code(double x, double y, double z, double t) {
	double t_1 = (log(y) * x) - t;
	double t_2 = ((x - 1.0) * log(y)) + ((z - 1.0) * log((1.0 - y)));
	double tmp;
	if (t_2 <= -1e+48) {
		tmp = t_1;
	} else if (t_2 <= 150.0) {
		tmp = fma(-y, z, y) - t;
	} else if (t_2 <= 665.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)
	t_2 = Float64(Float64(Float64(x - 1.0) * log(y)) + Float64(Float64(z - 1.0) * log(Float64(1.0 - y))))
	tmp = 0.0
	if (t_2 <= -1e+48)
		tmp = t_1;
	elseif (t_2 <= 150.0)
		tmp = Float64(fma(Float64(-y), z, y) - t);
	elseif (t_2 <= 665.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]}, Block[{t$95$2 = 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]}, If[LessEqual[t$95$2, -1e+48], t$95$1, If[LessEqual[t$95$2, 150.0], N[(N[((-y) * z + y), $MachinePrecision] - t), $MachinePrecision], If[LessEqual[t$95$2, 665.0], N[((-N[Log[y], $MachinePrecision]) - t), $MachinePrecision], t$95$1]]]]]
\begin{array}{l}

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

\mathbf{elif}\;t\_2 \leq 150:\\
\;\;\;\;\mathsf{fma}\left(-y, z, y\right) - t\\

\mathbf{elif}\;t\_2 \leq 665:\\
\;\;\;\;\left(-\log y\right) - t\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y)))) < -1.00000000000000004e48 or 665 < (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y))))

    1. Initial program 97.0%

      \[\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.f6492.7

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

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

    if -1.00000000000000004e48 < (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y)))) < 150

    1. Initial program 68.4%

      \[\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-*r*N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \left(y + -1 \cdot \color{blue}{\left(y \cdot z\right)}\right) - t \]
        3. Step-by-step derivation
          1. Applied rewrites76.4%

            \[\leadsto \mathsf{fma}\left(-y, z, y\right) - t \]

          if 150 < (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y)))) < 665

          1. Initial program 89.4%

            \[\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-log.f64N/A

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

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

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

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

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

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

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

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

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

              \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-y\right)} \cdot y\right) - \log \left(1 + y\right)\right)\right) - t \]
            11. lower-log1p.f64100.0

              \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\left(-y\right) \cdot y\right) - \color{blue}{\mathsf{log1p}\left(y\right)}\right)\right) - t \]
          4. Applied rewrites100.0%

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

            \[\leadsto \color{blue}{\log y \cdot \left(x - 1\right)} - t \]
          6. 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. mul-1-negN/A

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

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

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

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

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

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

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

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

              \[\leadsto \color{blue}{\log y} \cdot \left(x - 1\right) - t \]
            11. lower--.f6489.4

              \[\leadsto \log y \cdot \color{blue}{\left(x - 1\right)} - t \]
          7. Applied rewrites89.4%

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

            \[\leadsto \log y \cdot -1 - t \]
          9. Step-by-step derivation
            1. Applied rewrites89.4%

              \[\leadsto \log y \cdot -1 - t \]
            2. Taylor expanded in x around 0

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

                \[\leadsto \left(-\log y\right) - t \]
            4. Recombined 3 regimes into one program.
            5. Add Preprocessing

            Alternative 3: 74.7% accurate, 0.3× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} t_1 := \log y \cdot x\\ t_2 := \left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \log \left(1 - y\right)\\ \mathbf{if}\;t\_2 \leq -1 \cdot 10^{+102}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t\_2 \leq 150:\\ \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot z\right) \cdot y - t\\ \mathbf{elif}\;t\_2 \leq 10^{+142}:\\ \;\;\;\;\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_2 (+ (* (- x 1.0) (log y)) (* (- z 1.0) (log (- 1.0 y))))))
               (if (<= t_2 -1e+102)
                 t_1
                 (if (<= t_2 150.0)
                   (- (* (* (- (* -0.5 y) 1.0) z) y) t)
                   (if (<= t_2 1e+142) (- (- (log y)) t) t_1)))))
            double code(double x, double y, double z, double t) {
            	double t_1 = log(y) * x;
            	double t_2 = ((x - 1.0) * log(y)) + ((z - 1.0) * log((1.0 - y)));
            	double tmp;
            	if (t_2 <= -1e+102) {
            		tmp = t_1;
            	} else if (t_2 <= 150.0) {
            		tmp = ((((-0.5 * y) - 1.0) * z) * y) - t;
            	} else if (t_2 <= 1e+142) {
            		tmp = -log(y) - t;
            	} else {
            		tmp = t_1;
            	}
            	return tmp;
            }
            
            module fmin_fmax_functions
                implicit none
                private
                public fmax
                public fmin
            
                interface fmax
                    module procedure fmax88
                    module procedure fmax44
                    module procedure fmax84
                    module procedure fmax48
                end interface
                interface fmin
                    module procedure fmin88
                    module procedure fmin44
                    module procedure fmin84
                    module procedure fmin48
                end interface
            contains
                real(8) function fmax88(x, y) result (res)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                end function
                real(4) function fmax44(x, y) result (res)
                    real(4), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                end function
                real(8) function fmax84(x, y) result(res)
                    real(8), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                end function
                real(8) function fmax48(x, y) result(res)
                    real(4), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                end function
                real(8) function fmin88(x, y) result (res)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                end function
                real(4) function fmin44(x, y) result (res)
                    real(4), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                end function
                real(8) function fmin84(x, y) result(res)
                    real(8), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                end function
                real(8) function fmin48(x, y) result(res)
                    real(4), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                end function
            end module
            
            real(8) function code(x, y, z, t)
            use fmin_fmax_functions
                real(8), intent (in) :: x
                real(8), intent (in) :: y
                real(8), intent (in) :: z
                real(8), intent (in) :: t
                real(8) :: t_1
                real(8) :: t_2
                real(8) :: tmp
                t_1 = log(y) * x
                t_2 = ((x - 1.0d0) * log(y)) + ((z - 1.0d0) * log((1.0d0 - y)))
                if (t_2 <= (-1d+102)) then
                    tmp = t_1
                else if (t_2 <= 150.0d0) then
                    tmp = (((((-0.5d0) * y) - 1.0d0) * z) * y) - t
                else if (t_2 <= 1d+142) then
                    tmp = -log(y) - t
                else
                    tmp = t_1
                end if
                code = tmp
            end function
            
            public static double code(double x, double y, double z, double t) {
            	double t_1 = Math.log(y) * x;
            	double t_2 = ((x - 1.0) * Math.log(y)) + ((z - 1.0) * Math.log((1.0 - y)));
            	double tmp;
            	if (t_2 <= -1e+102) {
            		tmp = t_1;
            	} else if (t_2 <= 150.0) {
            		tmp = ((((-0.5 * y) - 1.0) * z) * y) - t;
            	} else if (t_2 <= 1e+142) {
            		tmp = -Math.log(y) - t;
            	} else {
            		tmp = t_1;
            	}
            	return tmp;
            }
            
            def code(x, y, z, t):
            	t_1 = math.log(y) * x
            	t_2 = ((x - 1.0) * math.log(y)) + ((z - 1.0) * math.log((1.0 - y)))
            	tmp = 0
            	if t_2 <= -1e+102:
            		tmp = t_1
            	elif t_2 <= 150.0:
            		tmp = ((((-0.5 * y) - 1.0) * z) * y) - t
            	elif t_2 <= 1e+142:
            		tmp = -math.log(y) - t
            	else:
            		tmp = t_1
            	return tmp
            
            function code(x, y, z, t)
            	t_1 = Float64(log(y) * x)
            	t_2 = Float64(Float64(Float64(x - 1.0) * log(y)) + Float64(Float64(z - 1.0) * log(Float64(1.0 - y))))
            	tmp = 0.0
            	if (t_2 <= -1e+102)
            		tmp = t_1;
            	elseif (t_2 <= 150.0)
            		tmp = Float64(Float64(Float64(Float64(Float64(-0.5 * y) - 1.0) * z) * y) - t);
            	elseif (t_2 <= 1e+142)
            		tmp = Float64(Float64(-log(y)) - t);
            	else
            		tmp = t_1;
            	end
            	return tmp
            end
            
            function tmp_2 = code(x, y, z, t)
            	t_1 = log(y) * x;
            	t_2 = ((x - 1.0) * log(y)) + ((z - 1.0) * log((1.0 - y)));
            	tmp = 0.0;
            	if (t_2 <= -1e+102)
            		tmp = t_1;
            	elseif (t_2 <= 150.0)
            		tmp = ((((-0.5 * y) - 1.0) * z) * y) - t;
            	elseif (t_2 <= 1e+142)
            		tmp = -log(y) - t;
            	else
            		tmp = t_1;
            	end
            	tmp_2 = tmp;
            end
            
            code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[Log[y], $MachinePrecision] * x), $MachinePrecision]}, Block[{t$95$2 = 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]}, If[LessEqual[t$95$2, -1e+102], t$95$1, If[LessEqual[t$95$2, 150.0], N[(N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * z), $MachinePrecision] * y), $MachinePrecision] - t), $MachinePrecision], If[LessEqual[t$95$2, 1e+142], N[((-N[Log[y], $MachinePrecision]) - t), $MachinePrecision], t$95$1]]]]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            t_1 := \log y \cdot x\\
            t_2 := \left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \log \left(1 - y\right)\\
            \mathbf{if}\;t\_2 \leq -1 \cdot 10^{+102}:\\
            \;\;\;\;t\_1\\
            
            \mathbf{elif}\;t\_2 \leq 150:\\
            \;\;\;\;\left(\left(-0.5 \cdot y - 1\right) \cdot z\right) \cdot y - t\\
            
            \mathbf{elif}\;t\_2 \leq 10^{+142}:\\
            \;\;\;\;\left(-\log y\right) - t\\
            
            \mathbf{else}:\\
            \;\;\;\;t\_1\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 3 regimes
            2. if (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y)))) < -9.99999999999999977e101 or 1.00000000000000005e142 < (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y))))

              1. Initial program 95.6%

                \[\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-log.f64N/A

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

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

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

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

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

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

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

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

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

                  \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-y\right)} \cdot y\right) - \log \left(1 + y\right)\right)\right) - t \]
                11. lower-log1p.f6499.5

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

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

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

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

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

                \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\color{blue}{\left(\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.25 \cdot y, y, -0.3333333333333333\right), y \cdot y, -0.5\right) \cdot y\right) \cdot y - 1\right) \cdot \left(y \cdot y\right)} - \mathsf{log1p}\left(y\right)\right)\right) - t \]
              8. Step-by-step derivation
                1. lift--.f64N/A

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

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

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

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

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

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

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

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

                  \[\leadsto \left(\mathsf{neg}\left(\color{blue}{-1 \cdot \log y}\right)\right) \cdot x \]
                4. distribute-rgt-neg-inN/A

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

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

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

                  \[\leadsto \left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \cdot x \]
                8. distribute-rgt-neg-inN/A

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

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

                  \[\leadsto \color{blue}{\log y} \cdot x \]
                11. lower-log.f6476.8

                  \[\leadsto \color{blue}{\log y} \cdot x \]
              12. Applied rewrites76.8%

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

              if -9.99999999999999977e101 < (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y)))) < 150

              1. Initial program 78.0%

                \[\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-log.f64N/A

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

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

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

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

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

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

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

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

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

                  \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-y\right)} \cdot y\right) - \log \left(1 + y\right)\right)\right) - t \]
                11. lower-log1p.f6499.9

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

                \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \color{blue}{\left(\mathsf{log1p}\left(\left(-y\right) \cdot y\right) - \mathsf{log1p}\left(y\right)\right)}\right) - t \]
              5. 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 \]
              6. Step-by-step derivation
                1. *-commutativeN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                if 150 < (+.f64 (*.f64 (-.f64 x #s(literal 1 binary64)) (log.f64 y)) (*.f64 (-.f64 z #s(literal 1 binary64)) (log.f64 (-.f64 #s(literal 1 binary64) y)))) < 1.00000000000000005e142

                1. Initial program 92.6%

                  \[\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-log.f64N/A

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

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

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

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

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

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

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

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

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

                    \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-y\right)} \cdot y\right) - \log \left(1 + y\right)\right)\right) - t \]
                  11. lower-log1p.f64100.0

                    \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{log1p}\left(\left(-y\right) \cdot y\right) - \color{blue}{\mathsf{log1p}\left(y\right)}\right)\right) - t \]
                4. Applied rewrites100.0%

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

                  \[\leadsto \color{blue}{\log y \cdot \left(x - 1\right)} - t \]
                6. 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. mul-1-negN/A

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

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

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

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

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

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

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

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

                    \[\leadsto \color{blue}{\log y} \cdot \left(x - 1\right) - t \]
                  11. lower--.f6492.6

                    \[\leadsto \log y \cdot \color{blue}{\left(x - 1\right)} - t \]
                7. Applied rewrites92.6%

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

                  \[\leadsto \log y \cdot -1 - t \]
                9. Step-by-step derivation
                  1. Applied rewrites81.5%

                    \[\leadsto \log y \cdot -1 - t \]
                  2. Taylor expanded in x around 0

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

                      \[\leadsto \left(-\log y\right) - t \]
                  4. Recombined 3 regimes into one program.
                  5. Add Preprocessing

                  Alternative 4: 99.7% accurate, 0.8× speedup?

                  \[\begin{array}{l} \\ \mathsf{fma}\left(\left(\mathsf{fma}\left(\mathsf{fma}\left(y \cdot y, \mathsf{fma}\left(-0.25 \cdot y, y, -0.3333333333333333\right), -0.5\right) \cdot y, y, -1\right) \cdot y\right) \cdot y - \mathsf{log1p}\left(y\right), z - 1, \log y \cdot \left(x - 1\right) - t\right) \end{array} \]
                  (FPCore (x y z t)
                   :precision binary64
                   (fma
                    (-
                     (*
                      (*
                       (fma
                        (* (fma (* y y) (fma (* -0.25 y) y -0.3333333333333333) -0.5) y)
                        y
                        -1.0)
                       y)
                      y)
                     (log1p y))
                    (- z 1.0)
                    (- (* (log y) (- x 1.0)) t)))
                  double code(double x, double y, double z, double t) {
                  	return fma((((fma((fma((y * y), fma((-0.25 * y), y, -0.3333333333333333), -0.5) * y), y, -1.0) * y) * y) - log1p(y)), (z - 1.0), ((log(y) * (x - 1.0)) - t));
                  }
                  
                  function code(x, y, z, t)
                  	return fma(Float64(Float64(Float64(fma(Float64(fma(Float64(y * y), fma(Float64(-0.25 * y), y, -0.3333333333333333), -0.5) * y), y, -1.0) * y) * y) - log1p(y)), Float64(z - 1.0), Float64(Float64(log(y) * Float64(x - 1.0)) - t))
                  end
                  
                  code[x_, y_, z_, t_] := N[(N[(N[(N[(N[(N[(N[(N[(y * y), $MachinePrecision] * N[(N[(-0.25 * y), $MachinePrecision] * y + -0.3333333333333333), $MachinePrecision] + -0.5), $MachinePrecision] * y), $MachinePrecision] * y + -1.0), $MachinePrecision] * y), $MachinePrecision] * y), $MachinePrecision] - N[Log[1 + y], $MachinePrecision]), $MachinePrecision] * N[(z - 1.0), $MachinePrecision] + N[(N[(N[Log[y], $MachinePrecision] * N[(x - 1.0), $MachinePrecision]), $MachinePrecision] - t), $MachinePrecision]), $MachinePrecision]
                  
                  \begin{array}{l}
                  
                  \\
                  \mathsf{fma}\left(\left(\mathsf{fma}\left(\mathsf{fma}\left(y \cdot y, \mathsf{fma}\left(-0.25 \cdot y, y, -0.3333333333333333\right), -0.5\right) \cdot y, y, -1\right) \cdot y\right) \cdot y - \mathsf{log1p}\left(y\right), z - 1, \log y \cdot \left(x - 1\right) - t\right)
                  \end{array}
                  
                  Derivation
                  1. Initial program 90.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-log.f64N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                    \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\color{blue}{\left(\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.25 \cdot y, y, -0.3333333333333333\right), y \cdot y, -0.5\right) \cdot y\right) \cdot y - 1\right) \cdot \left(y \cdot y\right)} - \mathsf{log1p}\left(y\right)\right)\right) - t \]
                  8. Step-by-step derivation
                    1. lift--.f64N/A

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

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

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

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

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

                  Alternative 5: 99.6% accurate, 1.5× speedup?

                  \[\begin{array}{l} \\ \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.25, y, -0.3333333333333333\right), y, -0.5\right), 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)
                      (* (fma (fma (fma -0.25 y -0.3333333333333333) y -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) * (fma(fma(fma(-0.25, y, -0.3333333333333333), y, -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(fma(fma(fma(-0.25, y, -0.3333333333333333), y, -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[(N[(-0.25 * y + -0.3333333333333333), $MachinePrecision] * y + -0.5), $MachinePrecision] * y + -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(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.25, y, -0.3333333333333333\right), y, -0.5\right), y, -1\right) \cdot y\right)\right) - t
                  \end{array}
                  
                  Derivation
                  1. Initial program 90.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 \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \color{blue}{\left(y \cdot \left(y \cdot \left(y \cdot \left(\frac{-1}{4} \cdot y - \frac{1}{3}\right) - \frac{1}{2}\right) - 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(y \cdot \left(y \cdot \left(\frac{-1}{4} \cdot y - \frac{1}{3}\right) - \frac{1}{2}\right) - 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(y \cdot \left(y \cdot \left(\frac{-1}{4} \cdot y - \frac{1}{3}\right) - \frac{1}{2}\right) - 1\right) \cdot y\right)}\right) - t \]
                  5. Applied rewrites99.7%

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

                  Alternative 6: 99.5% accurate, 1.6× speedup?

                  \[\begin{array}{l} \\ \mathsf{fma}\left(\log y, x - 1, \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
                     (log y)
                     (- x 1.0)
                     (* (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(log(y), (x - 1.0), (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(log(y), Float64(x - 1.0), 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[Log[y], $MachinePrecision] * N[(x - 1.0), $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(\log y, x - 1, \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 90.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}{\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 \]
                    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) + 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 \]
                    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) + 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 \]
                    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) + 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. 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) + 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 \]
                    6. log-recN/A

                      \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)} \cdot \left(x - 1\right)\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 \]
                    7. mul-1-negN/A

                      \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(-1 \cdot \log y\right)} \cdot \left(x - 1\right)\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 \]
                    8. associate-*r*N/A

                      \[\leadsto \left(\color{blue}{\left(-1 \cdot \left(-1 \cdot \log y\right)\right) \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 \]
                    9. mul-1-negN/A

                      \[\leadsto \left(\left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \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 \]
                    10. log-recN/A

                      \[\leadsto \left(\left(-1 \cdot \color{blue}{\log \left(\frac{1}{y}\right)}\right) \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 \]
                    11. lower-fma.f64N/A

                      \[\leadsto \color{blue}{\mathsf{fma}\left(-1 \cdot \log \left(\frac{1}{y}\right), x - 1, 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.6%

                    \[\leadsto \color{blue}{\mathsf{fma}\left(\log y, x - 1, \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 7: 99.5% accurate, 1.6× speedup?

                  \[\begin{array}{l} \\ \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\mathsf{fma}\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right), 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) (* (fma (fma -0.3333333333333333 y -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) * (fma(fma(-0.3333333333333333, y, -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(fma(fma(-0.3333333333333333, y, -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.3333333333333333 * y + -0.5), $MachinePrecision] * y + -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(\mathsf{fma}\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right), y, -1\right) \cdot y\right)\right) - t
                  \end{array}
                  
                  Derivation
                  1. Initial program 90.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 \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \color{blue}{\left(y \cdot \left(y \cdot \left(\frac{-1}{3} \cdot y - \frac{1}{2}\right) - 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(y \cdot \left(\frac{-1}{3} \cdot y - \frac{1}{2}\right) - 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(y \cdot \left(\frac{-1}{3} \cdot y - \frac{1}{2}\right) - 1\right) \cdot y\right)}\right) - t \]
                    3. metadata-evalN/A

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

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

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

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

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

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

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

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

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

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

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

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

                  Alternative 8: 99.4% accurate, 1.7× speedup?

                  \[\begin{array}{l} \\ \mathsf{fma}\left(\left(z - 1\right) \cdot \mathsf{fma}\left(-0.5, y, -1\right), y, \log y \cdot \left(x - 1\right)\right) - t \end{array} \]
                  (FPCore (x y z t)
                   :precision binary64
                   (- (fma (* (- z 1.0) (fma -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) * fma(-0.5, y, -1.0)), y, (log(y) * (x - 1.0))) - t;
                  }
                  
                  function code(x, y, z, t)
                  	return Float64(fma(Float64(Float64(z - 1.0) * fma(-0.5, y, -1.0)), y, Float64(log(y) * Float64(x - 1.0))) - t)
                  end
                  
                  code[x_, y_, z_, t_] := N[(N[(N[(N[(z - 1.0), $MachinePrecision] * N[(-0.5 * y + -1.0), $MachinePrecision]), $MachinePrecision] * y + N[(N[Log[y], $MachinePrecision] * N[(x - 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - t), $MachinePrecision]
                  
                  \begin{array}{l}
                  
                  \\
                  \mathsf{fma}\left(\left(z - 1\right) \cdot \mathsf{fma}\left(-0.5, y, -1\right), y, \log y \cdot \left(x - 1\right)\right) - t
                  \end{array}
                  
                  Derivation
                  1. Initial program 90.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-log.f64N/A

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

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

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

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

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

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

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

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

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

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

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

                    \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \color{blue}{\left(\mathsf{log1p}\left(\left(-y\right) \cdot y\right) - \mathsf{log1p}\left(y\right)\right)}\right) - t \]
                  5. 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 \]
                  6. Step-by-step derivation
                    1. *-commutativeN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                  Alternative 9: 99.4% accurate, 1.7× speedup?

                  \[\begin{array}{l} \\ \mathsf{fma}\left(\log y, x - 1, \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 (log y) (- x 1.0) (* (* (- z 1.0) y) (fma -0.5 y -1.0))) t))
                  double code(double x, double y, double z, double t) {
                  	return fma(log(y), (x - 1.0), (((z - 1.0) * y) * fma(-0.5, y, -1.0))) - t;
                  }
                  
                  function code(x, y, z, t)
                  	return Float64(fma(log(y), Float64(x - 1.0), Float64(Float64(Float64(z - 1.0) * y) * fma(-0.5, y, -1.0))) - t)
                  end
                  
                  code[x_, y_, z_, t_] := N[(N[(N[Log[y], $MachinePrecision] * N[(x - 1.0), $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(\log y, x - 1, \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 90.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}{\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 \]
                    6. log-recN/A

                      \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\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 \]
                    7. mul-1-negN/A

                      \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(-1 \cdot \log 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 \]
                    8. associate-*r*N/A

                      \[\leadsto \left(\color{blue}{\left(-1 \cdot \left(-1 \cdot \log y\right)\right) \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 \]
                    9. mul-1-negN/A

                      \[\leadsto \left(\left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \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 \]
                    10. log-recN/A

                      \[\leadsto \left(\left(-1 \cdot \color{blue}{\log \left(\frac{1}{y}\right)}\right) \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 \]
                    11. lower-fma.f64N/A

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

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

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

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

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

                      \[\leadsto \mathsf{fma}\left(\log y, \color{blue}{x - 1}, 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.3%

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

                  Alternative 10: 95.0% accurate, 1.8× speedup?

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

                    1. Initial program 98.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}{\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. lower-*.f64N/A

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

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

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

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

                        \[\leadsto \color{blue}{\log y} \cdot \left(x - 1\right) - t \]
                      9. lower--.f6496.6

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

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

                    if -1e3 < x < 1.85000000000000006e39

                    1. Initial program 83.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 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-*r*N/A

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

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

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

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

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

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

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

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

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

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

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

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

                        \[\leadsto \mathsf{fma}\left(-y, z - 1, \color{blue}{\log y} \cdot \left(x - 1\right)\right) - t \]
                      14. lower--.f6498.4

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

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

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

                        \[\leadsto \left(-\mathsf{fma}\left(z - 1, y, \log y\right)\right) - t \]

                      if 1.85000000000000006e39 < x

                      1. Initial program 99.4%

                        \[\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.f6497.7

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

                        \[\leadsto \color{blue}{\log y \cdot x} - t \]
                    8. Recombined 3 regimes into one program.
                    9. Add Preprocessing

                    Alternative 11: 65.2% accurate, 1.8× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x - 1 \leq -4 \cdot 10^{+144} \lor \neg \left(x - 1 \leq 5 \cdot 10^{+98}\right):\\ \;\;\;\;\log y \cdot x\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right) \cdot y - 1\right) \cdot z\right) \cdot y - t\\ \end{array} \end{array} \]
                    (FPCore (x y z t)
                     :precision binary64
                     (if (or (<= (- x 1.0) -4e+144) (not (<= (- x 1.0) 5e+98)))
                       (* (log y) x)
                       (- (* (* (- (* (fma -0.3333333333333333 y -0.5) y) 1.0) z) y) t)))
                    double code(double x, double y, double z, double t) {
                    	double tmp;
                    	if (((x - 1.0) <= -4e+144) || !((x - 1.0) <= 5e+98)) {
                    		tmp = log(y) * x;
                    	} else {
                    		tmp = ((((fma(-0.3333333333333333, y, -0.5) * y) - 1.0) * z) * y) - t;
                    	}
                    	return tmp;
                    }
                    
                    function code(x, y, z, t)
                    	tmp = 0.0
                    	if ((Float64(x - 1.0) <= -4e+144) || !(Float64(x - 1.0) <= 5e+98))
                    		tmp = Float64(log(y) * x);
                    	else
                    		tmp = Float64(Float64(Float64(Float64(Float64(fma(-0.3333333333333333, y, -0.5) * y) - 1.0) * z) * y) - t);
                    	end
                    	return tmp
                    end
                    
                    code[x_, y_, z_, t_] := If[Or[LessEqual[N[(x - 1.0), $MachinePrecision], -4e+144], N[Not[LessEqual[N[(x - 1.0), $MachinePrecision], 5e+98]], $MachinePrecision]], N[(N[Log[y], $MachinePrecision] * x), $MachinePrecision], N[(N[(N[(N[(N[(N[(-0.3333333333333333 * y + -0.5), $MachinePrecision] * y), $MachinePrecision] - 1.0), $MachinePrecision] * z), $MachinePrecision] * y), $MachinePrecision] - t), $MachinePrecision]]
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    \mathbf{if}\;x - 1 \leq -4 \cdot 10^{+144} \lor \neg \left(x - 1 \leq 5 \cdot 10^{+98}\right):\\
                    \;\;\;\;\log y \cdot x\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;\left(\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right) \cdot y - 1\right) \cdot z\right) \cdot y - t\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 2 regimes
                    2. if (-.f64 x #s(literal 1 binary64)) < -4.00000000000000009e144 or 4.9999999999999998e98 < (-.f64 x #s(literal 1 binary64))

                      1. Initial program 99.3%

                        \[\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-log.f64N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                        \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \left(\color{blue}{\left(\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.25 \cdot y, y, -0.3333333333333333\right), y \cdot y, -0.5\right) \cdot y\right) \cdot y - 1\right) \cdot \left(y \cdot y\right)} - \mathsf{log1p}\left(y\right)\right)\right) - t \]
                      8. Step-by-step derivation
                        1. lift--.f64N/A

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

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

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

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

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

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

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

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

                          \[\leadsto \left(\mathsf{neg}\left(\color{blue}{-1 \cdot \log y}\right)\right) \cdot x \]
                        4. distribute-rgt-neg-inN/A

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

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

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

                          \[\leadsto \left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \cdot x \]
                        8. distribute-rgt-neg-inN/A

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

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

                          \[\leadsto \color{blue}{\log y} \cdot x \]
                        11. lower-log.f6483.8

                          \[\leadsto \color{blue}{\log y} \cdot x \]
                      12. Applied rewrites83.8%

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

                      if -4.00000000000000009e144 < (-.f64 x #s(literal 1 binary64)) < 4.9999999999999998e98

                      1. Initial program 87.4%

                        \[\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 \]
                        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) + 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 \]
                        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) + 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 \]
                        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) + 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. 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) + 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 \]
                        6. log-recN/A

                          \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)} \cdot \left(x - 1\right)\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 \]
                        7. mul-1-negN/A

                          \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(-1 \cdot \log y\right)} \cdot \left(x - 1\right)\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 \]
                        8. associate-*r*N/A

                          \[\leadsto \left(\color{blue}{\left(-1 \cdot \left(-1 \cdot \log y\right)\right) \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 \]
                        9. mul-1-negN/A

                          \[\leadsto \left(\left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \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 \]
                        10. log-recN/A

                          \[\leadsto \left(\left(-1 \cdot \color{blue}{\log \left(\frac{1}{y}\right)}\right) \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 \]
                        11. lower-fma.f64N/A

                          \[\leadsto \color{blue}{\mathsf{fma}\left(-1 \cdot \log \left(\frac{1}{y}\right), x - 1, 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.8%

                        \[\leadsto \color{blue}{\mathsf{fma}\left(\log y, x - 1, \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. Taylor expanded in z around inf

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

                          \[\leadsto \left(\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right) \cdot y - 1\right) \cdot z\right) \cdot \color{blue}{y} - t \]
                      8. Recombined 2 regimes into one program.
                      9. Final simplification72.2%

                        \[\leadsto \begin{array}{l} \mathbf{if}\;x - 1 \leq -4 \cdot 10^{+144} \lor \neg \left(x - 1 \leq 5 \cdot 10^{+98}\right):\\ \;\;\;\;\log y \cdot x\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right) \cdot y - 1\right) \cdot z\right) \cdot y - t\\ \end{array} \]
                      10. Add Preprocessing

                      Alternative 12: 99.0% accurate, 1.9× speedup?

                      \[\begin{array}{l} \\ \mathsf{fma}\left(\log y, x - 1, \left(1 - z\right) \cdot y\right) - t \end{array} \]
                      (FPCore (x y z t)
                       :precision binary64
                       (- (fma (log y) (- x 1.0) (* (- 1.0 z) y)) t))
                      double code(double x, double y, double z, double t) {
                      	return fma(log(y), (x - 1.0), ((1.0 - z) * y)) - t;
                      }
                      
                      function code(x, y, z, t)
                      	return Float64(fma(log(y), Float64(x - 1.0), Float64(Float64(1.0 - z) * y)) - t)
                      end
                      
                      code[x_, y_, z_, t_] := N[(N[(N[Log[y], $MachinePrecision] * N[(x - 1.0), $MachinePrecision] + N[(N[(1.0 - z), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision] - t), $MachinePrecision]
                      
                      \begin{array}{l}
                      
                      \\
                      \mathsf{fma}\left(\log y, x - 1, \left(1 - z\right) \cdot y\right) - t
                      \end{array}
                      
                      Derivation
                      1. Initial program 90.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}{\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 \]
                        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) + 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 \]
                        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) + 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 \]
                        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) + 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. 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) + 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 \]
                        6. log-recN/A

                          \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)} \cdot \left(x - 1\right)\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 \]
                        7. mul-1-negN/A

                          \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(-1 \cdot \log y\right)} \cdot \left(x - 1\right)\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 \]
                        8. associate-*r*N/A

                          \[\leadsto \left(\color{blue}{\left(-1 \cdot \left(-1 \cdot \log y\right)\right) \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 \]
                        9. mul-1-negN/A

                          \[\leadsto \left(\left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \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 \]
                        10. log-recN/A

                          \[\leadsto \left(\left(-1 \cdot \color{blue}{\log \left(\frac{1}{y}\right)}\right) \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 \]
                        11. lower-fma.f64N/A

                          \[\leadsto \color{blue}{\mathsf{fma}\left(-1 \cdot \log \left(\frac{1}{y}\right), x - 1, 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.6%

                        \[\leadsto \color{blue}{\mathsf{fma}\left(\log y, x - 1, \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. Taylor expanded in y around 0

                        \[\leadsto \mathsf{fma}\left(\log y, x - 1, \left(1 - z\right) \cdot y\right) - t \]
                      7. Step-by-step derivation
                        1. Applied rewrites98.5%

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

                        Alternative 13: 89.1% accurate, 1.9× speedup?

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

                          1. Initial program 50.4%

                            \[\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 \]
                            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) + 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 \]
                            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) + 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 \]
                            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) + 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. 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) + 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 \]
                            6. log-recN/A

                              \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)} \cdot \left(x - 1\right)\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 \]
                            7. mul-1-negN/A

                              \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(-1 \cdot \log y\right)} \cdot \left(x - 1\right)\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 \]
                            8. associate-*r*N/A

                              \[\leadsto \left(\color{blue}{\left(-1 \cdot \left(-1 \cdot \log y\right)\right) \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 \]
                            9. mul-1-negN/A

                              \[\leadsto \left(\left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \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 \]
                            10. log-recN/A

                              \[\leadsto \left(\left(-1 \cdot \color{blue}{\log \left(\frac{1}{y}\right)}\right) \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 \]
                            11. lower-fma.f64N/A

                              \[\leadsto \color{blue}{\mathsf{fma}\left(-1 \cdot \log \left(\frac{1}{y}\right), x - 1, 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 rewrites97.8%

                            \[\leadsto \color{blue}{\mathsf{fma}\left(\log y, x - 1, \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. Taylor expanded in z around inf

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

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

                            if -2.5e179 < z

                            1. Initial program 95.6%

                              \[\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-*r*N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                            Alternative 14: 89.0% accurate, 1.9× speedup?

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

                              1. Initial program 50.4%

                                \[\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 \]
                                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) + 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 \]
                                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) + 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 \]
                                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) + 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. 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) + 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 \]
                                6. log-recN/A

                                  \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)} \cdot \left(x - 1\right)\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 \]
                                7. mul-1-negN/A

                                  \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(-1 \cdot \log y\right)} \cdot \left(x - 1\right)\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 \]
                                8. associate-*r*N/A

                                  \[\leadsto \left(\color{blue}{\left(-1 \cdot \left(-1 \cdot \log y\right)\right) \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 \]
                                9. mul-1-negN/A

                                  \[\leadsto \left(\left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \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 \]
                                10. log-recN/A

                                  \[\leadsto \left(\left(-1 \cdot \color{blue}{\log \left(\frac{1}{y}\right)}\right) \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 \]
                                11. lower-fma.f64N/A

                                  \[\leadsto \color{blue}{\mathsf{fma}\left(-1 \cdot \log \left(\frac{1}{y}\right), x - 1, 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 rewrites97.8%

                                \[\leadsto \color{blue}{\mathsf{fma}\left(\log y, x - 1, \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. Taylor expanded in z around inf

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

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

                                if -2.5e179 < z

                                1. Initial program 95.6%

                                  \[\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. lower-*.f64N/A

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

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

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

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

                                    \[\leadsto \color{blue}{\log y} \cdot \left(x - 1\right) - t \]
                                  9. lower--.f6494.0

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

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

                              Alternative 15: 46.2% accurate, 8.1× speedup?

                              \[\begin{array}{l} \\ \left(\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right) \cdot y - 1\right) \cdot z\right) \cdot y - t \end{array} \]
                              (FPCore (x y z t)
                               :precision binary64
                               (- (* (* (- (* (fma -0.3333333333333333 y -0.5) y) 1.0) z) y) t))
                              double code(double x, double y, double z, double t) {
                              	return ((((fma(-0.3333333333333333, y, -0.5) * y) - 1.0) * z) * y) - t;
                              }
                              
                              function code(x, y, z, t)
                              	return Float64(Float64(Float64(Float64(Float64(fma(-0.3333333333333333, y, -0.5) * y) - 1.0) * z) * y) - t)
                              end
                              
                              code[x_, y_, z_, t_] := N[(N[(N[(N[(N[(N[(-0.3333333333333333 * y + -0.5), $MachinePrecision] * y), $MachinePrecision] - 1.0), $MachinePrecision] * z), $MachinePrecision] * y), $MachinePrecision] - t), $MachinePrecision]
                              
                              \begin{array}{l}
                              
                              \\
                              \left(\left(\mathsf{fma}\left(-0.3333333333333333, y, -0.5\right) \cdot y - 1\right) \cdot z\right) \cdot y - t
                              \end{array}
                              
                              Derivation
                              1. Initial program 90.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}{\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 \]
                                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) + 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 \]
                                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) + 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 \]
                                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) + 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. 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) + 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 \]
                                6. log-recN/A

                                  \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)} \cdot \left(x - 1\right)\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 \]
                                7. mul-1-negN/A

                                  \[\leadsto \left(-1 \cdot \left(\color{blue}{\left(-1 \cdot \log y\right)} \cdot \left(x - 1\right)\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 \]
                                8. associate-*r*N/A

                                  \[\leadsto \left(\color{blue}{\left(-1 \cdot \left(-1 \cdot \log y\right)\right) \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 \]
                                9. mul-1-negN/A

                                  \[\leadsto \left(\left(-1 \cdot \color{blue}{\left(\mathsf{neg}\left(\log y\right)\right)}\right) \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 \]
                                10. log-recN/A

                                  \[\leadsto \left(\left(-1 \cdot \color{blue}{\log \left(\frac{1}{y}\right)}\right) \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 \]
                                11. lower-fma.f64N/A

                                  \[\leadsto \color{blue}{\mathsf{fma}\left(-1 \cdot \log \left(\frac{1}{y}\right), x - 1, 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.6%

                                \[\leadsto \color{blue}{\mathsf{fma}\left(\log y, x - 1, \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. Taylor expanded in z around inf

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

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

                                Alternative 16: 46.1% accurate, 10.3× speedup?

                                \[\begin{array}{l} \\ \left(\left(-0.5 \cdot y - 1\right) \cdot z\right) \cdot y - t \end{array} \]
                                (FPCore (x y z t) :precision binary64 (- (* (* (- (* -0.5 y) 1.0) z) y) t))
                                double code(double x, double y, double z, double t) {
                                	return ((((-0.5 * y) - 1.0) * z) * y) - t;
                                }
                                
                                module fmin_fmax_functions
                                    implicit none
                                    private
                                    public fmax
                                    public fmin
                                
                                    interface fmax
                                        module procedure fmax88
                                        module procedure fmax44
                                        module procedure fmax84
                                        module procedure fmax48
                                    end interface
                                    interface fmin
                                        module procedure fmin88
                                        module procedure fmin44
                                        module procedure fmin84
                                        module procedure fmin48
                                    end interface
                                contains
                                    real(8) function fmax88(x, y) result (res)
                                        real(8), intent (in) :: x
                                        real(8), intent (in) :: y
                                        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                    end function
                                    real(4) function fmax44(x, y) result (res)
                                        real(4), intent (in) :: x
                                        real(4), intent (in) :: y
                                        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                    end function
                                    real(8) function fmax84(x, y) result(res)
                                        real(8), intent (in) :: x
                                        real(4), intent (in) :: y
                                        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                                    end function
                                    real(8) function fmax48(x, y) result(res)
                                        real(4), intent (in) :: x
                                        real(8), intent (in) :: y
                                        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                                    end function
                                    real(8) function fmin88(x, y) result (res)
                                        real(8), intent (in) :: x
                                        real(8), intent (in) :: y
                                        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                    end function
                                    real(4) function fmin44(x, y) result (res)
                                        real(4), intent (in) :: x
                                        real(4), intent (in) :: y
                                        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                    end function
                                    real(8) function fmin84(x, y) result(res)
                                        real(8), intent (in) :: x
                                        real(4), intent (in) :: y
                                        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                                    end function
                                    real(8) function fmin48(x, y) result(res)
                                        real(4), intent (in) :: x
                                        real(8), intent (in) :: y
                                        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                                    end function
                                end module
                                
                                real(8) function code(x, y, z, t)
                                use fmin_fmax_functions
                                    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) * z) * y) - t
                                end function
                                
                                public static double code(double x, double y, double z, double t) {
                                	return ((((-0.5 * y) - 1.0) * z) * y) - t;
                                }
                                
                                def code(x, y, z, t):
                                	return ((((-0.5 * y) - 1.0) * z) * y) - t
                                
                                function code(x, y, z, t)
                                	return Float64(Float64(Float64(Float64(Float64(-0.5 * y) - 1.0) * z) * y) - t)
                                end
                                
                                function tmp = code(x, y, z, t)
                                	tmp = ((((-0.5 * y) - 1.0) * z) * y) - t;
                                end
                                
                                code[x_, y_, z_, t_] := N[(N[(N[(N[(N[(-0.5 * y), $MachinePrecision] - 1.0), $MachinePrecision] * z), $MachinePrecision] * y), $MachinePrecision] - t), $MachinePrecision]
                                
                                \begin{array}{l}
                                
                                \\
                                \left(\left(-0.5 \cdot y - 1\right) \cdot z\right) \cdot y - t
                                \end{array}
                                
                                Derivation
                                1. Initial program 90.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-log.f64N/A

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

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

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

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

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

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

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

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

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

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

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

                                  \[\leadsto \left(\left(x - 1\right) \cdot \log y + \left(z - 1\right) \cdot \color{blue}{\left(\mathsf{log1p}\left(\left(-y\right) \cdot y\right) - \mathsf{log1p}\left(y\right)\right)}\right) - t \]
                                5. 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 \]
                                6. Step-by-step derivation
                                  1. *-commutativeN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                  Alternative 17: 46.0% accurate, 18.8× speedup?

                                  \[\begin{array}{l} \\ \mathsf{fma}\left(-y, z, y\right) - t \end{array} \]
                                  (FPCore (x y z t) :precision binary64 (- (fma (- y) z y) t))
                                  double code(double x, double y, double z, double t) {
                                  	return fma(-y, z, y) - t;
                                  }
                                  
                                  function code(x, y, z, t)
                                  	return Float64(fma(Float64(-y), z, y) - t)
                                  end
                                  
                                  code[x_, y_, z_, t_] := N[(N[((-y) * z + y), $MachinePrecision] - t), $MachinePrecision]
                                  
                                  \begin{array}{l}
                                  
                                  \\
                                  \mathsf{fma}\left(-y, z, y\right) - t
                                  \end{array}
                                  
                                  Derivation
                                  1. Initial program 90.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}{\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-*r*N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                        \[\leadsto \left(y + -1 \cdot \color{blue}{\left(y \cdot z\right)}\right) - t \]
                                      3. Step-by-step derivation
                                        1. Applied rewrites51.5%

                                          \[\leadsto \mathsf{fma}\left(-y, z, y\right) - t \]
                                        2. Add Preprocessing

                                        Alternative 18: 45.8% accurate, 20.5× speedup?

                                        \[\begin{array}{l} \\ \left(-z\right) \cdot y - t \end{array} \]
                                        (FPCore (x y z t) :precision binary64 (- (* (- z) y) t))
                                        double code(double x, double y, double z, double t) {
                                        	return (-z * y) - t;
                                        }
                                        
                                        module fmin_fmax_functions
                                            implicit none
                                            private
                                            public fmax
                                            public fmin
                                        
                                            interface fmax
                                                module procedure fmax88
                                                module procedure fmax44
                                                module procedure fmax84
                                                module procedure fmax48
                                            end interface
                                            interface fmin
                                                module procedure fmin88
                                                module procedure fmin44
                                                module procedure fmin84
                                                module procedure fmin48
                                            end interface
                                        contains
                                            real(8) function fmax88(x, y) result (res)
                                                real(8), intent (in) :: x
                                                real(8), intent (in) :: y
                                                res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                            end function
                                            real(4) function fmax44(x, y) result (res)
                                                real(4), intent (in) :: x
                                                real(4), intent (in) :: y
                                                res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                            end function
                                            real(8) function fmax84(x, y) result(res)
                                                real(8), intent (in) :: x
                                                real(4), intent (in) :: y
                                                res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                                            end function
                                            real(8) function fmax48(x, y) result(res)
                                                real(4), intent (in) :: x
                                                real(8), intent (in) :: y
                                                res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                                            end function
                                            real(8) function fmin88(x, y) result (res)
                                                real(8), intent (in) :: x
                                                real(8), intent (in) :: y
                                                res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                            end function
                                            real(4) function fmin44(x, y) result (res)
                                                real(4), intent (in) :: x
                                                real(4), intent (in) :: y
                                                res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                            end function
                                            real(8) function fmin84(x, y) result(res)
                                                real(8), intent (in) :: x
                                                real(4), intent (in) :: y
                                                res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                                            end function
                                            real(8) function fmin48(x, y) result(res)
                                                real(4), intent (in) :: x
                                                real(8), intent (in) :: y
                                                res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                                            end function
                                        end module
                                        
                                        real(8) function code(x, y, z, t)
                                        use fmin_fmax_functions
                                            real(8), intent (in) :: x
                                            real(8), intent (in) :: y
                                            real(8), intent (in) :: z
                                            real(8), intent (in) :: t
                                            code = (-z * y) - t
                                        end function
                                        
                                        public static double code(double x, double y, double z, double t) {
                                        	return (-z * y) - t;
                                        }
                                        
                                        def code(x, y, z, t):
                                        	return (-z * y) - t
                                        
                                        function code(x, y, z, t)
                                        	return Float64(Float64(Float64(-z) * y) - t)
                                        end
                                        
                                        function tmp = code(x, y, z, t)
                                        	tmp = (-z * y) - t;
                                        end
                                        
                                        code[x_, y_, z_, t_] := N[(N[((-z) * y), $MachinePrecision] - t), $MachinePrecision]
                                        
                                        \begin{array}{l}
                                        
                                        \\
                                        \left(-z\right) \cdot y - t
                                        \end{array}
                                        
                                        Derivation
                                        1. Initial program 90.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}{\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-*r*N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                          Alternative 19: 35.7% 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;
                                          }
                                          
                                          module fmin_fmax_functions
                                              implicit none
                                              private
                                              public fmax
                                              public fmin
                                          
                                              interface fmax
                                                  module procedure fmax88
                                                  module procedure fmax44
                                                  module procedure fmax84
                                                  module procedure fmax48
                                              end interface
                                              interface fmin
                                                  module procedure fmin88
                                                  module procedure fmin44
                                                  module procedure fmin84
                                                  module procedure fmin48
                                              end interface
                                          contains
                                              real(8) function fmax88(x, y) result (res)
                                                  real(8), intent (in) :: x
                                                  real(8), intent (in) :: y
                                                  res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                              end function
                                              real(4) function fmax44(x, y) result (res)
                                                  real(4), intent (in) :: x
                                                  real(4), intent (in) :: y
                                                  res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                              end function
                                              real(8) function fmax84(x, y) result(res)
                                                  real(8), intent (in) :: x
                                                  real(4), intent (in) :: y
                                                  res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                                              end function
                                              real(8) function fmax48(x, y) result(res)
                                                  real(4), intent (in) :: x
                                                  real(8), intent (in) :: y
                                                  res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                                              end function
                                              real(8) function fmin88(x, y) result (res)
                                                  real(8), intent (in) :: x
                                                  real(8), intent (in) :: y
                                                  res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                              end function
                                              real(4) function fmin44(x, y) result (res)
                                                  real(4), intent (in) :: x
                                                  real(4), intent (in) :: y
                                                  res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                              end function
                                              real(8) function fmin84(x, y) result(res)
                                                  real(8), intent (in) :: x
                                                  real(4), intent (in) :: y
                                                  res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                                              end function
                                              real(8) function fmin48(x, y) result(res)
                                                  real(4), intent (in) :: x
                                                  real(8), intent (in) :: y
                                                  res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                                              end function
                                          end module
                                          
                                          real(8) function code(x, y, z, t)
                                          use fmin_fmax_functions
                                              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 90.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.f6441.8

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

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

                                          Reproduce

                                          ?
                                          herbie shell --seed 2025016 
                                          (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))