Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, C

Percentage Accurate: 94.5% → 96.0%
Time: 10.6s
Alternatives: 12
Speedup: 0.7×

Specification

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

\\
x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right)
\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 12 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: 94.5% accurate, 1.0× speedup?

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

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

Alternative 1: 96.0% accurate, 0.7× speedup?

\[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \leq 5 \cdot 10^{-121}:\\ \;\;\;\;\mathsf{fma}\left(x\_m \cdot t, \frac{1}{z + -1}, \frac{x\_m \cdot y}{z}\right)\\ \mathbf{else}:\\ \;\;\;\;x\_m \cdot \left(\frac{y}{z} + \frac{1}{\frac{z + -1}{t}}\right)\\ \end{array} \end{array} \]
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m y z t)
 :precision binary64
 (*
  x_s
  (if (<= x_m 5e-121)
    (fma (* x_m t) (/ 1.0 (+ z -1.0)) (/ (* x_m y) z))
    (* x_m (+ (/ y z) (/ 1.0 (/ (+ z -1.0) t)))))))
x\_m = fabs(x);
x\_s = copysign(1.0, x);
double code(double x_s, double x_m, double y, double z, double t) {
	double tmp;
	if (x_m <= 5e-121) {
		tmp = fma((x_m * t), (1.0 / (z + -1.0)), ((x_m * y) / z));
	} else {
		tmp = x_m * ((y / z) + (1.0 / ((z + -1.0) / t)));
	}
	return x_s * tmp;
}
x\_m = abs(x)
x\_s = copysign(1.0, x)
function code(x_s, x_m, y, z, t)
	tmp = 0.0
	if (x_m <= 5e-121)
		tmp = fma(Float64(x_m * t), Float64(1.0 / Float64(z + -1.0)), Float64(Float64(x_m * y) / z));
	else
		tmp = Float64(x_m * Float64(Float64(y / z) + Float64(1.0 / Float64(Float64(z + -1.0) / t))));
	end
	return Float64(x_s * tmp)
