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

Percentage Accurate: 98.1% → 96.9%
Time: 3.4s
Alternatives: 15
Speedup: N/A×

Specification

?
\[x + y \cdot \frac{z - t}{a - t} \]
(FPCore (x y z t a)
  :precision binary64
  :pre TRUE
  (+ x (* y (/ (- z t) (- a t)))))
double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (a - t)));
}
real(8) function code(x, y, z, t, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    code = x + (y * ((z - t) / (a - t)))
end function
public static double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (a - t)));
}
def code(x, y, z, t, a):
	return x + (y * ((z - t) / (a - t)))
function code(x, y, z, t, a)
	return Float64(x + Float64(y * Float64(Float64(z - t) / Float64(a - t))))
end
function tmp = code(x, y, z, t, a)
	tmp = x + (y * ((z - t) / (a - t)));
end
code[x_, y_, z_, t_, a_] := N[(x + N[(y * N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
f(x, y, z, t, a):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a: real): real =
	x + (y * ((z - t) / (a - t)))
END code
x + y \cdot \frac{z - t}{a - t}

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 15 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: 98.1% accurate, 1.0× speedup?

\[x + y \cdot \frac{z - t}{a - t} \]
(FPCore (x y z t a)
  :precision binary64
  :pre TRUE
  (+ x (* y (/ (- z t) (- a t)))))
double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (a - t)));
}
real(8) function code(x, y, z, t, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    code = x + (y * ((z - t) / (a - t)))
end function
public static double code(double x, double y, double z, double t, double a) {
	return x + (y * ((z - t) / (a - t)));
}
def code(x, y, z, t, a):
	return x + (y * ((z - t) / (a - t)))
function code(x, y, z, t, a)
	return Float64(x + Float64(y * Float64(Float64(z - t) / Float64(a - t))))
end
function tmp = code(x, y, z, t, a)
	tmp = x + (y * ((z - t) / (a - t)));
end
code[x_, y_, z_, t_, a_] := N[(x + N[(y * N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
f(x, y, z, t, a):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a: real): real =
	x + (y * ((z - t) / (a - t)))
END code
x + y \cdot \frac{z - t}{a - t}

Alternative 1: 96.9% accurate, 1.0× speedup?

\[\mathsf{fma}\left(t - z, \frac{y}{t - a}, x\right) \]
(FPCore (x y z t a)
  :precision binary64
  :pre TRUE
  (fma (- t z) (/ y (- t a)) x))
double code(double x, double y, double z, double t, double a) {
	return fma((t - z), (y / (t - a)), x);
}
function code(x, y, z, t, a)
	return fma(Float64(t - z), Float64(y / Float64(t - a)), x)
end
code[x_, y_, z_, t_, a_] := N[(N[(t - z), $MachinePrecision] * N[(y / N[(t - a), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]
f(x, y, z, t, a):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a: real): real =
	((t - z) * (y / (t - a))) + x
END code
\mathsf{fma}\left(t - z, \frac{y}{t - a}, x\right)
Derivation
  1. Initial program 98.1%

    \[x + y \cdot \frac{z - t}{a - t} \]
  2. Step-by-step derivation
    1. Applied rewrites95.8%

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

    Alternative 2: 96.9% accurate, 0.3× speedup?

    \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ \mathbf{if}\;t\_1 \leq -50:\\ \;\;\;\;x + \frac{y \cdot z}{a - t}\\ \mathbf{elif}\;t\_1 \leq 10^{-7}:\\ \;\;\;\;\mathsf{fma}\left(z - t, \frac{y}{a}, x\right)\\ \mathbf{elif}\;t\_1 \leq 1.02:\\ \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z - a}{t}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\ \end{array} \]
    (FPCore (x y z t a)
      :precision binary64
      :pre TRUE
      (let* ((t_1 (/ (- z t) (- a t))))
      (if (<= t_1 -50.0)
        (+ x (/ (* y z) (- a t)))
        (if (<= t_1 1e-7)
          (fma (- z t) (/ y a) x)
          (if (<= t_1 1.02)
            (fma y (- 1.0 (/ (- z a) t)) x)
            (fma y (/ z (- a t)) x))))))
    double code(double x, double y, double z, double t, double a) {
    	double t_1 = (z - t) / (a - t);
    	double tmp;
    	if (t_1 <= -50.0) {
    		tmp = x + ((y * z) / (a - t));
    	} else if (t_1 <= 1e-7) {
    		tmp = fma((z - t), (y / a), x);
    	} else if (t_1 <= 1.02) {
    		tmp = fma(y, (1.0 - ((z - a) / t)), x);
    	} else {
    		tmp = fma(y, (z / (a - t)), x);
    	}
    	return tmp;
    }
    
    function code(x, y, z, t, a)
    	t_1 = Float64(Float64(z - t) / Float64(a - t))
    	tmp = 0.0
    	if (t_1 <= -50.0)
    		tmp = Float64(x + Float64(Float64(y * z) / Float64(a - t)));
    	elseif (t_1 <= 1e-7)
    		tmp = fma(Float64(z - t), Float64(y / a), x);
    	elseif (t_1 <= 1.02)
    		tmp = fma(y, Float64(1.0 - Float64(Float64(z - a) / t)), x);
    	else
    		tmp = fma(y, Float64(z / Float64(a - t)), x);
    	end
    	return tmp
    end
    
    code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -50.0], N[(x + N[(N[(y * z), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 1e-7], N[(N[(z - t), $MachinePrecision] * N[(y / a), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[t$95$1, 1.02], N[(y * N[(1.0 - N[(N[(z - a), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], N[(y * N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]]]]]
    
    f(x, y, z, t, a):
    	x in [-inf, +inf],
    	y in [-inf, +inf],
    	z in [-inf, +inf],
    	t in [-inf, +inf],
    	a in [-inf, +inf]
    code: THEORY
    BEGIN
    f(x, y, z, t, a: real): real =
    	LET t_1 = ((z - t) / (a - t)) IN
    		LET tmp_2 = IF (t_1 <= (1020000000000000017763568394002504646778106689453125e-51)) THEN ((y * ((1) - ((z - a) / t))) + x) ELSE ((y * (z / (a - t))) + x) ENDIF IN
    		LET tmp_1 = IF (t_1 <= (999999999999999954748111825886258685613938723690807819366455078125e-73)) THEN (((z - t) * (y / a)) + x) ELSE tmp_2 ENDIF IN
    		LET tmp = IF (t_1 <= (-50)) THEN (x + ((y * z) / (a - t))) ELSE tmp_1 ENDIF IN
    	tmp
    END code
    \begin{array}{l}
    t_1 := \frac{z - t}{a - t}\\
    \mathbf{if}\;t\_1 \leq -50:\\
    \;\;\;\;x + \frac{y \cdot z}{a - t}\\
    
    \mathbf{elif}\;t\_1 \leq 10^{-7}:\\
    \;\;\;\;\mathsf{fma}\left(z - t, \frac{y}{a}, x\right)\\
    
    \mathbf{elif}\;t\_1 \leq 1.02:\\
    \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z - a}{t}, x\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\
    
    
    \end{array}
    
    Derivation
    1. Split input into 4 regimes
    2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -50

      1. Initial program 98.1%

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

        \[\leadsto x + \frac{y \cdot z}{a - t} \]
      3. Step-by-step derivation
        1. Applied rewrites73.9%

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

        if -50 < (/.f64 (-.f64 z t) (-.f64 a t)) < 9.9999999999999995e-8

        1. Initial program 98.1%

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

          \[\leadsto x + y \cdot \frac{z - t}{a} \]
        3. Step-by-step derivation
          1. Applied rewrites60.1%

            \[\leadsto x + y \cdot \frac{z - t}{a} \]
          2. Step-by-step derivation
            1. Applied rewrites61.1%

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

            if 9.9999999999999995e-8 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.02

            1. Initial program 98.1%

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

              \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
            3. Step-by-step derivation
              1. Applied rewrites60.8%

                \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
              2. Step-by-step derivation
                1. Applied rewrites60.8%

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

                if 1.02 < (/.f64 (-.f64 z t) (-.f64 a t))

                1. Initial program 98.1%

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

                  \[\leadsto x + y \cdot \frac{z}{a - t} \]
                3. Step-by-step derivation
                  1. Applied rewrites76.8%

                    \[\leadsto x + y \cdot \frac{z}{a - t} \]
                  2. Step-by-step derivation
                    1. Applied rewrites76.8%

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

                  Alternative 3: 96.3% accurate, 0.3× speedup?

                  \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ \mathbf{if}\;t\_1 \leq -50:\\ \;\;\;\;x + \frac{y \cdot z}{a - t}\\ \mathbf{elif}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(z - t, \frac{y}{a}, x\right)\\ \mathbf{elif}\;t\_1 \leq 1.02:\\ \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{t}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\ \end{array} \]
                  (FPCore (x y z t a)
                    :precision binary64
                    :pre TRUE
                    (let* ((t_1 (/ (- z t) (- a t))))
                    (if (<= t_1 -50.0)
                      (+ x (/ (* y z) (- a t)))
                      (if (<= t_1 1e-9)
                        (fma (- z t) (/ y a) x)
                        (if (<= t_1 1.02)
                          (fma y (- 1.0 (/ z t)) x)
                          (fma y (/ z (- a t)) x))))))
                  double code(double x, double y, double z, double t, double a) {
                  	double t_1 = (z - t) / (a - t);
                  	double tmp;
                  	if (t_1 <= -50.0) {
                  		tmp = x + ((y * z) / (a - t));
                  	} else if (t_1 <= 1e-9) {
                  		tmp = fma((z - t), (y / a), x);
                  	} else if (t_1 <= 1.02) {
                  		tmp = fma(y, (1.0 - (z / t)), x);
                  	} else {
                  		tmp = fma(y, (z / (a - t)), x);
                  	}
                  	return tmp;
                  }
                  
                  function code(x, y, z, t, a)
                  	t_1 = Float64(Float64(z - t) / Float64(a - t))
                  	tmp = 0.0
                  	if (t_1 <= -50.0)
                  		tmp = Float64(x + Float64(Float64(y * z) / Float64(a - t)));
                  	elseif (t_1 <= 1e-9)
                  		tmp = fma(Float64(z - t), Float64(y / a), x);
                  	elseif (t_1 <= 1.02)
                  		tmp = fma(y, Float64(1.0 - Float64(z / t)), x);
                  	else
                  		tmp = fma(y, Float64(z / Float64(a - t)), x);
                  	end
                  	return tmp
                  end
                  
                  code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -50.0], N[(x + N[(N[(y * z), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 1e-9], N[(N[(z - t), $MachinePrecision] * N[(y / a), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[t$95$1, 1.02], N[(y * N[(1.0 - N[(z / t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], N[(y * N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]]]]]
                  
                  f(x, y, z, t, a):
                  	x in [-inf, +inf],
                  	y in [-inf, +inf],
                  	z in [-inf, +inf],
                  	t in [-inf, +inf],
                  	a in [-inf, +inf]
                  code: THEORY
                  BEGIN
                  f(x, y, z, t, a: real): real =
                  	LET t_1 = ((z - t) / (a - t)) IN
                  		LET tmp_2 = IF (t_1 <= (1020000000000000017763568394002504646778106689453125e-51)) THEN ((y * ((1) - (z / t))) + x) ELSE ((y * (z / (a - t))) + x) ENDIF IN
                  		LET tmp_1 = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN (((z - t) * (y / a)) + x) ELSE tmp_2 ENDIF IN
                  		LET tmp = IF (t_1 <= (-50)) THEN (x + ((y * z) / (a - t))) ELSE tmp_1 ENDIF IN
                  	tmp
                  END code
                  \begin{array}{l}
                  t_1 := \frac{z - t}{a - t}\\
                  \mathbf{if}\;t\_1 \leq -50:\\
                  \;\;\;\;x + \frac{y \cdot z}{a - t}\\
                  
                  \mathbf{elif}\;t\_1 \leq 10^{-9}:\\
                  \;\;\;\;\mathsf{fma}\left(z - t, \frac{y}{a}, x\right)\\
                  
                  \mathbf{elif}\;t\_1 \leq 1.02:\\
                  \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{t}, x\right)\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\
                  
                  
                  \end{array}
                  
                  Derivation
                  1. Split input into 4 regimes
                  2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -50

                    1. Initial program 98.1%

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

                      \[\leadsto x + \frac{y \cdot z}{a - t} \]
                    3. Step-by-step derivation
                      1. Applied rewrites73.9%

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

                      if -50 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9

                      1. Initial program 98.1%

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

                        \[\leadsto x + y \cdot \frac{z - t}{a} \]
                      3. Step-by-step derivation
                        1. Applied rewrites60.1%

                          \[\leadsto x + y \cdot \frac{z - t}{a} \]
                        2. Step-by-step derivation
                          1. Applied rewrites61.1%

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

                          if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.02

                          1. Initial program 98.1%

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

                            \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
                          3. Step-by-step derivation
                            1. Applied rewrites60.8%

                              \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
                            2. Step-by-step derivation
                              1. Applied rewrites60.8%

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

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

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

                                if 1.02 < (/.f64 (-.f64 z t) (-.f64 a t))

                                1. Initial program 98.1%

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

                                  \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                3. Step-by-step derivation
                                  1. Applied rewrites76.8%

                                    \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                  2. Step-by-step derivation
                                    1. Applied rewrites76.8%

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

                                  Alternative 4: 96.1% accurate, 0.3× speedup?

                                  \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\ \mathbf{if}\;t\_1 \leq -50:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(z - t, \frac{y}{a}, x\right)\\ \mathbf{elif}\;t\_1 \leq 1.02:\\ \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{t}, x\right)\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
                                  (FPCore (x y z t a)
                                    :precision binary64
                                    :pre TRUE
                                    (let* ((t_1 (/ (- z t) (- a t))) (t_2 (fma y (/ z (- a t)) x)))
                                    (if (<= t_1 -50.0)
                                      t_2
                                      (if (<= t_1 1e-9)
                                        (fma (- z t) (/ y a) x)
                                        (if (<= t_1 1.02) (fma y (- 1.0 (/ z t)) x) t_2)))))
                                  double code(double x, double y, double z, double t, double a) {
                                  	double t_1 = (z - t) / (a - t);
                                  	double t_2 = fma(y, (z / (a - t)), x);
                                  	double tmp;
                                  	if (t_1 <= -50.0) {
                                  		tmp = t_2;
                                  	} else if (t_1 <= 1e-9) {
                                  		tmp = fma((z - t), (y / a), x);
                                  	} else if (t_1 <= 1.02) {
                                  		tmp = fma(y, (1.0 - (z / t)), x);
                                  	} else {
                                  		tmp = t_2;
                                  	}
                                  	return tmp;
                                  }
                                  
                                  function code(x, y, z, t, a)
                                  	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                  	t_2 = fma(y, Float64(z / Float64(a - t)), x)
                                  	tmp = 0.0
                                  	if (t_1 <= -50.0)
                                  		tmp = t_2;
                                  	elseif (t_1 <= 1e-9)
                                  		tmp = fma(Float64(z - t), Float64(y / a), x);
                                  	elseif (t_1 <= 1.02)
                                  		tmp = fma(y, Float64(1.0 - Float64(z / t)), x);
                                  	else
                                  		tmp = t_2;
                                  	end
                                  	return tmp
                                  end
                                  
                                  code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(y * N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, -50.0], t$95$2, If[LessEqual[t$95$1, 1e-9], N[(N[(z - t), $MachinePrecision] * N[(y / a), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[t$95$1, 1.02], N[(y * N[(1.0 - N[(z / t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], t$95$2]]]]]
                                  
                                  f(x, y, z, t, a):
                                  	x in [-inf, +inf],
                                  	y in [-inf, +inf],
                                  	z in [-inf, +inf],
                                  	t in [-inf, +inf],
                                  	a in [-inf, +inf]
                                  code: THEORY
                                  BEGIN
                                  f(x, y, z, t, a: real): real =
                                  	LET t_1 = ((z - t) / (a - t)) IN
                                  		LET t_2 = ((y * (z / (a - t))) + x) IN
                                  			LET tmp_2 = IF (t_1 <= (1020000000000000017763568394002504646778106689453125e-51)) THEN ((y * ((1) - (z / t))) + x) ELSE t_2 ENDIF IN
                                  			LET tmp_1 = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN (((z - t) * (y / a)) + x) ELSE tmp_2 ENDIF IN
                                  			LET tmp = IF (t_1 <= (-50)) THEN t_2 ELSE tmp_1 ENDIF IN
                                  	tmp
                                  END code
                                  \begin{array}{l}
                                  t_1 := \frac{z - t}{a - t}\\
                                  t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\
                                  \mathbf{if}\;t\_1 \leq -50:\\
                                  \;\;\;\;t\_2\\
                                  
                                  \mathbf{elif}\;t\_1 \leq 10^{-9}:\\
                                  \;\;\;\;\mathsf{fma}\left(z - t, \frac{y}{a}, x\right)\\
                                  
                                  \mathbf{elif}\;t\_1 \leq 1.02:\\
                                  \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{t}, x\right)\\
                                  
                                  \mathbf{else}:\\
                                  \;\;\;\;t\_2\\
                                  
                                  
                                  \end{array}
                                  
                                  Derivation
                                  1. Split input into 3 regimes
                                  2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -50 or 1.02 < (/.f64 (-.f64 z t) (-.f64 a t))

                                    1. Initial program 98.1%

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

                                      \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                    3. Step-by-step derivation
                                      1. Applied rewrites76.8%

                                        \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                      2. Step-by-step derivation
                                        1. Applied rewrites76.8%

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

                                        if -50 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9

                                        1. Initial program 98.1%

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

                                          \[\leadsto x + y \cdot \frac{z - t}{a} \]
                                        3. Step-by-step derivation
                                          1. Applied rewrites60.1%

                                            \[\leadsto x + y \cdot \frac{z - t}{a} \]
                                          2. Step-by-step derivation
                                            1. Applied rewrites61.1%

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

                                            if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.02

                                            1. Initial program 98.1%

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

                                              \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
                                            3. Step-by-step derivation
                                              1. Applied rewrites60.8%

                                                \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
                                              2. Step-by-step derivation
                                                1. Applied rewrites60.8%

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

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

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

                                                Alternative 5: 95.9% accurate, 0.3× speedup?

                                                \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\ \mathbf{if}\;t\_1 \leq -50:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{z - t}{a}, x\right)\\ \mathbf{elif}\;t\_1 \leq 1.02:\\ \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{t}, x\right)\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
                                                (FPCore (x y z t a)
                                                  :precision binary64
                                                  :pre TRUE
                                                  (let* ((t_1 (/ (- z t) (- a t))) (t_2 (fma y (/ z (- a t)) x)))
                                                  (if (<= t_1 -50.0)
                                                    t_2
                                                    (if (<= t_1 1e-9)
                                                      (fma y (/ (- z t) a) x)
                                                      (if (<= t_1 1.02) (fma y (- 1.0 (/ z t)) x) t_2)))))
                                                double code(double x, double y, double z, double t, double a) {
                                                	double t_1 = (z - t) / (a - t);
                                                	double t_2 = fma(y, (z / (a - t)), x);
                                                	double tmp;
                                                	if (t_1 <= -50.0) {
                                                		tmp = t_2;
                                                	} else if (t_1 <= 1e-9) {
                                                		tmp = fma(y, ((z - t) / a), x);
                                                	} else if (t_1 <= 1.02) {
                                                		tmp = fma(y, (1.0 - (z / t)), x);
                                                	} else {
                                                		tmp = t_2;
                                                	}
                                                	return tmp;
                                                }
                                                
                                                function code(x, y, z, t, a)
                                                	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                	t_2 = fma(y, Float64(z / Float64(a - t)), x)
                                                	tmp = 0.0
                                                	if (t_1 <= -50.0)
                                                		tmp = t_2;
                                                	elseif (t_1 <= 1e-9)
                                                		tmp = fma(y, Float64(Float64(z - t) / a), x);
                                                	elseif (t_1 <= 1.02)
                                                		tmp = fma(y, Float64(1.0 - Float64(z / t)), x);
                                                	else
                                                		tmp = t_2;
                                                	end
                                                	return tmp
                                                end
                                                
                                                code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(y * N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, -50.0], t$95$2, If[LessEqual[t$95$1, 1e-9], N[(y * N[(N[(z - t), $MachinePrecision] / a), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[t$95$1, 1.02], N[(y * N[(1.0 - N[(z / t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], t$95$2]]]]]
                                                
                                                f(x, y, z, t, a):
                                                	x in [-inf, +inf],
                                                	y in [-inf, +inf],
                                                	z in [-inf, +inf],
                                                	t in [-inf, +inf],
                                                	a in [-inf, +inf]
                                                code: THEORY
                                                BEGIN
                                                f(x, y, z, t, a: real): real =
                                                	LET t_1 = ((z - t) / (a - t)) IN
                                                		LET t_2 = ((y * (z / (a - t))) + x) IN
                                                			LET tmp_2 = IF (t_1 <= (1020000000000000017763568394002504646778106689453125e-51)) THEN ((y * ((1) - (z / t))) + x) ELSE t_2 ENDIF IN
                                                			LET tmp_1 = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN ((y * ((z - t) / a)) + x) ELSE tmp_2 ENDIF IN
                                                			LET tmp = IF (t_1 <= (-50)) THEN t_2 ELSE tmp_1 ENDIF IN
                                                	tmp
                                                END code
                                                \begin{array}{l}
                                                t_1 := \frac{z - t}{a - t}\\
                                                t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\
                                                \mathbf{if}\;t\_1 \leq -50:\\
                                                \;\;\;\;t\_2\\
                                                
                                                \mathbf{elif}\;t\_1 \leq 10^{-9}:\\
                                                \;\;\;\;\mathsf{fma}\left(y, \frac{z - t}{a}, x\right)\\
                                                
                                                \mathbf{elif}\;t\_1 \leq 1.02:\\
                                                \;\;\;\;\mathsf{fma}\left(y, 1 - \frac{z}{t}, x\right)\\
                                                
                                                \mathbf{else}:\\
                                                \;\;\;\;t\_2\\
                                                
                                                
                                                \end{array}
                                                
                                                Derivation
                                                1. Split input into 3 regimes
                                                2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -50 or 1.02 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                  1. Initial program 98.1%

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

                                                    \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                                  3. Step-by-step derivation
                                                    1. Applied rewrites76.8%

                                                      \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                                    2. Step-by-step derivation
                                                      1. Applied rewrites76.8%

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

                                                      if -50 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9

                                                      1. Initial program 98.1%

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

                                                        \[\leadsto x + y \cdot \frac{z - t}{a} \]
                                                      3. Step-by-step derivation
                                                        1. Applied rewrites60.1%

                                                          \[\leadsto x + y \cdot \frac{z - t}{a} \]
                                                        2. Step-by-step derivation
                                                          1. Applied rewrites60.1%

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

                                                          if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.02

                                                          1. Initial program 98.1%

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

                                                            \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
                                                          3. Step-by-step derivation
                                                            1. Applied rewrites60.8%

                                                              \[\leadsto x + y \cdot \left(1 + -1 \cdot \frac{z - a}{t}\right) \]
                                                            2. Step-by-step derivation
                                                              1. Applied rewrites60.8%

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

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

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

                                                              Alternative 6: 95.8% accurate, 0.3× speedup?

                                                              \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\ \mathbf{if}\;t\_1 \leq -50:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{z - t}{a}, x\right)\\ \mathbf{elif}\;t\_1 \leq 1.02:\\ \;\;\;\;x + y\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
                                                              (FPCore (x y z t a)
                                                                :precision binary64
                                                                :pre TRUE
                                                                (let* ((t_1 (/ (- z t) (- a t))) (t_2 (fma y (/ z (- a t)) x)))
                                                                (if (<= t_1 -50.0)
                                                                  t_2
                                                                  (if (<= t_1 1e-9)
                                                                    (fma y (/ (- z t) a) x)
                                                                    (if (<= t_1 1.02) (+ x y) t_2)))))
                                                              double code(double x, double y, double z, double t, double a) {
                                                              	double t_1 = (z - t) / (a - t);
                                                              	double t_2 = fma(y, (z / (a - t)), x);
                                                              	double tmp;
                                                              	if (t_1 <= -50.0) {
                                                              		tmp = t_2;
                                                              	} else if (t_1 <= 1e-9) {
                                                              		tmp = fma(y, ((z - t) / a), x);
                                                              	} else if (t_1 <= 1.02) {
                                                              		tmp = x + y;
                                                              	} else {
                                                              		tmp = t_2;
                                                              	}
                                                              	return tmp;
                                                              }
                                                              
                                                              function code(x, y, z, t, a)
                                                              	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                              	t_2 = fma(y, Float64(z / Float64(a - t)), x)
                                                              	tmp = 0.0
                                                              	if (t_1 <= -50.0)
                                                              		tmp = t_2;
                                                              	elseif (t_1 <= 1e-9)
                                                              		tmp = fma(y, Float64(Float64(z - t) / a), x);
                                                              	elseif (t_1 <= 1.02)
                                                              		tmp = Float64(x + y);
                                                              	else
                                                              		tmp = t_2;
                                                              	end
                                                              	return tmp
                                                              end
                                                              
                                                              code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(y * N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, -50.0], t$95$2, If[LessEqual[t$95$1, 1e-9], N[(y * N[(N[(z - t), $MachinePrecision] / a), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[t$95$1, 1.02], N[(x + y), $MachinePrecision], t$95$2]]]]]
                                                              
                                                              f(x, y, z, t, a):
                                                              	x in [-inf, +inf],
                                                              	y in [-inf, +inf],
                                                              	z in [-inf, +inf],
                                                              	t in [-inf, +inf],
                                                              	a in [-inf, +inf]
                                                              code: THEORY
                                                              BEGIN
                                                              f(x, y, z, t, a: real): real =
                                                              	LET t_1 = ((z - t) / (a - t)) IN
                                                              		LET t_2 = ((y * (z / (a - t))) + x) IN
                                                              			LET tmp_2 = IF (t_1 <= (1020000000000000017763568394002504646778106689453125e-51)) THEN (x + y) ELSE t_2 ENDIF IN
                                                              			LET tmp_1 = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN ((y * ((z - t) / a)) + x) ELSE tmp_2 ENDIF IN
                                                              			LET tmp = IF (t_1 <= (-50)) THEN t_2 ELSE tmp_1 ENDIF IN
                                                              	tmp
                                                              END code
                                                              \begin{array}{l}
                                                              t_1 := \frac{z - t}{a - t}\\
                                                              t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\
                                                              \mathbf{if}\;t\_1 \leq -50:\\
                                                              \;\;\;\;t\_2\\
                                                              
                                                              \mathbf{elif}\;t\_1 \leq 10^{-9}:\\
                                                              \;\;\;\;\mathsf{fma}\left(y, \frac{z - t}{a}, x\right)\\
                                                              
                                                              \mathbf{elif}\;t\_1 \leq 1.02:\\
                                                              \;\;\;\;x + y\\
                                                              
                                                              \mathbf{else}:\\
                                                              \;\;\;\;t\_2\\
                                                              
                                                              
                                                              \end{array}
                                                              
                                                              Derivation
                                                              1. Split input into 3 regimes
                                                              2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -50 or 1.02 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                1. Initial program 98.1%

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

                                                                  \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                                                3. Step-by-step derivation
                                                                  1. Applied rewrites76.8%

                                                                    \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                                                  2. Step-by-step derivation
                                                                    1. Applied rewrites76.8%

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

                                                                    if -50 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9

                                                                    1. Initial program 98.1%

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

                                                                      \[\leadsto x + y \cdot \frac{z - t}{a} \]
                                                                    3. Step-by-step derivation
                                                                      1. Applied rewrites60.1%

                                                                        \[\leadsto x + y \cdot \frac{z - t}{a} \]
                                                                      2. Step-by-step derivation
                                                                        1. Applied rewrites60.1%

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

                                                                        if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.02

                                                                        1. Initial program 98.1%

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

                                                                          \[\leadsto x + y \]
                                                                        3. Step-by-step derivation
                                                                          1. Applied rewrites61.3%

                                                                            \[\leadsto x + y \]
                                                                        4. Recombined 3 regimes into one program.
                                                                        5. Add Preprocessing

                                                                        Alternative 7: 92.5% accurate, 0.4× speedup?

                                                                        \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\ \mathbf{if}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 1.02:\\ \;\;\;\;x + y\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
                                                                        (FPCore (x y z t a)
                                                                          :precision binary64
                                                                          :pre TRUE
                                                                          (let* ((t_1 (/ (- z t) (- a t))) (t_2 (fma y (/ z (- a t)) x)))
                                                                          (if (<= t_1 1e-9) t_2 (if (<= t_1 1.02) (+ x y) t_2))))
                                                                        double code(double x, double y, double z, double t, double a) {
                                                                        	double t_1 = (z - t) / (a - t);
                                                                        	double t_2 = fma(y, (z / (a - t)), x);
                                                                        	double tmp;
                                                                        	if (t_1 <= 1e-9) {
                                                                        		tmp = t_2;
                                                                        	} else if (t_1 <= 1.02) {
                                                                        		tmp = x + y;
                                                                        	} else {
                                                                        		tmp = t_2;
                                                                        	}
                                                                        	return tmp;
                                                                        }
                                                                        
                                                                        function code(x, y, z, t, a)
                                                                        	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                                        	t_2 = fma(y, Float64(z / Float64(a - t)), x)
                                                                        	tmp = 0.0
                                                                        	if (t_1 <= 1e-9)
                                                                        		tmp = t_2;
                                                                        	elseif (t_1 <= 1.02)
                                                                        		tmp = Float64(x + y);
                                                                        	else
                                                                        		tmp = t_2;
                                                                        	end
                                                                        	return tmp
                                                                        end
                                                                        
                                                                        code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(y * N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, 1e-9], t$95$2, If[LessEqual[t$95$1, 1.02], N[(x + y), $MachinePrecision], t$95$2]]]]
                                                                        
                                                                        f(x, y, z, t, a):
                                                                        	x in [-inf, +inf],
                                                                        	y in [-inf, +inf],
                                                                        	z in [-inf, +inf],
                                                                        	t in [-inf, +inf],
                                                                        	a in [-inf, +inf]
                                                                        code: THEORY
                                                                        BEGIN
                                                                        f(x, y, z, t, a: real): real =
                                                                        	LET t_1 = ((z - t) / (a - t)) IN
                                                                        		LET t_2 = ((y * (z / (a - t))) + x) IN
                                                                        			LET tmp_1 = IF (t_1 <= (1020000000000000017763568394002504646778106689453125e-51)) THEN (x + y) ELSE t_2 ENDIF IN
                                                                        			LET tmp = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN t_2 ELSE tmp_1 ENDIF IN
                                                                        	tmp
                                                                        END code
                                                                        \begin{array}{l}
                                                                        t_1 := \frac{z - t}{a - t}\\
                                                                        t_2 := \mathsf{fma}\left(y, \frac{z}{a - t}, x\right)\\
                                                                        \mathbf{if}\;t\_1 \leq 10^{-9}:\\
                                                                        \;\;\;\;t\_2\\
                                                                        
                                                                        \mathbf{elif}\;t\_1 \leq 1.02:\\
                                                                        \;\;\;\;x + y\\
                                                                        
                                                                        \mathbf{else}:\\
                                                                        \;\;\;\;t\_2\\
                                                                        
                                                                        
                                                                        \end{array}
                                                                        
                                                                        Derivation
                                                                        1. Split input into 2 regimes
                                                                        2. if (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9 or 1.02 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                          1. Initial program 98.1%

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

                                                                            \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                                                          3. Step-by-step derivation
                                                                            1. Applied rewrites76.8%

                                                                              \[\leadsto x + y \cdot \frac{z}{a - t} \]
                                                                            2. Step-by-step derivation
                                                                              1. Applied rewrites76.8%

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

                                                                              if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.02

                                                                              1. Initial program 98.1%

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

                                                                                \[\leadsto x + y \]
                                                                              3. Step-by-step derivation
                                                                                1. Applied rewrites61.3%

                                                                                  \[\leadsto x + y \]
                                                                              4. Recombined 2 regimes into one program.
                                                                              5. Add Preprocessing

                                                                              Alternative 8: 84.0% accurate, 0.3× speedup?

                                                                              \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+104}:\\ \;\;\;\;z \cdot \frac{y}{a - t}\\ \mathbf{elif}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;x + z \cdot \frac{y}{a}\\ \mathbf{elif}\;t\_1 \leq 5000000000000:\\ \;\;\;\;x + y\\ \mathbf{else}:\\ \;\;\;\;\frac{z}{a - t} \cdot y\\ \end{array} \]
                                                                              (FPCore (x y z t a)
                                                                                :precision binary64
                                                                                :pre TRUE
                                                                                (let* ((t_1 (/ (- z t) (- a t))))
                                                                                (if (<= t_1 -1e+104)
                                                                                  (* z (/ y (- a t)))
                                                                                  (if (<= t_1 1e-9)
                                                                                    (+ x (* z (/ y a)))
                                                                                    (if (<= t_1 5000000000000.0) (+ x y) (* (/ z (- a t)) y))))))
                                                                              double code(double x, double y, double z, double t, double a) {
                                                                              	double t_1 = (z - t) / (a - t);
                                                                              	double tmp;
                                                                              	if (t_1 <= -1e+104) {
                                                                              		tmp = z * (y / (a - t));
                                                                              	} else if (t_1 <= 1e-9) {
                                                                              		tmp = x + (z * (y / a));
                                                                              	} else if (t_1 <= 5000000000000.0) {
                                                                              		tmp = x + y;
                                                                              	} else {
                                                                              		tmp = (z / (a - t)) * y;
                                                                              	}
                                                                              	return tmp;
                                                                              }
                                                                              
                                                                              real(8) function code(x, y, z, t, a)
                                                                              use fmin_fmax_functions
                                                                                  real(8), intent (in) :: x
                                                                                  real(8), intent (in) :: y
                                                                                  real(8), intent (in) :: z
                                                                                  real(8), intent (in) :: t
                                                                                  real(8), intent (in) :: a
                                                                                  real(8) :: t_1
                                                                                  real(8) :: tmp
                                                                                  t_1 = (z - t) / (a - t)
                                                                                  if (t_1 <= (-1d+104)) then
                                                                                      tmp = z * (y / (a - t))
                                                                                  else if (t_1 <= 1d-9) then
                                                                                      tmp = x + (z * (y / a))
                                                                                  else if (t_1 <= 5000000000000.0d0) then
                                                                                      tmp = x + y
                                                                                  else
                                                                                      tmp = (z / (a - t)) * y
                                                                                  end if
                                                                                  code = tmp
                                                                              end function
                                                                              
                                                                              public static double code(double x, double y, double z, double t, double a) {
                                                                              	double t_1 = (z - t) / (a - t);
                                                                              	double tmp;
                                                                              	if (t_1 <= -1e+104) {
                                                                              		tmp = z * (y / (a - t));
                                                                              	} else if (t_1 <= 1e-9) {
                                                                              		tmp = x + (z * (y / a));
                                                                              	} else if (t_1 <= 5000000000000.0) {
                                                                              		tmp = x + y;
                                                                              	} else {
                                                                              		tmp = (z / (a - t)) * y;
                                                                              	}
                                                                              	return tmp;
                                                                              }
                                                                              
                                                                              def code(x, y, z, t, a):
                                                                              	t_1 = (z - t) / (a - t)
                                                                              	tmp = 0
                                                                              	if t_1 <= -1e+104:
                                                                              		tmp = z * (y / (a - t))
                                                                              	elif t_1 <= 1e-9:
                                                                              		tmp = x + (z * (y / a))
                                                                              	elif t_1 <= 5000000000000.0:
                                                                              		tmp = x + y
                                                                              	else:
                                                                              		tmp = (z / (a - t)) * y
                                                                              	return tmp
                                                                              
                                                                              function code(x, y, z, t, a)
                                                                              	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                                              	tmp = 0.0
                                                                              	if (t_1 <= -1e+104)
                                                                              		tmp = Float64(z * Float64(y / Float64(a - t)));
                                                                              	elseif (t_1 <= 1e-9)
                                                                              		tmp = Float64(x + Float64(z * Float64(y / a)));
                                                                              	elseif (t_1 <= 5000000000000.0)
                                                                              		tmp = Float64(x + y);
                                                                              	else
                                                                              		tmp = Float64(Float64(z / Float64(a - t)) * y);
                                                                              	end
                                                                              	return tmp
                                                                              end
                                                                              
                                                                              function tmp_2 = code(x, y, z, t, a)
                                                                              	t_1 = (z - t) / (a - t);
                                                                              	tmp = 0.0;
                                                                              	if (t_1 <= -1e+104)
                                                                              		tmp = z * (y / (a - t));
                                                                              	elseif (t_1 <= 1e-9)
                                                                              		tmp = x + (z * (y / a));
                                                                              	elseif (t_1 <= 5000000000000.0)
                                                                              		tmp = x + y;
                                                                              	else
                                                                              		tmp = (z / (a - t)) * y;
                                                                              	end
                                                                              	tmp_2 = tmp;
                                                                              end
                                                                              
                                                                              code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -1e+104], N[(z * N[(y / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 1e-9], N[(x + N[(z * N[(y / a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 5000000000000.0], N[(x + y), $MachinePrecision], N[(N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision]]]]]
                                                                              
                                                                              f(x, y, z, t, a):
                                                                              	x in [-inf, +inf],
                                                                              	y in [-inf, +inf],
                                                                              	z in [-inf, +inf],
                                                                              	t in [-inf, +inf],
                                                                              	a in [-inf, +inf]
                                                                              code: THEORY
                                                                              BEGIN
                                                                              f(x, y, z, t, a: real): real =
                                                                              	LET t_1 = ((z - t) / (a - t)) IN
                                                                              		LET tmp_2 = IF (t_1 <= (5e12)) THEN (x + y) ELSE ((z / (a - t)) * y) ENDIF IN
                                                                              		LET tmp_1 = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN (x + (z * (y / a))) ELSE tmp_2 ENDIF IN
                                                                              		LET tmp = IF (t_1 <= (-100000000000000000191567508573466873621595512726519201115280351459937932420398875596123614510818032353280)) THEN (z * (y / (a - t))) ELSE tmp_1 ENDIF IN
                                                                              	tmp
                                                                              END code
                                                                              \begin{array}{l}
                                                                              t_1 := \frac{z - t}{a - t}\\
                                                                              \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+104}:\\
                                                                              \;\;\;\;z \cdot \frac{y}{a - t}\\
                                                                              
                                                                              \mathbf{elif}\;t\_1 \leq 10^{-9}:\\
                                                                              \;\;\;\;x + z \cdot \frac{y}{a}\\
                                                                              
                                                                              \mathbf{elif}\;t\_1 \leq 5000000000000:\\
                                                                              \;\;\;\;x + y\\
                                                                              
                                                                              \mathbf{else}:\\
                                                                              \;\;\;\;\frac{z}{a - t} \cdot y\\
                                                                              
                                                                              
                                                                              \end{array}
                                                                              
                                                                              Derivation
                                                                              1. Split input into 4 regimes
                                                                              2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -1e104

                                                                                1. Initial program 98.1%

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

                                                                                  \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                3. Step-by-step derivation
                                                                                  1. Applied rewrites62.0%

                                                                                    \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                  2. Step-by-step derivation
                                                                                    1. Applied rewrites62.0%

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

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

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

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

                                                                                        if -1e104 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9

                                                                                        1. Initial program 98.1%

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

                                                                                          \[\leadsto x + \frac{y \cdot z}{a} \]
                                                                                        3. Step-by-step derivation
                                                                                          1. Applied rewrites60.5%

                                                                                            \[\leadsto x + \frac{y \cdot z}{a} \]
                                                                                          2. Step-by-step derivation
                                                                                            1. Applied rewrites62.1%

                                                                                              \[\leadsto x + z \cdot \frac{y}{a} \]

                                                                                            if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 5e12

                                                                                            1. Initial program 98.1%

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

                                                                                              \[\leadsto x + y \]
                                                                                            3. Step-by-step derivation
                                                                                              1. Applied rewrites61.3%

                                                                                                \[\leadsto x + y \]

                                                                                              if 5e12 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                                              1. Initial program 98.1%

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

                                                                                                \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                              3. Step-by-step derivation
                                                                                                1. Applied rewrites62.0%

                                                                                                  \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                2. Step-by-step derivation
                                                                                                  1. Applied rewrites62.0%

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

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

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

                                                                                                        \[\leadsto \frac{z}{a - t} \cdot y \]
                                                                                                    3. Recombined 4 regimes into one program.
                                                                                                    4. Add Preprocessing

                                                                                                    Alternative 9: 83.8% accurate, 0.3× speedup?

                                                                                                    \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+104}:\\ \;\;\;\;z \cdot \frac{y}{a - t}\\ \mathbf{elif}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a}, x\right)\\ \mathbf{elif}\;t\_1 \leq 5000000000000:\\ \;\;\;\;x + y\\ \mathbf{else}:\\ \;\;\;\;\frac{z}{a - t} \cdot y\\ \end{array} \]
                                                                                                    (FPCore (x y z t a)
                                                                                                      :precision binary64
                                                                                                      :pre TRUE
                                                                                                      (let* ((t_1 (/ (- z t) (- a t))))
                                                                                                      (if (<= t_1 -1e+104)
                                                                                                        (* z (/ y (- a t)))
                                                                                                        (if (<= t_1 1e-9)
                                                                                                          (fma y (/ z a) x)
                                                                                                          (if (<= t_1 5000000000000.0) (+ x y) (* (/ z (- a t)) y))))))
                                                                                                    double code(double x, double y, double z, double t, double a) {
                                                                                                    	double t_1 = (z - t) / (a - t);
                                                                                                    	double tmp;
                                                                                                    	if (t_1 <= -1e+104) {
                                                                                                    		tmp = z * (y / (a - t));
                                                                                                    	} else if (t_1 <= 1e-9) {
                                                                                                    		tmp = fma(y, (z / a), x);
                                                                                                    	} else if (t_1 <= 5000000000000.0) {
                                                                                                    		tmp = x + y;
                                                                                                    	} else {
                                                                                                    		tmp = (z / (a - t)) * y;
                                                                                                    	}
                                                                                                    	return tmp;
                                                                                                    }
                                                                                                    
                                                                                                    function code(x, y, z, t, a)
                                                                                                    	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                                                                    	tmp = 0.0
                                                                                                    	if (t_1 <= -1e+104)
                                                                                                    		tmp = Float64(z * Float64(y / Float64(a - t)));
                                                                                                    	elseif (t_1 <= 1e-9)
                                                                                                    		tmp = fma(y, Float64(z / a), x);
                                                                                                    	elseif (t_1 <= 5000000000000.0)
                                                                                                    		tmp = Float64(x + y);
                                                                                                    	else
                                                                                                    		tmp = Float64(Float64(z / Float64(a - t)) * y);
                                                                                                    	end
                                                                                                    	return tmp
                                                                                                    end
                                                                                                    
                                                                                                    code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -1e+104], N[(z * N[(y / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 1e-9], N[(y * N[(z / a), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[t$95$1, 5000000000000.0], N[(x + y), $MachinePrecision], N[(N[(z / N[(a - t), $MachinePrecision]), $MachinePrecision] * y), $MachinePrecision]]]]]
                                                                                                    
                                                                                                    f(x, y, z, t, a):
                                                                                                    	x in [-inf, +inf],
                                                                                                    	y in [-inf, +inf],
                                                                                                    	z in [-inf, +inf],
                                                                                                    	t in [-inf, +inf],
                                                                                                    	a in [-inf, +inf]
                                                                                                    code: THEORY
                                                                                                    BEGIN
                                                                                                    f(x, y, z, t, a: real): real =
                                                                                                    	LET t_1 = ((z - t) / (a - t)) IN
                                                                                                    		LET tmp_2 = IF (t_1 <= (5e12)) THEN (x + y) ELSE ((z / (a - t)) * y) ENDIF IN
                                                                                                    		LET tmp_1 = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN ((y * (z / a)) + x) ELSE tmp_2 ENDIF IN
                                                                                                    		LET tmp = IF (t_1 <= (-100000000000000000191567508573466873621595512726519201115280351459937932420398875596123614510818032353280)) THEN (z * (y / (a - t))) ELSE tmp_1 ENDIF IN
                                                                                                    	tmp
                                                                                                    END code
                                                                                                    \begin{array}{l}
                                                                                                    t_1 := \frac{z - t}{a - t}\\
                                                                                                    \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+104}:\\
                                                                                                    \;\;\;\;z \cdot \frac{y}{a - t}\\
                                                                                                    
                                                                                                    \mathbf{elif}\;t\_1 \leq 10^{-9}:\\
                                                                                                    \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a}, x\right)\\
                                                                                                    
                                                                                                    \mathbf{elif}\;t\_1 \leq 5000000000000:\\
                                                                                                    \;\;\;\;x + y\\
                                                                                                    
                                                                                                    \mathbf{else}:\\
                                                                                                    \;\;\;\;\frac{z}{a - t} \cdot y\\
                                                                                                    
                                                                                                    
                                                                                                    \end{array}
                                                                                                    
                                                                                                    Derivation
                                                                                                    1. Split input into 4 regimes
                                                                                                    2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -1e104

                                                                                                      1. Initial program 98.1%

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

                                                                                                        \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                      3. Step-by-step derivation
                                                                                                        1. Applied rewrites62.0%

                                                                                                          \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                        2. Step-by-step derivation
                                                                                                          1. Applied rewrites62.0%

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

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

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

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

                                                                                                              if -1e104 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9

                                                                                                              1. Initial program 98.1%

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

                                                                                                                \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                              3. Step-by-step derivation
                                                                                                                1. Applied rewrites62.0%

                                                                                                                  \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                2. Step-by-step derivation
                                                                                                                  1. Applied rewrites62.0%

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

                                                                                                                  if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 5e12

                                                                                                                  1. Initial program 98.1%

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

                                                                                                                    \[\leadsto x + y \]
                                                                                                                  3. Step-by-step derivation
                                                                                                                    1. Applied rewrites61.3%

                                                                                                                      \[\leadsto x + y \]

                                                                                                                    if 5e12 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                                                                    1. Initial program 98.1%

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

                                                                                                                      \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                    3. Step-by-step derivation
                                                                                                                      1. Applied rewrites62.0%

                                                                                                                        \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                      2. Step-by-step derivation
                                                                                                                        1. Applied rewrites62.0%

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

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

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

                                                                                                                              \[\leadsto \frac{z}{a - t} \cdot y \]
                                                                                                                          3. Recombined 4 regimes into one program.
                                                                                                                          4. Add Preprocessing

                                                                                                                          Alternative 10: 83.4% accurate, 0.3× speedup?

                                                                                                                          \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ t_2 := z \cdot \frac{y}{a - t}\\ \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+104}:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a}, x\right)\\ \mathbf{elif}\;t\_1 \leq 5000000000000:\\ \;\;\;\;x + y\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
                                                                                                                          (FPCore (x y z t a)
                                                                                                                            :precision binary64
                                                                                                                            :pre TRUE
                                                                                                                            (let* ((t_1 (/ (- z t) (- a t))) (t_2 (* z (/ y (- a t)))))
                                                                                                                            (if (<= t_1 -1e+104)
                                                                                                                              t_2
                                                                                                                              (if (<= t_1 1e-9)
                                                                                                                                (fma y (/ z a) x)
                                                                                                                                (if (<= t_1 5000000000000.0) (+ x y) t_2)))))
                                                                                                                          double code(double x, double y, double z, double t, double a) {
                                                                                                                          	double t_1 = (z - t) / (a - t);
                                                                                                                          	double t_2 = z * (y / (a - t));
                                                                                                                          	double tmp;
                                                                                                                          	if (t_1 <= -1e+104) {
                                                                                                                          		tmp = t_2;
                                                                                                                          	} else if (t_1 <= 1e-9) {
                                                                                                                          		tmp = fma(y, (z / a), x);
                                                                                                                          	} else if (t_1 <= 5000000000000.0) {
                                                                                                                          		tmp = x + y;
                                                                                                                          	} else {
                                                                                                                          		tmp = t_2;
                                                                                                                          	}
                                                                                                                          	return tmp;
                                                                                                                          }
                                                                                                                          
                                                                                                                          function code(x, y, z, t, a)
                                                                                                                          	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                                                                                          	t_2 = Float64(z * Float64(y / Float64(a - t)))
                                                                                                                          	tmp = 0.0
                                                                                                                          	if (t_1 <= -1e+104)
                                                                                                                          		tmp = t_2;
                                                                                                                          	elseif (t_1 <= 1e-9)
                                                                                                                          		tmp = fma(y, Float64(z / a), x);
                                                                                                                          	elseif (t_1 <= 5000000000000.0)
                                                                                                                          		tmp = Float64(x + y);
                                                                                                                          	else
                                                                                                                          		tmp = t_2;
                                                                                                                          	end
                                                                                                                          	return tmp
                                                                                                                          end
                                                                                                                          
                                                                                                                          code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(z * N[(y / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -1e+104], t$95$2, If[LessEqual[t$95$1, 1e-9], N[(y * N[(z / a), $MachinePrecision] + x), $MachinePrecision], If[LessEqual[t$95$1, 5000000000000.0], N[(x + y), $MachinePrecision], t$95$2]]]]]
                                                                                                                          
                                                                                                                          f(x, y, z, t, a):
                                                                                                                          	x in [-inf, +inf],
                                                                                                                          	y in [-inf, +inf],
                                                                                                                          	z in [-inf, +inf],
                                                                                                                          	t in [-inf, +inf],
                                                                                                                          	a in [-inf, +inf]
                                                                                                                          code: THEORY
                                                                                                                          BEGIN
                                                                                                                          f(x, y, z, t, a: real): real =
                                                                                                                          	LET t_1 = ((z - t) / (a - t)) IN
                                                                                                                          		LET t_2 = (z * (y / (a - t))) IN
                                                                                                                          			LET tmp_2 = IF (t_1 <= (5e12)) THEN (x + y) ELSE t_2 ENDIF IN
                                                                                                                          			LET tmp_1 = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN ((y * (z / a)) + x) ELSE tmp_2 ENDIF IN
                                                                                                                          			LET tmp = IF (t_1 <= (-100000000000000000191567508573466873621595512726519201115280351459937932420398875596123614510818032353280)) THEN t_2 ELSE tmp_1 ENDIF IN
                                                                                                                          	tmp
                                                                                                                          END code
                                                                                                                          \begin{array}{l}
                                                                                                                          t_1 := \frac{z - t}{a - t}\\
                                                                                                                          t_2 := z \cdot \frac{y}{a - t}\\
                                                                                                                          \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+104}:\\
                                                                                                                          \;\;\;\;t\_2\\
                                                                                                                          
                                                                                                                          \mathbf{elif}\;t\_1 \leq 10^{-9}:\\
                                                                                                                          \;\;\;\;\mathsf{fma}\left(y, \frac{z}{a}, x\right)\\
                                                                                                                          
                                                                                                                          \mathbf{elif}\;t\_1 \leq 5000000000000:\\
                                                                                                                          \;\;\;\;x + y\\
                                                                                                                          
                                                                                                                          \mathbf{else}:\\
                                                                                                                          \;\;\;\;t\_2\\
                                                                                                                          
                                                                                                                          
                                                                                                                          \end{array}
                                                                                                                          
                                                                                                                          Derivation
                                                                                                                          1. Split input into 3 regimes
                                                                                                                          2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -1e104 or 5e12 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                                                                            1. Initial program 98.1%

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

                                                                                                                              \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                            3. Step-by-step derivation
                                                                                                                              1. Applied rewrites62.0%

                                                                                                                                \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                              2. Step-by-step derivation
                                                                                                                                1. Applied rewrites62.0%

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

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

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

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

                                                                                                                                    if -1e104 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9

                                                                                                                                    1. Initial program 98.1%

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

                                                                                                                                      \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                                    3. Step-by-step derivation
                                                                                                                                      1. Applied rewrites62.0%

                                                                                                                                        \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                                      2. Step-by-step derivation
                                                                                                                                        1. Applied rewrites62.0%

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

                                                                                                                                        if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 5e12

                                                                                                                                        1. Initial program 98.1%

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

                                                                                                                                          \[\leadsto x + y \]
                                                                                                                                        3. Step-by-step derivation
                                                                                                                                          1. Applied rewrites61.3%

                                                                                                                                            \[\leadsto x + y \]
                                                                                                                                        4. Recombined 3 regimes into one program.
                                                                                                                                        5. Add Preprocessing

                                                                                                                                        Alternative 11: 81.0% accurate, 0.4× speedup?

                                                                                                                                        \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ t_2 := \mathsf{fma}\left(y, \frac{z}{a}, x\right)\\ \mathbf{if}\;t\_1 \leq 10^{-9}:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 1.02:\\ \;\;\;\;x + y\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
                                                                                                                                        (FPCore (x y z t a)
                                                                                                                                          :precision binary64
                                                                                                                                          :pre TRUE
                                                                                                                                          (let* ((t_1 (/ (- z t) (- a t))) (t_2 (fma y (/ z a) x)))
                                                                                                                                          (if (<= t_1 1e-9) t_2 (if (<= t_1 1.02) (+ x y) t_2))))
                                                                                                                                        double code(double x, double y, double z, double t, double a) {
                                                                                                                                        	double t_1 = (z - t) / (a - t);
                                                                                                                                        	double t_2 = fma(y, (z / a), x);
                                                                                                                                        	double tmp;
                                                                                                                                        	if (t_1 <= 1e-9) {
                                                                                                                                        		tmp = t_2;
                                                                                                                                        	} else if (t_1 <= 1.02) {
                                                                                                                                        		tmp = x + y;
                                                                                                                                        	} else {
                                                                                                                                        		tmp = t_2;
                                                                                                                                        	}
                                                                                                                                        	return tmp;
                                                                                                                                        }
                                                                                                                                        
                                                                                                                                        function code(x, y, z, t, a)
                                                                                                                                        	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                                                                                                        	t_2 = fma(y, Float64(z / a), x)
                                                                                                                                        	tmp = 0.0
                                                                                                                                        	if (t_1 <= 1e-9)
                                                                                                                                        		tmp = t_2;
                                                                                                                                        	elseif (t_1 <= 1.02)
                                                                                                                                        		tmp = Float64(x + y);
                                                                                                                                        	else
                                                                                                                                        		tmp = t_2;
                                                                                                                                        	end
                                                                                                                                        	return tmp
                                                                                                                                        end
                                                                                                                                        
                                                                                                                                        code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(y * N[(z / a), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$1, 1e-9], t$95$2, If[LessEqual[t$95$1, 1.02], N[(x + y), $MachinePrecision], t$95$2]]]]
                                                                                                                                        
                                                                                                                                        f(x, y, z, t, a):
                                                                                                                                        	x in [-inf, +inf],
                                                                                                                                        	y in [-inf, +inf],
                                                                                                                                        	z in [-inf, +inf],
                                                                                                                                        	t in [-inf, +inf],
                                                                                                                                        	a in [-inf, +inf]
                                                                                                                                        code: THEORY
                                                                                                                                        BEGIN
                                                                                                                                        f(x, y, z, t, a: real): real =
                                                                                                                                        	LET t_1 = ((z - t) / (a - t)) IN
                                                                                                                                        		LET t_2 = ((y * (z / a)) + x) IN
                                                                                                                                        			LET tmp_1 = IF (t_1 <= (1020000000000000017763568394002504646778106689453125e-51)) THEN (x + y) ELSE t_2 ENDIF IN
                                                                                                                                        			LET tmp = IF (t_1 <= (10000000000000000622815914577798564188970686927859787829220294952392578125e-82)) THEN t_2 ELSE tmp_1 ENDIF IN
                                                                                                                                        	tmp
                                                                                                                                        END code
                                                                                                                                        \begin{array}{l}
                                                                                                                                        t_1 := \frac{z - t}{a - t}\\
                                                                                                                                        t_2 := \mathsf{fma}\left(y, \frac{z}{a}, x\right)\\
                                                                                                                                        \mathbf{if}\;t\_1 \leq 10^{-9}:\\
                                                                                                                                        \;\;\;\;t\_2\\
                                                                                                                                        
                                                                                                                                        \mathbf{elif}\;t\_1 \leq 1.02:\\
                                                                                                                                        \;\;\;\;x + y\\
                                                                                                                                        
                                                                                                                                        \mathbf{else}:\\
                                                                                                                                        \;\;\;\;t\_2\\
                                                                                                                                        
                                                                                                                                        
                                                                                                                                        \end{array}
                                                                                                                                        
                                                                                                                                        Derivation
                                                                                                                                        1. Split input into 2 regimes
                                                                                                                                        2. if (/.f64 (-.f64 z t) (-.f64 a t)) < 1.0000000000000001e-9 or 1.02 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                                                                                          1. Initial program 98.1%

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

                                                                                                                                            \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                                          3. Step-by-step derivation
                                                                                                                                            1. Applied rewrites62.0%

                                                                                                                                              \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                                            2. Step-by-step derivation
                                                                                                                                              1. Applied rewrites62.0%

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

                                                                                                                                              if 1.0000000000000001e-9 < (/.f64 (-.f64 z t) (-.f64 a t)) < 1.02

                                                                                                                                              1. Initial program 98.1%

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

                                                                                                                                                \[\leadsto x + y \]
                                                                                                                                              3. Step-by-step derivation
                                                                                                                                                1. Applied rewrites61.3%

                                                                                                                                                  \[\leadsto x + y \]
                                                                                                                                              4. Recombined 2 regimes into one program.
                                                                                                                                              5. Add Preprocessing

                                                                                                                                              Alternative 12: 72.1% accurate, 0.3× speedup?

                                                                                                                                              \[\begin{array}{l} t_1 := \frac{z - t}{a - t}\\ t_2 := \frac{y \cdot z}{a}\\ \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+103}:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 2 \cdot 10^{-42}:\\ \;\;\;\;x \cdot 1\\ \mathbf{elif}\;t\_1 \leq 5 \cdot 10^{+107}:\\ \;\;\;\;x + y\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
                                                                                                                                              (FPCore (x y z t a)
                                                                                                                                                :precision binary64
                                                                                                                                                :pre TRUE
                                                                                                                                                (let* ((t_1 (/ (- z t) (- a t))) (t_2 (/ (* y z) a)))
                                                                                                                                                (if (<= t_1 -1e+103)
                                                                                                                                                  t_2
                                                                                                                                                  (if (<= t_1 2e-42) (* x 1.0) (if (<= t_1 5e+107) (+ x y) t_2)))))
                                                                                                                                              double code(double x, double y, double z, double t, double a) {
                                                                                                                                              	double t_1 = (z - t) / (a - t);
                                                                                                                                              	double t_2 = (y * z) / a;
                                                                                                                                              	double tmp;
                                                                                                                                              	if (t_1 <= -1e+103) {
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	} else if (t_1 <= 2e-42) {
                                                                                                                                              		tmp = x * 1.0;
                                                                                                                                              	} else if (t_1 <= 5e+107) {
                                                                                                                                              		tmp = x + y;
                                                                                                                                              	} else {
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	}
                                                                                                                                              	return tmp;
                                                                                                                                              }
                                                                                                                                              
                                                                                                                                              real(8) function code(x, y, z, t, a)
                                                                                                                                              use fmin_fmax_functions
                                                                                                                                                  real(8), intent (in) :: x
                                                                                                                                                  real(8), intent (in) :: y
                                                                                                                                                  real(8), intent (in) :: z
                                                                                                                                                  real(8), intent (in) :: t
                                                                                                                                                  real(8), intent (in) :: a
                                                                                                                                                  real(8) :: t_1
                                                                                                                                                  real(8) :: t_2
                                                                                                                                                  real(8) :: tmp
                                                                                                                                                  t_1 = (z - t) / (a - t)
                                                                                                                                                  t_2 = (y * z) / a
                                                                                                                                                  if (t_1 <= (-1d+103)) then
                                                                                                                                                      tmp = t_2
                                                                                                                                                  else if (t_1 <= 2d-42) then
                                                                                                                                                      tmp = x * 1.0d0
                                                                                                                                                  else if (t_1 <= 5d+107) then
                                                                                                                                                      tmp = x + y
                                                                                                                                                  else
                                                                                                                                                      tmp = t_2
                                                                                                                                                  end if
                                                                                                                                                  code = tmp
                                                                                                                                              end function
                                                                                                                                              
                                                                                                                                              public static double code(double x, double y, double z, double t, double a) {
                                                                                                                                              	double t_1 = (z - t) / (a - t);
                                                                                                                                              	double t_2 = (y * z) / a;
                                                                                                                                              	double tmp;
                                                                                                                                              	if (t_1 <= -1e+103) {
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	} else if (t_1 <= 2e-42) {
                                                                                                                                              		tmp = x * 1.0;
                                                                                                                                              	} else if (t_1 <= 5e+107) {
                                                                                                                                              		tmp = x + y;
                                                                                                                                              	} else {
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	}
                                                                                                                                              	return tmp;
                                                                                                                                              }
                                                                                                                                              
                                                                                                                                              def code(x, y, z, t, a):
                                                                                                                                              	t_1 = (z - t) / (a - t)
                                                                                                                                              	t_2 = (y * z) / a
                                                                                                                                              	tmp = 0
                                                                                                                                              	if t_1 <= -1e+103:
                                                                                                                                              		tmp = t_2
                                                                                                                                              	elif t_1 <= 2e-42:
                                                                                                                                              		tmp = x * 1.0
                                                                                                                                              	elif t_1 <= 5e+107:
                                                                                                                                              		tmp = x + y
                                                                                                                                              	else:
                                                                                                                                              		tmp = t_2
                                                                                                                                              	return tmp
                                                                                                                                              
                                                                                                                                              function code(x, y, z, t, a)
                                                                                                                                              	t_1 = Float64(Float64(z - t) / Float64(a - t))
                                                                                                                                              	t_2 = Float64(Float64(y * z) / a)
                                                                                                                                              	tmp = 0.0
                                                                                                                                              	if (t_1 <= -1e+103)
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	elseif (t_1 <= 2e-42)
                                                                                                                                              		tmp = Float64(x * 1.0);
                                                                                                                                              	elseif (t_1 <= 5e+107)
                                                                                                                                              		tmp = Float64(x + y);
                                                                                                                                              	else
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	end
                                                                                                                                              	return tmp
                                                                                                                                              end
                                                                                                                                              
                                                                                                                                              function tmp_2 = code(x, y, z, t, a)
                                                                                                                                              	t_1 = (z - t) / (a - t);
                                                                                                                                              	t_2 = (y * z) / a;
                                                                                                                                              	tmp = 0.0;
                                                                                                                                              	if (t_1 <= -1e+103)
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	elseif (t_1 <= 2e-42)
                                                                                                                                              		tmp = x * 1.0;
                                                                                                                                              	elseif (t_1 <= 5e+107)
                                                                                                                                              		tmp = x + y;
                                                                                                                                              	else
                                                                                                                                              		tmp = t_2;
                                                                                                                                              	end
                                                                                                                                              	tmp_2 = tmp;
                                                                                                                                              end
                                                                                                                                              
                                                                                                                                              code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[(y * z), $MachinePrecision] / a), $MachinePrecision]}, If[LessEqual[t$95$1, -1e+103], t$95$2, If[LessEqual[t$95$1, 2e-42], N[(x * 1.0), $MachinePrecision], If[LessEqual[t$95$1, 5e+107], N[(x + y), $MachinePrecision], t$95$2]]]]]
                                                                                                                                              
                                                                                                                                              f(x, y, z, t, a):
                                                                                                                                              	x in [-inf, +inf],
                                                                                                                                              	y in [-inf, +inf],
                                                                                                                                              	z in [-inf, +inf],
                                                                                                                                              	t in [-inf, +inf],
                                                                                                                                              	a in [-inf, +inf]
                                                                                                                                              code: THEORY
                                                                                                                                              BEGIN
                                                                                                                                              f(x, y, z, t, a: real): real =
                                                                                                                                              	LET t_1 = ((z - t) / (a - t)) IN
                                                                                                                                              		LET t_2 = ((y * z) / a) IN
                                                                                                                                              			LET tmp_2 = IF (t_1 <= (500000000000000016999495856501412297471987359856449023856715357418937635861600416646370808190366722960654336)) THEN (x + y) ELSE t_2 ENDIF IN
                                                                                                                                              			LET tmp_1 = IF (t_1 <= (200000000000000007524625871377379968058902433453275290835288395066001500595069327282634990631972526265675645269770388523511428502388298511505126953125e-191)) THEN (x * (1)) ELSE tmp_2 ENDIF IN
                                                                                                                                              			LET tmp = IF (t_1 <= (-10000000000000000019156750857346687362159551272651920111528035145993793242039887559612361451081803235328)) THEN t_2 ELSE tmp_1 ENDIF IN
                                                                                                                                              	tmp
                                                                                                                                              END code
                                                                                                                                              \begin{array}{l}
                                                                                                                                              t_1 := \frac{z - t}{a - t}\\
                                                                                                                                              t_2 := \frac{y \cdot z}{a}\\
                                                                                                                                              \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+103}:\\
                                                                                                                                              \;\;\;\;t\_2\\
                                                                                                                                              
                                                                                                                                              \mathbf{elif}\;t\_1 \leq 2 \cdot 10^{-42}:\\
                                                                                                                                              \;\;\;\;x \cdot 1\\
                                                                                                                                              
                                                                                                                                              \mathbf{elif}\;t\_1 \leq 5 \cdot 10^{+107}:\\
                                                                                                                                              \;\;\;\;x + y\\
                                                                                                                                              
                                                                                                                                              \mathbf{else}:\\
                                                                                                                                              \;\;\;\;t\_2\\
                                                                                                                                              
                                                                                                                                              
                                                                                                                                              \end{array}
                                                                                                                                              
                                                                                                                                              Derivation
                                                                                                                                              1. Split input into 3 regimes
                                                                                                                                              2. if (/.f64 (-.f64 z t) (-.f64 a t)) < -1e103 or 5.0000000000000002e107 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                                                                                                1. Initial program 98.1%

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

                                                                                                                                                  \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                                                3. Step-by-step derivation
                                                                                                                                                  1. Applied rewrites62.0%

                                                                                                                                                    \[\leadsto x + y \cdot \frac{z}{a} \]
                                                                                                                                                  2. Step-by-step derivation
                                                                                                                                                    1. Applied rewrites62.0%

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

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

                                                                                                                                                        \[\leadsto \frac{y \cdot z}{a - t} \]
                                                                                                                                                      2. Taylor expanded in t around 0

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

                                                                                                                                                          \[\leadsto \frac{y \cdot z}{a} \]

                                                                                                                                                        if -1e103 < (/.f64 (-.f64 z t) (-.f64 a t)) < 2.0000000000000001e-42

                                                                                                                                                        1. Initial program 98.1%

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

                                                                                                                                                          \[\leadsto x \cdot \left(1 + \frac{y \cdot \left(z - t\right)}{x \cdot \left(a - t\right)}\right) \]
                                                                                                                                                        3. Step-by-step derivation
                                                                                                                                                          1. Applied rewrites79.3%

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

                                                                                                                                                            \[\leadsto x \cdot 1 \]
                                                                                                                                                          3. Step-by-step derivation
                                                                                                                                                            1. Applied rewrites51.3%

                                                                                                                                                              \[\leadsto x \cdot 1 \]

                                                                                                                                                            if 2.0000000000000001e-42 < (/.f64 (-.f64 z t) (-.f64 a t)) < 5.0000000000000002e107

                                                                                                                                                            1. Initial program 98.1%

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

                                                                                                                                                              \[\leadsto x + y \]
                                                                                                                                                            3. Step-by-step derivation
                                                                                                                                                              1. Applied rewrites61.3%

                                                                                                                                                                \[\leadsto x + y \]
                                                                                                                                                            4. Recombined 3 regimes into one program.
                                                                                                                                                            5. Add Preprocessing

                                                                                                                                                            Alternative 13: 67.6% accurate, 0.9× speedup?

                                                                                                                                                            \[\begin{array}{l} \mathbf{if}\;\frac{z - t}{a - t} \leq 1.7911263122038114 \cdot 10^{-38}:\\ \;\;\;\;x \cdot 1\\ \mathbf{else}:\\ \;\;\;\;x + y\\ \end{array} \]
                                                                                                                                                            (FPCore (x y z t a)
                                                                                                                                                              :precision binary64
                                                                                                                                                              :pre TRUE
                                                                                                                                                              (if (<= (/ (- z t) (- a t)) 1.7911263122038114e-38) (* x 1.0) (+ x y)))
                                                                                                                                                            double code(double x, double y, double z, double t, double a) {
                                                                                                                                                            	double tmp;
                                                                                                                                                            	if (((z - t) / (a - t)) <= 1.7911263122038114e-38) {
                                                                                                                                                            		tmp = x * 1.0;
                                                                                                                                                            	} else {
                                                                                                                                                            		tmp = x + y;
                                                                                                                                                            	}
                                                                                                                                                            	return tmp;
                                                                                                                                                            }
                                                                                                                                                            
                                                                                                                                                            real(8) function code(x, y, z, t, a)
                                                                                                                                                            use fmin_fmax_functions
                                                                                                                                                                real(8), intent (in) :: x
                                                                                                                                                                real(8), intent (in) :: y
                                                                                                                                                                real(8), intent (in) :: z
                                                                                                                                                                real(8), intent (in) :: t
                                                                                                                                                                real(8), intent (in) :: a
                                                                                                                                                                real(8) :: tmp
                                                                                                                                                                if (((z - t) / (a - t)) <= 1.7911263122038114d-38) then
                                                                                                                                                                    tmp = x * 1.0d0
                                                                                                                                                                else
                                                                                                                                                                    tmp = x + y
                                                                                                                                                                end if
                                                                                                                                                                code = tmp
                                                                                                                                                            end function
                                                                                                                                                            
                                                                                                                                                            public static double code(double x, double y, double z, double t, double a) {
                                                                                                                                                            	double tmp;
                                                                                                                                                            	if (((z - t) / (a - t)) <= 1.7911263122038114e-38) {
                                                                                                                                                            		tmp = x * 1.0;
                                                                                                                                                            	} else {
                                                                                                                                                            		tmp = x + y;
                                                                                                                                                            	}
                                                                                                                                                            	return tmp;
                                                                                                                                                            }
                                                                                                                                                            
                                                                                                                                                            def code(x, y, z, t, a):
                                                                                                                                                            	tmp = 0
                                                                                                                                                            	if ((z - t) / (a - t)) <= 1.7911263122038114e-38:
                                                                                                                                                            		tmp = x * 1.0
                                                                                                                                                            	else:
                                                                                                                                                            		tmp = x + y
                                                                                                                                                            	return tmp
                                                                                                                                                            
                                                                                                                                                            function code(x, y, z, t, a)
                                                                                                                                                            	tmp = 0.0
                                                                                                                                                            	if (Float64(Float64(z - t) / Float64(a - t)) <= 1.7911263122038114e-38)
                                                                                                                                                            		tmp = Float64(x * 1.0);
                                                                                                                                                            	else
                                                                                                                                                            		tmp = Float64(x + y);
                                                                                                                                                            	end
                                                                                                                                                            	return tmp
                                                                                                                                                            end
                                                                                                                                                            
                                                                                                                                                            function tmp_2 = code(x, y, z, t, a)
                                                                                                                                                            	tmp = 0.0;
                                                                                                                                                            	if (((z - t) / (a - t)) <= 1.7911263122038114e-38)
                                                                                                                                                            		tmp = x * 1.0;
                                                                                                                                                            	else
                                                                                                                                                            		tmp = x + y;
                                                                                                                                                            	end
                                                                                                                                                            	tmp_2 = tmp;
                                                                                                                                                            end
                                                                                                                                                            
                                                                                                                                                            code[x_, y_, z_, t_, a_] := If[LessEqual[N[(N[(z - t), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision], 1.7911263122038114e-38], N[(x * 1.0), $MachinePrecision], N[(x + y), $MachinePrecision]]
                                                                                                                                                            
                                                                                                                                                            f(x, y, z, t, a):
                                                                                                                                                            	x in [-inf, +inf],
                                                                                                                                                            	y in [-inf, +inf],
                                                                                                                                                            	z in [-inf, +inf],
                                                                                                                                                            	t in [-inf, +inf],
                                                                                                                                                            	a in [-inf, +inf]
                                                                                                                                                            code: THEORY
                                                                                                                                                            BEGIN
                                                                                                                                                            f(x, y, z, t, a: real): real =
                                                                                                                                                            	LET tmp = IF (((z - t) / (a - t)) <= (17911263122038113614022299391481853749243922013103198506950602435491052738411005562298008890597810112421672812388351303525269031524658203125e-177)) THEN (x * (1)) ELSE (x + y) ENDIF IN
                                                                                                                                                            	tmp
                                                                                                                                                            END code
                                                                                                                                                            \begin{array}{l}
                                                                                                                                                            \mathbf{if}\;\frac{z - t}{a - t} \leq 1.7911263122038114 \cdot 10^{-38}:\\
                                                                                                                                                            \;\;\;\;x \cdot 1\\
                                                                                                                                                            
                                                                                                                                                            \mathbf{else}:\\
                                                                                                                                                            \;\;\;\;x + y\\
                                                                                                                                                            
                                                                                                                                                            
                                                                                                                                                            \end{array}
                                                                                                                                                            
                                                                                                                                                            Derivation
                                                                                                                                                            1. Split input into 2 regimes
                                                                                                                                                            2. if (/.f64 (-.f64 z t) (-.f64 a t)) < 1.7911263122038114e-38

                                                                                                                                                              1. Initial program 98.1%

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

                                                                                                                                                                \[\leadsto x \cdot \left(1 + \frac{y \cdot \left(z - t\right)}{x \cdot \left(a - t\right)}\right) \]
                                                                                                                                                              3. Step-by-step derivation
                                                                                                                                                                1. Applied rewrites79.3%

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

                                                                                                                                                                  \[\leadsto x \cdot 1 \]
                                                                                                                                                                3. Step-by-step derivation
                                                                                                                                                                  1. Applied rewrites51.3%

                                                                                                                                                                    \[\leadsto x \cdot 1 \]

                                                                                                                                                                  if 1.7911263122038114e-38 < (/.f64 (-.f64 z t) (-.f64 a t))

                                                                                                                                                                  1. Initial program 98.1%

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

                                                                                                                                                                    \[\leadsto x + y \]
                                                                                                                                                                  3. Step-by-step derivation
                                                                                                                                                                    1. Applied rewrites61.3%

                                                                                                                                                                      \[\leadsto x + y \]
                                                                                                                                                                  4. Recombined 2 regimes into one program.
                                                                                                                                                                  5. Add Preprocessing

                                                                                                                                                                  Alternative 14: 61.3% accurate, 4.3× speedup?

                                                                                                                                                                  \[x + y \]
                                                                                                                                                                  (FPCore (x y z t a)
                                                                                                                                                                    :precision binary64
                                                                                                                                                                    :pre TRUE
                                                                                                                                                                    (+ x y))
                                                                                                                                                                  double code(double x, double y, double z, double t, double a) {
                                                                                                                                                                  	return x + y;
                                                                                                                                                                  }
                                                                                                                                                                  
                                                                                                                                                                  real(8) function code(x, y, z, t, a)
                                                                                                                                                                  use fmin_fmax_functions
                                                                                                                                                                      real(8), intent (in) :: x
                                                                                                                                                                      real(8), intent (in) :: y
                                                                                                                                                                      real(8), intent (in) :: z
                                                                                                                                                                      real(8), intent (in) :: t
                                                                                                                                                                      real(8), intent (in) :: a
                                                                                                                                                                      code = x + y
                                                                                                                                                                  end function
                                                                                                                                                                  
                                                                                                                                                                  public static double code(double x, double y, double z, double t, double a) {
                                                                                                                                                                  	return x + y;
                                                                                                                                                                  }
                                                                                                                                                                  
                                                                                                                                                                  def code(x, y, z, t, a):
                                                                                                                                                                  	return x + y
                                                                                                                                                                  
                                                                                                                                                                  function code(x, y, z, t, a)
                                                                                                                                                                  	return Float64(x + y)
                                                                                                                                                                  end
                                                                                                                                                                  
                                                                                                                                                                  function tmp = code(x, y, z, t, a)
                                                                                                                                                                  	tmp = x + y;
                                                                                                                                                                  end
                                                                                                                                                                  
                                                                                                                                                                  code[x_, y_, z_, t_, a_] := N[(x + y), $MachinePrecision]
                                                                                                                                                                  
                                                                                                                                                                  f(x, y, z, t, a):
                                                                                                                                                                  	x in [-inf, +inf],
                                                                                                                                                                  	y in [-inf, +inf],
                                                                                                                                                                  	z in [-inf, +inf],
                                                                                                                                                                  	t in [-inf, +inf],
                                                                                                                                                                  	a in [-inf, +inf]
                                                                                                                                                                  code: THEORY
                                                                                                                                                                  BEGIN
                                                                                                                                                                  f(x, y, z, t, a: real): real =
                                                                                                                                                                  	x + y
                                                                                                                                                                  END code
                                                                                                                                                                  x + y
                                                                                                                                                                  
                                                                                                                                                                  Derivation
                                                                                                                                                                  1. Initial program 98.1%

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

                                                                                                                                                                    \[\leadsto x + y \]
                                                                                                                                                                  3. Step-by-step derivation
                                                                                                                                                                    1. Applied rewrites61.3%

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

                                                                                                                                                                    Alternative 15: 18.7% accurate, 15.6× speedup?

                                                                                                                                                                    \[y \]
                                                                                                                                                                    (FPCore (x y z t a)
                                                                                                                                                                      :precision binary64
                                                                                                                                                                      :pre TRUE
                                                                                                                                                                      y)
                                                                                                                                                                    double code(double x, double y, double z, double t, double a) {
                                                                                                                                                                    	return y;
                                                                                                                                                                    }
                                                                                                                                                                    
                                                                                                                                                                    real(8) function code(x, y, z, t, a)
                                                                                                                                                                    use fmin_fmax_functions
                                                                                                                                                                        real(8), intent (in) :: x
                                                                                                                                                                        real(8), intent (in) :: y
                                                                                                                                                                        real(8), intent (in) :: z
                                                                                                                                                                        real(8), intent (in) :: t
                                                                                                                                                                        real(8), intent (in) :: a
                                                                                                                                                                        code = y
                                                                                                                                                                    end function
                                                                                                                                                                    
                                                                                                                                                                    public static double code(double x, double y, double z, double t, double a) {
                                                                                                                                                                    	return y;
                                                                                                                                                                    }
                                                                                                                                                                    
                                                                                                                                                                    def code(x, y, z, t, a):
                                                                                                                                                                    	return y
                                                                                                                                                                    
                                                                                                                                                                    function code(x, y, z, t, a)
                                                                                                                                                                    	return y
                                                                                                                                                                    end
                                                                                                                                                                    
                                                                                                                                                                    function tmp = code(x, y, z, t, a)
                                                                                                                                                                    	tmp = y;
                                                                                                                                                                    end
                                                                                                                                                                    
                                                                                                                                                                    code[x_, y_, z_, t_, a_] := y
                                                                                                                                                                    
                                                                                                                                                                    f(x, y, z, t, a):
                                                                                                                                                                    	x in [-inf, +inf],
                                                                                                                                                                    	y in [-inf, +inf],
                                                                                                                                                                    	z in [-inf, +inf],
                                                                                                                                                                    	t in [-inf, +inf],
                                                                                                                                                                    	a in [-inf, +inf]
                                                                                                                                                                    code: THEORY
                                                                                                                                                                    BEGIN
                                                                                                                                                                    f(x, y, z, t, a: real): real =
                                                                                                                                                                    	y
                                                                                                                                                                    END code
                                                                                                                                                                    y
                                                                                                                                                                    
                                                                                                                                                                    Derivation
                                                                                                                                                                    1. Initial program 98.1%

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

                                                                                                                                                                      \[\leadsto x + y \]
                                                                                                                                                                    3. Step-by-step derivation
                                                                                                                                                                      1. Applied rewrites61.3%

                                                                                                                                                                        \[\leadsto x + y \]
                                                                                                                                                                      2. Taylor expanded in x around 0

                                                                                                                                                                        \[\leadsto y \]
                                                                                                                                                                      3. Step-by-step derivation
                                                                                                                                                                        1. Applied rewrites18.7%

                                                                                                                                                                          \[\leadsto y \]
                                                                                                                                                                        2. Add Preprocessing

                                                                                                                                                                        Reproduce

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