Numeric.Signal.Multichannel:$cput from hsignal-0.2.7.1

Percentage Accurate: 96.8% → 96.8%
Time: 9.9s
Alternatives: 11
Speedup: 1.0×

Specification

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

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

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

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

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

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

Alternative 1: 96.8% accurate, 1.0× speedup?

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

\\
\frac{x - y}{z - y} \cdot t
\end{array}
Derivation
  1. Initial program 96.7%

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

Alternative 2: 71.4% accurate, 0.2× speedup?

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

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

\mathbf{elif}\;t\_1 \leq 2 \cdot 10^{-179}:\\
\;\;\;\;-\frac{y \cdot t}{z}\\

\mathbf{elif}\;t\_1 \leq 0.4:\\
\;\;\;\;t\_2\\

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

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (-.f64 x y) (-.f64 z y)) < -5.0000000000000002e-142 or 2e-179 < (/.f64 (-.f64 x y) (-.f64 z y)) < 0.40000000000000002 or 2 < (/.f64 (-.f64 x y) (-.f64 z y))

    1. Initial program 96.7%

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

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

        \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
    5. Simplified63.4%

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

    if -5.0000000000000002e-142 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2e-179

    1. Initial program 91.0%

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \mathsf{neg}\left(\color{blue}{\frac{t \cdot y}{z}}\right) \]
      4. lower-*.f6479.1

        \[\leadsto -\frac{\color{blue}{t \cdot y}}{z} \]
    8. Simplified79.1%

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

    if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{x - y}{\color{blue}{z - y}} \cdot t \]
      3. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
      14. lower-/.f6475.5

        \[\leadsto \frac{y - x}{\color{blue}{\frac{y - z}{t}}} \]
    6. Applied egg-rr75.5%

      \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{t \cdot y}{y - z}} \]
    8. Step-by-step derivation
      1. associate-/l*N/A

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

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

        \[\leadsto t \cdot \color{blue}{\frac{y}{y - z}} \]
      4. lower--.f6499.7

        \[\leadsto t \cdot \frac{y}{\color{blue}{y - z}} \]
    9. Simplified99.7%

      \[\leadsto \color{blue}{t \cdot \frac{y}{y - z}} \]
    10. Taylor expanded in y around inf

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

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

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

        \[\leadsto \color{blue}{\mathsf{fma}\left(t, \frac{z}{y}, t\right)} \]
      4. lower-/.f6499.3

        \[\leadsto \mathsf{fma}\left(t, \color{blue}{\frac{z}{y}}, t\right) \]
    12. Simplified99.3%

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

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

Alternative 3: 94.1% accurate, 0.3× speedup?

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

\\
\begin{array}{l}
t_1 := \frac{x - y}{z - y}\\
\mathbf{if}\;t\_1 \leq -2 \cdot 10^{+37}:\\
\;\;\;\;\frac{x \cdot t}{z - y}\\

\mathbf{elif}\;t\_1 \leq 0.4:\\
\;\;\;\;t \cdot \frac{x - y}{z}\\

\mathbf{elif}\;t\_1 \leq 2:\\
\;\;\;\;t \cdot \frac{y}{y - z}\\

\mathbf{else}:\\
\;\;\;\;t \cdot \frac{x}{z - y}\\


