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

Percentage Accurate: 95.4% → 98.4%
Time: 8.2s
Alternatives: 13
Speedup: 3.5×

Specification

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

\\
x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y}
\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 13 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: 95.4% accurate, 1.0× speedup?

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

\\
x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y}
\end{array}

Alternative 1: 98.4% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq 5 \cdot 10^{+286}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{-1}{x} + x\\ \end{array} \end{array} \]
(FPCore (x y z)
 :precision binary64
 (if (<= (+ (/ y (- (* (exp z) 1.1283791670955126) (* y x))) x) 5e+286)
   (- x (/ y (fma -1.1283791670955126 (exp z) (* y x))))
   (+ (/ -1.0 x) x)))
double code(double x, double y, double z) {
	double tmp;
	if (((y / ((exp(z) * 1.1283791670955126) - (y * x))) + x) <= 5e+286) {
		tmp = x - (y / fma(-1.1283791670955126, exp(z), (y * x)));
	} else {
		tmp = (-1.0 / x) + x;
	}
	return tmp;
}
function code(x, y, z)
	tmp = 0.0
	if (Float64(Float64(y / Float64(Float64(exp(z) * 1.1283791670955126) - Float64(y * x))) + x) <= 5e+286)
		tmp = Float64(x - Float64(y / fma(-1.1283791670955126, exp(z), Float64(y * x))));
	else
		tmp = Float64(Float64(-1.0 / x) + x);
	end
	return tmp
end
code[x_, y_, z_] := If[LessEqual[N[(N[(y / N[(N[(N[Exp[z], $MachinePrecision] * 1.1283791670955126), $MachinePrecision] - N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], 5e+286], N[(x - N[(y / N[(-1.1283791670955126 * N[Exp[z], $MachinePrecision] + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq 5 \cdot 10^{+286}:\\
\;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{-1}{x} + x\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y)))) < 5.0000000000000004e286

    1. Initial program 98.7%

      \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
      2. lift-/.f64N/A

        \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
      3. frac-2negN/A

        \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
      4. distribute-frac-neg2N/A

        \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
      5. unsub-negN/A

        \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
      6. distribute-frac-negN/A

        \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
      7. lift-/.f64N/A

        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
      8. lower--.f64N/A

        \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
      9. lift-/.f64N/A

        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
      10. distribute-frac-neg2N/A

        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
      11. lower-/.f64N/A

        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
      12. lift--.f64N/A

        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
      13. sub-negN/A

        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
      14. distribute-neg-inN/A

        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
      15. lift-*.f64N/A

        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
      16. distribute-lft-neg-inN/A

        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
      17. remove-double-negN/A

        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
      18. lower-fma.f64N/A

        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
    4. Applied rewrites98.7%

      \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]

    if 5.0000000000000004e286 < (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y))))

    1. Initial program 40.0%

      \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
    2. Add Preprocessing
    3. Taylor expanded in x around inf

      \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
    4. Step-by-step derivation
      1. lower-/.f64100.0

        \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
    5. Applied rewrites100.0%

      \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification98.8%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq 5 \cdot 10^{+286}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{-1}{x} + x\\ \end{array} \]
  5. Add Preprocessing

Alternative 2: 86.9% accurate, 0.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{-1}{x} + x\\ t_1 := \frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x\\ \mathbf{if}\;t\_1 \leq -1:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;t\_1 \leq 0.05:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, -1.1283791670955126\right)}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (+ (/ -1.0 x) x))
        (t_1 (+ (/ y (- (* (exp z) 1.1283791670955126) (* y x))) x)))
   (if (<= t_1 -1.0)
     t_0
     (if (<= t_1 0.05)
       (- x (/ y (fma -1.1283791670955126 z -1.1283791670955126)))
       t_0))))
double code(double x, double y, double z) {
	double t_0 = (-1.0 / x) + x;
	double t_1 = (y / ((exp(z) * 1.1283791670955126) - (y * x))) + x;
	double tmp;
	if (t_1 <= -1.0) {
		tmp = t_0;
	} else if (t_1 <= 0.05) {
		tmp = x - (y / fma(-1.1283791670955126, z, -1.1283791670955126));
	} else {
		tmp = t_0;
	}
	return tmp;
}
function code(x, y, z)
	t_0 = Float64(Float64(-1.0 / x) + x)
	t_1 = Float64(Float64(y / Float64(Float64(exp(z) * 1.1283791670955126) - Float64(y * x))) + x)
	tmp = 0.0
	if (t_1 <= -1.0)
		tmp = t_0;
	elseif (t_1 <= 0.05)
		tmp = Float64(x - Float64(y / fma(-1.1283791670955126, z, -1.1283791670955126)));
	else
		tmp = t_0;
	end
	return tmp
