Graphics.Rendering.Plot.Render.Plot.Axis:renderAxisLine from plot-0.2.3.4, A

Percentage Accurate: 97.9% → 98.4%
Time: 7.9s
Alternatives: 14
Speedup: 1.1×

Specification

?
\[\begin{array}{l} \\ x + y \cdot \frac{z - t}{z - a} \end{array} \]
(FPCore (x y z t a) :precision binary64 (+ x (* y (/ (- z t) (- z a)))))
double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (z - a)));
}
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) / (z - a)))
end function
public static double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (z - a)));
}
def code(x, y, z, t, a):
	return x + (y * ((z - t) / (z - a)))
function code(x, y, z, t, a)
	return Float64(x + Float64(y * Float64(Float64(z - t) / Float64(z - a))))
end
function tmp = code(x, y, z, t, a)
	tmp = x + (y * ((z - t) / (z - a)));
end
code[x_, y_, z_, t_, a_] := N[(x + N[(y * N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
x + y \cdot \frac{z - t}{z - a}
\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 14 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: 97.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ x + y \cdot \frac{z - t}{z - a} \end{array} \]
(FPCore (x y z t a) :precision binary64 (+ x (* y (/ (- z t) (- z a)))))
double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (z - a)));
}
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) / (z - a)))
end function
public static double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (z - a)));
}
def code(x, y, z, t, a):
	return x + (y * ((z - t) / (z - a)))
function code(x, y, z, t, a)
	return Float64(x + Float64(y * Float64(Float64(z - t) / Float64(z - a))))
end
function tmp = code(x, y, z, t, a)
	tmp = x + (y * ((z - t) / (z - a)));
end
code[x_, y_, z_, t_, a_] := N[(x + N[(y * N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
x + y \cdot \frac{z - t}{z - a}
\end{array}

Alternative 1: 98.4% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{z - t}{z - a} \leq 5 \cdot 10^{+100}:\\ \;\;\;\;x + \frac{y}{\frac{a - z}{t - z}}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\left(z - t\right) \cdot y}{z - a}\\ \end{array} \end{array} \]
(FPCore (x y z t a)
 :precision binary64
 (if (<= (/ (- z t) (- z a)) 5e+100)
   (+ x (/ y (/ (- a z) (- t z))))
   (+ x (/ (* (- z t) y) (- z a)))))
double code(double x, double y, double z, double t, double a) {
	double tmp;
	if (((z - t) / (z - a)) <= 5e+100) {
		tmp = x + (y / ((a - z) / (t - z)));
	} else {
		tmp = x + (((z - t) * y) / (z - a));
	}
	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 (((z - t) / (z - a)) <= 5d+100) then
        tmp = x + (y / ((a - z) / (t - z)))
    else
        tmp = x + (((z - t) * y) / (z - a))
    end if
    code = tmp
end function
public static double code(double x, double y, double z, double t, double a) {
	double tmp;
	if (((z - t) / (z - a)) <= 5e+100) {
		tmp = x + (y / ((a - z) / (t - z)));
	} else {
		tmp = x + (((z - t) * y) / (z - a));
	}
	return tmp;
}
def code(x, y, z, t, a):
	tmp = 0
	if ((z - t) / (z - a)) <= 5e+100:
		tmp = x + (y / ((a - z) / (t - z)))
	else:
		tmp = x + (((z - t) * y) / (z - a))
	return tmp
function code(x, y, z, t, a)
	tmp = 0.0
	if (Float64(Float64(z - t) / Float64(z - a)) <= 5e+100)
		tmp = Float64(x + Float64(y / Float64(Float64(a - z) / Float64(t - z))));
	else
		tmp = Float64(x + Float64(Float64(Float64(z - t) * y) / Float64(z - a)));
	end
	return tmp
end
function tmp_2 = code(x, y, z, t, a)
	tmp = 0.0;
	if (((z - t) / (z - a)) <= 5e+100)
		tmp = x + (y / ((a - z) / (t - z)));
	else
		tmp = x + (((z - t) * y) / (z - a));
	end
	tmp_2 = tmp;
end
code[x_, y_, z_, t_, a_] := If[LessEqual[N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision], 5e+100], N[(x + N[(y / N[(N[(a - z), $MachinePrecision] / N[(t - z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x + N[(N[(N[(z - t), $MachinePrecision] * y), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{z - t}{z - a} \leq 5 \cdot 10^{+100}:\\
\;\;\;\;x + \frac{y}{\frac{a - z}{t - z}}\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 (-.f64 z t) (-.f64 z a)) < 4.9999999999999999e100

    1. Initial program 99.0%

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

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

        \[\leadsto x + y \cdot \color{blue}{\frac{z - t}{z - a}} \]
      3. clear-numN/A

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

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

        \[\leadsto x + \color{blue}{\frac{y}{\frac{z - a}{z - t}}} \]
      6. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t} - z}} \]
      23. lower--.f6499.3

        \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t - z}}} \]
    4. Applied rewrites99.3%

      \[\leadsto x + \color{blue}{\frac{y}{\frac{a - z}{t - z}}} \]

    if 4.9999999999999999e100 < (/.f64 (-.f64 z t) (-.f64 z a))

    1. Initial program 78.1%

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

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

        \[\leadsto x + y \cdot \color{blue}{\frac{z - t}{z - a}} \]
      3. associate-*r/N/A

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

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

        \[\leadsto x + \frac{\color{blue}{\left(z - t\right) \cdot y}}{z - a} \]
      6. lower-*.f6499.8

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

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

Alternative 2: 95.7% accurate, 0.3× speedup?

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

\\
\begin{array}{l}
t_1 := \frac{z - t}{z - a}\\
t_2 := x + y \cdot \frac{t}{a - z}\\
\mathbf{if}\;t\_1 \leq -1 \cdot 10^{-70}:\\
\;\;\;\;t\_2\\

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

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

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (-.f64 z t) (-.f64 z a)) < -9.99999999999999996e-71 or 2 < (/.f64 (-.f64 z t) (-.f64 z a))

    1. Initial program 92.4%

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

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

        \[\leadsto x + y \cdot \color{blue}{\frac{z - t}{z - a}} \]
      3. clear-numN/A

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

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

        \[\leadsto x + \color{blue}{\frac{y}{\frac{z - a}{z - t}}} \]
      6. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t} - z}} \]
      23. lower--.f6493.8

        \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t - z}}} \]
    4. Applied rewrites93.8%

      \[\leadsto x + \color{blue}{\frac{y}{\frac{a - z}{t - z}}} \]
    5. Taylor expanded in t around inf

      \[\leadsto x + \color{blue}{\frac{t \cdot y}{a - z}} \]
    6. Step-by-step derivation
      1. *-commutativeN/A

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

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

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

        \[\leadsto x + y \cdot \color{blue}{\frac{t}{a - z}} \]
      5. lower--.f6489.2

        \[\leadsto x + y \cdot \frac{t}{\color{blue}{a - z}} \]
    7. Applied rewrites89.2%

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

    if -9.99999999999999996e-71 < (/.f64 (-.f64 z t) (-.f64 z a)) < 0.10000000000000001

    1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    if 0.10000000000000001 < (/.f64 (-.f64 z t) (-.f64 z a)) < 2

    1. Initial program 99.9%

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

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

        \[\leadsto \color{blue}{\frac{y \cdot z}{z - a} + x} \]
      2. associate-/l*N/A

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

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

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

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

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

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

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