\end{array}
\end{array}
Derivation
  1. Split input into 4 regimes
  2. if (/.f64 (-.f64 x y) (-.f64 z y)) < -1.99999999999999991e37

    1. Initial program 93.6%

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{\left(x - y\right) \cdot t}{z - y}} \]
      15. lower-*.f6496.8

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

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

      \[\leadsto \frac{\color{blue}{t \cdot x}}{z - y} \]
    6. Step-by-step derivation
      1. lower-*.f6496.8

        \[\leadsto \frac{\color{blue}{t \cdot x}}{z - y} \]
    7. Simplified96.8%

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

    if -1.99999999999999991e37 < (/.f64 (-.f64 x y) (-.f64 z y)) < 0.40000000000000002

    1. Initial program 95.8%

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

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

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

        \[\leadsto \frac{\color{blue}{x - y}}{z} \cdot t \]
    5. Simplified94.2%

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

    if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{x - y}{\color{blue}{z - y}} \cdot t \]
      3. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
      14. lower-/.f6475.5

        \[\leadsto \frac{y - x}{\color{blue}{\frac{y - z}{t}}} \]
    6. Applied egg-rr75.5%

      \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{t \cdot y}{y - z}} \]
    8. Step-by-step derivation
      1. associate-/l*N/A

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

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

        \[\leadsto t \cdot \color{blue}{\frac{y}{y - z}} \]
      4. lower--.f6499.7

        \[\leadsto t \cdot \frac{y}{\color{blue}{y - z}} \]
    9. Simplified99.7%

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

    if 2 < (/.f64 (-.f64 x y) (-.f64 z y))

    1. Initial program 95.0%

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

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

        \[\leadsto \color{blue}{\frac{x}{z - y}} \cdot t \]
      2. lower--.f6493.6

        \[\leadsto \frac{x}{\color{blue}{z - y}} \cdot t \]
    5. Simplified93.6%

      \[\leadsto \color{blue}{\frac{x}{z - y}} \cdot t \]
  3. Recombined 4 regimes into one program.
  4. Final simplification96.1%

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

Alternative 4: 95.4% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{x - y}{z - y}\\ t_2 := t \cdot \frac{x}{z - y}\\ \mathbf{if}\;t\_1 \leq -4000000000:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 0.4:\\ \;\;\;\;t \cdot \frac{x - y}{z}\\ \mathbf{elif}\;t\_1 \leq 2:\\ \;\;\;\;t \cdot \frac{y}{y - z}\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \end{array} \]
(FPCore (x y z t)
 :precision binary64
 (let* ((t_1 (/ (- x y) (- z y))) (t_2 (* t (/ x (- z y)))))
   (if (<= t_1 -4000000000.0)
     t_2
     (if (<= t_1 0.4)
       (* t (/ (- x y) z))
       (if (<= t_1 2.0) (* t (/ y (- y z))) t_2)))))
double code(double x, double y, double z, double t) {
	double t_1 = (x - y) / (z - y);
	double t_2 = t * (x / (z - y));
	double tmp;
	if (t_1 <= -4000000000.0) {
		tmp = t_2;
	} else if (t_1 <= 0.4) {
		tmp = t * ((x - y) / z);
	} else if (t_1 <= 2.0) {
		tmp = t * (y / (y - z));
	} else {
		tmp = t_2;
	}
	return tmp;
}
real(8) function code(x, y, z, t)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8) :: t_1
    real(8) :: t_2
    real(8) :: tmp
    t_1 = (x - y) / (z - y)
    t_2 = t * (x / (z - y))
    if (t_1 <= (-4000000000.0d0)) then
        tmp = t_2
    else if (t_1 <= 0.4d0) then
        tmp = t * ((x - y) / z)
    else if (t_1 <= 2.0d0) then
        tmp = t * (y / (y - z))
    else
        tmp = t_2
    end if
    code = tmp
end function
public static double code(double x, double y, double z, double t) {
	double t_1 = (x - y) / (z - y);
	double t_2 = t * (x / (z - y));
	double tmp;
	if (t_1 <= -4000000000.0) {
		tmp = t_2;
	} else if (t_1 <= 0.4) {
		tmp = t * ((x - y) / z);
	} else if (t_1 <= 2.0) {
		tmp = t * (y / (y - z));
	} else {
		tmp = t_2;
	}
	return tmp;
}
def code(x, y, z, t):
	t_1 = (x - y) / (z - y)
	t_2 = t * (x / (z - y))
	tmp = 0
	if t_1 <= -4000000000.0:
		tmp = t_2
	elif t_1 <= 0.4:
		tmp = t * ((x - y) / z)
	elif t_1 <= 2.0:
		tmp = t * (y / (y - z))
	else:
		tmp = t_2
	return tmp
function code(x, y, z, t)
	t_1 = Float64(Float64(x - y) / Float64(z - y))
	t_2 = Float64(t * Float64(x / Float64(z - y)))
	tmp = 0.0
	if (t_1 <= -4000000000.0)
		tmp = t_2;
	elseif (t_1 <= 0.4)
		tmp = Float64(t * Float64(Float64(x - y) / z));
	elseif (t_1 <= 2.0)
		tmp = Float64(t * Float64(y / Float64(y - z)));
	else
		tmp = t_2;
	end
	return tmp
