Numeric.SpecFunctions:logBeta from math-functions-0.1.5.2, A

Percentage Accurate: 99.8% → 99.9%
Time: 10.5s
Alternatives: 17
Speedup: 1.0×

Specification

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

\\
\left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \left(a - 0.5\right) \cdot b
\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 17 alternatives:

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

Initial Program: 99.8% accurate, 1.0× speedup?

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

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

Alternative 1: 99.9% accurate, 1.0× speedup?

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

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

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

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

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

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

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

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

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

      \[\leadsto \left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \mathsf{fma}\left(b, a, \color{blue}{b \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right) \]
    8. metadata-eval99.9

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Alternative 2: 46.5% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \left(a - 0.5\right) \cdot b\\ \mathbf{if}\;t\_1 \leq -4.5 \cdot 10^{+307}:\\ \;\;\;\;b \cdot a\\ \mathbf{elif}\;t\_1 \leq -1 \cdot 10^{-102}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, b, x\right)\\ \mathbf{elif}\;t\_1 \leq 2 \cdot 10^{+302}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, b, y\right)\\ \mathbf{else}:\\ \;\;\;\;b \cdot a\\ \end{array} \end{array} \]
(FPCore (x y z t a b)
 :precision binary64
 (let* ((t_1 (+ (- (+ (+ x y) z) (* z (log t))) (* (- a 0.5) b))))
   (if (<= t_1 -4.5e+307)
     (* b a)
     (if (<= t_1 -1e-102)
       (fma -0.5 b x)
       (if (<= t_1 2e+302) (fma -0.5 b y) (* b a))))))