Alternative 3: 86.7% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{z - t}{z - a}\\ \mathbf{if}\;t\_1 \leq -2:\\ \;\;\;\;\frac{y}{z - a} \cdot \left(z - t\right)\\ \mathbf{elif}\;t\_1 \leq 0.1 \lor \neg \left(t\_1 \leq 100000000000\right):\\ \;\;\;\;\mathsf{fma}\left(t - z, \frac{y}{a}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{z}{z - a}, y, x\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a)
 :precision binary64
 (let* ((t_1 (/ (- z t) (- z a))))
   (if (<= t_1 -2.0)
     (* (/ y (- z a)) (- z t))
     (if (or (<= t_1 0.1) (not (<= t_1 100000000000.0)))
       (fma (- t z) (/ y a) x)
       (fma (/ z (- z a)) y x)))))
double code(double x, double y, double z, double t, double a) {
	double t_1 = (z - t) / (z - a);
	double tmp;
	if (t_1 <= -2.0) {
		tmp = (y / (z - a)) * (z - t);
	} else if ((t_1 <= 0.1) || !(t_1 <= 100000000000.0)) {
		tmp = fma((t - z), (y / a), x);
	} else {
		tmp = fma((z / (z - a)), y, x);
	}
	return tmp;
}
function code(x, y, z, t, a)
	t_1 = Float64(Float64(z - t) / Float64(z - a))
	tmp = 0.0
	if (t_1 <= -2.0)
		tmp = Float64(Float64(y / Float64(z - a)) * Float64(z - t));
	elseif ((t_1 <= 0.1) || !(t_1 <= 100000000000.0))
		tmp = fma(Float64(t - z), Float64(y / a), x);
	else
		tmp = fma(Float64(z / Float64(z - a)), y, x);
	end
	return tmp
end
code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -2.0], N[(N[(y / N[(z - a), $MachinePrecision]), $MachinePrecision] * N[(z - t), $MachinePrecision]), $MachinePrecision], If[Or[LessEqual[t$95$1, 0.1], N[Not[LessEqual[t$95$1, 100000000000.0]], $MachinePrecision]], N[(N[(t - z), $MachinePrecision] * N[(y / a), $MachinePrecision] + x), $MachinePrecision], N[(N[(z / N[(z - a), $MachinePrecision]), $MachinePrecision] * y + x), $MachinePrecision]]]]
\begin{array}{l}

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

