Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, H

Percentage Accurate: 95.7% → 95.7%
Time: 6.6s
Alternatives: 12
Speedup: 1.4×

Specification

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

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

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

Herbie found 12 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 95.7% accurate, 1.0× speedup?

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

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

Alternative 1: 95.7% accurate, 1.3× speedup?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      \[\leadsto x - \frac{\color{blue}{y - \frac{t}{y}}}{z \cdot 3} \]
    13. lower-/.f6498.0

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

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

      \[\leadsto x - \frac{y - \frac{t}{y}}{\color{blue}{3 \cdot z}} \]
    16. lower-*.f6498.0

      \[\leadsto x - \frac{y - \frac{t}{y}}{\color{blue}{3 \cdot z}} \]
  4. Applied rewrites98.0%

    \[\leadsto \color{blue}{x - \frac{y - \frac{t}{y}}{3 \cdot z}} \]
  5. Add Preprocessing

Alternative 2: 92.2% accurate, 1.1× speedup?

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

\\
\begin{array}{l}
\mathbf{if}\;y \leq -3.3 \cdot 10^{+64}:\\
\;\;\;\;\mathsf{fma}\left(-y, \frac{0.3333333333333333}{z}, x\right)\\

\mathbf{elif}\;y \leq 5.8 \cdot 10^{+54}:\\
\;\;\;\;\mathsf{fma}\left(\frac{0.3333333333333333}{y}, \frac{t}{z}, x\right)\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if y < -3.29999999999999988e64

    1. Initial program 99.8%

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

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

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

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

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

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

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{t}{y}}{z}} - \frac{y}{z}, \frac{1}{3}, x\right) \]
      7. div-subN/A

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

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

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

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

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

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

        \[\leadsto \mathsf{fma}\left(-1 \cdot y, \frac{\color{blue}{\frac{1}{3}}}{z}, x\right) \]
      3. Step-by-step derivation
        1. Applied rewrites96.3%

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

        if -3.29999999999999988e64 < y < 5.7999999999999997e54

        1. Initial program 91.6%

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

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

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

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

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

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

            \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} + \color{blue}{x \cdot \frac{y}{y}} \]
          6. fp-cancel-sign-sub-invN/A

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

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

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

            \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{-1 \cdot x} \]
          10. metadata-evalN/A

            \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \cdot x \]
          11. fp-cancel-sign-sub-invN/A

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

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

            \[\leadsto \color{blue}{\frac{\frac{1}{3} \cdot t}{y \cdot z}} + x \]
          14. times-fracN/A

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

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

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

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

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

        if 5.7999999999999997e54 < y

        1. Initial program 99.8%

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

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

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

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

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

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

            \[\leadsto y \cdot \color{blue}{\frac{\frac{-1}{3} \cdot 1}{z}} + y \cdot \frac{x}{y} \]
          6. metadata-evalN/A

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

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

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

            \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z}} + y \cdot \frac{x}{y} \]
          10. fp-cancel-sign-subN/A

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

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

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

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

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

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

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

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

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

            \[\leadsto \frac{-1}{3} \cdot \frac{y}{z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right) \cdot x} \]
          20. fp-cancel-sign-sub-invN/A

            \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z} + 1 \cdot x} \]
          21. *-lft-identityN/A

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

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

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

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

      Alternative 3: 92.2% accurate, 1.1× speedup?

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

        1. Initial program 99.8%

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

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{t}{y}}{z}} - \frac{y}{z}, \frac{1}{3}, x\right) \]
          7. div-subN/A

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

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

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

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

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

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

            \[\leadsto \mathsf{fma}\left(-1 \cdot y, \frac{\color{blue}{\frac{1}{3}}}{z}, x\right) \]
          3. Step-by-step derivation
            1. Applied rewrites96.3%

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

            if -3.29999999999999988e64 < y < 5.7999999999999997e54

            1. Initial program 91.6%

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

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

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

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

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

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

                \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} + \color{blue}{x \cdot \frac{y}{y}} \]
              6. fp-cancel-sign-sub-invN/A

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

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

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

                \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{-1 \cdot x} \]
              10. metadata-evalN/A

                \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \cdot x \]
              11. fp-cancel-sign-sub-invN/A

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

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

                \[\leadsto \color{blue}{\frac{\frac{1}{3} \cdot t}{y \cdot z}} + x \]
              14. times-fracN/A

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

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

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

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

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

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

              if 5.7999999999999997e54 < y

              1. Initial program 99.8%

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

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

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

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

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

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

                  \[\leadsto y \cdot \color{blue}{\frac{\frac{-1}{3} \cdot 1}{z}} + y \cdot \frac{x}{y} \]
                6. metadata-evalN/A

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

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

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

                  \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z}} + y \cdot \frac{x}{y} \]
                10. fp-cancel-sign-subN/A

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

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

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

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

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

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

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

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

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

                  \[\leadsto \frac{-1}{3} \cdot \frac{y}{z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right) \cdot x} \]
                20. fp-cancel-sign-sub-invN/A

                  \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z} + 1 \cdot x} \]
                21. *-lft-identityN/A

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

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

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

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

            Alternative 4: 88.8% accurate, 1.2× speedup?

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

              1. Initial program 99.8%

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

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

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

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

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

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

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

                  \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{t}{y}}{z}} - \frac{y}{z}, \frac{1}{3}, x\right) \]
                7. div-subN/A

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

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

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

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

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

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

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

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

                  if -3.59999999999999995e80 < y < 5.7999999999999997e54

                  1. Initial program 91.7%

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

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

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

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

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

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

                      \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} + \color{blue}{x \cdot \frac{y}{y}} \]
                    6. fp-cancel-sign-sub-invN/A

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

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

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

                      \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{-1 \cdot x} \]
                    10. metadata-evalN/A

                      \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \cdot x \]
                    11. fp-cancel-sign-sub-invN/A

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

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

                      \[\leadsto \color{blue}{\frac{\frac{1}{3} \cdot t}{y \cdot z}} + x \]
                    14. times-fracN/A

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

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

                      \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{1}{3}}{y}}, \frac{t}{z}, x\right) \]
                    17. lower-/.f6489.0

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

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

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

                        \[\leadsto \mathsf{fma}\left(t, \color{blue}{\frac{0.3333333333333333}{z \cdot y}}, x\right) \]
                      2. Step-by-step derivation
                        1. Applied rewrites83.6%

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

                        if 5.7999999999999997e54 < y

                        1. Initial program 99.8%

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

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

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

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

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

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

                            \[\leadsto y \cdot \color{blue}{\frac{\frac{-1}{3} \cdot 1}{z}} + y \cdot \frac{x}{y} \]
                          6. metadata-evalN/A

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

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

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

                            \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z}} + y \cdot \frac{x}{y} \]
                          10. fp-cancel-sign-subN/A

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

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

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

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

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

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

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

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

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

                            \[\leadsto \frac{-1}{3} \cdot \frac{y}{z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right) \cdot x} \]
                          20. fp-cancel-sign-sub-invN/A

                            \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z} + 1 \cdot x} \]
                          21. *-lft-identityN/A

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

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

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

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

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

                      Alternative 5: 88.8% accurate, 1.3× speedup?

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

                        1. Initial program 99.8%

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

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

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

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

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

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

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

                            \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{t}{y}}{z}} - \frac{y}{z}, \frac{1}{3}, x\right) \]
                          7. div-subN/A

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

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

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

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

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

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

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

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

                            if -3.59999999999999995e80 < y < 5.7999999999999997e54

                            1. Initial program 91.7%

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

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

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

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

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

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

                                \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} + \color{blue}{x \cdot \frac{y}{y}} \]
                              6. fp-cancel-sign-sub-invN/A

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

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

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

                                \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{-1 \cdot x} \]
                              10. metadata-evalN/A

                                \[\leadsto \frac{1}{3} \cdot \frac{t}{y \cdot z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \cdot x \]
                              11. fp-cancel-sign-sub-invN/A

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

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

                                \[\leadsto \color{blue}{\frac{\frac{1}{3} \cdot t}{y \cdot z}} + x \]
                              14. times-fracN/A

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

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

                                \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{1}{3}}{y}}, \frac{t}{z}, x\right) \]
                              17. lower-/.f6489.0

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

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

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

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

                                if 5.7999999999999997e54 < y

                                1. Initial program 99.8%

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

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

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

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

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

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

                                    \[\leadsto y \cdot \color{blue}{\frac{\frac{-1}{3} \cdot 1}{z}} + y \cdot \frac{x}{y} \]
                                  6. metadata-evalN/A

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

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

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

                                    \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z}} + y \cdot \frac{x}{y} \]
                                  10. fp-cancel-sign-subN/A

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

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

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

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

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

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

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

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

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

                                    \[\leadsto \frac{-1}{3} \cdot \frac{y}{z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right) \cdot x} \]
                                  20. fp-cancel-sign-sub-invN/A

                                    \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z} + 1 \cdot x} \]
                                  21. *-lft-identityN/A

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

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

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

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

                              Alternative 6: 75.6% accurate, 1.3× speedup?

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

                                1. Initial program 96.9%

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

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

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

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

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

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

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

                                    \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{t}{y}}{z}} - \frac{y}{z}, \frac{1}{3}, x\right) \]
                                  7. div-subN/A

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

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

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

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

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

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

                                    \[\leadsto \mathsf{fma}\left(-1 \cdot y, \frac{\color{blue}{\frac{1}{3}}}{z}, x\right) \]
                                  3. Step-by-step derivation
                                    1. Applied rewrites76.6%

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

                                    if -6.49999999999999997e-182 < y < 3.7999999999999997e-95

                                    1. Initial program 87.7%

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

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

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

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

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

                                        \[\leadsto \frac{t}{\color{blue}{z \cdot y}} \cdot \frac{1}{3} \]
                                      5. lower-*.f6469.5

                                        \[\leadsto \frac{t}{\color{blue}{z \cdot y}} \cdot 0.3333333333333333 \]
                                    5. Applied rewrites69.5%

                                      \[\leadsto \color{blue}{\frac{t}{z \cdot y} \cdot 0.3333333333333333} \]
                                    6. Step-by-step derivation
                                      1. Applied rewrites69.5%

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

                                      if 3.7999999999999997e-95 < y

                                      1. Initial program 98.4%

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

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

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

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

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

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

                                          \[\leadsto y \cdot \color{blue}{\frac{\frac{-1}{3} \cdot 1}{z}} + y \cdot \frac{x}{y} \]
                                        6. metadata-evalN/A

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

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

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

                                          \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z}} + y \cdot \frac{x}{y} \]
                                        10. fp-cancel-sign-subN/A

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

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

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

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

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

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

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

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

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

                                          \[\leadsto \frac{-1}{3} \cdot \frac{y}{z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right) \cdot x} \]
                                        20. fp-cancel-sign-sub-invN/A

                                          \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z} + 1 \cdot x} \]
                                        21. *-lft-identityN/A

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

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

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

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

                                    Alternative 7: 95.6% accurate, 1.4× speedup?

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

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

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

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

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

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

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

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

                                        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{t}{y}}{z}} - \frac{y}{z}, \frac{1}{3}, x\right) \]
                                      7. div-subN/A

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

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

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

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

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

                                    Alternative 8: 95.7% accurate, 1.4× speedup?

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

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

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

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

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

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

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

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

                                        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\frac{t}{y}}{z}} - \frac{y}{z}, \frac{1}{3}, x\right) \]
                                      7. div-subN/A

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

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

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

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

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

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

                                      Alternative 9: 47.7% accurate, 1.5× speedup?

                                      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -6.5 \cdot 10^{-22} \lor \neg \left(x \leq 1.45 \cdot 10^{+48}\right):\\ \;\;\;\;1 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{-0.3333333333333333 \cdot y}{z}\\ \end{array} \end{array} \]
                                      (FPCore (x y z t)
                                       :precision binary64
                                       (if (or (<= x -6.5e-22) (not (<= x 1.45e+48)))
                                         (* 1.0 x)
                                         (/ (* -0.3333333333333333 y) z)))
                                      double code(double x, double y, double z, double t) {
                                      	double tmp;
                                      	if ((x <= -6.5e-22) || !(x <= 1.45e+48)) {
                                      		tmp = 1.0 * x;
                                      	} else {
                                      		tmp = (-0.3333333333333333 * y) / z;
                                      	}
                                      	return tmp;
                                      }
                                      
                                      real(8) function code(x, y, z, t)
                                          real(8), intent (in) :: x
                                          real(8), intent (in) :: y
                                          real(8), intent (in) :: z
                                          real(8), intent (in) :: t
                                          real(8) :: tmp
                                          if ((x <= (-6.5d-22)) .or. (.not. (x <= 1.45d+48))) then
                                              tmp = 1.0d0 * x
                                          else
                                              tmp = ((-0.3333333333333333d0) * y) / z
                                          end if
                                          code = tmp
                                      end function
                                      
                                      public static double code(double x, double y, double z, double t) {
                                      	double tmp;
                                      	if ((x <= -6.5e-22) || !(x <= 1.45e+48)) {
                                      		tmp = 1.0 * x;
                                      	} else {
                                      		tmp = (-0.3333333333333333 * y) / z;
                                      	}
                                      	return tmp;
                                      }
                                      
                                      def code(x, y, z, t):
                                      	tmp = 0
                                      	if (x <= -6.5e-22) or not (x <= 1.45e+48):
                                      		tmp = 1.0 * x
                                      	else:
                                      		tmp = (-0.3333333333333333 * y) / z
                                      	return tmp
                                      
                                      function code(x, y, z, t)
                                      	tmp = 0.0
                                      	if ((x <= -6.5e-22) || !(x <= 1.45e+48))
                                      		tmp = Float64(1.0 * x);
                                      	else
                                      		tmp = Float64(Float64(-0.3333333333333333 * y) / z);
                                      	end
                                      	return tmp
                                      end
                                      
                                      function tmp_2 = code(x, y, z, t)
                                      	tmp = 0.0;
                                      	if ((x <= -6.5e-22) || ~((x <= 1.45e+48)))
                                      		tmp = 1.0 * x;
                                      	else
                                      		tmp = (-0.3333333333333333 * y) / z;
                                      	end
                                      	tmp_2 = tmp;
                                      end
                                      
                                      code[x_, y_, z_, t_] := If[Or[LessEqual[x, -6.5e-22], N[Not[LessEqual[x, 1.45e+48]], $MachinePrecision]], N[(1.0 * x), $MachinePrecision], N[(N[(-0.3333333333333333 * y), $MachinePrecision] / z), $MachinePrecision]]
                                      
                                      \begin{array}{l}
                                      
                                      \\
                                      \begin{array}{l}
                                      \mathbf{if}\;x \leq -6.5 \cdot 10^{-22} \lor \neg \left(x \leq 1.45 \cdot 10^{+48}\right):\\
                                      \;\;\;\;1 \cdot x\\
                                      
                                      \mathbf{else}:\\
                                      \;\;\;\;\frac{-0.3333333333333333 \cdot y}{z}\\
                                      
                                      
                                      \end{array}
                                      \end{array}
                                      
                                      Derivation
                                      1. Split input into 2 regimes
                                      2. if x < -6.50000000000000043e-22 or 1.4499999999999999e48 < x

                                        1. Initial program 95.3%

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

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

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

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

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

                                          \[\leadsto 1 \cdot x \]
                                        7. Step-by-step derivation
                                          1. Applied rewrites55.0%

                                            \[\leadsto 1 \cdot x \]

                                          if -6.50000000000000043e-22 < x < 1.4499999999999999e48

                                          1. Initial program 94.6%

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

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

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

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

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

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

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

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

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

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

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

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

                                              \[\leadsto x - \frac{\color{blue}{y - \frac{t}{y}}}{z \cdot 3} \]
                                            13. lower-/.f6499.1

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

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

                                              \[\leadsto x - \frac{y - \frac{t}{y}}{\color{blue}{3 \cdot z}} \]
                                            16. lower-*.f6499.1

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

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

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

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

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

                                              \[\leadsto x - \color{blue}{\frac{\frac{y - \frac{t}{y}}{3}}{z}} \]
                                            5. lower-/.f6499.0

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

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

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

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

                                              \[\leadsto \color{blue}{\frac{y}{z} \cdot \frac{-1}{3}} \]
                                            3. lower-/.f6446.5

                                              \[\leadsto \color{blue}{\frac{y}{z}} \cdot -0.3333333333333333 \]
                                          9. Applied rewrites46.5%

                                            \[\leadsto \color{blue}{\frac{y}{z} \cdot -0.3333333333333333} \]
                                          10. Step-by-step derivation
                                            1. Applied rewrites46.5%

                                              \[\leadsto \frac{-0.3333333333333333 \cdot y}{\color{blue}{z}} \]
                                          11. Recombined 2 regimes into one program.
                                          12. Final simplification50.6%

                                            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -6.5 \cdot 10^{-22} \lor \neg \left(x \leq 1.45 \cdot 10^{+48}\right):\\ \;\;\;\;1 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{-0.3333333333333333 \cdot y}{z}\\ \end{array} \]
                                          13. Add Preprocessing

                                          Alternative 10: 47.7% accurate, 1.5× speedup?

                                          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -6.5 \cdot 10^{-22} \lor \neg \left(x \leq 1.45 \cdot 10^{+48}\right):\\ \;\;\;\;1 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{z} \cdot -0.3333333333333333\\ \end{array} \end{array} \]
                                          (FPCore (x y z t)
                                           :precision binary64
                                           (if (or (<= x -6.5e-22) (not (<= x 1.45e+48)))
                                             (* 1.0 x)
                                             (* (/ y z) -0.3333333333333333)))
                                          double code(double x, double y, double z, double t) {
                                          	double tmp;
                                          	if ((x <= -6.5e-22) || !(x <= 1.45e+48)) {
                                          		tmp = 1.0 * x;
                                          	} else {
                                          		tmp = (y / z) * -0.3333333333333333;
                                          	}
                                          	return tmp;
                                          }
                                          
                                          real(8) function code(x, y, z, t)
                                              real(8), intent (in) :: x
                                              real(8), intent (in) :: y
                                              real(8), intent (in) :: z
                                              real(8), intent (in) :: t
                                              real(8) :: tmp
                                              if ((x <= (-6.5d-22)) .or. (.not. (x <= 1.45d+48))) then
                                                  tmp = 1.0d0 * x
                                              else
                                                  tmp = (y / z) * (-0.3333333333333333d0)
                                              end if
                                              code = tmp
                                          end function
                                          
                                          public static double code(double x, double y, double z, double t) {
                                          	double tmp;
                                          	if ((x <= -6.5e-22) || !(x <= 1.45e+48)) {
                                          		tmp = 1.0 * x;
                                          	} else {
                                          		tmp = (y / z) * -0.3333333333333333;
                                          	}
                                          	return tmp;
                                          }
                                          
                                          def code(x, y, z, t):
                                          	tmp = 0
                                          	if (x <= -6.5e-22) or not (x <= 1.45e+48):
                                          		tmp = 1.0 * x
                                          	else:
                                          		tmp = (y / z) * -0.3333333333333333
                                          	return tmp
                                          
                                          function code(x, y, z, t)
                                          	tmp = 0.0
                                          	if ((x <= -6.5e-22) || !(x <= 1.45e+48))
                                          		tmp = Float64(1.0 * x);
                                          	else
                                          		tmp = Float64(Float64(y / z) * -0.3333333333333333);
                                          	end
                                          	return tmp
                                          end
                                          
                                          function tmp_2 = code(x, y, z, t)
                                          	tmp = 0.0;
                                          	if ((x <= -6.5e-22) || ~((x <= 1.45e+48)))
                                          		tmp = 1.0 * x;
                                          	else
                                          		tmp = (y / z) * -0.3333333333333333;
                                          	end
                                          	tmp_2 = tmp;
                                          end
                                          
                                          code[x_, y_, z_, t_] := If[Or[LessEqual[x, -6.5e-22], N[Not[LessEqual[x, 1.45e+48]], $MachinePrecision]], N[(1.0 * x), $MachinePrecision], N[(N[(y / z), $MachinePrecision] * -0.3333333333333333), $MachinePrecision]]
                                          
                                          \begin{array}{l}
                                          
                                          \\
                                          \begin{array}{l}
                                          \mathbf{if}\;x \leq -6.5 \cdot 10^{-22} \lor \neg \left(x \leq 1.45 \cdot 10^{+48}\right):\\
                                          \;\;\;\;1 \cdot x\\
                                          
                                          \mathbf{else}:\\
                                          \;\;\;\;\frac{y}{z} \cdot -0.3333333333333333\\
                                          
                                          
                                          \end{array}
                                          \end{array}
                                          
                                          Derivation
                                          1. Split input into 2 regimes
                                          2. if x < -6.50000000000000043e-22 or 1.4499999999999999e48 < x

                                            1. Initial program 95.3%

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

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

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

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

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

                                              \[\leadsto 1 \cdot x \]
                                            7. Step-by-step derivation
                                              1. Applied rewrites55.0%

                                                \[\leadsto 1 \cdot x \]

                                              if -6.50000000000000043e-22 < x < 1.4499999999999999e48

                                              1. Initial program 94.6%

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

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

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

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

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

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

                                                  \[\leadsto y \cdot \color{blue}{\frac{\frac{-1}{3} \cdot 1}{z}} + y \cdot \frac{x}{y} \]
                                                6. metadata-evalN/A

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

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

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

                                                  \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z}} + y \cdot \frac{x}{y} \]
                                                10. fp-cancel-sign-subN/A

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

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

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

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

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

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

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

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

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

                                                  \[\leadsto \frac{-1}{3} \cdot \frac{y}{z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right) \cdot x} \]
                                                20. fp-cancel-sign-sub-invN/A

                                                  \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z} + 1 \cdot x} \]
                                                21. *-lft-identityN/A

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

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

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

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

                                                \[\leadsto \frac{-1}{3} \cdot \color{blue}{\frac{y}{z}} \]
                                              7. Step-by-step derivation
                                                1. Applied rewrites46.5%

                                                  \[\leadsto \frac{y}{z} \cdot \color{blue}{-0.3333333333333333} \]
                                              8. Recombined 2 regimes into one program.
                                              9. Final simplification50.6%

                                                \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -6.5 \cdot 10^{-22} \lor \neg \left(x \leq 1.45 \cdot 10^{+48}\right):\\ \;\;\;\;1 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{z} \cdot -0.3333333333333333\\ \end{array} \]
                                              10. Add Preprocessing

                                              Alternative 11: 63.7% accurate, 2.4× speedup?

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

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

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

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

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

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

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

                                                  \[\leadsto y \cdot \color{blue}{\frac{\frac{-1}{3} \cdot 1}{z}} + y \cdot \frac{x}{y} \]
                                                6. metadata-evalN/A

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

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

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

                                                  \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z}} + y \cdot \frac{x}{y} \]
                                                10. fp-cancel-sign-subN/A

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

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

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

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

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

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

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

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

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

                                                  \[\leadsto \frac{-1}{3} \cdot \frac{y}{z} - \color{blue}{\left(\mathsf{neg}\left(1\right)\right) \cdot x} \]
                                                20. fp-cancel-sign-sub-invN/A

                                                  \[\leadsto \color{blue}{\frac{-1}{3} \cdot \frac{y}{z} + 1 \cdot x} \]
                                                21. *-lft-identityN/A

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

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

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

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

                                              Alternative 12: 30.3% accurate, 7.3× speedup?

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

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

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

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

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

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

                                                \[\leadsto 1 \cdot x \]
                                              7. Step-by-step derivation
                                                1. Applied rewrites32.0%

                                                  \[\leadsto 1 \cdot x \]
                                                2. Add Preprocessing

                                                Developer Target 1: 95.9% accurate, 0.9× speedup?

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

                                                Reproduce

                                                ?
                                                herbie shell --seed 2024327 
                                                (FPCore (x y z t)
                                                  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, H"
                                                  :precision binary64
                                                
                                                  :alt
                                                  (! :herbie-platform default (+ (- x (/ y (* z 3))) (/ (/ t (* z 3)) y)))
                                                
                                                  (+ (- x (/ y (* z 3.0))) (/ t (* (* z 3.0) y))))