Graphics.Rendering.Plot.Render.Plot.Axis:renderAxisTick from plot-0.2.3.4, B

Percentage Accurate: 76.9% → 90.3%
Time: 8.7s
Alternatives: 10
Speedup: 0.9×

Specification

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

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

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 10 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: 76.9% accurate, 1.0× speedup?

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

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

Alternative 1: 90.3% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;t \leq -1.05 \cdot 10^{+78}:\\ \;\;\;\;\mathsf{fma}\left(\frac{z - a}{t}, y, x\right)\\ \mathbf{elif}\;t \leq 1.55 \cdot 10^{+60}:\\ \;\;\;\;\left(y + x\right) - \frac{-1}{\frac{\frac{t - a}{y}}{z - t}}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{y}{t}, z - a, x\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a)
 :precision binary64
 (if (<= t -1.05e+78)
   (fma (/ (- z a) t) y x)
   (if (<= t 1.55e+60)
     (- (+ y x) (/ -1.0 (/ (/ (- t a) y) (- z t))))
     (fma (/ y t) (- z a) x))))
double code(double x, double y, double z, double t, double a) {
	double tmp;
	if (t <= -1.05e+78) {
		tmp = fma(((z - a) / t), y, x);
	} else if (t <= 1.55e+60) {
		tmp = (y + x) - (-1.0 / (((t - a) / y) / (z - t)));
	} else {
		tmp = fma((y / t), (z - a), x);
	}
	return tmp;
}
function code(x, y, z, t, a)
	tmp = 0.0
	if (t <= -1.05e+78)
		tmp = fma(Float64(Float64(z - a) / t), y, x);
	elseif (t <= 1.55e+60)
		tmp = Float64(Float64(y + x) - Float64(-1.0 / Float64(Float64(Float64(t - a) / y) / Float64(z - t))));
	else
		tmp = fma(Float64(y / t), Float64(z - a), x);
	end
	return tmp
end
code[x_, y_, z_, t_, a_] := If[LessEqual[t, -1.05e+78], N[(N[(N[(z - a), $MachinePrecision] / t), $MachinePrecision] * y + x), $MachinePrecision], If[LessEqual[t, 1.55e+60], N[(N[(y + x), $MachinePrecision] - N[(-1.0 / N[(N[(N[(t - a), $MachinePrecision] / y), $MachinePrecision] / N[(z - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(y / t), $MachinePrecision] * N[(z - a), $MachinePrecision] + x), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;t \leq -1.05 \cdot 10^{+78}:\\
\;\;\;\;\mathsf{fma}\left(\frac{z - a}{t}, y, x\right)\\

\mathbf{elif}\;t \leq 1.55 \cdot 10^{+60}:\\
\;\;\;\;\left(y + x\right) - \frac{-1}{\frac{\frac{t - a}{y}}{z - t}}\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{y}{t}, z - a, x\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if t < -1.05e78

    1. Initial program 59.9%

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

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

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

        \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
      3. *-lft-identityN/A

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

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

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

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

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

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

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

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

        \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
      12. distribute-rgt-out--N/A

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

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
      15. lower--.f6490.8

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{y \cdot z - a \cdot y}{t}} + x \]
      10. *-commutativeN/A

        \[\leadsto \frac{y \cdot z - \color{blue}{y \cdot a}}{t} + x \]
      11. distribute-lft-out--N/A

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

        \[\leadsto \color{blue}{y \cdot \frac{z - a}{t}} + x \]
      13. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{z - a}{t} \cdot y} + x \]
      14. lower-fma.f64N/A

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{z - a}{t}}, y, x\right) \]
      16. lower--.f6493.5

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

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

    if -1.05e78 < t < 1.55e60

    1. Initial program 91.8%

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

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

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

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

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

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

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

        \[\leadsto \left(x + y\right) - \frac{1}{\color{blue}{\frac{\frac{a - t}{y}}{z - t}}} \]
      8. lower-/.f6494.8

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

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

    if 1.55e60 < t

    1. Initial program 57.8%

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

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

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

        \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
      3. *-lft-identityN/A

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

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

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

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

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

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

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

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

        \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
      12. distribute-rgt-out--N/A

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

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
      15. lower--.f6490.8

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

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y}{t}, z - a, x\right)} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification93.7%

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