end
code[x_, y_, z_] := Block[{t$95$0 = N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision]}, Block[{t$95$1 = N[(N[(y / N[(N[(N[Exp[z], $MachinePrecision] * 1.1283791670955126), $MachinePrecision] - N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, -1.0], t$95$0, If[LessEqual[t$95$1, 0.05], N[(x - N[(y / N[(-1.1283791670955126 * z + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$0]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{-1}{x} + x\\
t_1 := \frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x\\
\mathbf{if}\;t\_1 \leq -1:\\
\;\;\;\;t\_0\\

\mathbf{elif}\;t\_1 \leq 0.05:\\
\;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, -1.1283791670955126\right)}\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y)))) < -1 or 0.050000000000000003 < (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y))))

    1. Initial program 94.1%

      \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
    2. Add Preprocessing
    3. Taylor expanded in x around inf

      \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
    4. Step-by-step derivation
      1. lower-/.f6491.0

        \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
    5. Applied rewrites91.0%

      \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

    if -1 < (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y)))) < 0.050000000000000003

    1. Initial program 99.9%

      \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
      2. lift-/.f64N/A

        \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
      3. frac-2negN/A

        \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
      4. distribute-frac-neg2N/A

        \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
      5. unsub-negN/A

        \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
      6. distribute-frac-negN/A

        \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
      7. lift-/.f64N/A

        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
      8. lower--.f64N/A

        \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
      9. lift-/.f64N/A

        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
      10. distribute-frac-neg2N/A

        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
      11. lower-/.f64N/A

        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
      12. lift--.f64N/A

        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
      13. sub-negN/A

        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
      14. distribute-neg-inN/A

        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
      15. lift-*.f64N/A

        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
      16. distribute-lft-neg-inN/A

        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
      17. remove-double-negN/A

        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
      18. lower-fma.f64N/A

        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
    4. Applied rewrites99.9%

      \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
    5. Taylor expanded in z around 0

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

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

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

        \[\leadsto x - \frac{y}{\color{blue}{\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
      4. lower-fma.f64N/A

        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
      5. sub-negN/A

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{10000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
      6. metadata-evalN/A

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
      7. lower-fma.f64N/A

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
      8. sub-negN/A

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
      9. *-commutativeN/A

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
      10. metadata-evalN/A

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
      11. lower-fma.f6494.1

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
    7. Applied rewrites94.1%

      \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
    8. Taylor expanded in x around 0

      \[\leadsto x - \frac{y}{z \cdot \left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) - \color{blue}{\frac{5641895835477563}{5000000000000000}}} \]
    9. Step-by-step derivation
      1. Applied rewrites93.7%

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), \color{blue}{z}, -1.1283791670955126\right)} \]
      2. Taylor expanded in z around 0

        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)} \]
      3. Step-by-step derivation
        1. Applied rewrites81.4%

          \[\leadsto x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, -1.1283791670955126\right)} \]
      4. Recombined 2 regimes into one program.
      5. Final simplification88.3%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq -1:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq 0.05:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, -1.1283791670955126\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{-1}{x} + x\\ \end{array} \]
      6. Add Preprocessing

      Alternative 3: 74.0% accurate, 0.4× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{-1}{x} + x\\ t_1 := \frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x\\ \mathbf{if}\;t\_1 \leq -1:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;t\_1 \leq 0.05:\\ \;\;\;\;\frac{0.8862269254527579}{1 + z} \cdot y\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
      (FPCore (x y z)
       :precision binary64
       (let* ((t_0 (+ (/ -1.0 x) x))
              (t_1 (+ (/ y (- (* (exp z) 1.1283791670955126) (* y x))) x)))
         (if (<= t_1 -1.0)
           t_0
           (if (<= t_1 0.05) (* (/ 0.8862269254527579 (+ 1.0 z)) y) t_0))))
      double code(double x, double y, double z) {
      	double t_0 = (-1.0 / x) + x;
      	double t_1 = (y / ((exp(z) * 1.1283791670955126) - (y * x))) + x;
      	double tmp;
      	if (t_1 <= -1.0) {
      		tmp = t_0;
      	} else if (t_1 <= 0.05) {
      		tmp = (0.8862269254527579 / (1.0 + z)) * y;
      	} else {
      		tmp = t_0;
      	}
      	return tmp;
      }
      
      real(8) function code(x, y, z)
          real(8), intent (in) :: x
          real(8), intent (in) :: y
          real(8), intent (in) :: z
          real(8) :: t_0
          real(8) :: t_1
          real(8) :: tmp
          t_0 = ((-1.0d0) / x) + x
          t_1 = (y / ((exp(z) * 1.1283791670955126d0) - (y * x))) + x
          if (t_1 <= (-1.0d0)) then
              tmp = t_0
          else if (t_1 <= 0.05d0) then
              tmp = (0.8862269254527579d0 / (1.0d0 + z)) * y
          else
              tmp = t_0
          end if
          code = tmp
      end function
      
      public static double code(double x, double y, double z) {
      	double t_0 = (-1.0 / x) + x;
      	double t_1 = (y / ((Math.exp(z) * 1.1283791670955126) - (y * x))) + x;
      	double tmp;
      	if (t_1 <= -1.0) {
      		tmp = t_0;
      	} else if (t_1 <= 0.05) {
      		tmp = (0.8862269254527579 / (1.0 + z)) * y;
      	} else {
      		tmp = t_0;
      	}
      	return tmp;
      }
      
      def code(x, y, z):
      	t_0 = (-1.0 / x) + x
      	t_1 = (y / ((math.exp(z) * 1.1283791670955126) - (y * x))) + x
      	tmp = 0
      	if t_1 <= -1.0:
      		tmp = t_0
      	elif t_1 <= 0.05:
      		tmp = (0.8862269254527579 / (1.0 + z)) * y
      	else:
      		tmp = t_0
      	return tmp
      
      function code(x, y, z)
      	t_0 = Float64(Float64(-1.0 / x) + x)
      	t_1 = Float64(Float64(y / Float64(Float64(exp(z) * 1.1283791670955126) - Float64(y * x))) + x)
      	tmp = 0.0
      	if (t_1 <= -1.0)
      		tmp = t_0;
      	elseif (t_1 <= 0.05)
      		tmp = Float64(Float64(0.8862269254527579 / Float64(1.0 + z)) * y);
      	else
      		tmp = t_0;
      	end
      	return tmp
      end
      
      function tmp_2 = code(x, y, z)
      	t_0 = (-1.0 / x) + x;
      	t_1 = (y / ((exp(z) * 1.1283791670955126) - (y * x))) + x;
      	tmp = 0.0;
      	if (t_1 <= -1.0)
      		tmp = t_0;
      	elseif (t_1 <= 0.05)
      		tmp = (0.8862269254527579 / (1.0 + z)) * y;
      	else
      		tmp = t_0;
      	end
      	tmp_2 = tmp;
      end
      
      code[x_, y_, z_] := Block[{t$95$0 = N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision]}, Block[{t$95$1 = N[(N[(y / N[(N[(N[Exp[z], $MachinePrecision] * 1.1283791670955126), $MachinePrecision] - N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, -1.0], t$95$0, If[LessEqual[t$95$1, 0.05], N[(N[(0.8862269254527579 / N[(1.0 + z), $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision], t$95$0]]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := \frac{-1}{x} + x\\
      t_1 := \frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x\\
      \mathbf{if}\;t\_1 \leq -1:\\
      \;\;\;\;t\_0\\
      
      \mathbf{elif}\;t\_1 \leq 0.05:\\
      \;\;\;\;\frac{0.8862269254527579}{1 + z} \cdot y\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_0\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y)))) < -1 or 0.050000000000000003 < (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y))))

        1. Initial program 94.1%

          \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
        2. Add Preprocessing
        3. Taylor expanded in x around inf

          \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
        4. Step-by-step derivation
          1. lower-/.f6491.0

            \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
        5. Applied rewrites91.0%

          \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

        if -1 < (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y)))) < 0.050000000000000003

        1. Initial program 99.9%

          \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-+.f64N/A

            \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
          2. lift-/.f64N/A

            \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
          3. frac-2negN/A

            \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
          4. distribute-frac-neg2N/A

            \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
          5. unsub-negN/A

            \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
          6. distribute-frac-negN/A

            \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
          7. lift-/.f64N/A

            \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
          8. lower--.f64N/A

            \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
          9. lift-/.f64N/A

            \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
          10. distribute-frac-neg2N/A

            \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
          11. lower-/.f64N/A

            \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
          12. lift--.f64N/A

            \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
          13. sub-negN/A

            \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
          14. distribute-neg-inN/A

            \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
          15. lift-*.f64N/A

            \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
          16. distribute-lft-neg-inN/A

            \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
          17. remove-double-negN/A

            \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
          18. lower-fma.f64N/A

            \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
        4. Applied rewrites99.9%

          \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
        5. Taylor expanded in x around 0

          \[\leadsto \color{blue}{\frac{5000000000000000}{5641895835477563} \cdot \frac{y}{e^{z}}} \]
        6. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
          2. lower-*.f64N/A

            \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
          3. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{y}{e^{z}}} \cdot \frac{5000000000000000}{5641895835477563} \]
          4. lower-exp.f6426.6

            \[\leadsto \frac{y}{\color{blue}{e^{z}}} \cdot 0.8862269254527579 \]
        7. Applied rewrites26.6%

          \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot 0.8862269254527579} \]
        8. Taylor expanded in z around 0

          \[\leadsto \frac{y}{1 + z} \cdot \frac{5000000000000000}{5641895835477563} \]
        9. Step-by-step derivation
          1. Applied rewrites26.7%

            \[\leadsto \frac{y}{1 + z} \cdot 0.8862269254527579 \]
          2. Step-by-step derivation
            1. Applied rewrites26.7%

              \[\leadsto y \cdot \color{blue}{\frac{0.8862269254527579}{1 + z}} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification73.1%

            \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq -1:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq 0.05:\\ \;\;\;\;\frac{0.8862269254527579}{1 + z} \cdot y\\ \mathbf{else}:\\ \;\;\;\;\frac{-1}{x} + x\\ \end{array} \]
          5. Add Preprocessing

          Alternative 4: 73.8% accurate, 0.5× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{-1}{x} + x\\ t_1 := \frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x\\ \mathbf{if}\;t\_1 \leq -1:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;t\_1 \leq 0.05:\\ \;\;\;\;0.8862269254527579 \cdot y\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
          (FPCore (x y z)
           :precision binary64
           (let* ((t_0 (+ (/ -1.0 x) x))
                  (t_1 (+ (/ y (- (* (exp z) 1.1283791670955126) (* y x))) x)))
             (if (<= t_1 -1.0) t_0 (if (<= t_1 0.05) (* 0.8862269254527579 y) t_0))))
          double code(double x, double y, double z) {
          	double t_0 = (-1.0 / x) + x;
          	double t_1 = (y / ((exp(z) * 1.1283791670955126) - (y * x))) + x;
          	double tmp;
          	if (t_1 <= -1.0) {
          		tmp = t_0;
          	} else if (t_1 <= 0.05) {
          		tmp = 0.8862269254527579 * y;
          	} else {
          		tmp = t_0;
          	}
          	return tmp;
          }
          
          real(8) function code(x, y, z)
              real(8), intent (in) :: x
              real(8), intent (in) :: y
              real(8), intent (in) :: z
              real(8) :: t_0
              real(8) :: t_1
              real(8) :: tmp
              t_0 = ((-1.0d0) / x) + x
              t_1 = (y / ((exp(z) * 1.1283791670955126d0) - (y * x))) + x
              if (t_1 <= (-1.0d0)) then
                  tmp = t_0
              else if (t_1 <= 0.05d0) then
                  tmp = 0.8862269254527579d0 * y
              else
                  tmp = t_0
              end if
              code = tmp
          end function
          
          public static double code(double x, double y, double z) {
          	double t_0 = (-1.0 / x) + x;
          	double t_1 = (y / ((Math.exp(z) * 1.1283791670955126) - (y * x))) + x;
          	double tmp;
          	if (t_1 <= -1.0) {
          		tmp = t_0;
          	} else if (t_1 <= 0.05) {
          		tmp = 0.8862269254527579 * y;
          	} else {
          		tmp = t_0;
          	}
          	return tmp;
          }
          
          def code(x, y, z):
          	t_0 = (-1.0 / x) + x
          	t_1 = (y / ((math.exp(z) * 1.1283791670955126) - (y * x))) + x
          	tmp = 0
          	if t_1 <= -1.0:
          		tmp = t_0
          	elif t_1 <= 0.05:
          		tmp = 0.8862269254527579 * y
          	else:
          		tmp = t_0
          	return tmp
          
          function code(x, y, z)
          	t_0 = Float64(Float64(-1.0 / x) + x)
          	t_1 = Float64(Float64(y / Float64(Float64(exp(z) * 1.1283791670955126) - Float64(y * x))) + x)
          	tmp = 0.0
          	if (t_1 <= -1.0)
          		tmp = t_0;
          	elseif (t_1 <= 0.05)
          		tmp = Float64(0.8862269254527579 * y);
          	else
          		tmp = t_0;
          	end
          	return tmp
          end
          
          function tmp_2 = code(x, y, z)
          	t_0 = (-1.0 / x) + x;
          	t_1 = (y / ((exp(z) * 1.1283791670955126) - (y * x))) + x;
          	tmp = 0.0;
          	if (t_1 <= -1.0)
          		tmp = t_0;
          	elseif (t_1 <= 0.05)
          		tmp = 0.8862269254527579 * y;
          	else
          		tmp = t_0;
          	end
          	tmp_2 = tmp;
          end
          
          code[x_, y_, z_] := Block[{t$95$0 = N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision]}, Block[{t$95$1 = N[(N[(y / N[(N[(N[Exp[z], $MachinePrecision] * 1.1283791670955126), $MachinePrecision] - N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, -1.0], t$95$0, If[LessEqual[t$95$1, 0.05], N[(0.8862269254527579 * y), $MachinePrecision], t$95$0]]]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          t_0 := \frac{-1}{x} + x\\
          t_1 := \frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x\\
          \mathbf{if}\;t\_1 \leq -1:\\
          \;\;\;\;t\_0\\
          
          \mathbf{elif}\;t\_1 \leq 0.05:\\
          \;\;\;\;0.8862269254527579 \cdot y\\
          
          \mathbf{else}:\\
          \;\;\;\;t\_0\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y)))) < -1 or 0.050000000000000003 < (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y))))

            1. Initial program 94.1%

              \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
            2. Add Preprocessing
            3. Taylor expanded in x around inf

              \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
            4. Step-by-step derivation
              1. lower-/.f6491.0

                \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
            5. Applied rewrites91.0%

              \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

            if -1 < (+.f64 x (/.f64 y (-.f64 (*.f64 #s(literal 5641895835477563/5000000000000000 binary64) (exp.f64 z)) (*.f64 x y)))) < 0.050000000000000003

            1. Initial program 99.9%

              \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-+.f64N/A

                \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
              2. lift-/.f64N/A

                \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
              3. frac-2negN/A

                \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
              4. distribute-frac-neg2N/A

                \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
              5. unsub-negN/A

                \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
              6. distribute-frac-negN/A

                \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
              7. lift-/.f64N/A

                \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
              8. lower--.f64N/A

                \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
              9. lift-/.f64N/A

                \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
              10. distribute-frac-neg2N/A

                \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
              11. lower-/.f64N/A

                \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
              12. lift--.f64N/A

                \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
              13. sub-negN/A

                \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
              14. distribute-neg-inN/A

                \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
              15. lift-*.f64N/A

                \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
              16. distribute-lft-neg-inN/A

                \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
              17. remove-double-negN/A

                \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
              18. lower-fma.f64N/A

                \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
            4. Applied rewrites99.9%

              \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
            5. Taylor expanded in x around 0

              \[\leadsto \color{blue}{\frac{5000000000000000}{5641895835477563} \cdot \frac{y}{e^{z}}} \]
            6. Step-by-step derivation
              1. *-commutativeN/A

                \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
              2. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
              3. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{y}{e^{z}}} \cdot \frac{5000000000000000}{5641895835477563} \]
              4. lower-exp.f6426.6

                \[\leadsto \frac{y}{\color{blue}{e^{z}}} \cdot 0.8862269254527579 \]
            7. Applied rewrites26.6%

              \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot 0.8862269254527579} \]
            8. Taylor expanded in z around 0

              \[\leadsto \frac{5000000000000000}{5641895835477563} \cdot \color{blue}{y} \]
            9. Step-by-step derivation
              1. Applied rewrites26.3%

                \[\leadsto 0.8862269254527579 \cdot \color{blue}{y} \]
            10. Recombined 2 regimes into one program.
            11. Final simplification73.0%

              \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq -1:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;\frac{y}{e^{z} \cdot 1.1283791670955126 - y \cdot x} + x \leq 0.05:\\ \;\;\;\;0.8862269254527579 \cdot y\\ \mathbf{else}:\\ \;\;\;\;\frac{-1}{x} + x\\ \end{array} \]
            12. Add Preprocessing

            Alternative 5: 98.8% accurate, 0.8× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;e^{z} \leq 0:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\left(\frac{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, -1.1283791670955126\right)}{x} + y\right) \cdot x}\\ \end{array} \end{array} \]
            (FPCore (x y z)
             :precision binary64
             (if (<= (exp z) 0.0)
               (+ (/ -1.0 x) x)
               (-
                x
                (/
                 y
                 (*
                  (+
                   (/
                    (fma
                     (fma
                      (fma -0.18806319451591877 z -0.5641895835477563)
                      z
                      -1.1283791670955126)
                     z
                     -1.1283791670955126)
                    x)
                   y)
                  x)))))
            double code(double x, double y, double z) {
            	double tmp;
            	if (exp(z) <= 0.0) {
            		tmp = (-1.0 / x) + x;
            	} else {
            		tmp = x - (y / (((fma(fma(fma(-0.18806319451591877, z, -0.5641895835477563), z, -1.1283791670955126), z, -1.1283791670955126) / x) + y) * x));
            	}
            	return tmp;
            }
            
            function code(x, y, z)
            	tmp = 0.0
            	if (exp(z) <= 0.0)
            		tmp = Float64(Float64(-1.0 / x) + x);
            	else
            		tmp = Float64(x - Float64(y / Float64(Float64(Float64(fma(fma(fma(-0.18806319451591877, z, -0.5641895835477563), z, -1.1283791670955126), z, -1.1283791670955126) / x) + y) * x)));
            	end
            	return tmp
            end
            
            code[x_, y_, z_] := If[LessEqual[N[Exp[z], $MachinePrecision], 0.0], N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision], N[(x - N[(y / N[(N[(N[(N[(N[(N[(-0.18806319451591877 * z + -0.5641895835477563), $MachinePrecision] * z + -1.1283791670955126), $MachinePrecision] * z + -1.1283791670955126), $MachinePrecision] / x), $MachinePrecision] + y), $MachinePrecision] * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            \mathbf{if}\;e^{z} \leq 0:\\
            \;\;\;\;\frac{-1}{x} + x\\
            
            \mathbf{else}:\\
            \;\;\;\;x - \frac{y}{\left(\frac{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, -1.1283791670955126\right)}{x} + y\right) \cdot x}\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if (exp.f64 z) < 0.0

              1. Initial program 87.0%

                \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
              2. Add Preprocessing
              3. Taylor expanded in x around inf

                \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
              4. Step-by-step derivation
                1. lower-/.f64100.0

                  \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
              5. Applied rewrites100.0%

                \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

              if 0.0 < (exp.f64 z)

              1. Initial program 98.0%

                \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
              2. Add Preprocessing
              3. Step-by-step derivation
                1. lift-+.f64N/A

                  \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                2. lift-/.f64N/A

                  \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                3. frac-2negN/A

                  \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                4. distribute-frac-neg2N/A

                  \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                5. unsub-negN/A

                  \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                6. distribute-frac-negN/A

                  \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                7. lift-/.f64N/A

                  \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                8. lower--.f64N/A

                  \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                9. lift-/.f64N/A

                  \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                10. distribute-frac-neg2N/A

                  \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                11. lower-/.f64N/A

                  \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                12. lift--.f64N/A

                  \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                13. sub-negN/A

                  \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                14. distribute-neg-inN/A

                  \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                15. lift-*.f64N/A

                  \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                16. distribute-lft-neg-inN/A

                  \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                17. remove-double-negN/A

                  \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                18. lower-fma.f64N/A

                  \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
              4. Applied rewrites98.0%

                \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
              5. Taylor expanded in z around 0

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

                  \[\leadsto x - \frac{y}{\color{blue}{\left(z \cdot \left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right) + x \cdot y\right)} - \frac{5641895835477563}{5000000000000000}} \]
                2. associate--l+N/A

                  \[\leadsto x - \frac{y}{\color{blue}{z \cdot \left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right) + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                3. *-commutativeN/A

                  \[\leadsto x - \frac{y}{\color{blue}{\left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                4. lower-fma.f64N/A

                  \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                5. sub-negN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                6. *-commutativeN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) \cdot z} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                7. metadata-evalN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                8. lower-fma.f64N/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                9. sub-negN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{30000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{10000000000000000}\right)\right)}, z, \frac{-5641895835477563}{5000000000000000}\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                10. metadata-evalN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{10000000000000000}}, z, \frac{-5641895835477563}{5000000000000000}\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                11. lower-fma.f64N/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right)}, z, \frac{-5641895835477563}{5000000000000000}\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                12. sub-negN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right), z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                13. *-commutativeN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right), z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                14. metadata-evalN/A

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right), z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                15. lower-fma.f6497.0

                  \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
              7. Applied rewrites97.0%

                \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
              8. Taylor expanded in x around inf

                \[\leadsto x - \frac{y}{x \cdot \color{blue}{\left(\left(y + \frac{z \cdot \left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right)}{x}\right) - \frac{5641895835477563}{5000000000000000} \cdot \frac{1}{x}\right)}} \]
              9. Step-by-step derivation
                1. Applied rewrites98.0%

                  \[\leadsto x - \frac{y}{\left(\frac{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, -1.1283791670955126\right)}{x} + y\right) \cdot \color{blue}{x}} \]
              10. Recombined 2 regimes into one program.
              11. Final simplification98.4%

                \[\leadsto \begin{array}{l} \mathbf{if}\;e^{z} \leq 0:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\left(\frac{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, -1.1283791670955126\right)}{x} + y\right) \cdot x}\\ \end{array} \]
              12. Add Preprocessing

              Alternative 6: 96.6% accurate, 0.9× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;e^{z} \leq 0:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\ \end{array} \end{array} \]
              (FPCore (x y z)
               :precision binary64
               (if (<= (exp z) 0.0)
                 (+ (/ -1.0 x) x)
                 (-
                  x
                  (/
                   y
                   (fma
                    (fma -0.5641895835477563 z -1.1283791670955126)
                    z
                    (fma y x -1.1283791670955126))))))
              double code(double x, double y, double z) {
              	double tmp;
              	if (exp(z) <= 0.0) {
              		tmp = (-1.0 / x) + x;
              	} else {
              		tmp = x - (y / fma(fma(-0.5641895835477563, z, -1.1283791670955126), z, fma(y, x, -1.1283791670955126)));
              	}
              	return tmp;
              }
              
              function code(x, y, z)
              	tmp = 0.0
              	if (exp(z) <= 0.0)
              		tmp = Float64(Float64(-1.0 / x) + x);
              	else
              		tmp = Float64(x - Float64(y / fma(fma(-0.5641895835477563, z, -1.1283791670955126), z, fma(y, x, -1.1283791670955126))));
              	end
              	return tmp
              end
              
              code[x_, y_, z_] := If[LessEqual[N[Exp[z], $MachinePrecision], 0.0], N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision], N[(x - N[(y / N[(N[(-0.5641895835477563 * z + -1.1283791670955126), $MachinePrecision] * z + N[(y * x + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              \mathbf{if}\;e^{z} \leq 0:\\
              \;\;\;\;\frac{-1}{x} + x\\
              
              \mathbf{else}:\\
              \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 2 regimes
              2. if (exp.f64 z) < 0.0

                1. Initial program 87.0%

                  \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                2. Add Preprocessing
                3. Taylor expanded in x around inf

                  \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                4. Step-by-step derivation
                  1. lower-/.f64100.0

                    \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                5. Applied rewrites100.0%

                  \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

                if 0.0 < (exp.f64 z)

                1. Initial program 98.0%

                  \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-+.f64N/A

                    \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  2. lift-/.f64N/A

                    \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  3. frac-2negN/A

                    \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  4. distribute-frac-neg2N/A

                    \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  5. unsub-negN/A

                    \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  6. distribute-frac-negN/A

                    \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  7. lift-/.f64N/A

                    \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                  8. lower--.f64N/A

                    \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  9. lift-/.f64N/A

                    \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                  10. distribute-frac-neg2N/A

                    \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  11. lower-/.f64N/A

                    \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  12. lift--.f64N/A

                    \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                  13. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                  14. distribute-neg-inN/A

                    \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                  15. lift-*.f64N/A

                    \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                  16. distribute-lft-neg-inN/A

                    \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                  17. remove-double-negN/A

                    \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                  18. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                4. Applied rewrites98.0%

                  \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                5. Taylor expanded in z around 0

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

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

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

                    \[\leadsto x - \frac{y}{\color{blue}{\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  4. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                  5. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{10000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  6. metadata-evalN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  7. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  8. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                  9. *-commutativeN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                  10. metadata-evalN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                  11. lower-fma.f6497.5

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
                7. Applied rewrites97.5%

                  \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
              3. Recombined 2 regimes into one program.
              4. Final simplification98.0%

                \[\leadsto \begin{array}{l} \mathbf{if}\;e^{z} \leq 0:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\ \end{array} \]
              5. Add Preprocessing

              Alternative 7: 97.4% accurate, 2.8× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z \leq -118:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\ \end{array} \end{array} \]
              (FPCore (x y z)
               :precision binary64
               (if (<= z -118.0)
                 (+ (/ -1.0 x) x)
                 (if (<= z 1.35e+19)
                   (- x (/ y (fma -1.1283791670955126 z (fma y x -1.1283791670955126))))
                   (-
                    x
                    (/
                     y
                     (fma
                      (fma
                       (fma -0.18806319451591877 z -0.5641895835477563)
                       z
                       -1.1283791670955126)
                      z
                      -1.1283791670955126))))))
              double code(double x, double y, double z) {
              	double tmp;
              	if (z <= -118.0) {
              		tmp = (-1.0 / x) + x;
              	} else if (z <= 1.35e+19) {
              		tmp = x - (y / fma(-1.1283791670955126, z, fma(y, x, -1.1283791670955126)));
              	} else {
              		tmp = x - (y / fma(fma(fma(-0.18806319451591877, z, -0.5641895835477563), z, -1.1283791670955126), z, -1.1283791670955126));
              	}
              	return tmp;
              }
              
              function code(x, y, z)
              	tmp = 0.0
              	if (z <= -118.0)
              		tmp = Float64(Float64(-1.0 / x) + x);
              	elseif (z <= 1.35e+19)
              		tmp = Float64(x - Float64(y / fma(-1.1283791670955126, z, fma(y, x, -1.1283791670955126))));
              	else
              		tmp = Float64(x - Float64(y / fma(fma(fma(-0.18806319451591877, z, -0.5641895835477563), z, -1.1283791670955126), z, -1.1283791670955126)));
              	end
              	return tmp
              end
              
              code[x_, y_, z_] := If[LessEqual[z, -118.0], N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[z, 1.35e+19], N[(x - N[(y / N[(-1.1283791670955126 * z + N[(y * x + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x - N[(y / N[(N[(N[(-0.18806319451591877 * z + -0.5641895835477563), $MachinePrecision] * z + -1.1283791670955126), $MachinePrecision] * z + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              \mathbf{if}\;z \leq -118:\\
              \;\;\;\;\frac{-1}{x} + x\\
              
              \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\
              \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\
              
              \mathbf{else}:\\
              \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 3 regimes
              2. if z < -118

                1. Initial program 87.0%

                  \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                2. Add Preprocessing
                3. Taylor expanded in x around inf

                  \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                4. Step-by-step derivation
                  1. lower-/.f64100.0

                    \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                5. Applied rewrites100.0%

                  \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

                if -118 < z < 1.35e19

                1. Initial program 99.2%

                  \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-+.f64N/A

                    \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  2. lift-/.f64N/A

                    \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  3. frac-2negN/A

                    \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  4. distribute-frac-neg2N/A

                    \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  5. unsub-negN/A

                    \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  6. distribute-frac-negN/A

                    \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  7. lift-/.f64N/A

                    \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                  8. lower--.f64N/A

                    \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  9. lift-/.f64N/A

                    \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                  10. distribute-frac-neg2N/A

                    \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  11. lower-/.f64N/A

                    \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  12. lift--.f64N/A

                    \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                  13. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                  14. distribute-neg-inN/A

                    \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                  15. lift-*.f64N/A

                    \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                  16. distribute-lft-neg-inN/A

                    \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                  17. remove-double-negN/A

                    \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                  18. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                4. Applied rewrites99.2%

                  \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                5. Taylor expanded in z around 0

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

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

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

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                  4. *-commutativeN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                  5. metadata-evalN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                  6. lower-fma.f6498.4

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

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

                if 1.35e19 < z

                1. Initial program 94.9%

                  \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-+.f64N/A

                    \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  2. lift-/.f64N/A

                    \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  3. frac-2negN/A

                    \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  4. distribute-frac-neg2N/A

                    \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  5. unsub-negN/A

                    \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                  6. distribute-frac-negN/A

                    \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  7. lift-/.f64N/A

                    \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                  8. lower--.f64N/A

                    \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                  9. lift-/.f64N/A

                    \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                  10. distribute-frac-neg2N/A

                    \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  11. lower-/.f64N/A

                    \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                  12. lift--.f64N/A

                    \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                  13. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                  14. distribute-neg-inN/A

                    \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                  15. lift-*.f64N/A

                    \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                  16. distribute-lft-neg-inN/A

                    \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                  17. remove-double-negN/A

                    \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                  18. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                4. Applied rewrites94.9%

                  \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                5. Taylor expanded in z around 0

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

                    \[\leadsto x - \frac{y}{\color{blue}{\left(z \cdot \left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right) + x \cdot y\right)} - \frac{5641895835477563}{5000000000000000}} \]
                  2. associate--l+N/A

                    \[\leadsto x - \frac{y}{\color{blue}{z \cdot \left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right) + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                  3. *-commutativeN/A

                    \[\leadsto x - \frac{y}{\color{blue}{\left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  4. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                  5. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  6. *-commutativeN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) \cdot z} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  7. metadata-evalN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  8. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  9. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{30000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{10000000000000000}\right)\right)}, z, \frac{-5641895835477563}{5000000000000000}\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  10. metadata-evalN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{10000000000000000}}, z, \frac{-5641895835477563}{5000000000000000}\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  11. lower-fma.f64N/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right)}, z, \frac{-5641895835477563}{5000000000000000}\right), z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                  12. sub-negN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right), z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                  13. *-commutativeN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right), z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                  14. metadata-evalN/A

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{30000000000000000}, z, \frac{-5641895835477563}{10000000000000000}\right), z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                  15. lower-fma.f6493.6

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
                7. Applied rewrites93.6%

                  \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
                8. Taylor expanded in x around 0

                  \[\leadsto x - \frac{y}{z \cdot \left(z \cdot \left(\frac{-5641895835477563}{30000000000000000} \cdot z - \frac{5641895835477563}{10000000000000000}\right) - \frac{5641895835477563}{5000000000000000}\right) - \color{blue}{\frac{5641895835477563}{5000000000000000}}} \]
                9. Step-by-step derivation
                  1. Applied rewrites95.2%

                    \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), \color{blue}{z}, -1.1283791670955126\right)} \]
                10. Recombined 3 regimes into one program.
                11. Final simplification98.0%

                  \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -118:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.18806319451591877, z, -0.5641895835477563\right), z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\ \end{array} \]
                12. Add Preprocessing

                Alternative 8: 96.1% accurate, 3.3× speedup?

                \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z \leq -118:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\ \end{array} \end{array} \]
                (FPCore (x y z)
                 :precision binary64
                 (if (<= z -118.0)
                   (+ (/ -1.0 x) x)
                   (if (<= z 1.35e+19)
                     (- x (/ y (fma -1.1283791670955126 z (fma y x -1.1283791670955126))))
                     (-
                      x
                      (/
                       y
                       (fma
                        (fma -0.5641895835477563 z -1.1283791670955126)
                        z
                        -1.1283791670955126))))))
                double code(double x, double y, double z) {
                	double tmp;
                	if (z <= -118.0) {
                		tmp = (-1.0 / x) + x;
                	} else if (z <= 1.35e+19) {
                		tmp = x - (y / fma(-1.1283791670955126, z, fma(y, x, -1.1283791670955126)));
                	} else {
                		tmp = x - (y / fma(fma(-0.5641895835477563, z, -1.1283791670955126), z, -1.1283791670955126));
                	}
                	return tmp;
                }
                
                function code(x, y, z)
                	tmp = 0.0
                	if (z <= -118.0)
                		tmp = Float64(Float64(-1.0 / x) + x);
                	elseif (z <= 1.35e+19)
                		tmp = Float64(x - Float64(y / fma(-1.1283791670955126, z, fma(y, x, -1.1283791670955126))));
                	else
                		tmp = Float64(x - Float64(y / fma(fma(-0.5641895835477563, z, -1.1283791670955126), z, -1.1283791670955126)));
                	end
                	return tmp
                end
                
                code[x_, y_, z_] := If[LessEqual[z, -118.0], N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[z, 1.35e+19], N[(x - N[(y / N[(-1.1283791670955126 * z + N[(y * x + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x - N[(y / N[(N[(-0.5641895835477563 * z + -1.1283791670955126), $MachinePrecision] * z + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
                
                \begin{array}{l}
                
                \\
                \begin{array}{l}
                \mathbf{if}\;z \leq -118:\\
                \;\;\;\;\frac{-1}{x} + x\\
                
                \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\
                \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\
                
                \mathbf{else}:\\
                \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\
                
                
                \end{array}
                \end{array}
                
                Derivation
                1. Split input into 3 regimes
                2. if z < -118

                  1. Initial program 87.0%

                    \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                  2. Add Preprocessing
                  3. Taylor expanded in x around inf

                    \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                  4. Step-by-step derivation
                    1. lower-/.f64100.0

                      \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                  5. Applied rewrites100.0%

                    \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

                  if -118 < z < 1.35e19

                  1. Initial program 99.2%

                    \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-+.f64N/A

                      \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                    2. lift-/.f64N/A

                      \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                    3. frac-2negN/A

                      \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                    4. distribute-frac-neg2N/A

                      \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                    5. unsub-negN/A

                      \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                    6. distribute-frac-negN/A

                      \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                    7. lift-/.f64N/A

                      \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                    8. lower--.f64N/A

                      \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                    9. lift-/.f64N/A

                      \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                    10. distribute-frac-neg2N/A

                      \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                    11. lower-/.f64N/A

                      \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                    12. lift--.f64N/A

                      \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                    13. sub-negN/A

                      \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                    14. distribute-neg-inN/A

                      \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                    15. lift-*.f64N/A

                      \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                    16. distribute-lft-neg-inN/A

                      \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                    17. remove-double-negN/A

                      \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                    18. lower-fma.f64N/A

                      \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                  4. Applied rewrites99.2%

                    \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                  5. Taylor expanded in z around 0

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

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

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

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                    4. *-commutativeN/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                    5. metadata-evalN/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                    6. lower-fma.f6498.4

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

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

                  if 1.35e19 < z

                  1. Initial program 94.9%

                    \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-+.f64N/A

                      \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                    2. lift-/.f64N/A

                      \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                    3. frac-2negN/A

                      \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                    4. distribute-frac-neg2N/A

                      \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                    5. unsub-negN/A

                      \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                    6. distribute-frac-negN/A

                      \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                    7. lift-/.f64N/A

                      \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                    8. lower--.f64N/A

                      \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                    9. lift-/.f64N/A

                      \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                    10. distribute-frac-neg2N/A

                      \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                    11. lower-/.f64N/A

                      \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                    12. lift--.f64N/A

                      \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                    13. sub-negN/A

                      \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                    14. distribute-neg-inN/A

                      \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                    15. lift-*.f64N/A

                      \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                    16. distribute-lft-neg-inN/A

                      \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                    17. remove-double-negN/A

                      \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                    18. lower-fma.f64N/A

                      \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                  4. Applied rewrites94.9%

                    \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                  5. Taylor expanded in z around 0

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

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

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

                      \[\leadsto x - \frac{y}{\color{blue}{\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                    4. lower-fma.f64N/A

                      \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                    5. sub-negN/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{10000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                    6. metadata-evalN/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                    7. lower-fma.f64N/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                    8. sub-negN/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                    9. *-commutativeN/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                    10. metadata-evalN/A

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                    11. lower-fma.f6495.2

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
                  7. Applied rewrites95.2%

                    \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
                  8. Taylor expanded in x around 0

                    \[\leadsto x - \frac{y}{z \cdot \left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) - \color{blue}{\frac{5641895835477563}{5000000000000000}}} \]
                  9. Step-by-step derivation
                    1. Applied rewrites95.2%

                      \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), \color{blue}{z}, -1.1283791670955126\right)} \]
                  10. Recombined 3 regimes into one program.
                  11. Final simplification98.0%

                    \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -118:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\ \end{array} \]
                  12. Add Preprocessing

                  Alternative 9: 96.0% accurate, 3.3× speedup?

                  \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z \leq -185:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\ \end{array} \end{array} \]
                  (FPCore (x y z)
                   :precision binary64
                   (if (<= z -185.0)
                     (+ (/ -1.0 x) x)
                     (if (<= z 1.35e+19)
                       (- x (/ y (fma y x -1.1283791670955126)))
                       (-
                        x
                        (/
                         y
                         (fma
                          (fma -0.5641895835477563 z -1.1283791670955126)
                          z
                          -1.1283791670955126))))))
                  double code(double x, double y, double z) {
                  	double tmp;
                  	if (z <= -185.0) {
                  		tmp = (-1.0 / x) + x;
                  	} else if (z <= 1.35e+19) {
                  		tmp = x - (y / fma(y, x, -1.1283791670955126));
                  	} else {
                  		tmp = x - (y / fma(fma(-0.5641895835477563, z, -1.1283791670955126), z, -1.1283791670955126));
                  	}
                  	return tmp;
                  }
                  
                  function code(x, y, z)
                  	tmp = 0.0
                  	if (z <= -185.0)
                  		tmp = Float64(Float64(-1.0 / x) + x);
                  	elseif (z <= 1.35e+19)
                  		tmp = Float64(x - Float64(y / fma(y, x, -1.1283791670955126)));
                  	else
                  		tmp = Float64(x - Float64(y / fma(fma(-0.5641895835477563, z, -1.1283791670955126), z, -1.1283791670955126)));
                  	end
                  	return tmp
                  end
                  
                  code[x_, y_, z_] := If[LessEqual[z, -185.0], N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[z, 1.35e+19], N[(x - N[(y / N[(y * x + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x - N[(y / N[(N[(-0.5641895835477563 * z + -1.1283791670955126), $MachinePrecision] * z + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
                  
                  \begin{array}{l}
                  
                  \\
                  \begin{array}{l}
                  \mathbf{if}\;z \leq -185:\\
                  \;\;\;\;\frac{-1}{x} + x\\
                  
                  \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\
                  \;\;\;\;x - \frac{y}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\
                  
                  
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 3 regimes
                  2. if z < -185

                    1. Initial program 87.0%

                      \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                    2. Add Preprocessing
                    3. Taylor expanded in x around inf

                      \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                    4. Step-by-step derivation
                      1. lower-/.f64100.0

                        \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                    5. Applied rewrites100.0%

                      \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

                    if -185 < z < 1.35e19

                    1. Initial program 99.2%

                      \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                    2. Add Preprocessing
                    3. Step-by-step derivation
                      1. lift-+.f64N/A

                        \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                      2. lift-/.f64N/A

                        \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                      3. frac-2negN/A

                        \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                      4. distribute-frac-neg2N/A

                        \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                      5. unsub-negN/A

                        \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                      6. distribute-frac-negN/A

                        \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                      7. lift-/.f64N/A

                        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                      8. lower--.f64N/A

                        \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                      9. lift-/.f64N/A

                        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                      10. distribute-frac-neg2N/A

                        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                      11. lower-/.f64N/A

                        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                      12. lift--.f64N/A

                        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                      13. sub-negN/A

                        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                      14. distribute-neg-inN/A

                        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                      15. lift-*.f64N/A

                        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                      16. distribute-lft-neg-inN/A

                        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                      17. remove-double-negN/A

                        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                      18. lower-fma.f64N/A

                        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                    4. Applied rewrites99.2%

                      \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                    5. Taylor expanded in z around 0

                      \[\leadsto x - \frac{y}{\color{blue}{x \cdot y - \frac{5641895835477563}{5000000000000000}}} \]
                    6. Step-by-step derivation
                      1. sub-negN/A

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

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

                        \[\leadsto x - \frac{y}{y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}} \]
                      4. lower-fma.f6498.4

                        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}} \]
                    7. Applied rewrites98.4%

                      \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}} \]

                    if 1.35e19 < z

                    1. Initial program 94.9%

                      \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                    2. Add Preprocessing
                    3. Step-by-step derivation
                      1. lift-+.f64N/A

                        \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                      2. lift-/.f64N/A

                        \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                      3. frac-2negN/A

                        \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                      4. distribute-frac-neg2N/A

                        \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                      5. unsub-negN/A

                        \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                      6. distribute-frac-negN/A

                        \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                      7. lift-/.f64N/A

                        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                      8. lower--.f64N/A

                        \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                      9. lift-/.f64N/A

                        \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                      10. distribute-frac-neg2N/A

                        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                      11. lower-/.f64N/A

                        \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                      12. lift--.f64N/A

                        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                      13. sub-negN/A

                        \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                      14. distribute-neg-inN/A

                        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                      15. lift-*.f64N/A

                        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                      16. distribute-lft-neg-inN/A

                        \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                      17. remove-double-negN/A

                        \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                      18. lower-fma.f64N/A

                        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                    4. Applied rewrites94.9%

                      \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                    5. Taylor expanded in z around 0

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

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

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

                        \[\leadsto x - \frac{y}{\color{blue}{\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                      4. lower-fma.f64N/A

                        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                      5. sub-negN/A

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{10000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                      6. metadata-evalN/A

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                      7. lower-fma.f64N/A

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                      8. sub-negN/A

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                      9. *-commutativeN/A

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                      10. metadata-evalN/A

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                      11. lower-fma.f6495.2

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
                    7. Applied rewrites95.2%

                      \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
                    8. Taylor expanded in x around 0

                      \[\leadsto x - \frac{y}{z \cdot \left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) - \color{blue}{\frac{5641895835477563}{5000000000000000}}} \]
                    9. Step-by-step derivation
                      1. Applied rewrites95.2%

                        \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), \color{blue}{z}, -1.1283791670955126\right)} \]
                    10. Recombined 3 regimes into one program.
                    11. Final simplification98.0%

                      \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -185:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, -1.1283791670955126\right)}\\ \end{array} \]
                    12. Add Preprocessing

                    Alternative 10: 96.0% accurate, 3.5× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z \leq -185:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\left(z \cdot z\right) \cdot -0.5641895835477563}\\ \end{array} \end{array} \]
                    (FPCore (x y z)
                     :precision binary64
                     (if (<= z -185.0)
                       (+ (/ -1.0 x) x)
                       (if (<= z 1.35e+19)
                         (- x (/ y (fma y x -1.1283791670955126)))
                         (- x (/ y (* (* z z) -0.5641895835477563))))))
                    double code(double x, double y, double z) {
                    	double tmp;
                    	if (z <= -185.0) {
                    		tmp = (-1.0 / x) + x;
                    	} else if (z <= 1.35e+19) {
                    		tmp = x - (y / fma(y, x, -1.1283791670955126));
                    	} else {
                    		tmp = x - (y / ((z * z) * -0.5641895835477563));
                    	}
                    	return tmp;
                    }
                    
                    function code(x, y, z)
                    	tmp = 0.0
                    	if (z <= -185.0)
                    		tmp = Float64(Float64(-1.0 / x) + x);
                    	elseif (z <= 1.35e+19)
                    		tmp = Float64(x - Float64(y / fma(y, x, -1.1283791670955126)));
                    	else
                    		tmp = Float64(x - Float64(y / Float64(Float64(z * z) * -0.5641895835477563)));
                    	end
                    	return tmp
                    end
                    
                    code[x_, y_, z_] := If[LessEqual[z, -185.0], N[(N[(-1.0 / x), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[z, 1.35e+19], N[(x - N[(y / N[(y * x + -1.1283791670955126), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x - N[(y / N[(N[(z * z), $MachinePrecision] * -0.5641895835477563), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    \mathbf{if}\;z \leq -185:\\
                    \;\;\;\;\frac{-1}{x} + x\\
                    
                    \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\
                    \;\;\;\;x - \frac{y}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;x - \frac{y}{\left(z \cdot z\right) \cdot -0.5641895835477563}\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 3 regimes
                    2. if z < -185

                      1. Initial program 87.0%

                        \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                      2. Add Preprocessing
                      3. Taylor expanded in x around inf

                        \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                      4. Step-by-step derivation
                        1. lower-/.f64100.0

                          \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                      5. Applied rewrites100.0%

                        \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

                      if -185 < z < 1.35e19

                      1. Initial program 99.2%

                        \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                      2. Add Preprocessing
                      3. Step-by-step derivation
                        1. lift-+.f64N/A

                          \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                        2. lift-/.f64N/A

                          \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                        3. frac-2negN/A

                          \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                        4. distribute-frac-neg2N/A

                          \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                        5. unsub-negN/A

                          \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                        6. distribute-frac-negN/A

                          \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                        7. lift-/.f64N/A

                          \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                        8. lower--.f64N/A

                          \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                        9. lift-/.f64N/A

                          \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                        10. distribute-frac-neg2N/A

                          \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                        11. lower-/.f64N/A

                          \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                        12. lift--.f64N/A

                          \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                        13. sub-negN/A

                          \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                        14. distribute-neg-inN/A

                          \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                        15. lift-*.f64N/A

                          \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                        16. distribute-lft-neg-inN/A

                          \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                        17. remove-double-negN/A

                          \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                        18. lower-fma.f64N/A

                          \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                      4. Applied rewrites99.2%

                        \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                      5. Taylor expanded in z around 0

                        \[\leadsto x - \frac{y}{\color{blue}{x \cdot y - \frac{5641895835477563}{5000000000000000}}} \]
                      6. Step-by-step derivation
                        1. sub-negN/A

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

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

                          \[\leadsto x - \frac{y}{y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}} \]
                        4. lower-fma.f6498.4

                          \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}} \]
                      7. Applied rewrites98.4%

                        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}} \]

                      if 1.35e19 < z

                      1. Initial program 94.9%

                        \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                      2. Add Preprocessing
                      3. Step-by-step derivation
                        1. lift-+.f64N/A

                          \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                        2. lift-/.f64N/A

                          \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                        3. frac-2negN/A

                          \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                        4. distribute-frac-neg2N/A

                          \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                        5. unsub-negN/A

                          \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                        6. distribute-frac-negN/A

                          \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                        7. lift-/.f64N/A

                          \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                        8. lower--.f64N/A

                          \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                        9. lift-/.f64N/A

                          \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                        10. distribute-frac-neg2N/A

                          \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                        11. lower-/.f64N/A

                          \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                        12. lift--.f64N/A

                          \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                        13. sub-negN/A

                          \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                        14. distribute-neg-inN/A

                          \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                        15. lift-*.f64N/A

                          \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                        16. distribute-lft-neg-inN/A

                          \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                        17. remove-double-negN/A

                          \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                        18. lower-fma.f64N/A

                          \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                      4. Applied rewrites94.9%

                        \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                      5. Taylor expanded in z around 0

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

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

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

                          \[\leadsto x - \frac{y}{\color{blue}{\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                        4. lower-fma.f64N/A

                          \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                        5. sub-negN/A

                          \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{10000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                        6. metadata-evalN/A

                          \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                        7. lower-fma.f64N/A

                          \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                        8. sub-negN/A

                          \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                        9. *-commutativeN/A

                          \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                        10. metadata-evalN/A

                          \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                        11. lower-fma.f6495.2

                          \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
                      7. Applied rewrites95.2%

                        \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
                      8. Taylor expanded in z around inf

                        \[\leadsto x - \frac{y}{\frac{-5641895835477563}{10000000000000000} \cdot \color{blue}{{z}^{2}}} \]
                      9. Step-by-step derivation
                        1. Applied rewrites95.2%

                          \[\leadsto x - \frac{y}{\left(z \cdot z\right) \cdot \color{blue}{-0.5641895835477563}} \]
                      10. Recombined 3 regimes into one program.
                      11. Final simplification98.0%

                        \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -185:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 1.35 \cdot 10^{+19}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\left(z \cdot z\right) \cdot -0.5641895835477563}\\ \end{array} \]
                      12. Add Preprocessing

                      Alternative 11: 92.7% accurate, 3.9× speedup?

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

                        1. Initial program 87.0%

                          \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                        2. Add Preprocessing
                        3. Taylor expanded in x around inf

                          \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                        4. Step-by-step derivation
                          1. lower-/.f64100.0

                            \[\leadsto x + \color{blue}{\frac{-1}{x}} \]
                        5. Applied rewrites100.0%

                          \[\leadsto x + \color{blue}{\frac{-1}{x}} \]

                        if -185 < z < 6.4000000000000005e129

                        1. Initial program 98.1%

                          \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                        2. Add Preprocessing
                        3. Step-by-step derivation
                          1. lift-+.f64N/A

                            \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                          2. lift-/.f64N/A

                            \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                          3. frac-2negN/A

                            \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                          4. distribute-frac-neg2N/A

                            \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                          5. unsub-negN/A

                            \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                          6. distribute-frac-negN/A

                            \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                          7. lift-/.f64N/A

                            \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                          8. lower--.f64N/A

                            \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                          9. lift-/.f64N/A

                            \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                          10. distribute-frac-neg2N/A

                            \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                          11. lower-/.f64N/A

                            \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                          12. lift--.f64N/A

                            \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                          13. sub-negN/A

                            \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                          14. distribute-neg-inN/A

                            \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                          15. lift-*.f64N/A

                            \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                          16. distribute-lft-neg-inN/A

                            \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                          17. remove-double-negN/A

                            \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                          18. lower-fma.f64N/A

                            \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                        4. Applied rewrites98.1%

                          \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                        5. Taylor expanded in z around 0

                          \[\leadsto x - \frac{y}{\color{blue}{x \cdot y - \frac{5641895835477563}{5000000000000000}}} \]
                        6. Step-by-step derivation
                          1. sub-negN/A

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

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

                            \[\leadsto x - \frac{y}{y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}} \]
                          4. lower-fma.f6495.2

                            \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}} \]
                        7. Applied rewrites95.2%

                          \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}} \]

                        if 6.4000000000000005e129 < z

                        1. Initial program 97.2%

                          \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                        2. Add Preprocessing
                        3. Step-by-step derivation
                          1. lift-+.f64N/A

                            \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                          2. lift-/.f64N/A

                            \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                          3. frac-2negN/A

                            \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                          4. distribute-frac-neg2N/A

                            \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                          5. unsub-negN/A

                            \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                          6. distribute-frac-negN/A

                            \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                          7. lift-/.f64N/A

                            \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                          8. lower--.f64N/A

                            \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                          9. lift-/.f64N/A

                            \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                          10. distribute-frac-neg2N/A

                            \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                          11. lower-/.f64N/A

                            \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                          12. lift--.f64N/A

                            \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                          13. sub-negN/A

                            \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                          14. distribute-neg-inN/A

                            \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                          15. lift-*.f64N/A

                            \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                          16. distribute-lft-neg-inN/A

                            \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                          17. remove-double-negN/A

                            \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                          18. lower-fma.f64N/A

                            \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                        4. Applied rewrites97.2%

                          \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                        5. Taylor expanded in z around 0

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

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

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

                            \[\leadsto x - \frac{y}{\color{blue}{\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) \cdot z} + \left(x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                          4. lower-fma.f64N/A

                            \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)}} \]
                          5. sub-negN/A

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\frac{-5641895835477563}{10000000000000000} \cdot z + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                          6. metadata-evalN/A

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000} \cdot z + \color{blue}{\frac{-5641895835477563}{5000000000000000}}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                          7. lower-fma.f64N/A

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)}, z, x \cdot y - \frac{5641895835477563}{5000000000000000}\right)} \]
                          8. sub-negN/A

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{x \cdot y + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)}\right)} \]
                          9. *-commutativeN/A

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, \color{blue}{y \cdot x} + \left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right)\right)} \]
                          10. metadata-evalN/A

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-5641895835477563}{10000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right), z, y \cdot x + \color{blue}{\frac{-5641895835477563}{5000000000000000}}\right)} \]
                          11. lower-fma.f64100.0

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \color{blue}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\right)} \]
                        7. Applied rewrites100.0%

                          \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), z, \mathsf{fma}\left(y, x, -1.1283791670955126\right)\right)}} \]
                        8. Taylor expanded in x around 0

                          \[\leadsto x - \frac{y}{z \cdot \left(\frac{-5641895835477563}{10000000000000000} \cdot z - \frac{5641895835477563}{5000000000000000}\right) - \color{blue}{\frac{5641895835477563}{5000000000000000}}} \]
                        9. Step-by-step derivation
                          1. Applied rewrites100.0%

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\mathsf{fma}\left(-0.5641895835477563, z, -1.1283791670955126\right), \color{blue}{z}, -1.1283791670955126\right)} \]
                          2. Taylor expanded in z around 0

                            \[\leadsto x - \frac{y}{\mathsf{fma}\left(\frac{-5641895835477563}{5000000000000000}, z, \frac{-5641895835477563}{5000000000000000}\right)} \]
                          3. Step-by-step derivation
                            1. Applied rewrites83.7%

                              \[\leadsto x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, -1.1283791670955126\right)} \]
                          4. Recombined 3 regimes into one program.
                          5. Final simplification94.6%

                            \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -185:\\ \;\;\;\;\frac{-1}{x} + x\\ \mathbf{elif}\;z \leq 6.4 \cdot 10^{+129}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(y, x, -1.1283791670955126\right)}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, z, -1.1283791670955126\right)}\\ \end{array} \]
                          6. Add Preprocessing

                          Alternative 12: 26.2% accurate, 7.1× speedup?

                          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z \leq -45:\\ \;\;\;\;\frac{-1}{x}\\ \mathbf{else}:\\ \;\;\;\;0.8862269254527579 \cdot y\\ \end{array} \end{array} \]
                          (FPCore (x y z)
                           :precision binary64
                           (if (<= z -45.0) (/ -1.0 x) (* 0.8862269254527579 y)))
                          double code(double x, double y, double z) {
                          	double tmp;
                          	if (z <= -45.0) {
                          		tmp = -1.0 / x;
                          	} else {
                          		tmp = 0.8862269254527579 * y;
                          	}
                          	return tmp;
                          }
                          
                          real(8) function code(x, y, z)
                              real(8), intent (in) :: x
                              real(8), intent (in) :: y
                              real(8), intent (in) :: z
                              real(8) :: tmp
                              if (z <= (-45.0d0)) then
                                  tmp = (-1.0d0) / x
                              else
                                  tmp = 0.8862269254527579d0 * y
                              end if
                              code = tmp
                          end function
                          
                          public static double code(double x, double y, double z) {
                          	double tmp;
                          	if (z <= -45.0) {
                          		tmp = -1.0 / x;
                          	} else {
                          		tmp = 0.8862269254527579 * y;
                          	}
                          	return tmp;
                          }
                          
                          def code(x, y, z):
                          	tmp = 0
                          	if z <= -45.0:
                          		tmp = -1.0 / x
                          	else:
                          		tmp = 0.8862269254527579 * y
                          	return tmp
                          
                          function code(x, y, z)
                          	tmp = 0.0
                          	if (z <= -45.0)
                          		tmp = Float64(-1.0 / x);
                          	else
                          		tmp = Float64(0.8862269254527579 * y);
                          	end
                          	return tmp
                          end
                          
                          function tmp_2 = code(x, y, z)
                          	tmp = 0.0;
                          	if (z <= -45.0)
                          		tmp = -1.0 / x;
                          	else
                          		tmp = 0.8862269254527579 * y;
                          	end
                          	tmp_2 = tmp;
                          end
                          
                          code[x_, y_, z_] := If[LessEqual[z, -45.0], N[(-1.0 / x), $MachinePrecision], N[(0.8862269254527579 * y), $MachinePrecision]]
                          
                          \begin{array}{l}
                          
                          \\
                          \begin{array}{l}
                          \mathbf{if}\;z \leq -45:\\
                          \;\;\;\;\frac{-1}{x}\\
                          
                          \mathbf{else}:\\
                          \;\;\;\;0.8862269254527579 \cdot y\\
                          
                          
                          \end{array}
                          \end{array}
                          
                          Derivation
                          1. Split input into 2 regimes
                          2. if z < -45

                            1. Initial program 87.0%

                              \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                            2. Add Preprocessing
                            3. Step-by-step derivation
                              1. lift-+.f64N/A

                                \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                              2. lift-/.f64N/A

                                \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                              3. frac-2negN/A

                                \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                              4. distribute-frac-neg2N/A

                                \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                              5. unsub-negN/A

                                \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                              6. distribute-frac-negN/A

                                \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                              7. lift-/.f64N/A

                                \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                              8. lower--.f64N/A

                                \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                              9. lift-/.f64N/A

                                \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                              10. distribute-frac-neg2N/A

                                \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                              11. lower-/.f64N/A

                                \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                              12. lift--.f64N/A

                                \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                              13. sub-negN/A

                                \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                              14. distribute-neg-inN/A

                                \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                              15. lift-*.f64N/A

                                \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                              16. distribute-lft-neg-inN/A

                                \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                              17. remove-double-negN/A

                                \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                              18. lower-fma.f64N/A

                                \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                            4. Applied rewrites87.2%

                              \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                            5. Taylor expanded in x around inf

                              \[\leadsto \color{blue}{x \cdot \left(1 - \frac{1}{{x}^{2}}\right)} \]
                            6. Step-by-step derivation
                              1. sub-negN/A

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

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

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

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

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

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

                                \[\leadsto \color{blue}{\mathsf{neg}\left(x \cdot \left(\frac{1}{{x}^{2}} - 1\right)\right)} \]
                              8. sub-negN/A

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

                                \[\leadsto \mathsf{neg}\left(x \cdot \left(\frac{1}{{x}^{2}} + \color{blue}{-1}\right)\right) \]
                              10. distribute-rgt-inN/A

                                \[\leadsto \mathsf{neg}\left(\color{blue}{\left(\frac{1}{{x}^{2}} \cdot x + -1 \cdot x\right)}\right) \]
                              11. distribute-neg-inN/A

                                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\frac{1}{{x}^{2}} \cdot x\right)\right) + \left(\mathsf{neg}\left(-1 \cdot x\right)\right)} \]
                              12. distribute-lft-neg-outN/A

                                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\frac{1}{{x}^{2}}\right)\right) \cdot x} + \left(\mathsf{neg}\left(-1 \cdot x\right)\right) \]
                              13. mul-1-negN/A

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

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

                                \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{1}{{x}^{2}}\right), x, x\right)} \]
                              16. distribute-neg-fracN/A

                                \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\mathsf{neg}\left(1\right)}{{x}^{2}}}, x, x\right) \]
                              17. metadata-evalN/A

                                \[\leadsto \mathsf{fma}\left(\frac{\color{blue}{-1}}{{x}^{2}}, x, x\right) \]
                              18. lower-/.f64N/A

                                \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-1}{{x}^{2}}}, x, x\right) \]
                              19. unpow2N/A

                                \[\leadsto \mathsf{fma}\left(\frac{-1}{\color{blue}{x \cdot x}}, x, x\right) \]
                              20. lower-*.f6476.3

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

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

                              \[\leadsto \frac{-1}{\color{blue}{x}} \]
                            9. Step-by-step derivation
                              1. Applied rewrites48.1%

                                \[\leadsto \frac{-1}{\color{blue}{x}} \]

                              if -45 < z

                              1. Initial program 98.0%

                                \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                              2. Add Preprocessing
                              3. Step-by-step derivation
                                1. lift-+.f64N/A

                                  \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                                2. lift-/.f64N/A

                                  \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                                3. frac-2negN/A

                                  \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                                4. distribute-frac-neg2N/A

                                  \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                                5. unsub-negN/A

                                  \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                                6. distribute-frac-negN/A

                                  \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                                7. lift-/.f64N/A

                                  \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                                8. lower--.f64N/A

                                  \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                                9. lift-/.f64N/A

                                  \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                                10. distribute-frac-neg2N/A

                                  \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                                11. lower-/.f64N/A

                                  \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                                12. lift--.f64N/A

                                  \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                                13. sub-negN/A

                                  \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                                14. distribute-neg-inN/A

                                  \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                                15. lift-*.f64N/A

                                  \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                                16. distribute-lft-neg-inN/A

                                  \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                                17. remove-double-negN/A

                                  \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                                18. lower-fma.f64N/A

                                  \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                              4. Applied rewrites98.0%

                                \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                              5. Taylor expanded in x around 0

                                \[\leadsto \color{blue}{\frac{5000000000000000}{5641895835477563} \cdot \frac{y}{e^{z}}} \]
                              6. Step-by-step derivation
                                1. *-commutativeN/A

                                  \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
                                2. lower-*.f64N/A

                                  \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
                                3. lower-/.f64N/A

                                  \[\leadsto \color{blue}{\frac{y}{e^{z}}} \cdot \frac{5000000000000000}{5641895835477563} \]
                                4. lower-exp.f6418.7

                                  \[\leadsto \frac{y}{\color{blue}{e^{z}}} \cdot 0.8862269254527579 \]
                              7. Applied rewrites18.7%

                                \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot 0.8862269254527579} \]
                              8. Taylor expanded in z around 0

                                \[\leadsto \frac{5000000000000000}{5641895835477563} \cdot \color{blue}{y} \]
                              9. Step-by-step derivation
                                1. Applied rewrites18.4%

                                  \[\leadsto 0.8862269254527579 \cdot \color{blue}{y} \]
                              10. Recombined 2 regimes into one program.
                              11. Add Preprocessing

                              Alternative 13: 14.4% accurate, 21.3× speedup?

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

                                \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]
                              2. Add Preprocessing
                              3. Step-by-step derivation
                                1. lift-+.f64N/A

                                  \[\leadsto \color{blue}{x + \frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                                2. lift-/.f64N/A

                                  \[\leadsto x + \color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                                3. frac-2negN/A

                                  \[\leadsto x + \color{blue}{\frac{\mathsf{neg}\left(y\right)}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                                4. distribute-frac-neg2N/A

                                  \[\leadsto x + \color{blue}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                                5. unsub-negN/A

                                  \[\leadsto \color{blue}{x - \frac{\mathsf{neg}\left(y\right)}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}} \]
                                6. distribute-frac-negN/A

                                  \[\leadsto x - \color{blue}{\left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                                7. lift-/.f64N/A

                                  \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                                8. lower--.f64N/A

                                  \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}\right)\right)} \]
                                9. lift-/.f64N/A

                                  \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\frac{y}{\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y}}\right)\right) \]
                                10. distribute-frac-neg2N/A

                                  \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                                11. lower-/.f64N/A

                                  \[\leadsto x - \color{blue}{\frac{y}{\mathsf{neg}\left(\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)\right)}} \]
                                12. lift--.f64N/A

                                  \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} - x \cdot y\right)}\right)} \]
                                13. sub-negN/A

                                  \[\leadsto x - \frac{y}{\mathsf{neg}\left(\color{blue}{\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z} + \left(\mathsf{neg}\left(x \cdot y\right)\right)\right)}\right)} \]
                                14. distribute-neg-inN/A

                                  \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000} \cdot e^{z}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)}} \]
                                15. lift-*.f64N/A

                                  \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\color{blue}{\frac{5641895835477563}{5000000000000000} \cdot e^{z}}\right)\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                                16. distribute-lft-neg-inN/A

                                  \[\leadsto x - \frac{y}{\color{blue}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z}} + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x \cdot y\right)\right)\right)\right)} \]
                                17. remove-double-negN/A

                                  \[\leadsto x - \frac{y}{\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right)\right) \cdot e^{z} + \color{blue}{x \cdot y}} \]
                                18. lower-fma.f64N/A

                                  \[\leadsto x - \frac{y}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(\frac{5641895835477563}{5000000000000000}\right), e^{z}, x \cdot y\right)}} \]
                              4. Applied rewrites95.8%

                                \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(-1.1283791670955126, e^{z}, y \cdot x\right)}} \]
                              5. Taylor expanded in x around 0

                                \[\leadsto \color{blue}{\frac{5000000000000000}{5641895835477563} \cdot \frac{y}{e^{z}}} \]
                              6. Step-by-step derivation
                                1. *-commutativeN/A

                                  \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
                                2. lower-*.f64N/A

                                  \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot \frac{5000000000000000}{5641895835477563}} \]
                                3. lower-/.f64N/A

                                  \[\leadsto \color{blue}{\frac{y}{e^{z}}} \cdot \frac{5000000000000000}{5641895835477563} \]
                                4. lower-exp.f6415.6

                                  \[\leadsto \frac{y}{\color{blue}{e^{z}}} \cdot 0.8862269254527579 \]
                              7. Applied rewrites15.6%

                                \[\leadsto \color{blue}{\frac{y}{e^{z}} \cdot 0.8862269254527579} \]
                              8. Taylor expanded in z around 0

                                \[\leadsto \frac{5000000000000000}{5641895835477563} \cdot \color{blue}{y} \]
                              9. Step-by-step derivation
                                1. Applied rewrites15.4%

                                  \[\leadsto 0.8862269254527579 \cdot \color{blue}{y} \]
                                2. Add Preprocessing

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

                                \[\begin{array}{l} \\ x + \frac{1}{\frac{1.1283791670955126}{y} \cdot e^{z} - x} \end{array} \]
                                (FPCore (x y z)
                                 :precision binary64
                                 (+ x (/ 1.0 (- (* (/ 1.1283791670955126 y) (exp z)) x))))
                                double code(double x, double y, double z) {
                                	return x + (1.0 / (((1.1283791670955126 / y) * exp(z)) - x));
                                }
                                
                                real(8) function code(x, y, z)
                                    real(8), intent (in) :: x
                                    real(8), intent (in) :: y
                                    real(8), intent (in) :: z
                                    code = x + (1.0d0 / (((1.1283791670955126d0 / y) * exp(z)) - x))
                                end function
                                
                                public static double code(double x, double y, double z) {
                                	return x + (1.0 / (((1.1283791670955126 / y) * Math.exp(z)) - x));
                                }
                                
                                def code(x, y, z):
                                	return x + (1.0 / (((1.1283791670955126 / y) * math.exp(z)) - x))
                                
                                function code(x, y, z)
                                	return Float64(x + Float64(1.0 / Float64(Float64(Float64(1.1283791670955126 / y) * exp(z)) - x)))
                                end
                                
                                function tmp = code(x, y, z)
                                	tmp = x + (1.0 / (((1.1283791670955126 / y) * exp(z)) - x));
                                end
                                
                                code[x_, y_, z_] := N[(x + N[(1.0 / N[(N[(N[(1.1283791670955126 / y), $MachinePrecision] * N[Exp[z], $MachinePrecision]), $MachinePrecision] - x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
                                
                                \begin{array}{l}
                                
                                \\
                                x + \frac{1}{\frac{1.1283791670955126}{y} \cdot e^{z} - x}
                                \end{array}
                                

                                Reproduce

                                ?
                                herbie shell --seed 2024294 
                                (FPCore (x y z)
                                  :name "Numeric.SpecFunctions:invErfc from math-functions-0.1.5.2, A"
                                  :precision binary64
                                
                                  :alt
                                  (! :herbie-platform default (+ x (/ 1 (- (* (/ 5641895835477563/5000000000000000 y) (exp z)) x))))
                                
                                  (+ x (/ y (- (* 1.1283791670955126 (exp z)) (* x y)))))