end
x\_m = N[Abs[x], $MachinePrecision]
x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x$95$s_, x$95$m_, y_, z_, t_] := N[(x$95$s * If[LessEqual[x$95$m, 5e-121], N[(N[(x$95$m * t), $MachinePrecision] * N[(1.0 / N[(z + -1.0), $MachinePrecision]), $MachinePrecision] + N[(N[(x$95$m * y), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision], N[(x$95$m * N[(N[(y / z), $MachinePrecision] + N[(1.0 / N[(N[(z + -1.0), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]
\begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \leq 5 \cdot 10^{-121}:\\
\;\;\;\;\mathsf{fma}\left(x\_m \cdot t, \frac{1}{z + -1}, \frac{x\_m \cdot y}{z}\right)\\

\mathbf{else}:\\
\;\;\;\;x\_m \cdot \left(\frac{y}{z} + \frac{1}{\frac{z + -1}{t}}\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if x < 4.99999999999999989e-121

    1. Initial program 91.8%

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

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

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

        \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{\frac{1}{\frac{1 - z}{t}}}\right) \]
      4. lower-/.f6491.8

        \[\leadsto x \cdot \left(\frac{y}{z} - \frac{1}{\color{blue}{\frac{1 - z}{t}}}\right) \]
    4. Applied rewrites91.8%

      \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{\frac{1}{\frac{1 - z}{t}}}\right) \]
    5. Step-by-step derivation
      1. lift-*.f64N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto x \cdot \frac{y}{z} + x \cdot \color{blue}{\frac{t}{z + -1}} \]
      18. div-invN/A

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

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

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

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

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

    if 4.99999999999999989e-121 < x

    1. Initial program 97.7%

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

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

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

        \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{\frac{1}{\frac{1 - z}{t}}}\right) \]
      4. lower-/.f6497.7

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

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

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

Alternative 2: 96.6% accurate, 0.5× speedup?

\[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \frac{y}{z} + \frac{t}{z + -1}\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t\_1 \leq -\infty:\\ \;\;\;\;\frac{x\_m \cdot y}{z}\\ \mathbf{else}:\\ \;\;\;\;x\_m \cdot t\_1\\ \end{array} \end{array} \end{array} \]
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m y z t)
 :precision binary64
 (let* ((t_1 (+ (/ y z) (/ t (+ z -1.0)))))
   (* x_s (if (<= t_1 (- INFINITY)) (/ (* x_m y) z) (* x_m t_1)))))
x\_m = fabs(x);
x\_s = copysign(1.0, x);
double code(double x_s, double x_m, double y, double z, double t) {
	double t_1 = (y / z) + (t / (z + -1.0));
	double tmp;
	if (t_1 <= -((double) INFINITY)) {
		tmp = (x_m * y) / z;
	} else {
		tmp = x_m * t_1;
	}
	return x_s * tmp;
}
x\_m = Math.abs(x);
x\_s = Math.copySign(1.0, x);
public static double code(double x_s, double x_m, double y, double z, double t) {
	double t_1 = (y / z) + (t / (z + -1.0));
	double tmp;
	if (t_1 <= -Double.POSITIVE_INFINITY) {
		tmp = (x_m * y) / z;
	} else {
		tmp = x_m * t_1;
	}
	return x_s * tmp;
}
x\_m = math.fabs(x)
x\_s = math.copysign(1.0, x)
def code(x_s, x_m, y, z, t):
	t_1 = (y / z) + (t / (z + -1.0))
	tmp = 0
	if t_1 <= -math.inf:
		tmp = (x_m * y) / z
	else:
		tmp = x_m * t_1
	return x_s * tmp
x\_m = abs(x)
x\_s = copysign(1.0, x)
function code(x_s, x_m, y, z, t)
	t_1 = Float64(Float64(y / z) + Float64(t / Float64(z + -1.0)))
	tmp = 0.0
	if (t_1 <= Float64(-Inf))
		tmp = Float64(Float64(x_m * y) / z);
	else
		tmp = Float64(x_m * t_1);
	end
	return Float64(x_s * tmp)
end
x\_m = abs(x);
x\_s = sign(x) * abs(1.0);
function tmp_2 = code(x_s, x_m, y, z, t)
	t_1 = (y / z) + (t / (z + -1.0));
	tmp = 0.0;
	if (t_1 <= -Inf)
		tmp = (x_m * y) / z;
	else
		tmp = x_m * t_1;
	end
	tmp_2 = x_s * tmp;
end
x\_m = N[Abs[x], $MachinePrecision]
x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x$95$s_, x$95$m_, y_, z_, t_] := Block[{t$95$1 = N[(N[(y / z), $MachinePrecision] + N[(t / N[(z + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[t$95$1, (-Infinity)], N[(N[(x$95$m * y), $MachinePrecision] / z), $MachinePrecision], N[(x$95$m * t$95$1), $MachinePrecision]]), $MachinePrecision]]
\begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
\begin{array}{l}
t_1 := \frac{y}{z} + \frac{t}{z + -1}\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;t\_1 \leq -\infty:\\
\;\;\;\;\frac{x\_m \cdot y}{z}\\

\mathbf{else}:\\
\;\;\;\;x\_m \cdot t\_1\\


\end{array}
\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (-.f64 (/.f64 y z) (/.f64 t (-.f64 #s(literal 1 binary64) z))) < -inf.0

    1. Initial program 56.8%

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

      \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
    4. Step-by-step derivation
      1. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
      2. lower-*.f6499.9

        \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
    5. Applied rewrites99.9%

      \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]

    if -inf.0 < (-.f64 (/.f64 y z) (/.f64 t (-.f64 #s(literal 1 binary64) z)))

    1. Initial program 96.2%

      \[x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right) \]
    2. Add Preprocessing
  3. Recombined 2 regimes into one program.
  4. Final simplification96.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{z} + \frac{t}{z + -1} \leq -\infty:\\ \;\;\;\;\frac{x \cdot y}{z}\\ \mathbf{else}:\\ \;\;\;\;x \cdot \left(\frac{y}{z} + \frac{t}{z + -1}\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 96.2% accurate, 0.7× speedup?

\[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \leq 5 \cdot 10^{-121}:\\ \;\;\;\;\mathsf{fma}\left(x\_m \cdot t, \frac{1}{z + -1}, \frac{x\_m \cdot y}{z}\right)\\ \mathbf{else}:\\ \;\;\;\;x\_m \cdot \left(\frac{y}{z} + \frac{t}{z + -1}\right)\\ \end{array} \end{array} \]
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m y z t)
 :precision binary64
 (*
  x_s
  (if (<= x_m 5e-121)
    (fma (* x_m t) (/ 1.0 (+ z -1.0)) (/ (* x_m y) z))
    (* x_m (+ (/ y z) (/ t (+ z -1.0)))))))
x\_m = fabs(x);
x\_s = copysign(1.0, x);
double code(double x_s, double x_m, double y, double z, double t) {
	double tmp;
	if (x_m <= 5e-121) {
		tmp = fma((x_m * t), (1.0 / (z + -1.0)), ((x_m * y) / z));
	} else {
		tmp = x_m * ((y / z) + (t / (z + -1.0)));
	}
	return x_s * tmp;
}
x\_m = abs(x)
x\_s = copysign(1.0, x)
function code(x_s, x_m, y, z, t)
	tmp = 0.0
	if (x_m <= 5e-121)
		tmp = fma(Float64(x_m * t), Float64(1.0 / Float64(z + -1.0)), Float64(Float64(x_m * y) / z));
	else
		tmp = Float64(x_m * Float64(Float64(y / z) + Float64(t / Float64(z + -1.0))));
	end
	return Float64(x_s * tmp)
end
x\_m = N[Abs[x], $MachinePrecision]
x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x$95$s_, x$95$m_, y_, z_, t_] := N[(x$95$s * If[LessEqual[x$95$m, 5e-121], N[(N[(x$95$m * t), $MachinePrecision] * N[(1.0 / N[(z + -1.0), $MachinePrecision]), $MachinePrecision] + N[(N[(x$95$m * y), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision], N[(x$95$m * N[(N[(y / z), $MachinePrecision] + N[(t / N[(z + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]
\begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \leq 5 \cdot 10^{-121}:\\
\;\;\;\;\mathsf{fma}\left(x\_m \cdot t, \frac{1}{z + -1}, \frac{x\_m \cdot y}{z}\right)\\

\mathbf{else}:\\
\;\;\;\;x\_m \cdot \left(\frac{y}{z} + \frac{t}{z + -1}\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if x < 4.99999999999999989e-121

    1. Initial program 91.8%

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

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

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

        \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{\frac{1}{\frac{1 - z}{t}}}\right) \]
      4. lower-/.f6491.8

        \[\leadsto x \cdot \left(\frac{y}{z} - \frac{1}{\color{blue}{\frac{1 - z}{t}}}\right) \]
    4. Applied rewrites91.8%

      \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{\frac{1}{\frac{1 - z}{t}}}\right) \]
    5. Step-by-step derivation
      1. lift-*.f64N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto x \cdot \frac{y}{z} + x \cdot \color{blue}{\frac{t}{z + -1}} \]
      18. div-invN/A

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

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

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

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

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

    if 4.99999999999999989e-121 < x

    1. Initial program 97.7%

      \[x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right) \]
    2. Add Preprocessing
  3. Recombined 2 regimes into one program.
  4. Final simplification95.0%

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

Alternative 4: 88.8% accurate, 0.9× speedup?

\[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;z \leq -0.75:\\ \;\;\;\;\frac{x\_m}{z} \cdot \left(t + y\right)\\ \mathbf{elif}\;z \leq 1:\\ \;\;\;\;x\_m \cdot \left(\frac{y}{z} - \mathsf{fma}\left(z, t, t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{x\_m \cdot \left(t + y\right)}{z}\\ \end{array} \end{array} \]
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m y z t)
 :precision binary64
 (*
  x_s
  (if (<= z -0.75)
    (* (/ x_m z) (+ t y))
    (if (<= z 1.0) (* x_m (- (/ y z) (fma z t t))) (/ (* x_m (+ t y)) z)))))
x\_m = fabs(x);
x\_s = copysign(1.0, x);
double code(double x_s, double x_m, double y, double z, double t) {
	double tmp;
	if (z <= -0.75) {
		tmp = (x_m / z) * (t + y);
	} else if (z <= 1.0) {
		tmp = x_m * ((y / z) - fma(z, t, t));
	} else {
		tmp = (x_m * (t + y)) / z;
	}
	return x_s * tmp;
}
x\_m = abs(x)
x\_s = copysign(1.0, x)
function code(x_s, x_m, y, z, t)
	tmp = 0.0
	if (z <= -0.75)
		tmp = Float64(Float64(x_m / z) * Float64(t + y));
	elseif (z <= 1.0)
		tmp = Float64(x_m * Float64(Float64(y / z) - fma(z, t, t)));
	else
		tmp = Float64(Float64(x_m * Float64(t + y)) / z);
	end
	return Float64(x_s * tmp)
end
x\_m = N[Abs[x], $MachinePrecision]
x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x$95$s_, x$95$m_, y_, z_, t_] := N[(x$95$s * If[LessEqual[z, -0.75], N[(N[(x$95$m / z), $MachinePrecision] * N[(t + y), $MachinePrecision]), $MachinePrecision], If[LessEqual[z, 1.0], N[(x$95$m * N[(N[(y / z), $MachinePrecision] - N[(z * t + t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * N[(t + y), $MachinePrecision]), $MachinePrecision] / z), $MachinePrecision]]]), $MachinePrecision]
\begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;z \leq -0.75:\\
\;\;\;\;\frac{x\_m}{z} \cdot \left(t + y\right)\\

\mathbf{elif}\;z \leq 1:\\
\;\;\;\;x\_m \cdot \left(\frac{y}{z} - \mathsf{fma}\left(z, t, t\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{x\_m \cdot \left(t + y\right)}{z}\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if z < -0.75

    1. Initial program 96.3%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      if -0.75 < z < 1

      1. Initial program 92.4%

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

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

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

          \[\leadsto x \cdot \left(\frac{y}{z} - \left(\color{blue}{z \cdot t} + t\right)\right) \]
        3. lower-fma.f6492.3

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

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

      if 1 < z

      1. Initial program 94.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{x \cdot \left(y + t\right)}{z}} \]
    7. Recombined 3 regimes into one program.
    8. Final simplification90.6%

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

    Alternative 5: 88.6% accurate, 1.0× speedup?

    \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;z \leq -0.85:\\ \;\;\;\;\frac{x\_m}{z} \cdot \left(t + y\right)\\ \mathbf{elif}\;z \leq 1:\\ \;\;\;\;x\_m \cdot \left(\frac{y}{z} + \left(-t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{x\_m \cdot \left(t + y\right)}{z}\\ \end{array} \end{array} \]
    x\_m = (fabs.f64 x)
    x\_s = (copysign.f64 #s(literal 1 binary64) x)
    (FPCore (x_s x_m y z t)
     :precision binary64
     (*
      x_s
      (if (<= z -0.85)
        (* (/ x_m z) (+ t y))
        (if (<= z 1.0) (* x_m (+ (/ y z) (- t))) (/ (* x_m (+ t y)) z)))))
    x\_m = fabs(x);
    x\_s = copysign(1.0, x);
    double code(double x_s, double x_m, double y, double z, double t) {
    	double tmp;
    	if (z <= -0.85) {
    		tmp = (x_m / z) * (t + y);
    	} else if (z <= 1.0) {
    		tmp = x_m * ((y / z) + -t);
    	} else {
    		tmp = (x_m * (t + y)) / z;
    	}
    	return x_s * tmp;
    }
    
    x\_m = abs(x)
    x\_s = copysign(1.0d0, x)
    real(8) function code(x_s, x_m, y, z, t)
        real(8), intent (in) :: x_s
        real(8), intent (in) :: x_m
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: tmp
        if (z <= (-0.85d0)) then
            tmp = (x_m / z) * (t + y)
        else if (z <= 1.0d0) then
            tmp = x_m * ((y / z) + -t)
        else
            tmp = (x_m * (t + y)) / z
        end if
        code = x_s * tmp
    end function
    
    x\_m = Math.abs(x);
    x\_s = Math.copySign(1.0, x);
    public static double code(double x_s, double x_m, double y, double z, double t) {
    	double tmp;
    	if (z <= -0.85) {
    		tmp = (x_m / z) * (t + y);
    	} else if (z <= 1.0) {
    		tmp = x_m * ((y / z) + -t);
    	} else {
    		tmp = (x_m * (t + y)) / z;
    	}
    	return x_s * tmp;
    }
    
    x\_m = math.fabs(x)
    x\_s = math.copysign(1.0, x)
    def code(x_s, x_m, y, z, t):
    	tmp = 0
    	if z <= -0.85:
    		tmp = (x_m / z) * (t + y)
    	elif z <= 1.0:
    		tmp = x_m * ((y / z) + -t)
    	else:
    		tmp = (x_m * (t + y)) / z
    	return x_s * tmp
    
    x\_m = abs(x)
    x\_s = copysign(1.0, x)
    function code(x_s, x_m, y, z, t)
    	tmp = 0.0
    	if (z <= -0.85)
    		tmp = Float64(Float64(x_m / z) * Float64(t + y));
    	elseif (z <= 1.0)
    		tmp = Float64(x_m * Float64(Float64(y / z) + Float64(-t)));
    	else
    		tmp = Float64(Float64(x_m * Float64(t + y)) / z);
    	end
    	return Float64(x_s * tmp)
    end
    
    x\_m = abs(x);
    x\_s = sign(x) * abs(1.0);
    function tmp_2 = code(x_s, x_m, y, z, t)
    	tmp = 0.0;
    	if (z <= -0.85)
    		tmp = (x_m / z) * (t + y);
    	elseif (z <= 1.0)
    		tmp = x_m * ((y / z) + -t);
    	else
    		tmp = (x_m * (t + y)) / z;
    	end
    	tmp_2 = x_s * tmp;
    end
    
    x\_m = N[Abs[x], $MachinePrecision]
    x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
    code[x$95$s_, x$95$m_, y_, z_, t_] := N[(x$95$s * If[LessEqual[z, -0.85], N[(N[(x$95$m / z), $MachinePrecision] * N[(t + y), $MachinePrecision]), $MachinePrecision], If[LessEqual[z, 1.0], N[(x$95$m * N[(N[(y / z), $MachinePrecision] + (-t)), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * N[(t + y), $MachinePrecision]), $MachinePrecision] / z), $MachinePrecision]]]), $MachinePrecision]
    
    \begin{array}{l}
    x\_m = \left|x\right|
    \\
    x\_s = \mathsf{copysign}\left(1, x\right)
    
    \\
    x\_s \cdot \begin{array}{l}
    \mathbf{if}\;z \leq -0.85:\\
    \;\;\;\;\frac{x\_m}{z} \cdot \left(t + y\right)\\
    
    \mathbf{elif}\;z \leq 1:\\
    \;\;\;\;x\_m \cdot \left(\frac{y}{z} + \left(-t\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{x\_m \cdot \left(t + y\right)}{z}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 3 regimes
    2. if z < -0.849999999999999978

      1. Initial program 96.3%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        if -0.849999999999999978 < z < 1

        1. Initial program 92.4%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto x \cdot \mathsf{fma}\left(\frac{1}{z}, y, \frac{t}{-1 + \color{blue}{z}}\right) \]
          16. lower-+.f6492.3

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

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

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

            \[\leadsto x \cdot \mathsf{fma}\left(\frac{1}{z}, y, \color{blue}{\mathsf{neg}\left(t\right)}\right) \]
          2. lower-neg.f6491.8

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

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

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

            \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{z}, y, \mathsf{neg}\left(t\right)\right) \cdot x} \]
          3. lower-*.f6491.8

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

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

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

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

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

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

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

            \[\leadsto \left(\left(\mathsf{neg}\left(t\right)\right) + \color{blue}{\frac{y}{z}}\right) \cdot x \]
        9. Applied rewrites91.8%

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

        if 1 < z

        1. Initial program 94.9%

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \color{blue}{\frac{x \cdot \left(y + t\right)}{z}} \]
      7. Recombined 3 regimes into one program.
      8. Final simplification90.3%

        \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -0.85:\\ \;\;\;\;\frac{x}{z} \cdot \left(t + y\right)\\ \mathbf{elif}\;z \leq 1:\\ \;\;\;\;x \cdot \left(\frac{y}{z} + \left(-t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot \left(t + y\right)}{z}\\ \end{array} \]
      9. Add Preprocessing

      Alternative 6: 74.2% accurate, 1.1× speedup?

      \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := x\_m \cdot \frac{t}{z + -1}\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t \leq -1.35 \cdot 10^{+66}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t \leq 330000000000:\\ \;\;\;\;\frac{x\_m \cdot y}{z}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \end{array} \]
      x\_m = (fabs.f64 x)
      x\_s = (copysign.f64 #s(literal 1 binary64) x)
      (FPCore (x_s x_m y z t)
       :precision binary64
       (let* ((t_1 (* x_m (/ t (+ z -1.0)))))
         (*
          x_s
          (if (<= t -1.35e+66) t_1 (if (<= t 330000000000.0) (/ (* x_m y) z) t_1)))))
      x\_m = fabs(x);
      x\_s = copysign(1.0, x);
      double code(double x_s, double x_m, double y, double z, double t) {
      	double t_1 = x_m * (t / (z + -1.0));
      	double tmp;
      	if (t <= -1.35e+66) {
      		tmp = t_1;
      	} else if (t <= 330000000000.0) {
      		tmp = (x_m * y) / z;
      	} else {
      		tmp = t_1;
      	}
      	return x_s * tmp;
      }
      
      x\_m = abs(x)
      x\_s = copysign(1.0d0, x)
      real(8) function code(x_s, x_m, y, z, t)
          real(8), intent (in) :: x_s
          real(8), intent (in) :: x_m
          real(8), intent (in) :: y
          real(8), intent (in) :: z
          real(8), intent (in) :: t
          real(8) :: t_1
          real(8) :: tmp
          t_1 = x_m * (t / (z + (-1.0d0)))
          if (t <= (-1.35d+66)) then
              tmp = t_1
          else if (t <= 330000000000.0d0) then
              tmp = (x_m * y) / z
          else
              tmp = t_1
          end if
          code = x_s * tmp
      end function
      
      x\_m = Math.abs(x);
      x\_s = Math.copySign(1.0, x);
      public static double code(double x_s, double x_m, double y, double z, double t) {
      	double t_1 = x_m * (t / (z + -1.0));
      	double tmp;
      	if (t <= -1.35e+66) {
      		tmp = t_1;
      	} else if (t <= 330000000000.0) {
      		tmp = (x_m * y) / z;
      	} else {
      		tmp = t_1;
      	}
      	return x_s * tmp;
      }
      
      x\_m = math.fabs(x)
      x\_s = math.copysign(1.0, x)
      def code(x_s, x_m, y, z, t):
      	t_1 = x_m * (t / (z + -1.0))
      	tmp = 0
      	if t <= -1.35e+66:
      		tmp = t_1
      	elif t <= 330000000000.0:
      		tmp = (x_m * y) / z
      	else:
      		tmp = t_1
      	return x_s * tmp
      
      x\_m = abs(x)
      x\_s = copysign(1.0, x)
      function code(x_s, x_m, y, z, t)
      	t_1 = Float64(x_m * Float64(t / Float64(z + -1.0)))
      	tmp = 0.0
      	if (t <= -1.35e+66)
      		tmp = t_1;
      	elseif (t <= 330000000000.0)
      		tmp = Float64(Float64(x_m * y) / z);
      	else
      		tmp = t_1;
      	end
      	return Float64(x_s * tmp)
      end
      
      x\_m = abs(x);
      x\_s = sign(x) * abs(1.0);
      function tmp_2 = code(x_s, x_m, y, z, t)
      	t_1 = x_m * (t / (z + -1.0));
      	tmp = 0.0;
      	if (t <= -1.35e+66)
      		tmp = t_1;
      	elseif (t <= 330000000000.0)
      		tmp = (x_m * y) / z;
      	else
      		tmp = t_1;
      	end
      	tmp_2 = x_s * tmp;
      end
      
      x\_m = N[Abs[x], $MachinePrecision]
      x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      code[x$95$s_, x$95$m_, y_, z_, t_] := Block[{t$95$1 = N[(x$95$m * N[(t / N[(z + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[t, -1.35e+66], t$95$1, If[LessEqual[t, 330000000000.0], N[(N[(x$95$m * y), $MachinePrecision] / z), $MachinePrecision], t$95$1]]), $MachinePrecision]]
      
      \begin{array}{l}
      x\_m = \left|x\right|
      \\
      x\_s = \mathsf{copysign}\left(1, x\right)
      
      \\
      \begin{array}{l}
      t_1 := x\_m \cdot \frac{t}{z + -1}\\
      x\_s \cdot \begin{array}{l}
      \mathbf{if}\;t \leq -1.35 \cdot 10^{+66}:\\
      \;\;\;\;t\_1\\
      
      \mathbf{elif}\;t \leq 330000000000:\\
      \;\;\;\;\frac{x\_m \cdot y}{z}\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_1\\
      
      
      \end{array}
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if t < -1.35e66 or 3.3e11 < t

        1. Initial program 95.4%

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

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

            \[\leadsto x \cdot \color{blue}{\left(\mathsf{neg}\left(\frac{t}{1 - z}\right)\right)} \]
          2. distribute-neg-frac2N/A

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

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

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

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

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

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

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

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

            \[\leadsto x \cdot \frac{t}{z + \color{blue}{-1}} \]
          11. lower-+.f6476.0

            \[\leadsto x \cdot \frac{t}{\color{blue}{z + -1}} \]
        5. Applied rewrites76.0%

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

        if -1.35e66 < t < 3.3e11

        1. Initial program 92.8%

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

          \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
        4. Step-by-step derivation
          1. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
          2. lower-*.f6487.9

            \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
        5. Applied rewrites87.9%

          \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
      3. Recombined 2 regimes into one program.
      4. Add Preprocessing

      Alternative 7: 74.6% accurate, 1.1× speedup?

      \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \frac{x\_m}{z} \cdot \left(t + y\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;y \leq -8.8 \cdot 10^{-162}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;y \leq 4.7 \cdot 10^{-246}:\\ \;\;\;\;\frac{x\_m \cdot t}{z + -1}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \end{array} \]
      x\_m = (fabs.f64 x)
      x\_s = (copysign.f64 #s(literal 1 binary64) x)
      (FPCore (x_s x_m y z t)
       :precision binary64
       (let* ((t_1 (* (/ x_m z) (+ t y))))
         (*
          x_s
          (if (<= y -8.8e-162)
            t_1
            (if (<= y 4.7e-246) (/ (* x_m t) (+ z -1.0)) t_1)))))
      x\_m = fabs(x);
      x\_s = copysign(1.0, x);
      double code(double x_s, double x_m, double y, double z, double t) {
      	double t_1 = (x_m / z) * (t + y);
      	double tmp;
      	if (y <= -8.8e-162) {
      		tmp = t_1;
      	} else if (y <= 4.7e-246) {
      		tmp = (x_m * t) / (z + -1.0);
      	} else {
      		tmp = t_1;
      	}
      	return x_s * tmp;
      }
      
      x\_m = abs(x)
      x\_s = copysign(1.0d0, x)
      real(8) function code(x_s, x_m, y, z, t)
          real(8), intent (in) :: x_s
          real(8), intent (in) :: x_m
          real(8), intent (in) :: y
          real(8), intent (in) :: z
          real(8), intent (in) :: t
          real(8) :: t_1
          real(8) :: tmp
          t_1 = (x_m / z) * (t + y)
          if (y <= (-8.8d-162)) then
              tmp = t_1
          else if (y <= 4.7d-246) then
              tmp = (x_m * t) / (z + (-1.0d0))
          else
              tmp = t_1
          end if
          code = x_s * tmp
      end function
      
      x\_m = Math.abs(x);
      x\_s = Math.copySign(1.0, x);
      public static double code(double x_s, double x_m, double y, double z, double t) {
      	double t_1 = (x_m / z) * (t + y);
      	double tmp;
      	if (y <= -8.8e-162) {
      		tmp = t_1;
      	} else if (y <= 4.7e-246) {
      		tmp = (x_m * t) / (z + -1.0);
      	} else {
      		tmp = t_1;
      	}
      	return x_s * tmp;
      }
      
      x\_m = math.fabs(x)
      x\_s = math.copysign(1.0, x)
      def code(x_s, x_m, y, z, t):
      	t_1 = (x_m / z) * (t + y)
      	tmp = 0
      	if y <= -8.8e-162:
      		tmp = t_1
      	elif y <= 4.7e-246:
      		tmp = (x_m * t) / (z + -1.0)
      	else:
      		tmp = t_1
      	return x_s * tmp
      
      x\_m = abs(x)
      x\_s = copysign(1.0, x)
      function code(x_s, x_m, y, z, t)
      	t_1 = Float64(Float64(x_m / z) * Float64(t + y))
      	tmp = 0.0
      	if (y <= -8.8e-162)
      		tmp = t_1;
      	elseif (y <= 4.7e-246)
      		tmp = Float64(Float64(x_m * t) / Float64(z + -1.0));
      	else
      		tmp = t_1;
      	end
      	return Float64(x_s * tmp)
      end
      
      x\_m = abs(x);
      x\_s = sign(x) * abs(1.0);
      function tmp_2 = code(x_s, x_m, y, z, t)
      	t_1 = (x_m / z) * (t + y);
      	tmp = 0.0;
      	if (y <= -8.8e-162)
      		tmp = t_1;
      	elseif (y <= 4.7e-246)
      		tmp = (x_m * t) / (z + -1.0);
      	else
      		tmp = t_1;
      	end
      	tmp_2 = x_s * tmp;
      end
      
      x\_m = N[Abs[x], $MachinePrecision]
      x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      code[x$95$s_, x$95$m_, y_, z_, t_] := Block[{t$95$1 = N[(N[(x$95$m / z), $MachinePrecision] * N[(t + y), $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[y, -8.8e-162], t$95$1, If[LessEqual[y, 4.7e-246], N[(N[(x$95$m * t), $MachinePrecision] / N[(z + -1.0), $MachinePrecision]), $MachinePrecision], t$95$1]]), $MachinePrecision]]
      
      \begin{array}{l}
      x\_m = \left|x\right|
      \\
      x\_s = \mathsf{copysign}\left(1, x\right)
      
      \\
      \begin{array}{l}
      t_1 := \frac{x\_m}{z} \cdot \left(t + y\right)\\
      x\_s \cdot \begin{array}{l}
      \mathbf{if}\;y \leq -8.8 \cdot 10^{-162}:\\
      \;\;\;\;t\_1\\
      
      \mathbf{elif}\;y \leq 4.7 \cdot 10^{-246}:\\
      \;\;\;\;\frac{x\_m \cdot t}{z + -1}\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_1\\
      
      
      \end{array}
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if y < -8.7999999999999997e-162 or 4.69999999999999955e-246 < y

        1. Initial program 93.4%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          if -8.7999999999999997e-162 < y < 4.69999999999999955e-246

          1. Initial program 95.9%

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

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

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

              \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{\frac{1}{\frac{1 - z}{t}}}\right) \]
            4. lower-/.f6495.9

              \[\leadsto x \cdot \left(\frac{y}{z} - \frac{1}{\color{blue}{\frac{1 - z}{t}}}\right) \]
          4. Applied rewrites95.9%

            \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{\frac{1}{\frac{1 - z}{t}}}\right) \]
          5. Step-by-step derivation
            1. lift-*.f64N/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

              \[\leadsto x \cdot \frac{y}{z} + x \cdot \color{blue}{\frac{t}{z + -1}} \]
            18. div-invN/A

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{t \cdot x}{z - 1}} \]
          8. Step-by-step derivation
            1. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{t \cdot x}{z - 1}} \]
            2. *-commutativeN/A

              \[\leadsto \frac{\color{blue}{x \cdot t}}{z - 1} \]
            3. lower-*.f64N/A

              \[\leadsto \frac{\color{blue}{x \cdot t}}{z - 1} \]
            4. sub-negN/A

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

              \[\leadsto \frac{x \cdot t}{z + \color{blue}{-1}} \]
            6. lower-+.f6483.9

              \[\leadsto \frac{x \cdot t}{\color{blue}{z + -1}} \]
          9. Applied rewrites83.9%

            \[\leadsto \color{blue}{\frac{x \cdot t}{z + -1}} \]
        7. Recombined 2 regimes into one program.
        8. Final simplification81.3%

          \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -8.8 \cdot 10^{-162}:\\ \;\;\;\;\frac{x}{z} \cdot \left(t + y\right)\\ \mathbf{elif}\;y \leq 4.7 \cdot 10^{-246}:\\ \;\;\;\;\frac{x \cdot t}{z + -1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{z} \cdot \left(t + y\right)\\ \end{array} \]
        9. Add Preprocessing

        Alternative 8: 71.1% accurate, 1.1× speedup?

        \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := t \cdot \frac{x\_m}{z + -1}\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t \leq -2.5 \cdot 10^{+85}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t \leq 350000000000:\\ \;\;\;\;\frac{x\_m \cdot y}{z}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \end{array} \]
        x\_m = (fabs.f64 x)
        x\_s = (copysign.f64 #s(literal 1 binary64) x)
        (FPCore (x_s x_m y z t)
         :precision binary64
         (let* ((t_1 (* t (/ x_m (+ z -1.0)))))
           (*
            x_s
            (if (<= t -2.5e+85) t_1 (if (<= t 350000000000.0) (/ (* x_m y) z) t_1)))))
        x\_m = fabs(x);
        x\_s = copysign(1.0, x);
        double code(double x_s, double x_m, double y, double z, double t) {
        	double t_1 = t * (x_m / (z + -1.0));
        	double tmp;
        	if (t <= -2.5e+85) {
        		tmp = t_1;
        	} else if (t <= 350000000000.0) {
        		tmp = (x_m * y) / z;
        	} else {
        		tmp = t_1;
        	}
        	return x_s * tmp;
        }
        
        x\_m = abs(x)
        x\_s = copysign(1.0d0, x)
        real(8) function code(x_s, x_m, y, z, t)
            real(8), intent (in) :: x_s
            real(8), intent (in) :: x_m
            real(8), intent (in) :: y
            real(8), intent (in) :: z
            real(8), intent (in) :: t
            real(8) :: t_1
            real(8) :: tmp
            t_1 = t * (x_m / (z + (-1.0d0)))
            if (t <= (-2.5d+85)) then
                tmp = t_1
            else if (t <= 350000000000.0d0) then
                tmp = (x_m * y) / z
            else
                tmp = t_1
            end if
            code = x_s * tmp
        end function
        
        x\_m = Math.abs(x);
        x\_s = Math.copySign(1.0, x);
        public static double code(double x_s, double x_m, double y, double z, double t) {
        	double t_1 = t * (x_m / (z + -1.0));
        	double tmp;
        	if (t <= -2.5e+85) {
        		tmp = t_1;
        	} else if (t <= 350000000000.0) {
        		tmp = (x_m * y) / z;
        	} else {
        		tmp = t_1;
        	}
        	return x_s * tmp;
        }
        
        x\_m = math.fabs(x)
        x\_s = math.copysign(1.0, x)
        def code(x_s, x_m, y, z, t):
        	t_1 = t * (x_m / (z + -1.0))
        	tmp = 0
        	if t <= -2.5e+85:
        		tmp = t_1
        	elif t <= 350000000000.0:
        		tmp = (x_m * y) / z
        	else:
        		tmp = t_1
        	return x_s * tmp
        
        x\_m = abs(x)
        x\_s = copysign(1.0, x)
        function code(x_s, x_m, y, z, t)
        	t_1 = Float64(t * Float64(x_m / Float64(z + -1.0)))
        	tmp = 0.0
        	if (t <= -2.5e+85)
        		tmp = t_1;
        	elseif (t <= 350000000000.0)
        		tmp = Float64(Float64(x_m * y) / z);
        	else
        		tmp = t_1;
        	end
        	return Float64(x_s * tmp)
        end
        
        x\_m = abs(x);
        x\_s = sign(x) * abs(1.0);
        function tmp_2 = code(x_s, x_m, y, z, t)
        	t_1 = t * (x_m / (z + -1.0));
        	tmp = 0.0;
        	if (t <= -2.5e+85)
        		tmp = t_1;
        	elseif (t <= 350000000000.0)
        		tmp = (x_m * y) / z;
        	else
        		tmp = t_1;
        	end
        	tmp_2 = x_s * tmp;
        end
        
        x\_m = N[Abs[x], $MachinePrecision]
        x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$95$s_, x$95$m_, y_, z_, t_] := Block[{t$95$1 = N[(t * N[(x$95$m / N[(z + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[t, -2.5e+85], t$95$1, If[LessEqual[t, 350000000000.0], N[(N[(x$95$m * y), $MachinePrecision] / z), $MachinePrecision], t$95$1]]), $MachinePrecision]]
        
        \begin{array}{l}
        x\_m = \left|x\right|
        \\
        x\_s = \mathsf{copysign}\left(1, x\right)
        
        \\
        \begin{array}{l}
        t_1 := t \cdot \frac{x\_m}{z + -1}\\
        x\_s \cdot \begin{array}{l}
        \mathbf{if}\;t \leq -2.5 \cdot 10^{+85}:\\
        \;\;\;\;t\_1\\
        
        \mathbf{elif}\;t \leq 350000000000:\\
        \;\;\;\;\frac{x\_m \cdot y}{z}\\
        
        \mathbf{else}:\\
        \;\;\;\;t\_1\\
        
        
        \end{array}
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if t < -2.5e85 or 3.5e11 < t

          1. Initial program 95.2%

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

            \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
          4. Step-by-step derivation
            1. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
            2. lower-*.f6431.2

              \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
          5. Applied rewrites31.2%

            \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
          6. Taylor expanded in y around 0

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

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

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

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

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

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

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

              \[\leadsto \mathsf{neg}\left(\frac{t \cdot x}{\mathsf{neg}\left(\color{blue}{\left(z - 1\right)}\right)}\right) \]
            8. distribute-neg-frac2N/A

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

              \[\leadsto \color{blue}{\frac{t \cdot x}{z - 1}} \]
            10. associate-/l*N/A

              \[\leadsto \color{blue}{t \cdot \frac{x}{z - 1}} \]
            11. lower-*.f64N/A

              \[\leadsto \color{blue}{t \cdot \frac{x}{z - 1}} \]
            12. lower-/.f64N/A

              \[\leadsto t \cdot \color{blue}{\frac{x}{z - 1}} \]
            13. sub-negN/A

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

              \[\leadsto t \cdot \frac{x}{z + \color{blue}{-1}} \]
            15. lower-+.f6471.6

              \[\leadsto t \cdot \frac{x}{\color{blue}{z + -1}} \]
          8. Applied rewrites71.6%

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

          if -2.5e85 < t < 3.5e11

          1. Initial program 92.9%

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

            \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
          4. Step-by-step derivation
            1. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
            2. lower-*.f6487.1

              \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
          5. Applied rewrites87.1%

            \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
        3. Recombined 2 regimes into one program.
        4. Add Preprocessing

        Alternative 9: 66.7% accurate, 1.2× speedup?

        \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := x\_m \cdot \frac{t}{z}\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t \leq -1.45 \cdot 10^{+67}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t \leq 6.5 \cdot 10^{+109}:\\ \;\;\;\;\frac{x\_m \cdot y}{z}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \end{array} \]
        x\_m = (fabs.f64 x)
        x\_s = (copysign.f64 #s(literal 1 binary64) x)
        (FPCore (x_s x_m y z t)
         :precision binary64
         (let* ((t_1 (* x_m (/ t z))))
           (* x_s (if (<= t -1.45e+67) t_1 (if (<= t 6.5e+109) (/ (* x_m y) z) t_1)))))
        x\_m = fabs(x);
        x\_s = copysign(1.0, x);
        double code(double x_s, double x_m, double y, double z, double t) {
        	double t_1 = x_m * (t / z);
        	double tmp;
        	if (t <= -1.45e+67) {
        		tmp = t_1;
        	} else if (t <= 6.5e+109) {
        		tmp = (x_m * y) / z;
        	} else {
        		tmp = t_1;
        	}
        	return x_s * tmp;
        }
        
        x\_m = abs(x)
        x\_s = copysign(1.0d0, x)
        real(8) function code(x_s, x_m, y, z, t)
            real(8), intent (in) :: x_s
            real(8), intent (in) :: x_m
            real(8), intent (in) :: y
            real(8), intent (in) :: z
            real(8), intent (in) :: t
            real(8) :: t_1
            real(8) :: tmp
            t_1 = x_m * (t / z)
            if (t <= (-1.45d+67)) then
                tmp = t_1
            else if (t <= 6.5d+109) then
                tmp = (x_m * y) / z
            else
                tmp = t_1
            end if
            code = x_s * tmp
        end function
        
        x\_m = Math.abs(x);
        x\_s = Math.copySign(1.0, x);
        public static double code(double x_s, double x_m, double y, double z, double t) {
        	double t_1 = x_m * (t / z);
        	double tmp;
        	if (t <= -1.45e+67) {
        		tmp = t_1;
        	} else if (t <= 6.5e+109) {
        		tmp = (x_m * y) / z;
        	} else {
        		tmp = t_1;
        	}
        	return x_s * tmp;
        }
        
        x\_m = math.fabs(x)
        x\_s = math.copysign(1.0, x)
        def code(x_s, x_m, y, z, t):
        	t_1 = x_m * (t / z)
        	tmp = 0
        	if t <= -1.45e+67:
        		tmp = t_1
        	elif t <= 6.5e+109:
        		tmp = (x_m * y) / z
        	else:
        		tmp = t_1
        	return x_s * tmp
        
        x\_m = abs(x)
        x\_s = copysign(1.0, x)
        function code(x_s, x_m, y, z, t)
        	t_1 = Float64(x_m * Float64(t / z))
        	tmp = 0.0
        	if (t <= -1.45e+67)
        		tmp = t_1;
        	elseif (t <= 6.5e+109)
        		tmp = Float64(Float64(x_m * y) / z);
        	else
        		tmp = t_1;
        	end
        	return Float64(x_s * tmp)
        end
        
        x\_m = abs(x);
        x\_s = sign(x) * abs(1.0);
        function tmp_2 = code(x_s, x_m, y, z, t)
        	t_1 = x_m * (t / z);
        	tmp = 0.0;
        	if (t <= -1.45e+67)
        		tmp = t_1;
        	elseif (t <= 6.5e+109)
        		tmp = (x_m * y) / z;
        	else
        		tmp = t_1;
        	end
        	tmp_2 = x_s * tmp;
        end
        
        x\_m = N[Abs[x], $MachinePrecision]
        x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        code[x$95$s_, x$95$m_, y_, z_, t_] := Block[{t$95$1 = N[(x$95$m * N[(t / z), $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[t, -1.45e+67], t$95$1, If[LessEqual[t, 6.5e+109], N[(N[(x$95$m * y), $MachinePrecision] / z), $MachinePrecision], t$95$1]]), $MachinePrecision]]
        
        \begin{array}{l}
        x\_m = \left|x\right|
        \\
        x\_s = \mathsf{copysign}\left(1, x\right)
        
        \\
        \begin{array}{l}
        t_1 := x\_m \cdot \frac{t}{z}\\
        x\_s \cdot \begin{array}{l}
        \mathbf{if}\;t \leq -1.45 \cdot 10^{+67}:\\
        \;\;\;\;t\_1\\
        
        \mathbf{elif}\;t \leq 6.5 \cdot 10^{+109}:\\
        \;\;\;\;\frac{x\_m \cdot y}{z}\\
        
        \mathbf{else}:\\
        \;\;\;\;t\_1\\
        
        
        \end{array}
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if t < -1.45000000000000012e67 or 6.5e109 < t

          1. Initial program 95.4%

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

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

              \[\leadsto x \cdot \color{blue}{\left(\mathsf{neg}\left(\frac{t}{1 - z}\right)\right)} \]
            2. distribute-neg-frac2N/A

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

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

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

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

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

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

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

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

              \[\leadsto x \cdot \frac{t}{z + \color{blue}{-1}} \]
            11. lower-+.f6476.9

              \[\leadsto x \cdot \frac{t}{\color{blue}{z + -1}} \]
          5. Applied rewrites76.9%

            \[\leadsto x \cdot \color{blue}{\frac{t}{z + -1}} \]
          6. Taylor expanded in z around inf

            \[\leadsto x \cdot \frac{t}{\color{blue}{z}} \]
          7. Step-by-step derivation
            1. Applied rewrites50.4%

              \[\leadsto x \cdot \frac{t}{\color{blue}{z}} \]

            if -1.45000000000000012e67 < t < 6.5e109

            1. Initial program 93.1%

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

              \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
            4. Step-by-step derivation
              1. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
              2. lower-*.f6482.2

                \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
            5. Applied rewrites82.2%

              \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
          8. Recombined 2 regimes into one program.
          9. Add Preprocessing

          Alternative 10: 62.6% accurate, 1.2× speedup?

          \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;y \leq -8.5 \cdot 10^{-178}:\\ \;\;\;\;\frac{x\_m \cdot y}{z}\\ \mathbf{elif}\;y \leq 4.7 \cdot 10^{-246}:\\ \;\;\;\;x\_m \cdot \left(-t\right)\\ \mathbf{else}:\\ \;\;\;\;y \cdot \frac{x\_m}{z}\\ \end{array} \end{array} \]
          x\_m = (fabs.f64 x)
          x\_s = (copysign.f64 #s(literal 1 binary64) x)
          (FPCore (x_s x_m y z t)
           :precision binary64
           (*
            x_s
            (if (<= y -8.5e-178)
              (/ (* x_m y) z)
              (if (<= y 4.7e-246) (* x_m (- t)) (* y (/ x_m z))))))
          x\_m = fabs(x);
          x\_s = copysign(1.0, x);
          double code(double x_s, double x_m, double y, double z, double t) {
          	double tmp;
          	if (y <= -8.5e-178) {
          		tmp = (x_m * y) / z;
          	} else if (y <= 4.7e-246) {
          		tmp = x_m * -t;
          	} else {
          		tmp = y * (x_m / z);
          	}
          	return x_s * tmp;
          }
          
          x\_m = abs(x)
          x\_s = copysign(1.0d0, x)
          real(8) function code(x_s, x_m, y, z, t)
              real(8), intent (in) :: x_s
              real(8), intent (in) :: x_m
              real(8), intent (in) :: y
              real(8), intent (in) :: z
              real(8), intent (in) :: t
              real(8) :: tmp
              if (y <= (-8.5d-178)) then
                  tmp = (x_m * y) / z
              else if (y <= 4.7d-246) then
                  tmp = x_m * -t
              else
                  tmp = y * (x_m / z)
              end if
              code = x_s * tmp
          end function
          
          x\_m = Math.abs(x);
          x\_s = Math.copySign(1.0, x);
          public static double code(double x_s, double x_m, double y, double z, double t) {
          	double tmp;
          	if (y <= -8.5e-178) {
          		tmp = (x_m * y) / z;
          	} else if (y <= 4.7e-246) {
          		tmp = x_m * -t;
          	} else {
          		tmp = y * (x_m / z);
          	}
          	return x_s * tmp;
          }
          
          x\_m = math.fabs(x)
          x\_s = math.copysign(1.0, x)
          def code(x_s, x_m, y, z, t):
          	tmp = 0
          	if y <= -8.5e-178:
          		tmp = (x_m * y) / z
          	elif y <= 4.7e-246:
          		tmp = x_m * -t
          	else:
          		tmp = y * (x_m / z)
          	return x_s * tmp
          
          x\_m = abs(x)
          x\_s = copysign(1.0, x)
          function code(x_s, x_m, y, z, t)
          	tmp = 0.0
          	if (y <= -8.5e-178)
          		tmp = Float64(Float64(x_m * y) / z);
          	elseif (y <= 4.7e-246)
          		tmp = Float64(x_m * Float64(-t));
          	else
          		tmp = Float64(y * Float64(x_m / z));
          	end
          	return Float64(x_s * tmp)
          end
          
          x\_m = abs(x);
          x\_s = sign(x) * abs(1.0);
          function tmp_2 = code(x_s, x_m, y, z, t)
          	tmp = 0.0;
          	if (y <= -8.5e-178)
          		tmp = (x_m * y) / z;
          	elseif (y <= 4.7e-246)
          		tmp = x_m * -t;
          	else
          		tmp = y * (x_m / z);
          	end
          	tmp_2 = x_s * tmp;
          end
          
          x\_m = N[Abs[x], $MachinePrecision]
          x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
          code[x$95$s_, x$95$m_, y_, z_, t_] := N[(x$95$s * If[LessEqual[y, -8.5e-178], N[(N[(x$95$m * y), $MachinePrecision] / z), $MachinePrecision], If[LessEqual[y, 4.7e-246], N[(x$95$m * (-t)), $MachinePrecision], N[(y * N[(x$95$m / z), $MachinePrecision]), $MachinePrecision]]]), $MachinePrecision]
          
          \begin{array}{l}
          x\_m = \left|x\right|
          \\
          x\_s = \mathsf{copysign}\left(1, x\right)
          
          \\
          x\_s \cdot \begin{array}{l}
          \mathbf{if}\;y \leq -8.5 \cdot 10^{-178}:\\
          \;\;\;\;\frac{x\_m \cdot y}{z}\\
          
          \mathbf{elif}\;y \leq 4.7 \cdot 10^{-246}:\\
          \;\;\;\;x\_m \cdot \left(-t\right)\\
          
          \mathbf{else}:\\
          \;\;\;\;y \cdot \frac{x\_m}{z}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 3 regimes
          2. if y < -8.5000000000000001e-178

            1. Initial program 94.2%

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

              \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
            4. Step-by-step derivation
              1. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
              2. lower-*.f6474.4

                \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
            5. Applied rewrites74.4%

              \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]

            if -8.5000000000000001e-178 < y < 4.69999999999999955e-246

            1. Initial program 95.8%

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

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

                \[\leadsto x \cdot \color{blue}{\left(\mathsf{neg}\left(\frac{t}{1 - z}\right)\right)} \]
              2. distribute-neg-frac2N/A

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

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

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

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

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

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

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

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

                \[\leadsto x \cdot \frac{t}{z + \color{blue}{-1}} \]
              11. lower-+.f6485.0

                \[\leadsto x \cdot \frac{t}{\color{blue}{z + -1}} \]
            5. Applied rewrites85.0%

              \[\leadsto x \cdot \color{blue}{\frac{t}{z + -1}} \]
            6. Taylor expanded in z around 0

              \[\leadsto x \cdot \left(-1 \cdot \color{blue}{t}\right) \]
            7. Step-by-step derivation
              1. Applied rewrites59.5%

                \[\leadsto x \cdot \left(-t\right) \]

              if 4.69999999999999955e-246 < y

              1. Initial program 92.7%

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

                \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
              4. Step-by-step derivation
                1. lower-/.f64N/A

                  \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
                2. lower-*.f6472.8

                  \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
              5. Applied rewrites72.8%

                \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
              6. Step-by-step derivation
                1. Applied rewrites73.9%

                  \[\leadsto y \cdot \color{blue}{\frac{x}{z}} \]
              7. Recombined 3 regimes into one program.
              8. Add Preprocessing

              Alternative 11: 62.4% accurate, 1.2× speedup?

              \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := y \cdot \frac{x\_m}{z}\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;y \leq -8.8 \cdot 10^{-178}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;y \leq 4.7 \cdot 10^{-246}:\\ \;\;\;\;x\_m \cdot \left(-t\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \end{array} \]
              x\_m = (fabs.f64 x)
              x\_s = (copysign.f64 #s(literal 1 binary64) x)
              (FPCore (x_s x_m y z t)
               :precision binary64
               (let* ((t_1 (* y (/ x_m z))))
                 (* x_s (if (<= y -8.8e-178) t_1 (if (<= y 4.7e-246) (* x_m (- t)) t_1)))))
              x\_m = fabs(x);
              x\_s = copysign(1.0, x);
              double code(double x_s, double x_m, double y, double z, double t) {
              	double t_1 = y * (x_m / z);
              	double tmp;
              	if (y <= -8.8e-178) {
              		tmp = t_1;
              	} else if (y <= 4.7e-246) {
              		tmp = x_m * -t;
              	} else {
              		tmp = t_1;
              	}
              	return x_s * tmp;
              }
              
              x\_m = abs(x)
              x\_s = copysign(1.0d0, x)
              real(8) function code(x_s, x_m, y, z, t)
                  real(8), intent (in) :: x_s
                  real(8), intent (in) :: x_m
                  real(8), intent (in) :: y
                  real(8), intent (in) :: z
                  real(8), intent (in) :: t
                  real(8) :: t_1
                  real(8) :: tmp
                  t_1 = y * (x_m / z)
                  if (y <= (-8.8d-178)) then
                      tmp = t_1
                  else if (y <= 4.7d-246) then
                      tmp = x_m * -t
                  else
                      tmp = t_1
                  end if
                  code = x_s * tmp
              end function
              
              x\_m = Math.abs(x);
              x\_s = Math.copySign(1.0, x);
              public static double code(double x_s, double x_m, double y, double z, double t) {
              	double t_1 = y * (x_m / z);
              	double tmp;
              	if (y <= -8.8e-178) {
              		tmp = t_1;
              	} else if (y <= 4.7e-246) {
              		tmp = x_m * -t;
              	} else {
              		tmp = t_1;
              	}
              	return x_s * tmp;
              }
              
              x\_m = math.fabs(x)
              x\_s = math.copysign(1.0, x)
              def code(x_s, x_m, y, z, t):
              	t_1 = y * (x_m / z)
              	tmp = 0
              	if y <= -8.8e-178:
              		tmp = t_1
              	elif y <= 4.7e-246:
              		tmp = x_m * -t
              	else:
              		tmp = t_1
              	return x_s * tmp
              
              x\_m = abs(x)
              x\_s = copysign(1.0, x)
              function code(x_s, x_m, y, z, t)
              	t_1 = Float64(y * Float64(x_m / z))
              	tmp = 0.0
              	if (y <= -8.8e-178)
              		tmp = t_1;
              	elseif (y <= 4.7e-246)
              		tmp = Float64(x_m * Float64(-t));
              	else
              		tmp = t_1;
              	end
              	return Float64(x_s * tmp)
              end
              
              x\_m = abs(x);
              x\_s = sign(x) * abs(1.0);
              function tmp_2 = code(x_s, x_m, y, z, t)
              	t_1 = y * (x_m / z);
              	tmp = 0.0;
              	if (y <= -8.8e-178)
              		tmp = t_1;
              	elseif (y <= 4.7e-246)
              		tmp = x_m * -t;
              	else
              		tmp = t_1;
              	end
              	tmp_2 = x_s * tmp;
              end
              
              x\_m = N[Abs[x], $MachinePrecision]
              x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
              code[x$95$s_, x$95$m_, y_, z_, t_] := Block[{t$95$1 = N[(y * N[(x$95$m / z), $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[y, -8.8e-178], t$95$1, If[LessEqual[y, 4.7e-246], N[(x$95$m * (-t)), $MachinePrecision], t$95$1]]), $MachinePrecision]]
              
              \begin{array}{l}
              x\_m = \left|x\right|
              \\
              x\_s = \mathsf{copysign}\left(1, x\right)
              
              \\
              \begin{array}{l}
              t_1 := y \cdot \frac{x\_m}{z}\\
              x\_s \cdot \begin{array}{l}
              \mathbf{if}\;y \leq -8.8 \cdot 10^{-178}:\\
              \;\;\;\;t\_1\\
              
              \mathbf{elif}\;y \leq 4.7 \cdot 10^{-246}:\\
              \;\;\;\;x\_m \cdot \left(-t\right)\\
              
              \mathbf{else}:\\
              \;\;\;\;t\_1\\
              
              
              \end{array}
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 2 regimes
              2. if y < -8.8000000000000005e-178 or 4.69999999999999955e-246 < y

                1. Initial program 93.4%

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

                  \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
                4. Step-by-step derivation
                  1. lower-/.f64N/A

                    \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
                  2. lower-*.f6473.5

                    \[\leadsto \frac{\color{blue}{x \cdot y}}{z} \]
                5. Applied rewrites73.5%

                  \[\leadsto \color{blue}{\frac{x \cdot y}{z}} \]
                6. Step-by-step derivation
                  1. Applied rewrites73.2%

                    \[\leadsto y \cdot \color{blue}{\frac{x}{z}} \]

                  if -8.8000000000000005e-178 < y < 4.69999999999999955e-246

                  1. Initial program 95.8%

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

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

                      \[\leadsto x \cdot \color{blue}{\left(\mathsf{neg}\left(\frac{t}{1 - z}\right)\right)} \]
                    2. distribute-neg-frac2N/A

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

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

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

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

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

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

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

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

                      \[\leadsto x \cdot \frac{t}{z + \color{blue}{-1}} \]
                    11. lower-+.f6485.0

                      \[\leadsto x \cdot \frac{t}{\color{blue}{z + -1}} \]
                  5. Applied rewrites85.0%

                    \[\leadsto x \cdot \color{blue}{\frac{t}{z + -1}} \]
                  6. Taylor expanded in z around 0

                    \[\leadsto x \cdot \left(-1 \cdot \color{blue}{t}\right) \]
                  7. Step-by-step derivation
                    1. Applied rewrites59.5%

                      \[\leadsto x \cdot \left(-t\right) \]
                  8. Recombined 2 regimes into one program.
                  9. Add Preprocessing

                  Alternative 12: 23.7% accurate, 4.3× speedup?

                  \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \left(x\_m \cdot \left(-t\right)\right) \end{array} \]
                  x\_m = (fabs.f64 x)
                  x\_s = (copysign.f64 #s(literal 1 binary64) x)
                  (FPCore (x_s x_m y z t) :precision binary64 (* x_s (* x_m (- t))))
                  x\_m = fabs(x);
                  x\_s = copysign(1.0, x);
                  double code(double x_s, double x_m, double y, double z, double t) {
                  	return x_s * (x_m * -t);
                  }
                  
                  x\_m = abs(x)
                  x\_s = copysign(1.0d0, x)
                  real(8) function code(x_s, x_m, y, z, t)
                      real(8), intent (in) :: x_s
                      real(8), intent (in) :: x_m
                      real(8), intent (in) :: y
                      real(8), intent (in) :: z
                      real(8), intent (in) :: t
                      code = x_s * (x_m * -t)
                  end function
                  
                  x\_m = Math.abs(x);
                  x\_s = Math.copySign(1.0, x);
                  public static double code(double x_s, double x_m, double y, double z, double t) {
                  	return x_s * (x_m * -t);
                  }
                  
                  x\_m = math.fabs(x)
                  x\_s = math.copysign(1.0, x)
                  def code(x_s, x_m, y, z, t):
                  	return x_s * (x_m * -t)
                  
                  x\_m = abs(x)
                  x\_s = copysign(1.0, x)
                  function code(x_s, x_m, y, z, t)
                  	return Float64(x_s * Float64(x_m * Float64(-t)))
                  end
                  
                  x\_m = abs(x);
                  x\_s = sign(x) * abs(1.0);
                  function tmp = code(x_s, x_m, y, z, t)
                  	tmp = x_s * (x_m * -t);
                  end
                  
                  x\_m = N[Abs[x], $MachinePrecision]
                  x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                  code[x$95$s_, x$95$m_, y_, z_, t_] := N[(x$95$s * N[(x$95$m * (-t)), $MachinePrecision]), $MachinePrecision]
                  
                  \begin{array}{l}
                  x\_m = \left|x\right|
                  \\
                  x\_s = \mathsf{copysign}\left(1, x\right)
                  
                  \\
                  x\_s \cdot \left(x\_m \cdot \left(-t\right)\right)
                  \end{array}
                  
                  Derivation
                  1. Initial program 93.9%

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

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

                      \[\leadsto x \cdot \color{blue}{\left(\mathsf{neg}\left(\frac{t}{1 - z}\right)\right)} \]
                    2. distribute-neg-frac2N/A

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

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

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

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

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

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

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

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

                      \[\leadsto x \cdot \frac{t}{z + \color{blue}{-1}} \]
                    11. lower-+.f6443.6

                      \[\leadsto x \cdot \frac{t}{\color{blue}{z + -1}} \]
                  5. Applied rewrites43.6%

                    \[\leadsto x \cdot \color{blue}{\frac{t}{z + -1}} \]
                  6. Taylor expanded in z around 0

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

                      \[\leadsto x \cdot \left(-t\right) \]
                    2. Add Preprocessing

                    Developer Target 1: 94.7% accurate, 0.3× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\ t_2 := x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right)\\ \mathbf{if}\;t\_2 < -7.623226303312042 \cdot 10^{-196}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t\_2 < 1.4133944927702302 \cdot 10^{-211}:\\ \;\;\;\;\frac{y \cdot x}{z} + \left(-\frac{t \cdot x}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
                    (FPCore (x y z t)
                     :precision binary64
                     (let* ((t_1 (* x (- (/ y z) (* t (/ 1.0 (- 1.0 z))))))
                            (t_2 (* x (- (/ y z) (/ t (- 1.0 z))))))
                       (if (< t_2 -7.623226303312042e-196)
                         t_1
                         (if (< t_2 1.4133944927702302e-211)
                           (+ (/ (* y x) z) (- (/ (* t x) (- 1.0 z))))
                           t_1))))
                    double code(double x, double y, double z, double t) {
                    	double t_1 = x * ((y / z) - (t * (1.0 / (1.0 - z))));
                    	double t_2 = x * ((y / z) - (t / (1.0 - z)));
                    	double tmp;
                    	if (t_2 < -7.623226303312042e-196) {
                    		tmp = t_1;
                    	} else if (t_2 < 1.4133944927702302e-211) {
                    		tmp = ((y * x) / z) + -((t * x) / (1.0 - z));
                    	} else {
                    		tmp = t_1;
                    	}
                    	return tmp;
                    }
                    
                    real(8) function code(x, y, z, t)
                        real(8), intent (in) :: x
                        real(8), intent (in) :: y
                        real(8), intent (in) :: z
                        real(8), intent (in) :: t
                        real(8) :: t_1
                        real(8) :: t_2
                        real(8) :: tmp
                        t_1 = x * ((y / z) - (t * (1.0d0 / (1.0d0 - z))))
                        t_2 = x * ((y / z) - (t / (1.0d0 - z)))
                        if (t_2 < (-7.623226303312042d-196)) then
                            tmp = t_1
                        else if (t_2 < 1.4133944927702302d-211) then
                            tmp = ((y * x) / z) + -((t * x) / (1.0d0 - z))
                        else
                            tmp = t_1
                        end if
                        code = tmp
                    end function
                    
                    public static double code(double x, double y, double z, double t) {
                    	double t_1 = x * ((y / z) - (t * (1.0 / (1.0 - z))));
                    	double t_2 = x * ((y / z) - (t / (1.0 - z)));
                    	double tmp;
                    	if (t_2 < -7.623226303312042e-196) {
                    		tmp = t_1;
                    	} else if (t_2 < 1.4133944927702302e-211) {
                    		tmp = ((y * x) / z) + -((t * x) / (1.0 - z));
                    	} else {
                    		tmp = t_1;
                    	}
                    	return tmp;
                    }
                    
                    def code(x, y, z, t):
                    	t_1 = x * ((y / z) - (t * (1.0 / (1.0 - z))))
                    	t_2 = x * ((y / z) - (t / (1.0 - z)))
                    	tmp = 0
                    	if t_2 < -7.623226303312042e-196:
                    		tmp = t_1
                    	elif t_2 < 1.4133944927702302e-211:
                    		tmp = ((y * x) / z) + -((t * x) / (1.0 - z))
                    	else:
                    		tmp = t_1
                    	return tmp
                    
                    function code(x, y, z, t)
                    	t_1 = Float64(x * Float64(Float64(y / z) - Float64(t * Float64(1.0 / Float64(1.0 - z)))))
                    	t_2 = Float64(x * Float64(Float64(y / z) - Float64(t / Float64(1.0 - z))))
                    	tmp = 0.0
                    	if (t_2 < -7.623226303312042e-196)
                    		tmp = t_1;
                    	elseif (t_2 < 1.4133944927702302e-211)
                    		tmp = Float64(Float64(Float64(y * x) / z) + Float64(-Float64(Float64(t * x) / Float64(1.0 - z))));
                    	else
                    		tmp = t_1;
                    	end
                    	return tmp
                    end
                    
                    function tmp_2 = code(x, y, z, t)
                    	t_1 = x * ((y / z) - (t * (1.0 / (1.0 - z))));
                    	t_2 = x * ((y / z) - (t / (1.0 - z)));
                    	tmp = 0.0;
                    	if (t_2 < -7.623226303312042e-196)
                    		tmp = t_1;
                    	elseif (t_2 < 1.4133944927702302e-211)
                    		tmp = ((y * x) / z) + -((t * x) / (1.0 - z));
                    	else
                    		tmp = t_1;
                    	end
                    	tmp_2 = tmp;
                    end
                    
                    code[x_, y_, z_, t_] := Block[{t$95$1 = N[(x * N[(N[(y / z), $MachinePrecision] - N[(t * N[(1.0 / N[(1.0 - z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(x * N[(N[(y / z), $MachinePrecision] - N[(t / N[(1.0 - z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[Less[t$95$2, -7.623226303312042e-196], t$95$1, If[Less[t$95$2, 1.4133944927702302e-211], N[(N[(N[(y * x), $MachinePrecision] / z), $MachinePrecision] + (-N[(N[(t * x), $MachinePrecision] / N[(1.0 - z), $MachinePrecision]), $MachinePrecision])), $MachinePrecision], t$95$1]]]]
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    t_1 := x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\
                    t_2 := x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right)\\
                    \mathbf{if}\;t\_2 < -7.623226303312042 \cdot 10^{-196}:\\
                    \;\;\;\;t\_1\\
                    
                    \mathbf{elif}\;t\_2 < 1.4133944927702302 \cdot 10^{-211}:\\
                    \;\;\;\;\frac{y \cdot x}{z} + \left(-\frac{t \cdot x}{1 - z}\right)\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;t\_1\\
                    
                    
                    \end{array}
                    \end{array}
                    

                    Reproduce

                    ?
                    herbie shell --seed 2024221 
                    (FPCore (x y z t)
                      :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, C"
                      :precision binary64
                    
                      :alt
                      (! :herbie-platform default (if (< (* x (- (/ y z) (/ t (- 1 z)))) -3811613151656021/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* x (- (/ y z) (* t (/ 1 (- 1 z))))) (if (< (* x (- (/ y z) (/ t (- 1 z)))) 7066972463851151/50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (+ (/ (* y x) z) (- (/ (* t x) (- 1 z)))) (* x (- (/ y z) (* t (/ 1 (- 1 z))))))))
                    
                      (* x (- (/ y z) (/ t (- 1.0 z)))))