double code(double x, double y, double z, double t, double a, double b) {
	double t_1 = (((x + y) + z) - (z * log(t))) + ((a - 0.5) * b);
	double tmp;
	if (t_1 <= -4.5e+307) {
		tmp = b * a;
	} else if (t_1 <= -1e-102) {
		tmp = fma(-0.5, b, x);
	} else if (t_1 <= 2e+302) {
		tmp = fma(-0.5, b, y);
	} else {
		tmp = b * a;
	}
	return tmp;
}
function code(x, y, z, t, a, b)
	t_1 = Float64(Float64(Float64(Float64(x + y) + z) - Float64(z * log(t))) + Float64(Float64(a - 0.5) * b))
	tmp = 0.0
	if (t_1 <= -4.5e+307)
		tmp = Float64(b * a);
	elseif (t_1 <= -1e-102)
		tmp = fma(-0.5, b, x);
	elseif (t_1 <= 2e+302)
		tmp = fma(-0.5, b, y);
	else
		tmp = Float64(b * a);
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(N[(N[(N[(x + y), $MachinePrecision] + z), $MachinePrecision] - N[(z * N[Log[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(a - 0.5), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -4.5e+307], N[(b * a), $MachinePrecision], If[LessEqual[t$95$1, -1e-102], N[(-0.5 * b + x), $MachinePrecision], If[LessEqual[t$95$1, 2e+302], N[(-0.5 * b + y), $MachinePrecision], N[(b * a), $MachinePrecision]]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \left(a - 0.5\right) \cdot b\\
\mathbf{if}\;t\_1 \leq -4.5 \cdot 10^{+307}:\\
\;\;\;\;b \cdot a\\

\mathbf{elif}\;t\_1 \leq -1 \cdot 10^{-102}:\\
\;\;\;\;\mathsf{fma}\left(-0.5, b, x\right)\\

\mathbf{elif}\;t\_1 \leq 2 \cdot 10^{+302}:\\
\;\;\;\;\mathsf{fma}\left(-0.5, b, y\right)\\

\mathbf{else}:\\
\;\;\;\;b \cdot a\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (+.f64 (-.f64 (+.f64 (+.f64 x y) z) (*.f64 z (log.f64 t))) (*.f64 (-.f64 a #s(literal 1/2 binary64)) b)) < -4.50000000000000025e307 or 2.0000000000000002e302 < (+.f64 (-.f64 (+.f64 (+.f64 x y) z) (*.f64 z (log.f64 t))) (*.f64 (-.f64 a #s(literal 1/2 binary64)) b))

    1. Initial program 100.0%

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

      \[\leadsto \color{blue}{a \cdot b} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \color{blue}{b \cdot a} \]
      2. lower-*.f6492.1

        \[\leadsto \color{blue}{b \cdot a} \]
    5. Applied rewrites92.1%

      \[\leadsto \color{blue}{b \cdot a} \]

    if -4.50000000000000025e307 < (+.f64 (-.f64 (+.f64 (+.f64 x y) z) (*.f64 z (log.f64 t))) (*.f64 (-.f64 a #s(literal 1/2 binary64)) b)) < -9.99999999999999933e-103

    1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto x + \frac{-1}{2} \cdot \color{blue}{b} \]
      3. Step-by-step derivation
        1. Applied rewrites35.6%

          \[\leadsto \mathsf{fma}\left(-0.5, b, x\right) \]

        if -9.99999999999999933e-103 < (+.f64 (-.f64 (+.f64 (+.f64 x y) z) (*.f64 z (log.f64 t))) (*.f64 (-.f64 a #s(literal 1/2 binary64)) b)) < 2.0000000000000002e302

        1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto y + \frac{-1}{2} \cdot \color{blue}{b} \]
          3. Step-by-step derivation
            1. Applied rewrites37.6%

              \[\leadsto \mathsf{fma}\left(-0.5, b, y\right) \]
          4. Recombined 3 regimes into one program.
          5. Add Preprocessing

          Alternative 3: 90.4% accurate, 0.9× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(a - 0.5\right) \cdot b\\ \mathbf{if}\;t\_1 \leq -5 \cdot 10^{+128} \lor \neg \left(t\_1 \leq 10^{+40}\right):\\ \;\;\;\;\mathsf{fma}\left(a - 0.5, b, y + x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(1 - \log t, z, x\right) + y\\ \end{array} \end{array} \]
          (FPCore (x y z t a b)
           :precision binary64
           (let* ((t_1 (* (- a 0.5) b)))
             (if (or (<= t_1 -5e+128) (not (<= t_1 1e+40)))
               (fma (- a 0.5) b (+ y x))
               (+ (fma (- 1.0 (log t)) z x) y))))
          double code(double x, double y, double z, double t, double a, double b) {
          	double t_1 = (a - 0.5) * b;
          	double tmp;
          	if ((t_1 <= -5e+128) || !(t_1 <= 1e+40)) {
          		tmp = fma((a - 0.5), b, (y + x));
          	} else {
          		tmp = fma((1.0 - log(t)), z, x) + y;
          	}
          	return tmp;
          }
          
          function code(x, y, z, t, a, b)
          	t_1 = Float64(Float64(a - 0.5) * b)
          	tmp = 0.0
          	if ((t_1 <= -5e+128) || !(t_1 <= 1e+40))
          		tmp = fma(Float64(a - 0.5), b, Float64(y + x));
          	else
          		tmp = Float64(fma(Float64(1.0 - log(t)), z, x) + y);
          	end
          	return tmp
          end
          
          code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(N[(a - 0.5), $MachinePrecision] * b), $MachinePrecision]}, If[Or[LessEqual[t$95$1, -5e+128], N[Not[LessEqual[t$95$1, 1e+40]], $MachinePrecision]], N[(N[(a - 0.5), $MachinePrecision] * b + N[(y + x), $MachinePrecision]), $MachinePrecision], N[(N[(N[(1.0 - N[Log[t], $MachinePrecision]), $MachinePrecision] * z + x), $MachinePrecision] + y), $MachinePrecision]]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          t_1 := \left(a - 0.5\right) \cdot b\\
          \mathbf{if}\;t\_1 \leq -5 \cdot 10^{+128} \lor \neg \left(t\_1 \leq 10^{+40}\right):\\
          \;\;\;\;\mathsf{fma}\left(a - 0.5, b, y + x\right)\\
          
          \mathbf{else}:\\
          \;\;\;\;\mathsf{fma}\left(1 - \log t, z, x\right) + y\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if (*.f64 (-.f64 a #s(literal 1/2 binary64)) b) < -5e128 or 1.00000000000000003e40 < (*.f64 (-.f64 a #s(literal 1/2 binary64)) b)

            1. Initial program 99.9%

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

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

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

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

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

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

                \[\leadsto \mathsf{fma}\left(\color{blue}{a - \frac{1}{2}}, b, x + y\right) \]
              6. +-commutativeN/A

                \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
              7. lower-+.f6491.0

                \[\leadsto \mathsf{fma}\left(a - 0.5, b, \color{blue}{y + x}\right) \]
            5. Applied rewrites91.0%

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

            if -5e128 < (*.f64 (-.f64 a #s(literal 1/2 binary64)) b) < 1.00000000000000003e40

            1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                \[\leadsto \color{blue}{\mathsf{fma}\left(1 - \log t, z, x + y\right)} \]
              5. Step-by-step derivation
                1. Applied rewrites92.8%

                  \[\leadsto \mathsf{fma}\left(1 - \log t, z, x\right) + \color{blue}{y} \]
              6. Recombined 2 regimes into one program.
              7. Final simplification91.9%

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

              Alternative 4: 91.4% accurate, 0.9× speedup?

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

                1. Initial program 99.9%

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

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

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

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

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

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

                    \[\leadsto \mathsf{fma}\left(\color{blue}{a - \frac{1}{2}}, b, x + y\right) \]
                  6. +-commutativeN/A

                    \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                  7. lower-+.f6491.9

                    \[\leadsto \mathsf{fma}\left(a - 0.5, b, \color{blue}{y + x}\right) \]
                5. Applied rewrites91.9%

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

                if -4 < (-.f64 a #s(literal 1/2 binary64)) < 3.99999999999999989e59

                1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                  \[\leadsto \color{blue}{\mathsf{fma}\left(1 - \log t, z, y\right) + \mathsf{fma}\left(-0.5, b, x\right)} \]
              3. Recombined 2 regimes into one program.
              4. Final simplification95.5%

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

              Alternative 5: 91.2% accurate, 0.9× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} t_1 := 1 - \log t\\ \mathbf{if}\;a - 0.5 \leq -4:\\ \;\;\;\;\mathsf{fma}\left(a - 0.5, b, y + x\right)\\ \mathbf{elif}\;a - 0.5 \leq 5 \cdot 10^{+37}:\\ \;\;\;\;\mathsf{fma}\left(t\_1, z, y\right) + \mathsf{fma}\left(-0.5, b, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t\_1, z, \mathsf{fma}\left(a - 0.5, b, x\right)\right)\\ \end{array} \end{array} \]
              (FPCore (x y z t a b)
               :precision binary64
               (let* ((t_1 (- 1.0 (log t))))
                 (if (<= (- a 0.5) -4.0)
                   (fma (- a 0.5) b (+ y x))
                   (if (<= (- a 0.5) 5e+37)
                     (+ (fma t_1 z y) (fma -0.5 b x))
                     (fma t_1 z (fma (- a 0.5) b x))))))
              double code(double x, double y, double z, double t, double a, double b) {
              	double t_1 = 1.0 - log(t);
              	double tmp;
              	if ((a - 0.5) <= -4.0) {
              		tmp = fma((a - 0.5), b, (y + x));
              	} else if ((a - 0.5) <= 5e+37) {
              		tmp = fma(t_1, z, y) + fma(-0.5, b, x);
              	} else {
              		tmp = fma(t_1, z, fma((a - 0.5), b, x));
              	}
              	return tmp;
              }
              
              function code(x, y, z, t, a, b)
              	t_1 = Float64(1.0 - log(t))
              	tmp = 0.0
              	if (Float64(a - 0.5) <= -4.0)
              		tmp = fma(Float64(a - 0.5), b, Float64(y + x));
              	elseif (Float64(a - 0.5) <= 5e+37)
              		tmp = Float64(fma(t_1, z, y) + fma(-0.5, b, x));
              	else
              		tmp = fma(t_1, z, fma(Float64(a - 0.5), b, x));
              	end
              	return tmp
              end
              
              code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(1.0 - N[Log[t], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(a - 0.5), $MachinePrecision], -4.0], N[(N[(a - 0.5), $MachinePrecision] * b + N[(y + x), $MachinePrecision]), $MachinePrecision], If[LessEqual[N[(a - 0.5), $MachinePrecision], 5e+37], N[(N[(t$95$1 * z + y), $MachinePrecision] + N[(-0.5 * b + x), $MachinePrecision]), $MachinePrecision], N[(t$95$1 * z + N[(N[(a - 0.5), $MachinePrecision] * b + x), $MachinePrecision]), $MachinePrecision]]]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              t_1 := 1 - \log t\\
              \mathbf{if}\;a - 0.5 \leq -4:\\
              \;\;\;\;\mathsf{fma}\left(a - 0.5, b, y + x\right)\\
              
              \mathbf{elif}\;a - 0.5 \leq 5 \cdot 10^{+37}:\\
              \;\;\;\;\mathsf{fma}\left(t\_1, z, y\right) + \mathsf{fma}\left(-0.5, b, x\right)\\
              
              \mathbf{else}:\\
              \;\;\;\;\mathsf{fma}\left(t\_1, z, \mathsf{fma}\left(a - 0.5, b, x\right)\right)\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 3 regimes
              2. if (-.f64 a #s(literal 1/2 binary64)) < -4

                1. Initial program 99.9%

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

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

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

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

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

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

                    \[\leadsto \mathsf{fma}\left(\color{blue}{a - \frac{1}{2}}, b, x + y\right) \]
                  6. +-commutativeN/A

                    \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                  7. lower-+.f6493.3

                    \[\leadsto \mathsf{fma}\left(a - 0.5, b, \color{blue}{y + x}\right) \]
                5. Applied rewrites93.3%

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

                if -4 < (-.f64 a #s(literal 1/2 binary64)) < 4.99999999999999989e37

                1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                if 4.99999999999999989e37 < (-.f64 a #s(literal 1/2 binary64))

                1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

                    \[\leadsto \color{blue}{\left(z \cdot \log \left(\frac{1}{t}\right) + z\right) + \left(b \cdot \left(a - \frac{1}{2}\right) + x\right)} \]
                  9. *-rgt-identityN/A

                    \[\leadsto \left(z \cdot \log \left(\frac{1}{t}\right) + \color{blue}{z \cdot 1}\right) + \left(b \cdot \left(a - \frac{1}{2}\right) + x\right) \]
                  10. distribute-lft-inN/A

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

                    \[\leadsto z \cdot \color{blue}{\left(1 + \log \left(\frac{1}{t}\right)\right)} + \left(b \cdot \left(a - \frac{1}{2}\right) + x\right) \]
                  12. log-recN/A

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

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

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

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

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

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

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

              Alternative 6: 59.2% accurate, 1.0× speedup?

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

                1. Initial program 99.9%

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

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

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

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

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

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

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

                    \[\leadsto \left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \mathsf{fma}\left(b, a, \color{blue}{b \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right) \]
                  8. metadata-eval99.9

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

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

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

                    \[\leadsto \color{blue}{\left(x + y\right) + \left(\frac{-1}{2} \cdot b + a \cdot b\right)} \]
                  2. distribute-rgt-outN/A

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

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

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

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

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

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

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

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

                    \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                  11. lower-+.f6481.4

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

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

                  \[\leadsto x + \color{blue}{b \cdot \left(a - \frac{1}{2}\right)} \]
                9. Step-by-step derivation
                  1. Applied rewrites60.2%

                    \[\leadsto \mathsf{fma}\left(a - 0.5, \color{blue}{b}, x\right) \]

                  if -9.99999999999999933e-103 < (-.f64 (+.f64 (+.f64 x y) z) (*.f64 z (log.f64 t)))

                  1. Initial program 99.8%

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

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

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

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

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

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

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

                      \[\leadsto \left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \mathsf{fma}\left(b, a, \color{blue}{b \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right) \]
                    8. metadata-eval99.8

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

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

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

                      \[\leadsto \color{blue}{\left(x + y\right) + \left(\frac{-1}{2} \cdot b + a \cdot b\right)} \]
                    2. distribute-rgt-outN/A

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

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

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

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

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

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

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

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

                      \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                    11. lower-+.f6480.9

                      \[\leadsto \mathsf{fma}\left(a - 0.5, b, \color{blue}{y + x}\right) \]
                  7. Applied rewrites80.9%

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

                    \[\leadsto y + \color{blue}{b \cdot \left(a - \frac{1}{2}\right)} \]
                  9. Step-by-step derivation
                    1. Applied rewrites58.5%

                      \[\leadsto \mathsf{fma}\left(a - 0.5, \color{blue}{b}, y\right) \]
                  10. Recombined 2 regimes into one program.
                  11. Final simplification59.3%

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

                  Alternative 7: 79.1% accurate, 1.0× speedup?

                  \[\begin{array}{l} \\ \begin{array}{l} t_1 := 1 - \log t\\ \mathbf{if}\;x + y \leq -1 \cdot 10^{-102}:\\ \;\;\;\;\mathsf{fma}\left(t\_1, z, \mathsf{fma}\left(a - 0.5, b, x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t\_1, z, \mathsf{fma}\left(a - 0.5, b, y\right)\right)\\ \end{array} \end{array} \]
                  (FPCore (x y z t a b)
                   :precision binary64
                   (let* ((t_1 (- 1.0 (log t))))
                     (if (<= (+ x y) -1e-102)
                       (fma t_1 z (fma (- a 0.5) b x))
                       (fma t_1 z (fma (- a 0.5) b y)))))
                  double code(double x, double y, double z, double t, double a, double b) {
                  	double t_1 = 1.0 - log(t);
                  	double tmp;
                  	if ((x + y) <= -1e-102) {
                  		tmp = fma(t_1, z, fma((a - 0.5), b, x));
                  	} else {
                  		tmp = fma(t_1, z, fma((a - 0.5), b, y));
                  	}
                  	return tmp;
                  }
                  
                  function code(x, y, z, t, a, b)
                  	t_1 = Float64(1.0 - log(t))
                  	tmp = 0.0
                  	if (Float64(x + y) <= -1e-102)
                  		tmp = fma(t_1, z, fma(Float64(a - 0.5), b, x));
                  	else
                  		tmp = fma(t_1, z, fma(Float64(a - 0.5), b, y));
                  	end
                  	return tmp
                  end
                  
                  code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(1.0 - N[Log[t], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(x + y), $MachinePrecision], -1e-102], N[(t$95$1 * z + N[(N[(a - 0.5), $MachinePrecision] * b + x), $MachinePrecision]), $MachinePrecision], N[(t$95$1 * z + N[(N[(a - 0.5), $MachinePrecision] * b + y), $MachinePrecision]), $MachinePrecision]]]
                  
                  \begin{array}{l}
                  
                  \\
                  \begin{array}{l}
                  t_1 := 1 - \log t\\
                  \mathbf{if}\;x + y \leq -1 \cdot 10^{-102}:\\
                  \;\;\;\;\mathsf{fma}\left(t\_1, z, \mathsf{fma}\left(a - 0.5, b, x\right)\right)\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;\mathsf{fma}\left(t\_1, z, \mathsf{fma}\left(a - 0.5, b, y\right)\right)\\
                  
                  
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 2 regimes
                  2. if (+.f64 x y) < -9.99999999999999933e-103

                    1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

                        \[\leadsto \color{blue}{\left(z \cdot \log \left(\frac{1}{t}\right) + z\right) + \left(b \cdot \left(a - \frac{1}{2}\right) + x\right)} \]
                      9. *-rgt-identityN/A

                        \[\leadsto \left(z \cdot \log \left(\frac{1}{t}\right) + \color{blue}{z \cdot 1}\right) + \left(b \cdot \left(a - \frac{1}{2}\right) + x\right) \]
                      10. distribute-lft-inN/A

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

                        \[\leadsto z \cdot \color{blue}{\left(1 + \log \left(\frac{1}{t}\right)\right)} + \left(b \cdot \left(a - \frac{1}{2}\right) + x\right) \]
                      12. log-recN/A

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

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

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

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

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

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

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

                    if -9.99999999999999933e-103 < (+.f64 x y)

                    1. Initial program 99.9%

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

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

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

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

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

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

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

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

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

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

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

                        \[\leadsto \left(\color{blue}{\log \left(\frac{1}{t}\right) \cdot z} + z\right) + \left(y + b \cdot \left(a - \frac{1}{2}\right)\right) \]
                      11. distribute-lft1-inN/A

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

                        \[\leadsto \color{blue}{\left(1 + \log \left(\frac{1}{t}\right)\right)} \cdot z + \left(y + b \cdot \left(a - \frac{1}{2}\right)\right) \]
                      13. log-recN/A

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

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

                        \[\leadsto \color{blue}{\mathsf{fma}\left(1 + -1 \cdot \log t, z, y + b \cdot \left(a - \frac{1}{2}\right)\right)} \]
                    5. Applied rewrites77.0%

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

                  Alternative 8: 99.8% accurate, 1.0× speedup?

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

                    \[\left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \left(a - 0.5\right) \cdot b \]
                  2. Add Preprocessing
                  3. Add Preprocessing

                  Alternative 9: 85.3% accurate, 1.0× speedup?

                  \[\begin{array}{l} \\ \begin{array}{l} t_1 := 1 - \log t\\ \mathbf{if}\;z \leq -6.5 \cdot 10^{+174}:\\ \;\;\;\;\mathsf{fma}\left(t\_1, z, y\right)\\ \mathbf{elif}\;z \leq 8.2 \cdot 10^{+119}:\\ \;\;\;\;\mathsf{fma}\left(a - 0.5, b, y + x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t\_1, z, x\right)\\ \end{array} \end{array} \]
                  (FPCore (x y z t a b)
                   :precision binary64
                   (let* ((t_1 (- 1.0 (log t))))
                     (if (<= z -6.5e+174)
                       (fma t_1 z y)
                       (if (<= z 8.2e+119) (fma (- a 0.5) b (+ y x)) (fma t_1 z x)))))
                  double code(double x, double y, double z, double t, double a, double b) {
                  	double t_1 = 1.0 - log(t);
                  	double tmp;
                  	if (z <= -6.5e+174) {
                  		tmp = fma(t_1, z, y);
                  	} else if (z <= 8.2e+119) {
                  		tmp = fma((a - 0.5), b, (y + x));
                  	} else {
                  		tmp = fma(t_1, z, x);
                  	}
                  	return tmp;
                  }
                  
                  function code(x, y, z, t, a, b)
                  	t_1 = Float64(1.0 - log(t))
                  	tmp = 0.0
                  	if (z <= -6.5e+174)
                  		tmp = fma(t_1, z, y);
                  	elseif (z <= 8.2e+119)
                  		tmp = fma(Float64(a - 0.5), b, Float64(y + x));
                  	else
                  		tmp = fma(t_1, z, x);
                  	end
                  	return tmp
                  end
                  
                  code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(1.0 - N[Log[t], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z, -6.5e+174], N[(t$95$1 * z + y), $MachinePrecision], If[LessEqual[z, 8.2e+119], N[(N[(a - 0.5), $MachinePrecision] * b + N[(y + x), $MachinePrecision]), $MachinePrecision], N[(t$95$1 * z + x), $MachinePrecision]]]]
                  
                  \begin{array}{l}
                  
                  \\
                  \begin{array}{l}
                  t_1 := 1 - \log t\\
                  \mathbf{if}\;z \leq -6.5 \cdot 10^{+174}:\\
                  \;\;\;\;\mathsf{fma}\left(t\_1, z, y\right)\\
                  
                  \mathbf{elif}\;z \leq 8.2 \cdot 10^{+119}:\\
                  \;\;\;\;\mathsf{fma}\left(a - 0.5, b, y + x\right)\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;\mathsf{fma}\left(t\_1, z, x\right)\\
                  
                  
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 3 regimes
                  2. if z < -6.5000000000000001e174

                    1. Initial program 99.7%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                        if -6.5000000000000001e174 < z < 8.1999999999999994e119

                        1. Initial program 99.9%

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

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

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

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

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

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

                            \[\leadsto \mathsf{fma}\left(\color{blue}{a - \frac{1}{2}}, b, x + y\right) \]
                          6. +-commutativeN/A

                            \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                          7. lower-+.f6493.0

                            \[\leadsto \mathsf{fma}\left(a - 0.5, b, \color{blue}{y + x}\right) \]
                        5. Applied rewrites93.0%

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

                        if 8.1999999999999994e119 < z

                        1. Initial program 99.6%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                          Alternative 10: 81.8% accurate, 1.1× speedup?

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

                            1. Initial program 99.9%

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

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

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

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

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

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

                                \[\leadsto \mathsf{fma}\left(\color{blue}{a - \frac{1}{2}}, b, x + y\right) \]
                              6. +-commutativeN/A

                                \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                              7. lower-+.f6488.5

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

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

                            if 8.1999999999999994e119 < z

                            1. Initial program 99.6%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                              Alternative 11: 81.8% accurate, 1.1× speedup?

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

                                1. Initial program 99.9%

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

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

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

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

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

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

                                    \[\leadsto \mathsf{fma}\left(\color{blue}{a - \frac{1}{2}}, b, x + y\right) \]
                                  6. +-commutativeN/A

                                    \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                                  7. lower-+.f6487.7

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

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

                                if 2.2999999999999999e180 < z

                                1. Initial program 99.6%

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

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

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

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

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

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

                                    \[\leadsto \left(1 + \color{blue}{\left(\mathsf{neg}\left(\log t\right)\right)}\right) \cdot z \]
                                  6. sub-negN/A

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

                                    \[\leadsto \color{blue}{\left(1 - \log t\right)} \cdot z \]
                                  8. lower-log.f6462.4

                                    \[\leadsto \left(1 - \color{blue}{\log t}\right) \cdot z \]
                                5. Applied rewrites62.4%

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

                              Alternative 12: 72.8% accurate, 3.3× speedup?

                              \[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(a - 0.5\right) \cdot b\\ \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+116} \lor \neg \left(t\_1 \leq 5 \cdot 10^{+199}\right):\\ \;\;\;\;\mathsf{fma}\left(a - 0.5, b, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, b, y + x\right)\\ \end{array} \end{array} \]
                              (FPCore (x y z t a b)
                               :precision binary64
                               (let* ((t_1 (* (- a 0.5) b)))
                                 (if (or (<= t_1 -1e+116) (not (<= t_1 5e+199)))
                                   (fma (- a 0.5) b x)
                                   (fma -0.5 b (+ y x)))))
                              double code(double x, double y, double z, double t, double a, double b) {
                              	double t_1 = (a - 0.5) * b;
                              	double tmp;
                              	if ((t_1 <= -1e+116) || !(t_1 <= 5e+199)) {
                              		tmp = fma((a - 0.5), b, x);
                              	} else {
                              		tmp = fma(-0.5, b, (y + x));
                              	}
                              	return tmp;
                              }
                              
                              function code(x, y, z, t, a, b)
                              	t_1 = Float64(Float64(a - 0.5) * b)
                              	tmp = 0.0
                              	if ((t_1 <= -1e+116) || !(t_1 <= 5e+199))
                              		tmp = fma(Float64(a - 0.5), b, x);
                              	else
                              		tmp = fma(-0.5, b, Float64(y + x));
                              	end
                              	return tmp
                              end
                              
                              code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(N[(a - 0.5), $MachinePrecision] * b), $MachinePrecision]}, If[Or[LessEqual[t$95$1, -1e+116], N[Not[LessEqual[t$95$1, 5e+199]], $MachinePrecision]], N[(N[(a - 0.5), $MachinePrecision] * b + x), $MachinePrecision], N[(-0.5 * b + N[(y + x), $MachinePrecision]), $MachinePrecision]]]
                              
                              \begin{array}{l}
                              
                              \\
                              \begin{array}{l}
                              t_1 := \left(a - 0.5\right) \cdot b\\
                              \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+116} \lor \neg \left(t\_1 \leq 5 \cdot 10^{+199}\right):\\
                              \;\;\;\;\mathsf{fma}\left(a - 0.5, b, x\right)\\
                              
                              \mathbf{else}:\\
                              \;\;\;\;\mathsf{fma}\left(-0.5, b, y + x\right)\\
                              
                              
                              \end{array}
                              \end{array}
                              
                              Derivation
                              1. Split input into 2 regimes
                              2. if (*.f64 (-.f64 a #s(literal 1/2 binary64)) b) < -1.00000000000000002e116 or 4.9999999999999998e199 < (*.f64 (-.f64 a #s(literal 1/2 binary64)) b)

                                1. Initial program 99.9%

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

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

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

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

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

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

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

                                    \[\leadsto \left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \mathsf{fma}\left(b, a, \color{blue}{b \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right) \]
                                  8. metadata-eval99.9

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

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

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

                                    \[\leadsto \color{blue}{\left(x + y\right) + \left(\frac{-1}{2} \cdot b + a \cdot b\right)} \]
                                  2. distribute-rgt-outN/A

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

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

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

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

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

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

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

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

                                    \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                                  11. lower-+.f6491.9

                                    \[\leadsto \mathsf{fma}\left(a - 0.5, b, \color{blue}{y + x}\right) \]
                                7. Applied rewrites91.9%

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

                                  \[\leadsto x + \color{blue}{b \cdot \left(a - \frac{1}{2}\right)} \]
                                9. Step-by-step derivation
                                  1. Applied rewrites85.5%

                                    \[\leadsto \mathsf{fma}\left(a - 0.5, \color{blue}{b}, x\right) \]

                                  if -1.00000000000000002e116 < (*.f64 (-.f64 a #s(literal 1/2 binary64)) b) < 4.9999999999999998e199

                                  1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                      \[\leadsto \mathsf{fma}\left(-0.5, \color{blue}{b}, y + x\right) \]
                                  8. Recombined 2 regimes into one program.
                                  9. Final simplification76.1%

                                    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(a - 0.5\right) \cdot b \leq -1 \cdot 10^{+116} \lor \neg \left(\left(a - 0.5\right) \cdot b \leq 5 \cdot 10^{+199}\right):\\ \;\;\;\;\mathsf{fma}\left(a - 0.5, b, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, b, y + x\right)\\ \end{array} \]
                                  10. Add Preprocessing

                                  Alternative 13: 70.5% accurate, 3.3× speedup?

                                  \[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(a - 0.5\right) \cdot b\\ \mathbf{if}\;t\_1 \leq -5 \cdot 10^{+128} \lor \neg \left(t\_1 \leq 2 \cdot 10^{+229}\right):\\ \;\;\;\;t\_1\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, b, y + x\right)\\ \end{array} \end{array} \]
                                  (FPCore (x y z t a b)
                                   :precision binary64
                                   (let* ((t_1 (* (- a 0.5) b)))
                                     (if (or (<= t_1 -5e+128) (not (<= t_1 2e+229))) t_1 (fma -0.5 b (+ y x)))))
                                  double code(double x, double y, double z, double t, double a, double b) {
                                  	double t_1 = (a - 0.5) * b;
                                  	double tmp;
                                  	if ((t_1 <= -5e+128) || !(t_1 <= 2e+229)) {
                                  		tmp = t_1;
                                  	} else {
                                  		tmp = fma(-0.5, b, (y + x));
                                  	}
                                  	return tmp;
                                  }
                                  
                                  function code(x, y, z, t, a, b)
                                  	t_1 = Float64(Float64(a - 0.5) * b)
                                  	tmp = 0.0
                                  	if ((t_1 <= -5e+128) || !(t_1 <= 2e+229))
                                  		tmp = t_1;
                                  	else
                                  		tmp = fma(-0.5, b, Float64(y + x));
                                  	end
                                  	return tmp
                                  end
                                  
                                  code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(N[(a - 0.5), $MachinePrecision] * b), $MachinePrecision]}, If[Or[LessEqual[t$95$1, -5e+128], N[Not[LessEqual[t$95$1, 2e+229]], $MachinePrecision]], t$95$1, N[(-0.5 * b + N[(y + x), $MachinePrecision]), $MachinePrecision]]]
                                  
                                  \begin{array}{l}
                                  
                                  \\
                                  \begin{array}{l}
                                  t_1 := \left(a - 0.5\right) \cdot b\\
                                  \mathbf{if}\;t\_1 \leq -5 \cdot 10^{+128} \lor \neg \left(t\_1 \leq 2 \cdot 10^{+229}\right):\\
                                  \;\;\;\;t\_1\\
                                  
                                  \mathbf{else}:\\
                                  \;\;\;\;\mathsf{fma}\left(-0.5, b, y + x\right)\\
                                  
                                  
                                  \end{array}
                                  \end{array}
                                  
                                  Derivation
                                  1. Split input into 2 regimes
                                  2. if (*.f64 (-.f64 a #s(literal 1/2 binary64)) b) < -5e128 or 2e229 < (*.f64 (-.f64 a #s(literal 1/2 binary64)) b)

                                    1. Initial program 99.9%

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

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

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

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

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

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

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

                                        \[\leadsto \left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \mathsf{fma}\left(b, a, \color{blue}{b \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right) \]
                                      8. metadata-eval99.9

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                        \[\leadsto \color{blue}{\left(a - \frac{1}{2}\right) \cdot b} \]
                                      3. lower--.f6482.2

                                        \[\leadsto \color{blue}{\left(a - 0.5\right)} \cdot b \]
                                    9. Applied rewrites82.2%

                                      \[\leadsto \color{blue}{\left(a - 0.5\right) \cdot b} \]

                                    if -5e128 < (*.f64 (-.f64 a #s(literal 1/2 binary64)) b) < 2e229

                                    1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                        \[\leadsto \mathsf{fma}\left(-0.5, \color{blue}{b}, y + x\right) \]
                                    8. Recombined 2 regimes into one program.
                                    9. Final simplification73.6%

                                      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(a - 0.5\right) \cdot b \leq -5 \cdot 10^{+128} \lor \neg \left(\left(a - 0.5\right) \cdot b \leq 2 \cdot 10^{+229}\right):\\ \;\;\;\;\left(a - 0.5\right) \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, b, y + x\right)\\ \end{array} \]
                                    10. Add Preprocessing

                                    Alternative 14: 50.3% accurate, 6.6× speedup?

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

                                      1. Initial program 99.9%

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

                                        \[\leadsto \color{blue}{a \cdot b} \]
                                      4. Step-by-step derivation
                                        1. *-commutativeN/A

                                          \[\leadsto \color{blue}{b \cdot a} \]
                                        2. lower-*.f6466.5

                                          \[\leadsto \color{blue}{b \cdot a} \]
                                      5. Applied rewrites66.5%

                                        \[\leadsto \color{blue}{b \cdot a} \]

                                      if -1.04999999999999989e31 < a < 1.9999999999999999e60

                                      1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                          \[\leadsto x + \frac{-1}{2} \cdot \color{blue}{b} \]
                                        3. Step-by-step derivation
                                          1. Applied rewrites46.9%

                                            \[\leadsto \mathsf{fma}\left(-0.5, b, x\right) \]
                                        4. Recombined 2 regimes into one program.
                                        5. Final simplification55.0%

                                          \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -1.05 \cdot 10^{+31} \lor \neg \left(a \leq 2 \cdot 10^{+60}\right):\\ \;\;\;\;b \cdot a\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, b, x\right)\\ \end{array} \]
                                        6. Add Preprocessing

                                        Alternative 15: 37.2% accurate, 7.0× speedup?

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

                                          1. Initial program 99.9%

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

                                            \[\leadsto \color{blue}{a \cdot b} \]
                                          4. Step-by-step derivation
                                            1. *-commutativeN/A

                                              \[\leadsto \color{blue}{b \cdot a} \]
                                            2. lower-*.f6460.8

                                              \[\leadsto \color{blue}{b \cdot a} \]
                                          5. Applied rewrites60.8%

                                            \[\leadsto \color{blue}{b \cdot a} \]

                                          if -3.80000000000000015e-7 < a < 3.6999999999999999e37

                                          1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                              \[\leadsto x + \frac{-1}{2} \cdot \color{blue}{b} \]
                                            3. Step-by-step derivation
                                              1. Applied rewrites46.6%

                                                \[\leadsto \mathsf{fma}\left(-0.5, b, x\right) \]
                                              2. Taylor expanded in x around 0

                                                \[\leadsto \frac{-1}{2} \cdot b \]
                                              3. Step-by-step derivation
                                                1. Applied rewrites19.5%

                                                  \[\leadsto -0.5 \cdot b \]
                                              4. Recombined 2 regimes into one program.
                                              5. Final simplification38.7%

                                                \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -3.8 \cdot 10^{-7} \lor \neg \left(a \leq 3.7 \cdot 10^{+37}\right):\\ \;\;\;\;b \cdot a\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot b\\ \end{array} \]
                                              6. Add Preprocessing

                                              Alternative 16: 79.5% accurate, 9.7× speedup?

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

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

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

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

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

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

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

                                                  \[\leadsto \mathsf{fma}\left(\color{blue}{a - \frac{1}{2}}, b, x + y\right) \]
                                                6. +-commutativeN/A

                                                  \[\leadsto \mathsf{fma}\left(a - \frac{1}{2}, b, \color{blue}{y + x}\right) \]
                                                7. lower-+.f6481.2

                                                  \[\leadsto \mathsf{fma}\left(a - 0.5, b, \color{blue}{y + x}\right) \]
                                              5. Applied rewrites81.2%

                                                \[\leadsto \color{blue}{\mathsf{fma}\left(a - 0.5, b, y + x\right)} \]
                                              6. Add Preprocessing

                                              Alternative 17: 14.3% accurate, 21.0× speedup?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                                  \[\leadsto x + \frac{-1}{2} \cdot \color{blue}{b} \]
                                                3. Step-by-step derivation
                                                  1. Applied rewrites32.8%

                                                    \[\leadsto \mathsf{fma}\left(-0.5, b, x\right) \]
                                                  2. Taylor expanded in x around 0

                                                    \[\leadsto \frac{-1}{2} \cdot b \]
                                                  3. Step-by-step derivation
                                                    1. Applied rewrites11.9%

                                                      \[\leadsto -0.5 \cdot b \]
                                                    2. Add Preprocessing

                                                    Developer Target 1: 99.5% accurate, 0.4× speedup?

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

                                                    Reproduce

                                                    ?
                                                    herbie shell --seed 2024313 
                                                    (FPCore (x y z t a b)
                                                      :name "Numeric.SpecFunctions:logBeta from math-functions-0.1.5.2, A"
                                                      :precision binary64
                                                    
                                                      :alt
                                                      (! :herbie-platform default (+ (+ (+ x y) (/ (* (- 1 (pow (log t) 2)) z) (+ 1 (log t)))) (* (- a 1/2) b)))
                                                    
                                                      (+ (- (+ (+ x y) z) (* z (log t))) (* (- a 0.5) b)))