end
function tmp_2 = code(x, y, z, t)
	t_1 = (x - y) / (z - y);
	t_2 = t * (x / (z - y));
	tmp = 0.0;
	if (t_1 <= -4000000000.0)
		tmp = t_2;
	elseif (t_1 <= 0.4)
		tmp = t * ((x - y) / z);
	elseif (t_1 <= 2.0)
		tmp = t * (y / (y - z));
	else
		tmp = t_2;
	end
	tmp_2 = tmp;
end
code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[(x - y), $MachinePrecision] / N[(z - y), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(t * N[(x / N[(z - y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -4000000000.0], t$95$2, If[LessEqual[t$95$1, 0.4], N[(t * N[(N[(x - y), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 2.0], N[(t * N[(y / N[(y - z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$2]]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \frac{x - y}{z - y}\\
t_2 := t \cdot \frac{x}{z - y}\\
\mathbf{if}\;t\_1 \leq -4000000000:\\
\;\;\;\;t\_2\\

\mathbf{elif}\;t\_1 \leq 0.4:\\
\;\;\;\;t \cdot \frac{x - y}{z}\\

\mathbf{elif}\;t\_1 \leq 2:\\
\;\;\;\;t \cdot \frac{y}{y - z}\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (-.f64 x y) (-.f64 z y)) < -4e9 or 2 < (/.f64 (-.f64 x y) (-.f64 z y))

    1. Initial program 94.6%

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

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

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

        \[\leadsto \frac{x}{\color{blue}{z - y}} \cdot t \]
    5. Simplified93.4%

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

    if -4e9 < (/.f64 (-.f64 x y) (-.f64 z y)) < 0.40000000000000002

    1. Initial program 95.7%

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

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

        \[\leadsto \color{blue}{\frac{x - y}{z}} \cdot t \]
      2. lower--.f6495.0

        \[\leadsto \frac{\color{blue}{x - y}}{z} \cdot t \]
    5. Simplified95.0%

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

    if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{x - y}{\color{blue}{z - y}} \cdot t \]
      3. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
      14. lower-/.f6475.5

        \[\leadsto \frac{y - x}{\color{blue}{\frac{y - z}{t}}} \]
    6. Applied egg-rr75.5%

      \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{t \cdot y}{y - z}} \]
    8. Step-by-step derivation
      1. associate-/l*N/A

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

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

        \[\leadsto t \cdot \color{blue}{\frac{y}{y - z}} \]
      4. lower--.f6499.7

        \[\leadsto t \cdot \frac{y}{\color{blue}{y - z}} \]
    9. Simplified99.7%

      \[\leadsto \color{blue}{t \cdot \frac{y}{y - z}} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification96.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x - y}{z - y} \leq -4000000000:\\ \;\;\;\;t \cdot \frac{x}{z - y}\\ \mathbf{elif}\;\frac{x - y}{z - y} \leq 0.4:\\ \;\;\;\;t \cdot \frac{x - y}{z}\\ \mathbf{elif}\;\frac{x - y}{z - y} \leq 2:\\ \;\;\;\;t \cdot \frac{y}{y - z}\\ \mathbf{else}:\\ \;\;\;\;t \cdot \frac{x}{z - y}\\ \end{array} \]
  5. Add Preprocessing

Alternative 5: 94.0% accurate, 0.3× speedup?

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

\\
\begin{array}{l}
t_1 := \frac{x - y}{z - y}\\
t_2 := t \cdot \frac{x}{z - y}\\
\mathbf{if}\;t\_1 \leq -200000:\\
\;\;\;\;t\_2\\

\mathbf{elif}\;t\_1 \leq 0.4:\\
\;\;\;\;\left(x - y\right) \cdot \frac{t}{z}\\

\mathbf{elif}\;t\_1 \leq 2:\\
\;\;\;\;t \cdot \frac{y}{y - z}\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (-.f64 x y) (-.f64 z y)) < -2e5 or 2 < (/.f64 (-.f64 x y) (-.f64 z y))

    1. Initial program 94.7%

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

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

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

        \[\leadsto \frac{x}{\color{blue}{z - y}} \cdot t \]
    5. Simplified93.5%

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

    if -2e5 < (/.f64 (-.f64 x y) (-.f64 z y)) < 0.40000000000000002

    1. Initial program 95.6%

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

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

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

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

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

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

        \[\leadsto \left(x - y\right) \cdot \color{blue}{\frac{t}{z}} \]
    5. Simplified90.4%

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

    if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{x - y}{\color{blue}{z - y}} \cdot t \]
      3. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
      14. lower-/.f6475.5

        \[\leadsto \frac{y - x}{\color{blue}{\frac{y - z}{t}}} \]
    6. Applied egg-rr75.5%

      \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{t \cdot y}{y - z}} \]
    8. Step-by-step derivation
      1. associate-/l*N/A

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

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

        \[\leadsto t \cdot \color{blue}{\frac{y}{y - z}} \]
      4. lower--.f6499.7

        \[\leadsto t \cdot \frac{y}{\color{blue}{y - z}} \]
    9. Simplified99.7%

      \[\leadsto \color{blue}{t \cdot \frac{y}{y - z}} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification94.2%

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

Alternative 6: 80.1% accurate, 0.3× speedup?

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

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

\mathbf{elif}\;t\_1 \leq 2:\\
\;\;\;\;t \cdot \frac{y}{y - z}\\

\mathbf{else}:\\
\;\;\;\;t \cdot \frac{x}{z}\\


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

    1. Initial program 95.3%

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

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

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

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

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

        \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{t}{z} \]
      5. lower-/.f6481.5

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

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

    if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{x - y}{\color{blue}{z - y}} \cdot t \]
      3. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
      14. lower-/.f6475.5

        \[\leadsto \frac{y - x}{\color{blue}{\frac{y - z}{t}}} \]
    6. Applied egg-rr75.5%

      \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{t \cdot y}{y - z}} \]
    8. Step-by-step derivation
      1. associate-/l*N/A

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

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

        \[\leadsto t \cdot \color{blue}{\frac{y}{y - z}} \]
      4. lower--.f6499.7

        \[\leadsto t \cdot \frac{y}{\color{blue}{y - z}} \]
    9. Simplified99.7%

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

    if 2 < (/.f64 (-.f64 x y) (-.f64 z y))

    1. Initial program 95.0%

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

      \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
    4. Step-by-step derivation
      1. lower-/.f6462.9

        \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
    5. Simplified62.9%

      \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
  3. Recombined 3 regimes into one program.
  4. Final simplification84.4%

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

Alternative 7: 70.8% accurate, 0.4× speedup?

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

\\
\begin{array}{l}
t_1 := \frac{x - y}{z - y}\\
t_2 := t \cdot \frac{x}{z}\\
\mathbf{if}\;t\_1 \leq 0.4:\\
\;\;\;\;t\_2\\

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

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


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 (-.f64 x y) (-.f64 z y)) < 0.40000000000000002 or 2 < (/.f64 (-.f64 x y) (-.f64 z y))

    1. Initial program 95.2%

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

      \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
    4. Step-by-step derivation
      1. lower-/.f6462.3

        \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
    5. Simplified62.3%

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

    if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{x - y}{\color{blue}{z - y}} \cdot t \]
      3. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
      14. lower-/.f6475.5

        \[\leadsto \frac{y - x}{\color{blue}{\frac{y - z}{t}}} \]
    6. Applied egg-rr75.5%

      \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{t \cdot y}{y - z}} \]
    8. Step-by-step derivation
      1. associate-/l*N/A

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

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

        \[\leadsto t \cdot \color{blue}{\frac{y}{y - z}} \]
      4. lower--.f6499.7

        \[\leadsto t \cdot \frac{y}{\color{blue}{y - z}} \]
    9. Simplified99.7%

      \[\leadsto \color{blue}{t \cdot \frac{y}{y - z}} \]
    10. Taylor expanded in y around inf

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

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

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

        \[\leadsto \color{blue}{\mathsf{fma}\left(t, \frac{z}{y}, t\right)} \]
      4. lower-/.f6499.3

        \[\leadsto \mathsf{fma}\left(t, \color{blue}{\frac{z}{y}}, t\right) \]
    12. Simplified99.3%

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

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