Alternative 2: 63.8% accurate, 0.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{z \cdot y}{t}\\ t_2 := \left(y + x\right) - \frac{\left(z - t\right) \cdot y}{a - t}\\ \mathbf{if}\;t\_2 \leq -\infty:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t\_2 \leq -2 \cdot 10^{-21}:\\ \;\;\;\;y + x\\ \mathbf{elif}\;t\_2 \leq 4 \cdot 10^{-219}:\\ \;\;\;\;x\\ \mathbf{elif}\;t\_2 \leq 10^{+301}:\\ \;\;\;\;y + x\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
(FPCore (x y z t a)
 :precision binary64
 (let* ((t_1 (/ (* z y) t)) (t_2 (- (+ y x) (/ (* (- z t) y) (- a t)))))
   (if (<= t_2 (- INFINITY))
     t_1
     (if (<= t_2 -2e-21)
       (+ y x)
       (if (<= t_2 4e-219) x (if (<= t_2 1e+301) (+ y x) t_1))))))
double code(double x, double y, double z, double t, double a) {
	double t_1 = (z * y) / t;
	double t_2 = (y + x) - (((z - t) * y) / (a - t));
	double tmp;
	if (t_2 <= -((double) INFINITY)) {
		tmp = t_1;
	} else if (t_2 <= -2e-21) {
		tmp = y + x;
	} else if (t_2 <= 4e-219) {
		tmp = x;
	} else if (t_2 <= 1e+301) {
		tmp = y + x;
	} else {
		tmp = t_1;
	}
	return tmp;
}
public static double code(double x, double y, double z, double t, double a) {
	double t_1 = (z * y) / t;
	double t_2 = (y + x) - (((z - t) * y) / (a - t));
	double tmp;
	if (t_2 <= -Double.POSITIVE_INFINITY) {
		tmp = t_1;
	} else if (t_2 <= -2e-21) {
		tmp = y + x;
	} else if (t_2 <= 4e-219) {
		tmp = x;
	} else if (t_2 <= 1e+301) {
		tmp = y + x;
	} else {
		tmp = t_1;
	}
	return tmp;
}
def code(x, y, z, t, a):
	t_1 = (z * y) / t
	t_2 = (y + x) - (((z - t) * y) / (a - t))
	tmp = 0
	if t_2 <= -math.inf:
		tmp = t_1
	elif t_2 <= -2e-21:
		tmp = y + x
	elif t_2 <= 4e-219:
		tmp = x
	elif t_2 <= 1e+301:
		tmp = y + x
	else:
		tmp = t_1
	return tmp
function code(x, y, z, t, a)
	t_1 = Float64(Float64(z * y) / t)
	t_2 = Float64(Float64(y + x) - Float64(Float64(Float64(z - t) * y) / Float64(a - t)))
	tmp = 0.0
	if (t_2 <= Float64(-Inf))
		tmp = t_1;
	elseif (t_2 <= -2e-21)
		tmp = Float64(y + x);
	elseif (t_2 <= 4e-219)
		tmp = x;
	elseif (t_2 <= 1e+301)
		tmp = Float64(y + x);
	else
		tmp = t_1;
	end
	return tmp