\mathbf{elif}\;t\_1 \leq 0.1 \lor \neg \left(t\_1 \leq 100000000000\right):\\
\;\;\;\;\mathsf{fma}\left(t - z, \frac{y}{a}, x\right)\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (-.f64 z t) (-.f64 z a)) < -2

    1. Initial program 94.4%

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

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

        \[\leadsto \color{blue}{y \cdot \frac{z - t}{z - a}} \]
      2. div-subN/A

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

        \[\leadsto \color{blue}{y \cdot \frac{z}{z - a} - y \cdot \frac{t}{z - a}} \]
      4. associate-/l*N/A

        \[\leadsto \color{blue}{\frac{y \cdot z}{z - a}} - y \cdot \frac{t}{z - a} \]
      5. associate-/l*N/A

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

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

        \[\leadsto \frac{\color{blue}{z \cdot y}}{z - a} - \frac{t \cdot y}{z - a} \]
      8. associate-/l*N/A

        \[\leadsto \color{blue}{z \cdot \frac{y}{z - a}} - \frac{t \cdot y}{z - a} \]
      9. associate-/l*N/A

        \[\leadsto z \cdot \frac{y}{z - a} - \color{blue}{t \cdot \frac{y}{z - a}} \]
      10. distribute-rgt-out--N/A

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

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

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

        \[\leadsto \frac{y}{\color{blue}{z - a}} \cdot \left(z - t\right) \]
      14. lower--.f6481.9

        \[\leadsto \frac{y}{z - a} \cdot \color{blue}{\left(z - t\right)} \]
    5. Applied rewrites81.9%

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

    if -2 < (/.f64 (-.f64 z t) (-.f64 z a)) < 0.10000000000000001 or 1e11 < (/.f64 (-.f64 z t) (-.f64 z a))

    1. Initial program 96.1%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    if 0.10000000000000001 < (/.f64 (-.f64 z t) (-.f64 z a)) < 1e11

    1. Initial program 99.9%

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

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

        \[\leadsto \color{blue}{\frac{y \cdot z}{z - a} + x} \]
      2. associate-/l*N/A

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

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

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

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

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

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{z - t}{z - a} \leq -2:\\ \;\;\;\;\frac{y}{z - a} \cdot \left(z - t\right)\\ \mathbf{elif}\;\frac{z - t}{z - a} \leq 0.1 \lor \neg \left(\frac{z - t}{z - a} \leq 100000000000\right):\\ \;\;\;\;\mathsf{fma}\left(t - z, \frac{y}{a}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{z}{z - a}, y, x\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 4: 86.7% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{z - t}{z - a}\\ \mathbf{if}\;t\_1 \leq -2:\\ \;\;\;\;\frac{y}{z - a} \cdot \left(-t\right)\\ \mathbf{elif}\;t\_1 \leq 0.1 \lor \neg \left(t\_1 \leq 100000000000\right):\\ \;\;\;\;\mathsf{fma}\left(t - z, \frac{y}{a}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{z}{z - a}, y, x\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a)
 :precision binary64
 (let* ((t_1 (/ (- z t) (- z a))))
   (if (<= t_1 -2.0)
     (* (/ y (- z a)) (- t))
     (if (or (<= t_1 0.1) (not (<= t_1 100000000000.0)))
       (fma (- t z) (/ y a) x)
       (fma (/ z (- z a)) y x)))))
double code(double x, double y, double z, double t, double a) {
	double t_1 = (z - t) / (z - a);
	double tmp;
	if (t_1 <= -2.0) {
		tmp = (y / (z - a)) * -t;
	} else if ((t_1 <= 0.1) || !(t_1 <= 100000000000.0)) {
		tmp = fma((t - z), (y / a), x);
	} else {
		tmp = fma((z / (z - a)), y, x);
	}
	return tmp;
}
function code(x, y, z, t, a)
	t_1 = Float64(Float64(z - t) / Float64(z - a))
	tmp = 0.0
	if (t_1 <= -2.0)
		tmp = Float64(Float64(y / Float64(z - a)) * Float64(-t));
	elseif ((t_1 <= 0.1) || !(t_1 <= 100000000000.0))
		tmp = fma(Float64(t - z), Float64(y / a), x);
	else
		tmp = fma(Float64(z / Float64(z - a)), y, x);
	end
	return tmp