Alternative 8: 70.5% accurate, 0.4× speedup?

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

\\
\begin{array}{l}
t_1 := \frac{x - y}{z - y}\\
t_2 := t \cdot \frac{x}{z}\\
\mathbf{if}\;t\_1 \leq 0.4:\\
\;\;\;\;t\_2\\

\mathbf{elif}\;t\_1 \leq 2:\\
\;\;\;\;t\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 (-.f64 x y) (-.f64 z y)) < 0.40000000000000002 or 2 < (/.f64 (-.f64 x y) (-.f64 z y))

    1. Initial program 95.2%

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

      \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
    4. Step-by-step derivation
      1. lower-/.f6462.3

        \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
    5. Simplified62.3%

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

    if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

    1. Initial program 100.0%

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

      \[\leadsto \color{blue}{1} \cdot t \]
    4. Step-by-step derivation
      1. Simplified98.4%

        \[\leadsto \color{blue}{1} \cdot t \]
      2. Step-by-step derivation
        1. *-lft-identity98.4

          \[\leadsto \color{blue}{t} \]
      3. Applied egg-rr98.4%

        \[\leadsto \color{blue}{t} \]
    5. Recombined 2 regimes into one program.
    6. Final simplification73.7%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x - y}{z - y} \leq 0.4:\\ \;\;\;\;t \cdot \frac{x}{z}\\ \mathbf{elif}\;\frac{x - y}{z - y} \leq 2:\\ \;\;\;\;t\\ \mathbf{else}:\\ \;\;\;\;t \cdot \frac{x}{z}\\ \end{array} \]
    7. Add Preprocessing

    Alternative 9: 68.8% accurate, 0.4× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{x - y}{z - y}\\ t_2 := x \cdot \frac{t}{z}\\ \mathbf{if}\;t\_1 \leq 0.4:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 2:\\ \;\;\;\;t\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \end{array} \]
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (/ (- x y) (- z y))) (t_2 (* x (/ t z))))
       (if (<= t_1 0.4) t_2 (if (<= t_1 2.0) t t_2))))
    double code(double x, double y, double z, double t) {
    	double t_1 = (x - y) / (z - y);
    	double t_2 = x * (t / z);
    	double tmp;
    	if (t_1 <= 0.4) {
    		tmp = t_2;
    	} else if (t_1 <= 2.0) {
    		tmp = t;
    	} else {
    		tmp = t_2;
    	}
    	return tmp;
    }
    
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: t_2
        real(8) :: tmp
        t_1 = (x - y) / (z - y)
        t_2 = x * (t / z)
        if (t_1 <= 0.4d0) then
            tmp = t_2
        else if (t_1 <= 2.0d0) then
            tmp = t
        else
            tmp = t_2
        end if
        code = tmp
    end function
    
    public static double code(double x, double y, double z, double t) {
    	double t_1 = (x - y) / (z - y);
    	double t_2 = x * (t / z);
    	double tmp;
    	if (t_1 <= 0.4) {
    		tmp = t_2;
    	} else if (t_1 <= 2.0) {
    		tmp = t;
    	} else {
    		tmp = t_2;
    	}
    	return tmp;
    }
    
    def code(x, y, z, t):
    	t_1 = (x - y) / (z - y)
    	t_2 = x * (t / z)
    	tmp = 0
    	if t_1 <= 0.4:
    		tmp = t_2
    	elif t_1 <= 2.0:
    		tmp = t
    	else:
    		tmp = t_2
    	return tmp
    
    function code(x, y, z, t)
    	t_1 = Float64(Float64(x - y) / Float64(z - y))
    	t_2 = Float64(x * Float64(t / z))
    	tmp = 0.0
    	if (t_1 <= 0.4)
    		tmp = t_2;
    	elseif (t_1 <= 2.0)
    		tmp = t;
    	else
    		tmp = t_2;
    	end
    	return tmp
    end
    
    function tmp_2 = code(x, y, z, t)
    	t_1 = (x - y) / (z - y);
    	t_2 = x * (t / z);
    	tmp = 0.0;
    	if (t_1 <= 0.4)
    		tmp = t_2;
    	elseif (t_1 <= 2.0)
    		tmp = t;
    	else
    		tmp = t_2;
    	end
    	tmp_2 = tmp;
    end
    
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[(x - y), $MachinePrecision] / N[(z - y), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(x * N[(t / z), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, 0.4], t$95$2, If[LessEqual[t$95$1, 2.0], t, t$95$2]]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := \frac{x - y}{z - y}\\
    t_2 := x \cdot \frac{t}{z}\\
    \mathbf{if}\;t\_1 \leq 0.4:\\
    \;\;\;\;t\_2\\
    
    \mathbf{elif}\;t\_1 \leq 2:\\
    \;\;\;\;t\\
    
    \mathbf{else}:\\
    \;\;\;\;t\_2\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 (-.f64 x y) (-.f64 z y)) < 0.40000000000000002 or 2 < (/.f64 (-.f64 x y) (-.f64 z y))

      1. Initial program 95.2%

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

        \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
      4. Step-by-step derivation
        1. lower-/.f6462.3

          \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
      5. Simplified62.3%

        \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
      6. Step-by-step derivation
        1. associate-*l/N/A

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

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

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

          \[\leadsto \color{blue}{\frac{t}{z} \cdot x} \]
        5. lower-/.f6460.1

          \[\leadsto \color{blue}{\frac{t}{z}} \cdot x \]
      7. Applied egg-rr60.1%

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

      if 0.40000000000000002 < (/.f64 (-.f64 x y) (-.f64 z y)) < 2

      1. Initial program 100.0%

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

        \[\leadsto \color{blue}{1} \cdot t \]
      4. Step-by-step derivation
        1. Simplified98.4%

          \[\leadsto \color{blue}{1} \cdot t \]
        2. Step-by-step derivation
          1. *-lft-identity98.4

            \[\leadsto \color{blue}{t} \]
        3. Applied egg-rr98.4%

          \[\leadsto \color{blue}{t} \]
      5. Recombined 2 regimes into one program.
      6. Final simplification72.2%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x - y}{z - y} \leq 0.4:\\ \;\;\;\;x \cdot \frac{t}{z}\\ \mathbf{elif}\;\frac{x - y}{z - y} \leq 2:\\ \;\;\;\;t\\ \mathbf{else}:\\ \;\;\;\;x \cdot \frac{t}{z}\\ \end{array} \]
      7. Add Preprocessing

      Alternative 10: 69.8% accurate, 0.7× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_1 := t \cdot \frac{y}{y - z}\\ \mathbf{if}\;y \leq -1.65 \cdot 10^{-59}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;y \leq 3.1 \cdot 10^{-97}:\\ \;\;\;\;t \cdot \frac{x}{z}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
      (FPCore (x y z t)
       :precision binary64
       (let* ((t_1 (* t (/ y (- y z)))))
         (if (<= y -1.65e-59) t_1 (if (<= y 3.1e-97) (* t (/ x z)) t_1))))
      double code(double x, double y, double z, double t) {
      	double t_1 = t * (y / (y - z));
      	double tmp;
      	if (y <= -1.65e-59) {
      		tmp = t_1;
      	} else if (y <= 3.1e-97) {
      		tmp = t * (x / z);
      	} else {
      		tmp = t_1;
      	}
      	return tmp;
      }
      
      real(8) function code(x, y, z, t)
          real(8), intent (in) :: x
          real(8), intent (in) :: y
          real(8), intent (in) :: z
          real(8), intent (in) :: t
          real(8) :: t_1
          real(8) :: tmp
          t_1 = t * (y / (y - z))
          if (y <= (-1.65d-59)) then
              tmp = t_1
          else if (y <= 3.1d-97) then
              tmp = t * (x / z)
          else
              tmp = t_1
          end if
          code = tmp
      end function
      
      public static double code(double x, double y, double z, double t) {
      	double t_1 = t * (y / (y - z));
      	double tmp;
      	if (y <= -1.65e-59) {
      		tmp = t_1;
      	} else if (y <= 3.1e-97) {
      		tmp = t * (x / z);
      	} else {
      		tmp = t_1;
      	}
      	return tmp;
      }
      
      def code(x, y, z, t):
      	t_1 = t * (y / (y - z))
      	tmp = 0
      	if y <= -1.65e-59:
      		tmp = t_1
      	elif y <= 3.1e-97:
      		tmp = t * (x / z)
      	else:
      		tmp = t_1
      	return tmp
      
      function code(x, y, z, t)
      	t_1 = Float64(t * Float64(y / Float64(y - z)))
      	tmp = 0.0
      	if (y <= -1.65e-59)
      		tmp = t_1;
      	elseif (y <= 3.1e-97)
      		tmp = Float64(t * Float64(x / z));
      	else
      		tmp = t_1;
      	end
      	return tmp
      end
      
      function tmp_2 = code(x, y, z, t)
      	t_1 = t * (y / (y - z));
      	tmp = 0.0;
      	if (y <= -1.65e-59)
      		tmp = t_1;
      	elseif (y <= 3.1e-97)
      		tmp = t * (x / z);
      	else
      		tmp = t_1;
      	end
      	tmp_2 = tmp;
      end
      
      code[x_, y_, z_, t_] := Block[{t$95$1 = N[(t * N[(y / N[(y - z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[y, -1.65e-59], t$95$1, If[LessEqual[y, 3.1e-97], N[(t * N[(x / z), $MachinePrecision]), $MachinePrecision], t$95$1]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_1 := t \cdot \frac{y}{y - z}\\
      \mathbf{if}\;y \leq -1.65 \cdot 10^{-59}:\\
      \;\;\;\;t\_1\\
      
      \mathbf{elif}\;y \leq 3.1 \cdot 10^{-97}:\\
      \;\;\;\;t \cdot \frac{x}{z}\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_1\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if y < -1.64999999999999991e-59 or 3.10000000000000002e-97 < y

        1. Initial program 99.2%

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

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

            \[\leadsto \frac{x - y}{\color{blue}{z - y}} \cdot t \]
          3. frac-2negN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \left(y - x\right) \cdot \left(\frac{1}{\color{blue}{y} - z} \cdot t\right) \]
          24. lower--.f6479.0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
          14. lower-/.f6478.3

            \[\leadsto \frac{y - x}{\color{blue}{\frac{y - z}{t}}} \]
        6. Applied egg-rr78.3%

          \[\leadsto \color{blue}{\frac{y - x}{\frac{y - z}{t}}} \]
        7. Taylor expanded in x around 0

          \[\leadsto \color{blue}{\frac{t \cdot y}{y - z}} \]
        8. Step-by-step derivation
          1. associate-/l*N/A

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

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

            \[\leadsto t \cdot \color{blue}{\frac{y}{y - z}} \]
          4. lower--.f6476.7

            \[\leadsto t \cdot \frac{y}{\color{blue}{y - z}} \]
        9. Simplified76.7%

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

        if -1.64999999999999991e-59 < y < 3.10000000000000002e-97

        1. Initial program 93.6%

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

          \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
        4. Step-by-step derivation
          1. lower-/.f6473.3

            \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
        5. Simplified73.3%

          \[\leadsto \color{blue}{\frac{x}{z}} \cdot t \]
      3. Recombined 2 regimes into one program.
      4. Final simplification75.2%

        \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -1.65 \cdot 10^{-59}:\\ \;\;\;\;t \cdot \frac{y}{y - z}\\ \mathbf{elif}\;y \leq 3.1 \cdot 10^{-97}:\\ \;\;\;\;t \cdot \frac{x}{z}\\ \mathbf{else}:\\ \;\;\;\;t \cdot \frac{y}{y - z}\\ \end{array} \]
      5. Add Preprocessing

      Alternative 11: 35.2% accurate, 23.0× speedup?

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

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

        \[\leadsto \color{blue}{1} \cdot t \]
      4. Step-by-step derivation
        1. Simplified34.0%

          \[\leadsto \color{blue}{1} \cdot t \]
        2. Step-by-step derivation
          1. *-lft-identity34.0

            \[\leadsto \color{blue}{t} \]
        3. Applied egg-rr34.0%

          \[\leadsto \color{blue}{t} \]
        4. Add Preprocessing

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

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

        Reproduce

        ?
        herbie shell --seed 2024212 
        (FPCore (x y z t)
          :name "Numeric.Signal.Multichannel:$cput from hsignal-0.2.7.1"
          :precision binary64
        
          :alt
          (! :herbie-platform default (/ t (/ (- z y) (- x y))))
        
          (* (/ (- x y) (- z y)) t))