end
function tmp_2 = code(x, y, z, t, a)
	t_1 = (z * y) / t;
	t_2 = (y + x) - (((z - t) * y) / (a - t));
	tmp = 0.0;
	if (t_2 <= -Inf)
		tmp = t_1;
	elseif (t_2 <= -2e-21)
		tmp = y + x;
	elseif (t_2 <= 4e-219)
		tmp = x;
	elseif (t_2 <= 1e+301)
		tmp = y + x;
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end
code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z * y), $MachinePrecision] / t), $MachinePrecision]}, Block[{t$95$2 = N[(N[(y + x), $MachinePrecision] - N[(N[(N[(z - t), $MachinePrecision] * y), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$2, (-Infinity)], t$95$1, If[LessEqual[t$95$2, -2e-21], N[(y + x), $MachinePrecision], If[LessEqual[t$95$2, 4e-219], x, If[LessEqual[t$95$2, 1e+301], N[(y + x), $MachinePrecision], t$95$1]]]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \frac{z \cdot y}{t}\\
t_2 := \left(y + x\right) - \frac{\left(z - t\right) \cdot y}{a - t}\\
\mathbf{if}\;t\_2 \leq -\infty:\\
\;\;\;\;t\_1\\

\mathbf{elif}\;t\_2 \leq -2 \cdot 10^{-21}:\\
\;\;\;\;y + x\\

\mathbf{elif}\;t\_2 \leq 4 \cdot 10^{-219}:\\
\;\;\;\;x\\

\mathbf{elif}\;t\_2 \leq 10^{+301}:\\
\;\;\;\;y + x\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))) < -inf.0 or 1.00000000000000005e301 < (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))

    1. Initial program 41.5%

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

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

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

        \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
      3. *-lft-identityN/A

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

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

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

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

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

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

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

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

        \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
      12. distribute-rgt-out--N/A

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

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
      15. lower--.f6477.5

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

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

      \[\leadsto \frac{y \cdot z}{\color{blue}{t}} \]
    7. Step-by-step derivation
      1. Applied rewrites44.2%

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

      if -inf.0 < (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))) < -1.99999999999999982e-21 or 4.0000000000000001e-219 < (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))) < 1.00000000000000005e301

      1. Initial program 97.4%

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

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

          \[\leadsto \color{blue}{y + x} \]
        2. lower-+.f6473.4

          \[\leadsto \color{blue}{y + x} \]
      5. Applied rewrites73.4%

        \[\leadsto \color{blue}{y + x} \]

      if -1.99999999999999982e-21 < (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))) < 4.0000000000000001e-219

      1. Initial program 53.4%

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

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

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

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

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

          \[\leadsto \left(\mathsf{neg}\left(\frac{\color{blue}{\left(z - t\right) \cdot y}}{a - t}\right)\right) + \left(x + y\right) \]
        6. associate-/l*N/A

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

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

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

          \[\leadsto \mathsf{fma}\left(z - t, \color{blue}{-\frac{y}{a - t}}, x + y\right) \]
        10. lower-/.f6451.8

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

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

          \[\leadsto \mathsf{fma}\left(z - t, -\frac{y}{a - t}, \color{blue}{y + x}\right) \]
        13. lower-+.f6451.8

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

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

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

          \[\leadsto \color{blue}{\left(y + -1 \cdot y\right) + x} \]
        2. distribute-rgt1-inN/A

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

          \[\leadsto \color{blue}{0} \cdot y + x \]
        4. mul0-lftN/A

          \[\leadsto \color{blue}{0} + x \]
        5. lower-+.f6464.6

          \[\leadsto \color{blue}{0 + x} \]
      7. Applied rewrites64.6%

        \[\leadsto \color{blue}{0 + x} \]
      8. Step-by-step derivation
        1. Applied rewrites64.6%

          \[\leadsto x \]
      9. Recombined 3 regimes into one program.
      10. Final simplification65.9%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\left(y + x\right) - \frac{\left(z - t\right) \cdot y}{a - t} \leq -\infty:\\ \;\;\;\;\frac{z \cdot y}{t}\\ \mathbf{elif}\;\left(y + x\right) - \frac{\left(z - t\right) \cdot y}{a - t} \leq -2 \cdot 10^{-21}:\\ \;\;\;\;y + x\\ \mathbf{elif}\;\left(y + x\right) - \frac{\left(z - t\right) \cdot y}{a - t} \leq 4 \cdot 10^{-219}:\\ \;\;\;\;x\\ \mathbf{elif}\;\left(y + x\right) - \frac{\left(z - t\right) \cdot y}{a - t} \leq 10^{+301}:\\ \;\;\;\;y + x\\ \mathbf{else}:\\ \;\;\;\;\frac{z \cdot y}{t}\\ \end{array} \]
      11. Add Preprocessing

      Alternative 3: 90.1% accurate, 0.7× speedup?

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

        1. Initial program 62.1%

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

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

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

            \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
          3. *-lft-identityN/A

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

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

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
          12. distribute-rgt-out--N/A

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
          15. lower--.f6491.3

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{y \cdot z - a \cdot y}{t}} + x \]
          10. *-commutativeN/A

            \[\leadsto \frac{y \cdot z - \color{blue}{y \cdot a}}{t} + x \]
          11. distribute-lft-out--N/A

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

            \[\leadsto \color{blue}{y \cdot \frac{z - a}{t}} + x \]
          13. *-commutativeN/A

            \[\leadsto \color{blue}{\frac{z - a}{t} \cdot y} + x \]
          14. lower-fma.f64N/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{z - a}{t}}, y, x\right) \]
          16. lower--.f6493.8

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

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

        if -6.00000000000000021e73 < t < 1.55e60

        1. Initial program 91.6%

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

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

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

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

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

            \[\leadsto \left(\mathsf{neg}\left(\frac{\color{blue}{\left(z - t\right) \cdot y}}{a - t}\right)\right) + \left(x + y\right) \]
          6. associate-/l*N/A

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(z - t, -\frac{y}{a - t}, \color{blue}{y + x}\right) \]
          13. lower-+.f6494.1

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

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

        if 1.55e60 < t

        1. Initial program 57.8%

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

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

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

            \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
          3. *-lft-identityN/A

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

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

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
          12. distribute-rgt-out--N/A

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
          15. lower--.f6490.8

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y}{t}, z - a, x\right)} \]
      3. Recombined 3 regimes into one program.
      4. Final simplification93.3%

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

      Alternative 4: 89.3% accurate, 0.8× speedup?

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

        1. Initial program 59.9%

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

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

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

            \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
          3. *-lft-identityN/A

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

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

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
          12. distribute-rgt-out--N/A

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
          15. lower--.f6490.8

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{y \cdot z - a \cdot y}{t}} + x \]
          10. *-commutativeN/A

            \[\leadsto \frac{y \cdot z - \color{blue}{y \cdot a}}{t} + x \]
          11. distribute-lft-out--N/A

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

            \[\leadsto \color{blue}{y \cdot \frac{z - a}{t}} + x \]
          13. *-commutativeN/A

            \[\leadsto \color{blue}{\frac{z - a}{t} \cdot y} + x \]
          14. lower-fma.f64N/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{z - a}{t}}, y, x\right) \]
          16. lower--.f6493.5

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

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

        if -1.05e78 < t < 2.2000000000000001e58

        1. Initial program 91.8%

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

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

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

            \[\leadsto \left(x + y\right) - \frac{\color{blue}{z \cdot y}}{a} \]
          3. lower-*.f6476.2

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

          \[\leadsto \left(x + y\right) - \color{blue}{\frac{z \cdot y}{a}} \]
        6. Taylor expanded in z around inf

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

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

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

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

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

            \[\leadsto \left(x + y\right) - \frac{z}{\color{blue}{a - t}} \cdot y \]
        8. Applied rewrites92.0%

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

        if 2.2000000000000001e58 < t

        1. Initial program 57.8%

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

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

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

            \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
          3. *-lft-identityN/A

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

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

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
          12. distribute-rgt-out--N/A

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
          15. lower--.f6490.8

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y}{t}, z - a, x\right)} \]
      3. Recombined 3 regimes into one program.
      4. Final simplification92.1%

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

      Alternative 5: 81.2% accurate, 0.9× speedup?

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

        1. Initial program 62.1%

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

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

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

            \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
          3. *-lft-identityN/A

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

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

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
          12. distribute-rgt-out--N/A

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
          15. lower--.f6491.3

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{y \cdot z - a \cdot y}{t}} + x \]
          10. *-commutativeN/A

            \[\leadsto \frac{y \cdot z - \color{blue}{y \cdot a}}{t} + x \]
          11. distribute-lft-out--N/A

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

            \[\leadsto \color{blue}{y \cdot \frac{z - a}{t}} + x \]
          13. *-commutativeN/A

            \[\leadsto \color{blue}{\frac{z - a}{t} \cdot y} + x \]
          14. lower-fma.f64N/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{z - a}{t}}, y, x\right) \]
          16. lower--.f6493.8

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

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

        if -4.2000000000000003e73 < t < 4.60000000000000012e-76

        1. Initial program 92.4%

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

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(y, \color{blue}{1 - \frac{z}{a}}, x\right) \]
          8. lower-/.f6482.0

            \[\leadsto \mathsf{fma}\left(y, 1 - \color{blue}{\frac{z}{a}}, x\right) \]
        5. Applied rewrites82.0%

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

        if 4.60000000000000012e-76 < t

        1. Initial program 66.2%

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

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

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

            \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
          3. *-lft-identityN/A

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

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

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
          12. distribute-rgt-out--N/A

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
          15. lower--.f6485.0

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

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

      Alternative 6: 81.2% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{fma}\left(\frac{y}{t}, z - a, x\right)\\ \mathbf{if}\;t \leq -4.2 \cdot 10^{+73}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t \leq 4.6 \cdot 10^{-76}:\\ \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{a}, x\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
      (FPCore (x y z t a)
       :precision binary64
       (let* ((t_1 (fma (/ y t) (- z a) x)))
         (if (<= t -4.2e+73) t_1 (if (<= t 4.6e-76) (fma y (- 1.0 (/ z a)) x) t_1))))
      double code(double x, double y, double z, double t, double a) {
      	double t_1 = fma((y / t), (z - a), x);
      	double tmp;
      	if (t <= -4.2e+73) {
      		tmp = t_1;
      	} else if (t <= 4.6e-76) {
      		tmp = fma(y, (1.0 - (z / a)), x);
      	} else {
      		tmp = t_1;
      	}
      	return tmp;
      }
      
      function code(x, y, z, t, a)
      	t_1 = fma(Float64(y / t), Float64(z - a), x)
      	tmp = 0.0
      	if (t <= -4.2e+73)
      		tmp = t_1;
      	elseif (t <= 4.6e-76)
      		tmp = fma(y, Float64(1.0 - Float64(z / a)), x);
      	else
      		tmp = t_1;
      	end
      	return tmp
      end
      
      code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(y / t), $MachinePrecision] * N[(z - a), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t, -4.2e+73], t$95$1, If[LessEqual[t, 4.6e-76], N[(y * N[(1.0 - N[(z / a), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], t$95$1]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_1 := \mathsf{fma}\left(\frac{y}{t}, z - a, x\right)\\
      \mathbf{if}\;t \leq -4.2 \cdot 10^{+73}:\\
      \;\;\;\;t\_1\\
      
      \mathbf{elif}\;t \leq 4.6 \cdot 10^{-76}:\\
      \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{a}, x\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_1\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if t < -4.2000000000000003e73 or 4.60000000000000012e-76 < t

        1. Initial program 64.5%

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

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

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

            \[\leadsto \left(x + -1 \cdot \frac{a \cdot y}{t}\right) + \color{blue}{1} \cdot \frac{y \cdot z}{t} \]
          3. *-lft-identityN/A

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

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

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

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

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

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

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

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

            \[\leadsto \left(\color{blue}{z \cdot \frac{y}{t}} - a \cdot \frac{y}{t}\right) + x \]
          12. distribute-rgt-out--N/A

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t}}, z - a, x\right) \]
          15. lower--.f6487.6

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

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

        if -4.2000000000000003e73 < t < 4.60000000000000012e-76

        1. Initial program 92.4%

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

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(y, \color{blue}{1 - \frac{z}{a}}, x\right) \]
          8. lower-/.f6482.0

            \[\leadsto \mathsf{fma}\left(y, 1 - \color{blue}{\frac{z}{a}}, x\right) \]
        5. Applied rewrites82.0%

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

      Alternative 7: 82.1% accurate, 0.9× speedup?

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

        1. Initial program 82.4%

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

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(y, \color{blue}{1 - \frac{z}{a}}, x\right) \]
          8. lower-/.f6485.3

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

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

        if -4.50000000000000025e-43 < a < 1.99999999999999989e-29

        1. Initial program 73.2%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \mathsf{fma}\left(\frac{z}{t}, y, x\right) \]
        7. Step-by-step derivation
          1. Applied rewrites79.6%

            \[\leadsto \mathsf{fma}\left(\frac{z}{t}, y, x\right) \]
        8. Recombined 2 regimes into one program.
        9. Add Preprocessing

        Alternative 8: 76.7% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;a \leq -1.2 \cdot 10^{-39}:\\ \;\;\;\;y + x\\ \mathbf{elif}\;a \leq 3.1 \cdot 10^{+26}:\\ \;\;\;\;\mathsf{fma}\left(\frac{z}{t}, y, x\right)\\ \mathbf{else}:\\ \;\;\;\;y + x\\ \end{array} \end{array} \]
        (FPCore (x y z t a)
         :precision binary64
         (if (<= a -1.2e-39) (+ y x) (if (<= a 3.1e+26) (fma (/ z t) y x) (+ y x))))
        double code(double x, double y, double z, double t, double a) {
        	double tmp;
        	if (a <= -1.2e-39) {
        		tmp = y + x;
        	} else if (a <= 3.1e+26) {
        		tmp = fma((z / t), y, x);
        	} else {
        		tmp = y + x;
        	}
        	return tmp;
        }
        
        function code(x, y, z, t, a)
        	tmp = 0.0
        	if (a <= -1.2e-39)
        		tmp = Float64(y + x);
        	elseif (a <= 3.1e+26)
        		tmp = fma(Float64(z / t), y, x);
        	else
        		tmp = Float64(y + x);
        	end
        	return tmp
        end
        
        code[x_, y_, z_, t_, a_] := If[LessEqual[a, -1.2e-39], N[(y + x), $MachinePrecision], If[LessEqual[a, 3.1e+26], N[(N[(z / t), $MachinePrecision] * y + x), $MachinePrecision], N[(y + x), $MachinePrecision]]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;a \leq -1.2 \cdot 10^{-39}:\\
        \;\;\;\;y + x\\
        
        \mathbf{elif}\;a \leq 3.1 \cdot 10^{+26}:\\
        \;\;\;\;\mathsf{fma}\left(\frac{z}{t}, y, x\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;y + x\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if a < -1.20000000000000008e-39 or 3.1e26 < a

          1. Initial program 81.7%

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

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

              \[\leadsto \color{blue}{y + x} \]
            2. lower-+.f6474.2

              \[\leadsto \color{blue}{y + x} \]
          5. Applied rewrites74.2%

            \[\leadsto \color{blue}{y + x} \]

          if -1.20000000000000008e-39 < a < 3.1e26

          1. Initial program 74.7%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

              \[\leadsto \mathsf{fma}\left(\frac{z}{t}, y, x\right) \]
          8. Recombined 2 regimes into one program.
          9. Add Preprocessing

          Alternative 9: 62.7% accurate, 1.8× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;t \leq -1.12 \cdot 10^{+82}:\\ \;\;\;\;x\\ \mathbf{elif}\;t \leq 1.18 \cdot 10^{+57}:\\ \;\;\;\;y + x\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \end{array} \]
          (FPCore (x y z t a)
           :precision binary64
           (if (<= t -1.12e+82) x (if (<= t 1.18e+57) (+ y x) x)))
          double code(double x, double y, double z, double t, double a) {
          	double tmp;
          	if (t <= -1.12e+82) {
          		tmp = x;
          	} else if (t <= 1.18e+57) {
          		tmp = y + x;
          	} else {
          		tmp = x;
          	}
          	return tmp;
          }
          
          real(8) function code(x, y, z, t, a)
              real(8), intent (in) :: x
              real(8), intent (in) :: y
              real(8), intent (in) :: z
              real(8), intent (in) :: t
              real(8), intent (in) :: a
              real(8) :: tmp
              if (t <= (-1.12d+82)) then
                  tmp = x
              else if (t <= 1.18d+57) then
                  tmp = y + x
              else
                  tmp = x
              end if
              code = tmp
          end function
          
          public static double code(double x, double y, double z, double t, double a) {
          	double tmp;
          	if (t <= -1.12e+82) {
          		tmp = x;
          	} else if (t <= 1.18e+57) {
          		tmp = y + x;
          	} else {
          		tmp = x;
          	}
          	return tmp;
          }
          
          def code(x, y, z, t, a):
          	tmp = 0
          	if t <= -1.12e+82:
          		tmp = x
          	elif t <= 1.18e+57:
          		tmp = y + x
          	else:
          		tmp = x
          	return tmp
          
          function code(x, y, z, t, a)
          	tmp = 0.0
          	if (t <= -1.12e+82)
          		tmp = x;
          	elseif (t <= 1.18e+57)
          		tmp = Float64(y + x);
          	else
          		tmp = x;
          	end
          	return tmp
          end
          
          function tmp_2 = code(x, y, z, t, a)
          	tmp = 0.0;
          	if (t <= -1.12e+82)
          		tmp = x;
          	elseif (t <= 1.18e+57)
          		tmp = y + x;
          	else
          		tmp = x;
          	end
          	tmp_2 = tmp;
          end
          
          code[x_, y_, z_, t_, a_] := If[LessEqual[t, -1.12e+82], x, If[LessEqual[t, 1.18e+57], N[(y + x), $MachinePrecision], x]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;t \leq -1.12 \cdot 10^{+82}:\\
          \;\;\;\;x\\
          
          \mathbf{elif}\;t \leq 1.18 \cdot 10^{+57}:\\
          \;\;\;\;y + x\\
          
          \mathbf{else}:\\
          \;\;\;\;x\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if t < -1.11999999999999998e82 or 1.18e57 < t

            1. Initial program 59.3%

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

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

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

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

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

                \[\leadsto \left(\mathsf{neg}\left(\frac{\color{blue}{\left(z - t\right) \cdot y}}{a - t}\right)\right) + \left(x + y\right) \]
              6. associate-/l*N/A

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

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

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

                \[\leadsto \mathsf{fma}\left(z - t, \color{blue}{-\frac{y}{a - t}}, x + y\right) \]
              10. lower-/.f6466.5

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

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

                \[\leadsto \mathsf{fma}\left(z - t, -\frac{y}{a - t}, \color{blue}{y + x}\right) \]
              13. lower-+.f6466.5

                \[\leadsto \mathsf{fma}\left(z - t, -\frac{y}{a - t}, \color{blue}{y + x}\right) \]
            4. Applied rewrites66.5%

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

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

                \[\leadsto \color{blue}{\left(y + -1 \cdot y\right) + x} \]
              2. distribute-rgt1-inN/A

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

                \[\leadsto \color{blue}{0} \cdot y + x \]
              4. mul0-lftN/A

                \[\leadsto \color{blue}{0} + x \]
              5. lower-+.f6465.9

                \[\leadsto \color{blue}{0 + x} \]
            7. Applied rewrites65.9%

              \[\leadsto \color{blue}{0 + x} \]
            8. Step-by-step derivation
              1. Applied rewrites65.9%

                \[\leadsto x \]

              if -1.11999999999999998e82 < t < 1.18e57

              1. Initial program 91.2%

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

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

                  \[\leadsto \color{blue}{y + x} \]
                2. lower-+.f6459.6

                  \[\leadsto \color{blue}{y + x} \]
              5. Applied rewrites59.6%

                \[\leadsto \color{blue}{y + x} \]
            9. Recombined 2 regimes into one program.
            10. Add Preprocessing

            Alternative 10: 51.0% accurate, 29.0× speedup?

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

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

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

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

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

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

                \[\leadsto \left(\mathsf{neg}\left(\frac{\color{blue}{\left(z - t\right) \cdot y}}{a - t}\right)\right) + \left(x + y\right) \]
              6. associate-/l*N/A

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

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

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

                \[\leadsto \mathsf{fma}\left(z - t, \color{blue}{-\frac{y}{a - t}}, x + y\right) \]
              10. lower-/.f6482.6

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

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

                \[\leadsto \mathsf{fma}\left(z - t, -\frac{y}{a - t}, \color{blue}{y + x}\right) \]
              13. lower-+.f6482.6

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

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

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

                \[\leadsto \color{blue}{\left(y + -1 \cdot y\right) + x} \]
              2. distribute-rgt1-inN/A

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

                \[\leadsto \color{blue}{0} \cdot y + x \]
              4. mul0-lftN/A

                \[\leadsto \color{blue}{0} + x \]
              5. lower-+.f6448.9

                \[\leadsto \color{blue}{0 + x} \]
            7. Applied rewrites48.9%

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

                \[\leadsto x \]
              2. Add Preprocessing

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

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

              Reproduce

              ?
              herbie shell --seed 2024268 
              (FPCore (x y z t a)
                :name "Graphics.Rendering.Plot.Render.Plot.Axis:renderAxisTick from plot-0.2.3.4, B"
                :precision binary64
              
                :alt
                (! :herbie-platform default (if (< (- (+ x y) (/ (* (- z t) y) (- a t))) -13664970889390727/100000000000000000000000) (- (+ y x) (* (* (- z t) (/ 1 (- a t))) y)) (if (< (- (+ x y) (/ (* (- z t) y) (- a t))) 14754293444577233/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (/ (- (* y (- a z)) (* x t)) (- a t)) (- (+ y x) (* (* (- z t) (/ 1 (- a t))) y)))))
              
                (- (+ x y) (/ (* (- z t) y) (- a t))))