end
code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -2.0], N[(N[(y / N[(z - a), $MachinePrecision]), $MachinePrecision] * (-t)), $MachinePrecision], If[Or[LessEqual[t$95$1, 0.1], N[Not[LessEqual[t$95$1, 100000000000.0]], $MachinePrecision]], N[(N[(t - z), $MachinePrecision] * N[(y / a), $MachinePrecision] + x), $MachinePrecision], N[(N[(z / N[(z - a), $MachinePrecision]), $MachinePrecision] * y + x), $MachinePrecision]]]]
\begin{array}{l}

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

\mathbf{elif}\;t\_1 \leq 0.1 \lor \neg \left(t\_1 \leq 100000000000\right):\\
\;\;\;\;\mathsf{fma}\left(t - z, \frac{y}{a}, x\right)\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (-.f64 z t) (-.f64 z a)) < -2

    1. Initial program 94.4%

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

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

        \[\leadsto \color{blue}{y \cdot \frac{z - t}{z - a}} \]
      2. div-subN/A

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

        \[\leadsto \color{blue}{y \cdot \frac{z}{z - a} - y \cdot \frac{t}{z - a}} \]
      4. associate-/l*N/A

        \[\leadsto \color{blue}{\frac{y \cdot z}{z - a}} - y \cdot \frac{t}{z - a} \]
      5. associate-/l*N/A

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

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

        \[\leadsto \frac{\color{blue}{z \cdot y}}{z - a} - \frac{t \cdot y}{z - a} \]
      8. associate-/l*N/A

        \[\leadsto \color{blue}{z \cdot \frac{y}{z - a}} - \frac{t \cdot y}{z - a} \]
      9. associate-/l*N/A

        \[\leadsto z \cdot \frac{y}{z - a} - \color{blue}{t \cdot \frac{y}{z - a}} \]
      10. distribute-rgt-out--N/A

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

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

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

        \[\leadsto \frac{y}{\color{blue}{z - a}} \cdot \left(z - t\right) \]
      14. lower--.f6481.9

        \[\leadsto \frac{y}{z - a} \cdot \color{blue}{\left(z - t\right)} \]
    5. Applied rewrites81.9%

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

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

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

      if -2 < (/.f64 (-.f64 z t) (-.f64 z a)) < 0.10000000000000001 or 1e11 < (/.f64 (-.f64 z t) (-.f64 z a))

      1. Initial program 96.1%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      if 0.10000000000000001 < (/.f64 (-.f64 z t) (-.f64 z a)) < 1e11

      1. Initial program 99.9%

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

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

          \[\leadsto \color{blue}{\frac{y \cdot z}{z - a} + x} \]
        2. associate-/l*N/A

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

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

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

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

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

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

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{z - t}{z - a} \leq -2:\\ \;\;\;\;\frac{y}{z - a} \cdot \left(-t\right)\\ \mathbf{elif}\;\frac{z - t}{z - a} \leq 0.1 \lor \neg \left(\frac{z - t}{z - a} \leq 100000000000\right):\\ \;\;\;\;\mathsf{fma}\left(t - z, \frac{y}{a}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{z}{z - a}, y, x\right)\\ \end{array} \]
    10. Add Preprocessing

    Alternative 5: 86.0% accurate, 0.3× speedup?

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

      1. Initial program 94.6%

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

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

          \[\leadsto x + y \cdot \color{blue}{\frac{z - t}{z - a}} \]
        3. clear-numN/A

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

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

          \[\leadsto x + \color{blue}{\frac{y}{\frac{z - a}{z - t}}} \]
        6. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t} - z}} \]
        23. lower--.f6496.4

          \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t - z}}} \]
      4. Applied rewrites96.4%

        \[\leadsto x + \color{blue}{\frac{y}{\frac{a - z}{t - z}}} \]
      5. Taylor expanded in z around inf

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

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

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

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

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

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

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

          \[\leadsto x + \frac{y}{1 - \color{blue}{\frac{a - t}{z}}} \]
        8. lower--.f6416.2

          \[\leadsto x + \frac{y}{1 - \frac{\color{blue}{a - t}}{z}} \]
      7. Applied rewrites16.2%

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

        \[\leadsto \color{blue}{\frac{t \cdot y}{a - z}} \]
      9. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \frac{\color{blue}{y \cdot t}}{a - z} \]
        2. associate-/l*N/A

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

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

          \[\leadsto y \cdot \color{blue}{\frac{t}{a - z}} \]
        5. lower--.f6474.8

          \[\leadsto y \cdot \frac{t}{\color{blue}{a - z}} \]
      10. Applied rewrites74.8%

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

      if -1.00000000000000004e-10 < (/.f64 (-.f64 z t) (-.f64 z a)) < 0.10000000000000001 or 1e11 < (/.f64 (-.f64 z t) (-.f64 z a))

      1. Initial program 96.1%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      if 0.10000000000000001 < (/.f64 (-.f64 z t) (-.f64 z a)) < 1e11

      1. Initial program 99.9%

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

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

          \[\leadsto \color{blue}{\frac{y \cdot z}{z - a} + x} \]
        2. associate-/l*N/A

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

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

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

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

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

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

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

    Alternative 6: 85.8% accurate, 0.3× speedup?

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

      1. Initial program 94.6%

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

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

          \[\leadsto x + y \cdot \color{blue}{\frac{z - t}{z - a}} \]
        3. clear-numN/A

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

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

          \[\leadsto x + \color{blue}{\frac{y}{\frac{z - a}{z - t}}} \]
        6. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t} - z}} \]
        23. lower--.f6496.4

          \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t - z}}} \]
      4. Applied rewrites96.4%

        \[\leadsto x + \color{blue}{\frac{y}{\frac{a - z}{t - z}}} \]
      5. Taylor expanded in z around inf

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

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

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

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

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

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

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

          \[\leadsto x + \frac{y}{1 - \color{blue}{\frac{a - t}{z}}} \]
        8. lower--.f6416.2

          \[\leadsto x + \frac{y}{1 - \frac{\color{blue}{a - t}}{z}} \]
      7. Applied rewrites16.2%

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

        \[\leadsto \color{blue}{\frac{t \cdot y}{a - z}} \]
      9. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \frac{\color{blue}{y \cdot t}}{a - z} \]
        2. associate-/l*N/A

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

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

          \[\leadsto y \cdot \color{blue}{\frac{t}{a - z}} \]
        5. lower--.f6474.8

          \[\leadsto y \cdot \frac{t}{\color{blue}{a - z}} \]
      10. Applied rewrites74.8%

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

      if -1.00000000000000004e-10 < (/.f64 (-.f64 z t) (-.f64 z a)) < 0.5

      1. Initial program 99.8%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      if 0.5 < (/.f64 (-.f64 z t) (-.f64 z a)) < 1e18

      1. Initial program 99.9%

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

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

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

          \[\leadsto \color{blue}{y + x} \]
      5. Applied rewrites95.9%

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

      if 1e18 < (/.f64 (-.f64 z t) (-.f64 z a))

      1. Initial program 88.4%

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

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

          \[\leadsto \color{blue}{\frac{t \cdot y}{a} + x} \]
        2. associate-/l*N/A

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

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

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

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

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

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

    Alternative 7: 81.7% accurate, 0.3× speedup?

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

      1. Initial program 94.6%

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

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

          \[\leadsto x + y \cdot \color{blue}{\frac{z - t}{z - a}} \]
        3. clear-numN/A

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

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

          \[\leadsto x + \color{blue}{\frac{y}{\frac{z - a}{z - t}}} \]
        6. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t} - z}} \]
        23. lower--.f6496.4

          \[\leadsto x + \frac{y}{\frac{a - z}{\color{blue}{t - z}}} \]
      4. Applied rewrites96.4%

        \[\leadsto x + \color{blue}{\frac{y}{\frac{a - z}{t - z}}} \]
      5. Taylor expanded in z around inf

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

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

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

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

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

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

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

          \[\leadsto x + \frac{y}{1 - \color{blue}{\frac{a - t}{z}}} \]
        8. lower--.f6416.2

          \[\leadsto x + \frac{y}{1 - \frac{\color{blue}{a - t}}{z}} \]
      7. Applied rewrites16.2%

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

        \[\leadsto \color{blue}{\frac{t \cdot y}{a - z}} \]
      9. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \frac{\color{blue}{y \cdot t}}{a - z} \]
        2. associate-/l*N/A

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

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

          \[\leadsto y \cdot \color{blue}{\frac{t}{a - z}} \]
        5. lower--.f6474.8

          \[\leadsto y \cdot \frac{t}{\color{blue}{a - z}} \]
      10. Applied rewrites74.8%

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

      if -1.00000000000000004e-10 < (/.f64 (-.f64 z t) (-.f64 z a)) < 0.10000000000000001

      1. Initial program 99.8%

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

        \[\leadsto x + y \cdot \color{blue}{\frac{t}{a}} \]
      4. Step-by-step derivation
        1. lower-/.f6485.0

          \[\leadsto x + y \cdot \color{blue}{\frac{t}{a}} \]
      5. Applied rewrites85.0%

        \[\leadsto x + y \cdot \color{blue}{\frac{t}{a}} \]
      6. Step-by-step derivation
        1. lift-+.f64N/A

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

          \[\leadsto \color{blue}{y \cdot \frac{t}{a} + x} \]
        3. lift-*.f64N/A

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

          \[\leadsto \color{blue}{\frac{t}{a} \cdot y} + x \]
        5. lower-fma.f6485.0

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

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

      if 0.10000000000000001 < (/.f64 (-.f64 z t) (-.f64 z a)) < 1e18

      1. Initial program 99.9%

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

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

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

          \[\leadsto \color{blue}{y + x} \]
      5. Applied rewrites95.0%

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

      if 1e18 < (/.f64 (-.f64 z t) (-.f64 z a))

      1. Initial program 88.4%

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

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

          \[\leadsto \color{blue}{\frac{t \cdot y}{a} + x} \]
        2. associate-/l*N/A

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

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

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

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

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

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

    Alternative 8: 81.1% accurate, 0.4× speedup?

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

      1. Initial program 95.7%

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

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

          \[\leadsto \color{blue}{\frac{t \cdot y}{a} + x} \]
        2. associate-/l*N/A

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

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

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

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

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

      if 0.10000000000000001 < (/.f64 (-.f64 z t) (-.f64 z a)) < 1e18

      1. Initial program 99.9%

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

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

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

          \[\leadsto \color{blue}{y + x} \]
      5. Applied rewrites95.0%

        \[\leadsto \color{blue}{y + x} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification81.5%

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

    Alternative 9: 81.0% accurate, 0.4× speedup?

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

      1. Initial program 98.2%

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

        \[\leadsto x + y \cdot \color{blue}{\frac{t}{a}} \]
      4. Step-by-step derivation
        1. lower-/.f6475.2

          \[\leadsto x + y \cdot \color{blue}{\frac{t}{a}} \]
      5. Applied rewrites75.2%

        \[\leadsto x + y \cdot \color{blue}{\frac{t}{a}} \]
      6. Step-by-step derivation
        1. lift-+.f64N/A

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

          \[\leadsto \color{blue}{y \cdot \frac{t}{a} + x} \]
        3. lift-*.f64N/A

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

          \[\leadsto \color{blue}{\frac{t}{a} \cdot y} + x \]
        5. lower-fma.f6475.2

          \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{t}{a}, y, x\right)} \]
      7. Applied rewrites75.2%

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

      if 0.10000000000000001 < (/.f64 (-.f64 z t) (-.f64 z a)) < 1e18

      1. Initial program 99.9%

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

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

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

          \[\leadsto \color{blue}{y + x} \]
      5. Applied rewrites95.0%

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

      if 1e18 < (/.f64 (-.f64 z t) (-.f64 z a))

      1. Initial program 88.4%

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

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

          \[\leadsto \color{blue}{\frac{t \cdot y}{a} + x} \]
        2. associate-/l*N/A

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

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

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

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

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

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

    Alternative 10: 98.3% accurate, 0.5× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{z - t}{z - a}\\ \mathbf{if}\;t\_1 \leq 5 \cdot 10^{+100}:\\ \;\;\;\;x + y \cdot t\_1\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\left(z - t\right) \cdot y}{z - a}\\ \end{array} \end{array} \]
    (FPCore (x y z t a)
     :precision binary64
     (let* ((t_1 (/ (- z t) (- z a))))
       (if (<= t_1 5e+100) (+ x (* y t_1)) (+ x (/ (* (- z t) y) (- z a))))))
    double code(double x, double y, double z, double t, double a) {
    	double t_1 = (z - t) / (z - a);
    	double tmp;
    	if (t_1 <= 5e+100) {
    		tmp = x + (y * t_1);
    	} else {
    		tmp = x + (((z - t) * y) / (z - a));
    	}
    	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) :: tmp
        t_1 = (z - t) / (z - a)
        if (t_1 <= 5d+100) then
            tmp = x + (y * t_1)
        else
            tmp = x + (((z - t) * y) / (z - a))
        end if
        code = tmp
    end function
    
    public static double code(double x, double y, double z, double t, double a) {
    	double t_1 = (z - t) / (z - a);
    	double tmp;
    	if (t_1 <= 5e+100) {
    		tmp = x + (y * t_1);
    	} else {
    		tmp = x + (((z - t) * y) / (z - a));
    	}
    	return tmp;
    }
    
    def code(x, y, z, t, a):
    	t_1 = (z - t) / (z - a)
    	tmp = 0
    	if t_1 <= 5e+100:
    		tmp = x + (y * t_1)
    	else:
    		tmp = x + (((z - t) * y) / (z - a))
    	return tmp
    
    function code(x, y, z, t, a)
    	t_1 = Float64(Float64(z - t) / Float64(z - a))
    	tmp = 0.0
    	if (t_1 <= 5e+100)
    		tmp = Float64(x + Float64(y * t_1));
    	else
    		tmp = Float64(x + Float64(Float64(Float64(z - t) * y) / Float64(z - a)));
    	end
    	return tmp
    end
    
    function tmp_2 = code(x, y, z, t, a)
    	t_1 = (z - t) / (z - a);
    	tmp = 0.0;
    	if (t_1 <= 5e+100)
    		tmp = x + (y * t_1);
    	else
    		tmp = x + (((z - t) * y) / (z - a));
    	end
    	tmp_2 = tmp;
    end
    
    code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, 5e+100], N[(x + N[(y * t$95$1), $MachinePrecision]), $MachinePrecision], N[(x + N[(N[(N[(z - t), $MachinePrecision] * y), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := \frac{z - t}{z - a}\\
    \mathbf{if}\;t\_1 \leq 5 \cdot 10^{+100}:\\
    \;\;\;\;x + y \cdot t\_1\\
    
    \mathbf{else}:\\
    \;\;\;\;x + \frac{\left(z - t\right) \cdot y}{z - a}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 (-.f64 z t) (-.f64 z a)) < 4.9999999999999999e100

      1. Initial program 99.0%

        \[x + y \cdot \frac{z - t}{z - a} \]
      2. Add Preprocessing

      if 4.9999999999999999e100 < (/.f64 (-.f64 z t) (-.f64 z a))

      1. Initial program 78.1%

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

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

          \[\leadsto x + y \cdot \color{blue}{\frac{z - t}{z - a}} \]
        3. associate-*r/N/A

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

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

          \[\leadsto x + \frac{\color{blue}{\left(z - t\right) \cdot y}}{z - a} \]
        6. lower-*.f6499.8

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

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

    Alternative 11: 63.0% accurate, 0.5× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x + y \cdot \frac{z - t}{z - a} \leq 2 \cdot 10^{+298}:\\ \;\;\;\;y + x\\ \mathbf{else}:\\ \;\;\;\;\frac{t \cdot y}{a}\\ \end{array} \end{array} \]
    (FPCore (x y z t a)
     :precision binary64
     (if (<= (+ x (* y (/ (- z t) (- z a)))) 2e+298) (+ y x) (/ (* t y) a)))
    double code(double x, double y, double z, double t, double a) {
    	double tmp;
    	if ((x + (y * ((z - t) / (z - a)))) <= 2e+298) {
    		tmp = y + x;
    	} else {
    		tmp = (t * y) / a;
    	}
    	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 ((x + (y * ((z - t) / (z - a)))) <= 2d+298) then
            tmp = y + x
        else
            tmp = (t * y) / a
        end if
        code = tmp
    end function
    
    public static double code(double x, double y, double z, double t, double a) {
    	double tmp;
    	if ((x + (y * ((z - t) / (z - a)))) <= 2e+298) {
    		tmp = y + x;
    	} else {
    		tmp = (t * y) / a;
    	}
    	return tmp;
    }
    
    def code(x, y, z, t, a):
    	tmp = 0
    	if (x + (y * ((z - t) / (z - a)))) <= 2e+298:
    		tmp = y + x
    	else:
    		tmp = (t * y) / a
    	return tmp
    
    function code(x, y, z, t, a)
    	tmp = 0.0
    	if (Float64(x + Float64(y * Float64(Float64(z - t) / Float64(z - a)))) <= 2e+298)
    		tmp = Float64(y + x);
    	else
    		tmp = Float64(Float64(t * y) / a);
    	end
    	return tmp
    end
    
    function tmp_2 = code(x, y, z, t, a)
    	tmp = 0.0;
    	if ((x + (y * ((z - t) / (z - a)))) <= 2e+298)
    		tmp = y + x;
    	else
    		tmp = (t * y) / a;
    	end
    	tmp_2 = tmp;
    end
    
    code[x_, y_, z_, t_, a_] := If[LessEqual[N[(x + N[(y * N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 2e+298], N[(y + x), $MachinePrecision], N[(N[(t * y), $MachinePrecision] / a), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;x + y \cdot \frac{z - t}{z - a} \leq 2 \cdot 10^{+298}:\\
    \;\;\;\;y + x\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{t \cdot y}{a}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (+.f64 x (*.f64 y (/.f64 (-.f64 z t) (-.f64 z a)))) < 1.9999999999999999e298

      1. Initial program 98.6%

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

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

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

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

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

      if 1.9999999999999999e298 < (+.f64 x (*.f64 y (/.f64 (-.f64 z t) (-.f64 z a))))

      1. Initial program 76.2%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \frac{t \cdot y}{a} \]
        3. Step-by-step derivation
          1. Applied rewrites72.4%

            \[\leadsto \frac{t \cdot y}{a} \]
        4. Recombined 2 regimes into one program.
        5. Final simplification62.8%

          \[\leadsto \begin{array}{l} \mathbf{if}\;x + y \cdot \frac{z - t}{z - a} \leq 2 \cdot 10^{+298}:\\ \;\;\;\;y + x\\ \mathbf{else}:\\ \;\;\;\;\frac{t \cdot y}{a}\\ \end{array} \]
        6. Add Preprocessing

        Alternative 12: 97.9% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ x + y \cdot \frac{z - t}{z - a} \end{array} \]
        (FPCore (x y z t a) :precision binary64 (+ x (* y (/ (- z t) (- z a)))))
        double code(double x, double y, double z, double t, double a) {
        	return x + (y * ((z - t) / (z - a)));
        }
        
        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) / (z - a)))
        end function
        
        public static double code(double x, double y, double z, double t, double a) {
        	return x + (y * ((z - t) / (z - a)));
        }
        
        def code(x, y, z, t, a):
        	return x + (y * ((z - t) / (z - a)))
        
        function code(x, y, z, t, a)
        	return Float64(x + Float64(y * Float64(Float64(z - t) / Float64(z - a))))
        end
        
        function tmp = code(x, y, z, t, a)
        	tmp = x + (y * ((z - t) / (z - a)));
        end
        
        code[x_, y_, z_, t_, a_] := N[(x + N[(y * N[(N[(z - t), $MachinePrecision] / N[(z - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
        
        \begin{array}{l}
        
        \\
        x + y \cdot \frac{z - t}{z - a}
        \end{array}
        
        Derivation
        1. Initial program 97.2%

          \[x + y \cdot \frac{z - t}{z - a} \]
        2. Add Preprocessing
        3. Add Preprocessing

        Alternative 13: 97.9% accurate, 1.1× speedup?

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{z - t}{z - a} \cdot y} + x \]
          5. lower-fma.f6497.2

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(\frac{0 - \color{blue}{\left(\left(\mathsf{neg}\left(t\right)\right) + z\right)}}{\mathsf{neg}\left(\left(z - a\right)\right)}, y, x\right) \]
          13. associate--r+N/A

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(\frac{t - z}{0 - \color{blue}{\left(z - a\right)}}, y, x\right) \]
          19. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\frac{t - z}{0 - \color{blue}{\left(\left(\mathsf{neg}\left(a\right)\right) + z\right)}}, y, x\right) \]
          21. associate--r+N/A

            \[\leadsto \mathsf{fma}\left(\frac{t - z}{\color{blue}{\left(0 - \left(\mathsf{neg}\left(a\right)\right)\right) - z}}, y, x\right) \]
          22. neg-sub0N/A

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

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

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

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

        Alternative 14: 60.8% accurate, 6.5× speedup?

        \[\begin{array}{l} \\ y + x \end{array} \]
        (FPCore (x y z t a) :precision binary64 (+ y x))
        double code(double x, double y, double z, double t, double a) {
        	return y + 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 = y + x
        end function
        
        public static double code(double x, double y, double z, double t, double a) {
        	return y + x;
        }
        
        def code(x, y, z, t, a):
        	return y + x
        
        function code(x, y, z, t, a)
        	return Float64(y + x)
        end
        
        function tmp = code(x, y, z, t, a)
        	tmp = y + x;
        end
        
        code[x_, y_, z_, t_, a_] := N[(y + x), $MachinePrecision]
        
        \begin{array}{l}
        
        \\
        y + x
        \end{array}
        
        Derivation
        1. Initial program 97.2%

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

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

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

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

          \[\leadsto \color{blue}{y + x} \]
        6. Final simplification58.5%

          \[\leadsto y + x \]
        7. Add Preprocessing

        Developer Target 1: 98.1% accurate, 0.8× speedup?

        \[\begin{array}{l} \\ x + \frac{y}{\frac{z - a}{z - t}} \end{array} \]
        (FPCore (x y z t a) :precision binary64 (+ x (/ y (/ (- z a) (- z t)))))
        double code(double x, double y, double z, double t, double a) {
        	return x + (y / ((z - a) / (z - 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 - a) / (z - t)))
        end function
        
        public static double code(double x, double y, double z, double t, double a) {
        	return x + (y / ((z - a) / (z - t)));
        }
        
        def code(x, y, z, t, a):
        	return x + (y / ((z - a) / (z - t)))
        
        function code(x, y, z, t, a)
        	return Float64(x + Float64(y / Float64(Float64(z - a) / Float64(z - t))))
        end
        
        function tmp = code(x, y, z, t, a)
        	tmp = x + (y / ((z - a) / (z - t)));
        end
        
        code[x_, y_, z_, t_, a_] := N[(x + N[(y / N[(N[(z - a), $MachinePrecision] / N[(z - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
        
        \begin{array}{l}
        
        \\
        x + \frac{y}{\frac{z - a}{z - t}}
        \end{array}
        

        Reproduce

        ?
        herbie shell --seed 2024313 
        (FPCore (x y z t a)
          :name "Graphics.Rendering.Plot.Render.Plot.Axis:renderAxisLine from plot-0.2.3.4, A"
          :precision binary64
        
          :alt
          (! :herbie-platform default (+ x (/ y (/ (- z a) (- z t)))))
        
          (+ x (* y (/ (- z t) (- z a)))))