Rosa's DopplerBench

Percentage Accurate: 73.0% → 97.9%
Time: 10.7s
Alternatives: 7
Speedup: 0.9×

Specification

?
\[\begin{array}{l} \\ \frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \end{array} \]
(FPCore (u v t1) :precision binary64 (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))
double code(double u, double v, double t1) {
	return (-t1 * v) / ((t1 + u) * (t1 + u));
}
real(8) function code(u, v, t1)
    real(8), intent (in) :: u
    real(8), intent (in) :: v
    real(8), intent (in) :: t1
    code = (-t1 * v) / ((t1 + u) * (t1 + u))
end function
public static double code(double u, double v, double t1) {
	return (-t1 * v) / ((t1 + u) * (t1 + u));
}
def code(u, v, t1):
	return (-t1 * v) / ((t1 + u) * (t1 + u))
function code(u, v, t1)
	return Float64(Float64(Float64(-t1) * v) / Float64(Float64(t1 + u) * Float64(t1 + u)))
end
function tmp = code(u, v, t1)
	tmp = (-t1 * v) / ((t1 + u) * (t1 + u));
end
code[u_, v_, t1_] := N[(N[((-t1) * v), $MachinePrecision] / N[(N[(t1 + u), $MachinePrecision] * N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}
\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 7 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: 73.0% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \end{array} \]
(FPCore (u v t1) :precision binary64 (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))
double code(double u, double v, double t1) {
	return (-t1 * v) / ((t1 + u) * (t1 + u));
}
real(8) function code(u, v, t1)
    real(8), intent (in) :: u
    real(8), intent (in) :: v
    real(8), intent (in) :: t1
    code = (-t1 * v) / ((t1 + u) * (t1 + u))
end function
public static double code(double u, double v, double t1) {
	return (-t1 * v) / ((t1 + u) * (t1 + u));
}
def code(u, v, t1):
	return (-t1 * v) / ((t1 + u) * (t1 + u))
function code(u, v, t1)
	return Float64(Float64(Float64(-t1) * v) / Float64(Float64(t1 + u) * Float64(t1 + u)))
end
function tmp = code(u, v, t1)
	tmp = (-t1 * v) / ((t1 + u) * (t1 + u));
end
code[u_, v_, t1_] := N[(N[((-t1) * v), $MachinePrecision] / N[(N[(t1 + u), $MachinePrecision] * N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}
\end{array}

Alternative 1: 97.9% accurate, 0.9× speedup?

\[\begin{array}{l} \\ \frac{t1}{t1 + u} \cdot \left(0 - \frac{v}{t1 + u}\right) \end{array} \]
(FPCore (u v t1)
 :precision binary64
 (* (/ t1 (+ t1 u)) (- 0.0 (/ v (+ t1 u)))))
double code(double u, double v, double t1) {
	return (t1 / (t1 + u)) * (0.0 - (v / (t1 + u)));
}
real(8) function code(u, v, t1)
    real(8), intent (in) :: u
    real(8), intent (in) :: v
    real(8), intent (in) :: t1
    code = (t1 / (t1 + u)) * (0.0d0 - (v / (t1 + u)))
end function
public static double code(double u, double v, double t1) {
	return (t1 / (t1 + u)) * (0.0 - (v / (t1 + u)));
}
def code(u, v, t1):
	return (t1 / (t1 + u)) * (0.0 - (v / (t1 + u)))
function code(u, v, t1)
	return Float64(Float64(t1 / Float64(t1 + u)) * Float64(0.0 - Float64(v / Float64(t1 + u))))
end
function tmp = code(u, v, t1)
	tmp = (t1 / (t1 + u)) * (0.0 - (v / (t1 + u)));
end
code[u_, v_, t1_] := N[(N[(t1 / N[(t1 + u), $MachinePrecision]), $MachinePrecision] * N[(0.0 - N[(v / N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{t1}{t1 + u} \cdot \left(0 - \frac{v}{t1 + u}\right)
\end{array}
Derivation
  1. Initial program 75.0%

    \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. *-commutativeN/A

      \[\leadsto \frac{v \cdot \left(\mathsf{neg}\left(t1\right)\right)}{\color{blue}{\left(t1 + u\right)} \cdot \left(t1 + u\right)} \]
    2. times-fracN/A

      \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\frac{\mathsf{neg}\left(t1\right)}{t1 + u}} \]
    3. clear-numN/A

      \[\leadsto \frac{v}{t1 + u} \cdot \frac{1}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
    4. un-div-invN/A

      \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
    5. /-lowering-/.f64N/A

      \[\leadsto \mathsf{/.f64}\left(\left(\frac{v}{t1 + u}\right), \color{blue}{\left(\frac{t1 + u}{\mathsf{neg}\left(t1\right)}\right)}\right) \]
    6. /-lowering-/.f64N/A

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(t1 + u\right)\right), \left(\frac{\color{blue}{t1 + u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
    7. +-lowering-+.f64N/A

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{t1 + \color{blue}{u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
    8. frac-2negN/A

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(t1\right)\right)\right)}}\right)\right) \]
    9. remove-double-negN/A

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}\right)\right) \]
    10. /-lowering-/.f64N/A

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right), \color{blue}{t1}\right)\right) \]
    11. neg-sub0N/A

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(0 - \left(t1 + u\right)\right), t1\right)\right) \]
    12. --lowering--.f64N/A

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 + u\right)\right), t1\right)\right) \]
    13. +-lowering-+.f6498.0%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right), t1\right)\right) \]
  4. Applied egg-rr98.0%

    \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{0 - \left(t1 + u\right)}{t1}}} \]
  5. Step-by-step derivation
    1. clear-numN/A

      \[\leadsto \frac{1}{\color{blue}{\frac{\frac{0 - \left(t1 + u\right)}{t1}}{\frac{v}{t1 + u}}}} \]
    2. associate-/r/N/A

      \[\leadsto \frac{1}{\frac{0 - \left(t1 + u\right)}{t1}} \cdot \color{blue}{\frac{v}{t1 + u}} \]
    3. clear-numN/A

      \[\leadsto \frac{t1}{0 - \left(t1 + u\right)} \cdot \frac{\color{blue}{v}}{t1 + u} \]
    4. sub0-negN/A

      \[\leadsto \frac{t1}{\mathsf{neg}\left(\left(t1 + u\right)\right)} \cdot \frac{v}{t1 + u} \]
    5. distribute-frac-neg2N/A

      \[\leadsto \left(\mathsf{neg}\left(\frac{t1}{t1 + u}\right)\right) \cdot \frac{\color{blue}{v}}{t1 + u} \]
    6. distribute-lft-neg-outN/A

      \[\leadsto \mathsf{neg}\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right) \]
    7. neg-lowering-neg.f64N/A

      \[\leadsto \mathsf{neg.f64}\left(\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right)\right) \]
    8. *-lowering-*.f64N/A

      \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\left(\frac{t1}{t1 + u}\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
    9. /-lowering-/.f64N/A

      \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \left(t1 + u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
    10. +-lowering-+.f64N/A

      \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
    11. /-lowering-/.f64N/A

      \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \left(t1 + u\right)\right)\right)\right) \]
    12. +-lowering-+.f6498.1%

      \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right)\right)\right) \]
  6. Applied egg-rr98.1%

    \[\leadsto \color{blue}{-\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
  7. Final simplification98.1%

    \[\leadsto \frac{t1}{t1 + u} \cdot \left(0 - \frac{v}{t1 + u}\right) \]
  8. Add Preprocessing

Alternative 2: 76.7% accurate, 0.6× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;t1 \leq -8.2 \cdot 10^{-165}:\\ \;\;\;\;\frac{\frac{t1}{\frac{t1 + u}{v}}}{0 - t1}\\ \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\ \;\;\;\;\frac{0 - \frac{t1}{u}}{\frac{u}{v}}\\ \mathbf{else}:\\ \;\;\;\;0 - \frac{v}{t1 + u}\\ \end{array} \end{array} \]
(FPCore (u v t1)
 :precision binary64
 (if (<= t1 -8.2e-165)
   (/ (/ t1 (/ (+ t1 u) v)) (- 0.0 t1))
   (if (<= t1 9.5e+65) (/ (- 0.0 (/ t1 u)) (/ u v)) (- 0.0 (/ v (+ t1 u))))))
double code(double u, double v, double t1) {
	double tmp;
	if (t1 <= -8.2e-165) {
		tmp = (t1 / ((t1 + u) / v)) / (0.0 - t1);
	} else if (t1 <= 9.5e+65) {
		tmp = (0.0 - (t1 / u)) / (u / v);
	} else {
		tmp = 0.0 - (v / (t1 + u));
	}
	return tmp;
}
real(8) function code(u, v, t1)
    real(8), intent (in) :: u
    real(8), intent (in) :: v
    real(8), intent (in) :: t1
    real(8) :: tmp
    if (t1 <= (-8.2d-165)) then
        tmp = (t1 / ((t1 + u) / v)) / (0.0d0 - t1)
    else if (t1 <= 9.5d+65) then
        tmp = (0.0d0 - (t1 / u)) / (u / v)
    else
        tmp = 0.0d0 - (v / (t1 + u))
    end if
    code = tmp
end function
public static double code(double u, double v, double t1) {
	double tmp;
	if (t1 <= -8.2e-165) {
		tmp = (t1 / ((t1 + u) / v)) / (0.0 - t1);
	} else if (t1 <= 9.5e+65) {
		tmp = (0.0 - (t1 / u)) / (u / v);
	} else {
		tmp = 0.0 - (v / (t1 + u));
	}
	return tmp;
}
def code(u, v, t1):
	tmp = 0
	if t1 <= -8.2e-165:
		tmp = (t1 / ((t1 + u) / v)) / (0.0 - t1)
	elif t1 <= 9.5e+65:
		tmp = (0.0 - (t1 / u)) / (u / v)
	else:
		tmp = 0.0 - (v / (t1 + u))
	return tmp
function code(u, v, t1)
	tmp = 0.0
	if (t1 <= -8.2e-165)
		tmp = Float64(Float64(t1 / Float64(Float64(t1 + u) / v)) / Float64(0.0 - t1));
	elseif (t1 <= 9.5e+65)
		tmp = Float64(Float64(0.0 - Float64(t1 / u)) / Float64(u / v));
	else
		tmp = Float64(0.0 - Float64(v / Float64(t1 + u)));
	end
	return tmp
end
function tmp_2 = code(u, v, t1)
	tmp = 0.0;
	if (t1 <= -8.2e-165)
		tmp = (t1 / ((t1 + u) / v)) / (0.0 - t1);
	elseif (t1 <= 9.5e+65)
		tmp = (0.0 - (t1 / u)) / (u / v);
	else
		tmp = 0.0 - (v / (t1 + u));
	end
	tmp_2 = tmp;
end
code[u_, v_, t1_] := If[LessEqual[t1, -8.2e-165], N[(N[(t1 / N[(N[(t1 + u), $MachinePrecision] / v), $MachinePrecision]), $MachinePrecision] / N[(0.0 - t1), $MachinePrecision]), $MachinePrecision], If[LessEqual[t1, 9.5e+65], N[(N[(0.0 - N[(t1 / u), $MachinePrecision]), $MachinePrecision] / N[(u / v), $MachinePrecision]), $MachinePrecision], N[(0.0 - N[(v / N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;t1 \leq -8.2 \cdot 10^{-165}:\\
\;\;\;\;\frac{\frac{t1}{\frac{t1 + u}{v}}}{0 - t1}\\

\mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\
\;\;\;\;\frac{0 - \frac{t1}{u}}{\frac{u}{v}}\\

\mathbf{else}:\\
\;\;\;\;0 - \frac{v}{t1 + u}\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if t1 < -8.2000000000000004e-165

    1. Initial program 70.7%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in t1 around inf

      \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(t1\right), v\right), \mathsf{*.f64}\left(\mathsf{+.f64}\left(t1, u\right), \color{blue}{t1}\right)\right) \]
    4. Step-by-step derivation
      1. Simplified61.5%

        \[\leadsto \frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \color{blue}{t1}} \]
      2. Step-by-step derivation
        1. associate-/r*N/A

          \[\leadsto \frac{\frac{\left(\mathsf{neg}\left(t1\right)\right) \cdot v}{t1 + u}}{\color{blue}{t1}} \]
        2. associate-/l*N/A

          \[\leadsto \frac{\left(\mathsf{neg}\left(t1\right)\right) \cdot \frac{v}{t1 + u}}{t1} \]
        3. distribute-lft-neg-inN/A

          \[\leadsto \frac{\mathsf{neg}\left(t1 \cdot \frac{v}{t1 + u}\right)}{t1} \]
        4. clear-numN/A

          \[\leadsto \frac{\mathsf{neg}\left(t1 \cdot \frac{1}{\frac{t1 + u}{v}}\right)}{t1} \]
        5. div-invN/A

          \[\leadsto \frac{\mathsf{neg}\left(\frac{t1}{\frac{t1 + u}{v}}\right)}{t1} \]
        6. distribute-frac-negN/A

          \[\leadsto \mathsf{neg}\left(\frac{\frac{t1}{\frac{t1 + u}{v}}}{t1}\right) \]
        7. neg-lowering-neg.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\left(\frac{\frac{t1}{\frac{t1 + u}{v}}}{t1}\right)\right) \]
        8. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{t1}{\frac{t1 + u}{v}}\right), t1\right)\right) \]
        9. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(t1, \left(\frac{t1 + u}{v}\right)\right), t1\right)\right) \]
        10. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{/.f64}\left(\left(t1 + u\right), v\right)\right), t1\right)\right) \]
        11. +-lowering-+.f6482.8%

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), v\right)\right), t1\right)\right) \]
      3. Applied egg-rr82.8%

        \[\leadsto \color{blue}{-\frac{\frac{t1}{\frac{t1 + u}{v}}}{t1}} \]

      if -8.2000000000000004e-165 < t1 < 9.5000000000000005e65

      1. Initial program 82.2%

        \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
      2. Add Preprocessing
      3. Taylor expanded in t1 around 0

        \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
      4. Step-by-step derivation
        1. associate-*r/N/A

          \[\leadsto \frac{-1 \cdot \left(t1 \cdot v\right)}{\color{blue}{{u}^{2}}} \]
        2. unpow2N/A

          \[\leadsto \frac{-1 \cdot \left(t1 \cdot v\right)}{u \cdot \color{blue}{u}} \]
        3. associate-/r*N/A

          \[\leadsto \frac{\frac{-1 \cdot \left(t1 \cdot v\right)}{u}}{\color{blue}{u}} \]
        4. /-lowering-/.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\left(\frac{-1 \cdot \left(t1 \cdot v\right)}{u}\right), \color{blue}{u}\right) \]
        5. /-lowering-/.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(-1 \cdot \left(t1 \cdot v\right)\right), u\right), u\right) \]
        6. mul-1-negN/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(\mathsf{neg}\left(t1 \cdot v\right)\right), u\right), u\right) \]
        7. neg-sub0N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(0 - t1 \cdot v\right), u\right), u\right) \]
        8. --lowering--.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 \cdot v\right)\right), u\right), u\right) \]
        9. *-lowering-*.f6479.9%

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(t1, v\right)\right), u\right), u\right) \]
      5. Simplified79.9%

        \[\leadsto \color{blue}{\frac{\frac{0 - t1 \cdot v}{u}}{u}} \]
      6. Step-by-step derivation
        1. sub0-negN/A

          \[\leadsto \mathsf{/.f64}\left(\left(\frac{\mathsf{neg}\left(t1 \cdot v\right)}{u}\right), u\right) \]
        2. distribute-frac-negN/A

          \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\frac{t1 \cdot v}{u}\right)\right), u\right) \]
        3. *-commutativeN/A

          \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\frac{v \cdot t1}{u}\right)\right), u\right) \]
        4. associate-/l*N/A

          \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(v \cdot \frac{t1}{u}\right)\right), u\right) \]
        5. distribute-rgt-neg-inN/A

          \[\leadsto \mathsf{/.f64}\left(\left(v \cdot \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)\right), u\right) \]
        6. *-lowering-*.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)\right), u\right) \]
        7. neg-lowering-neg.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \mathsf{neg.f64}\left(\left(\frac{t1}{u}\right)\right)\right), u\right) \]
        8. /-lowering-/.f6482.9%

          \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \mathsf{neg.f64}\left(\mathsf{/.f64}\left(t1, u\right)\right)\right), u\right) \]
      7. Applied egg-rr82.9%

        \[\leadsto \frac{\color{blue}{v \cdot \left(-\frac{t1}{u}\right)}}{u} \]
      8. Step-by-step derivation
        1. clear-numN/A

          \[\leadsto \frac{1}{\color{blue}{\frac{u}{v \cdot \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)}}} \]
        2. associate-/r*N/A

          \[\leadsto \frac{1}{\frac{\frac{u}{v}}{\color{blue}{\mathsf{neg}\left(\frac{t1}{u}\right)}}} \]
        3. clear-numN/A

          \[\leadsto \frac{\mathsf{neg}\left(\frac{t1}{u}\right)}{\color{blue}{\frac{u}{v}}} \]
        4. distribute-frac-negN/A

          \[\leadsto \mathsf{neg}\left(\frac{\frac{t1}{u}}{\frac{u}{v}}\right) \]
        5. neg-lowering-neg.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\left(\frac{\frac{t1}{u}}{\frac{u}{v}}\right)\right) \]
        6. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{t1}{u}\right), \left(\frac{u}{v}\right)\right)\right) \]
        7. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(t1, u\right), \left(\frac{u}{v}\right)\right)\right) \]
        8. /-lowering-/.f6485.8%

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(t1, u\right), \mathsf{/.f64}\left(u, v\right)\right)\right) \]
      9. Applied egg-rr85.8%

        \[\leadsto \color{blue}{-\frac{\frac{t1}{u}}{\frac{u}{v}}} \]

      if 9.5000000000000005e65 < t1

      1. Initial program 71.3%

        \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \frac{v \cdot \left(\mathsf{neg}\left(t1\right)\right)}{\color{blue}{\left(t1 + u\right)} \cdot \left(t1 + u\right)} \]
        2. times-fracN/A

          \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\frac{\mathsf{neg}\left(t1\right)}{t1 + u}} \]
        3. clear-numN/A

          \[\leadsto \frac{v}{t1 + u} \cdot \frac{1}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
        4. un-div-invN/A

          \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
        5. /-lowering-/.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\left(\frac{v}{t1 + u}\right), \color{blue}{\left(\frac{t1 + u}{\mathsf{neg}\left(t1\right)}\right)}\right) \]
        6. /-lowering-/.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(t1 + u\right)\right), \left(\frac{\color{blue}{t1 + u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
        7. +-lowering-+.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{t1 + \color{blue}{u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
        8. frac-2negN/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(t1\right)\right)\right)}}\right)\right) \]
        9. remove-double-negN/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}\right)\right) \]
        10. /-lowering-/.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right), \color{blue}{t1}\right)\right) \]
        11. neg-sub0N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(0 - \left(t1 + u\right)\right), t1\right)\right) \]
        12. --lowering--.f64N/A

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 + u\right)\right), t1\right)\right) \]
        13. +-lowering-+.f6499.9%

          \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right), t1\right)\right) \]
      4. Applied egg-rr99.9%

        \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{0 - \left(t1 + u\right)}{t1}}} \]
      5. Step-by-step derivation
        1. clear-numN/A

          \[\leadsto \frac{1}{\color{blue}{\frac{\frac{0 - \left(t1 + u\right)}{t1}}{\frac{v}{t1 + u}}}} \]
        2. associate-/r/N/A

          \[\leadsto \frac{1}{\frac{0 - \left(t1 + u\right)}{t1}} \cdot \color{blue}{\frac{v}{t1 + u}} \]
        3. clear-numN/A

          \[\leadsto \frac{t1}{0 - \left(t1 + u\right)} \cdot \frac{\color{blue}{v}}{t1 + u} \]
        4. sub0-negN/A

          \[\leadsto \frac{t1}{\mathsf{neg}\left(\left(t1 + u\right)\right)} \cdot \frac{v}{t1 + u} \]
        5. distribute-frac-neg2N/A

          \[\leadsto \left(\mathsf{neg}\left(\frac{t1}{t1 + u}\right)\right) \cdot \frac{\color{blue}{v}}{t1 + u} \]
        6. distribute-lft-neg-outN/A

          \[\leadsto \mathsf{neg}\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right) \]
        7. neg-lowering-neg.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right)\right) \]
        8. *-lowering-*.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\left(\frac{t1}{t1 + u}\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
        9. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \left(t1 + u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
        10. +-lowering-+.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
        11. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \left(t1 + u\right)\right)\right)\right) \]
        12. +-lowering-+.f64100.0%

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right)\right)\right) \]
      6. Applied egg-rr100.0%

        \[\leadsto \color{blue}{-\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
      7. Step-by-step derivation
        1. associate-*r/N/A

          \[\leadsto \mathsf{neg.f64}\left(\left(\frac{\frac{t1}{t1 + u} \cdot v}{t1 + u}\right)\right) \]
        2. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{t1}{t1 + u} \cdot v\right), \left(t1 + u\right)\right)\right) \]
        3. *-commutativeN/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{t1}{t1 + u}\right), \left(t1 + u\right)\right)\right) \]
        4. clear-numN/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{1}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
        5. un-div-invN/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{v}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
        6. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(\frac{t1 + u}{t1}\right)\right), \left(t1 + u\right)\right)\right) \]
        7. /-lowering-/.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\left(t1 + u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
        8. +-lowering-+.f64N/A

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
        9. +-lowering-+.f64100.0%

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
      8. Applied egg-rr100.0%

        \[\leadsto -\color{blue}{\frac{\frac{v}{\frac{t1 + u}{t1}}}{t1 + u}} \]
      9. Taylor expanded in t1 around inf

        \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\color{blue}{v}, \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
      10. Step-by-step derivation
        1. Simplified87.2%

          \[\leadsto -\frac{\color{blue}{v}}{t1 + u} \]
      11. Recombined 3 regimes into one program.
      12. Final simplification84.7%

        \[\leadsto \begin{array}{l} \mathbf{if}\;t1 \leq -8.2 \cdot 10^{-165}:\\ \;\;\;\;\frac{\frac{t1}{\frac{t1 + u}{v}}}{0 - t1}\\ \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\ \;\;\;\;\frac{0 - \frac{t1}{u}}{\frac{u}{v}}\\ \mathbf{else}:\\ \;\;\;\;0 - \frac{v}{t1 + u}\\ \end{array} \]
      13. Add Preprocessing

      Alternative 3: 76.8% accurate, 0.6× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_1 := 0 - \frac{v}{t1 + u}\\ \mathbf{if}\;t1 \leq -4.3 \cdot 10^{-138}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\ \;\;\;\;\frac{0 - \frac{t1}{u}}{\frac{u}{v}}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
      (FPCore (u v t1)
       :precision binary64
       (let* ((t_1 (- 0.0 (/ v (+ t1 u)))))
         (if (<= t1 -4.3e-138)
           t_1
           (if (<= t1 9.5e+65) (/ (- 0.0 (/ t1 u)) (/ u v)) t_1))))
      double code(double u, double v, double t1) {
      	double t_1 = 0.0 - (v / (t1 + u));
      	double tmp;
      	if (t1 <= -4.3e-138) {
      		tmp = t_1;
      	} else if (t1 <= 9.5e+65) {
      		tmp = (0.0 - (t1 / u)) / (u / v);
      	} else {
      		tmp = t_1;
      	}
      	return tmp;
      }
      
      real(8) function code(u, v, t1)
          real(8), intent (in) :: u
          real(8), intent (in) :: v
          real(8), intent (in) :: t1
          real(8) :: t_1
          real(8) :: tmp
          t_1 = 0.0d0 - (v / (t1 + u))
          if (t1 <= (-4.3d-138)) then
              tmp = t_1
          else if (t1 <= 9.5d+65) then
              tmp = (0.0d0 - (t1 / u)) / (u / v)
          else
              tmp = t_1
          end if
          code = tmp
      end function
      
      public static double code(double u, double v, double t1) {
      	double t_1 = 0.0 - (v / (t1 + u));
      	double tmp;
      	if (t1 <= -4.3e-138) {
      		tmp = t_1;
      	} else if (t1 <= 9.5e+65) {
      		tmp = (0.0 - (t1 / u)) / (u / v);
      	} else {
      		tmp = t_1;
      	}
      	return tmp;
      }
      
      def code(u, v, t1):
      	t_1 = 0.0 - (v / (t1 + u))
      	tmp = 0
      	if t1 <= -4.3e-138:
      		tmp = t_1
      	elif t1 <= 9.5e+65:
      		tmp = (0.0 - (t1 / u)) / (u / v)
      	else:
      		tmp = t_1
      	return tmp
      
      function code(u, v, t1)
      	t_1 = Float64(0.0 - Float64(v / Float64(t1 + u)))
      	tmp = 0.0
      	if (t1 <= -4.3e-138)
      		tmp = t_1;
      	elseif (t1 <= 9.5e+65)
      		tmp = Float64(Float64(0.0 - Float64(t1 / u)) / Float64(u / v));
      	else
      		tmp = t_1;
      	end
      	return tmp
      end
      
      function tmp_2 = code(u, v, t1)
      	t_1 = 0.0 - (v / (t1 + u));
      	tmp = 0.0;
      	if (t1 <= -4.3e-138)
      		tmp = t_1;
      	elseif (t1 <= 9.5e+65)
      		tmp = (0.0 - (t1 / u)) / (u / v);
      	else
      		tmp = t_1;
      	end
      	tmp_2 = tmp;
      end
      
      code[u_, v_, t1_] := Block[{t$95$1 = N[(0.0 - N[(v / N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t1, -4.3e-138], t$95$1, If[LessEqual[t1, 9.5e+65], N[(N[(0.0 - N[(t1 / u), $MachinePrecision]), $MachinePrecision] / N[(u / v), $MachinePrecision]), $MachinePrecision], t$95$1]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_1 := 0 - \frac{v}{t1 + u}\\
      \mathbf{if}\;t1 \leq -4.3 \cdot 10^{-138}:\\
      \;\;\;\;t\_1\\
      
      \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\
      \;\;\;\;\frac{0 - \frac{t1}{u}}{\frac{u}{v}}\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_1\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if t1 < -4.3e-138 or 9.5000000000000005e65 < t1

        1. Initial program 70.9%

          \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto \frac{v \cdot \left(\mathsf{neg}\left(t1\right)\right)}{\color{blue}{\left(t1 + u\right)} \cdot \left(t1 + u\right)} \]
          2. times-fracN/A

            \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\frac{\mathsf{neg}\left(t1\right)}{t1 + u}} \]
          3. clear-numN/A

            \[\leadsto \frac{v}{t1 + u} \cdot \frac{1}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
          4. un-div-invN/A

            \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
          5. /-lowering-/.f64N/A

            \[\leadsto \mathsf{/.f64}\left(\left(\frac{v}{t1 + u}\right), \color{blue}{\left(\frac{t1 + u}{\mathsf{neg}\left(t1\right)}\right)}\right) \]
          6. /-lowering-/.f64N/A

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(t1 + u\right)\right), \left(\frac{\color{blue}{t1 + u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
          7. +-lowering-+.f64N/A

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{t1 + \color{blue}{u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
          8. frac-2negN/A

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(t1\right)\right)\right)}}\right)\right) \]
          9. remove-double-negN/A

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}\right)\right) \]
          10. /-lowering-/.f64N/A

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right), \color{blue}{t1}\right)\right) \]
          11. neg-sub0N/A

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(0 - \left(t1 + u\right)\right), t1\right)\right) \]
          12. --lowering--.f64N/A

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 + u\right)\right), t1\right)\right) \]
          13. +-lowering-+.f6499.3%

            \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right), t1\right)\right) \]
        4. Applied egg-rr99.3%

          \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{0 - \left(t1 + u\right)}{t1}}} \]
        5. Step-by-step derivation
          1. clear-numN/A

            \[\leadsto \frac{1}{\color{blue}{\frac{\frac{0 - \left(t1 + u\right)}{t1}}{\frac{v}{t1 + u}}}} \]
          2. associate-/r/N/A

            \[\leadsto \frac{1}{\frac{0 - \left(t1 + u\right)}{t1}} \cdot \color{blue}{\frac{v}{t1 + u}} \]
          3. clear-numN/A

            \[\leadsto \frac{t1}{0 - \left(t1 + u\right)} \cdot \frac{\color{blue}{v}}{t1 + u} \]
          4. sub0-negN/A

            \[\leadsto \frac{t1}{\mathsf{neg}\left(\left(t1 + u\right)\right)} \cdot \frac{v}{t1 + u} \]
          5. distribute-frac-neg2N/A

            \[\leadsto \left(\mathsf{neg}\left(\frac{t1}{t1 + u}\right)\right) \cdot \frac{\color{blue}{v}}{t1 + u} \]
          6. distribute-lft-neg-outN/A

            \[\leadsto \mathsf{neg}\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right) \]
          7. neg-lowering-neg.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right)\right) \]
          8. *-lowering-*.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\left(\frac{t1}{t1 + u}\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
          9. /-lowering-/.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \left(t1 + u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
          10. +-lowering-+.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
          11. /-lowering-/.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \left(t1 + u\right)\right)\right)\right) \]
          12. +-lowering-+.f6499.4%

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right)\right)\right) \]
        6. Applied egg-rr99.4%

          \[\leadsto \color{blue}{-\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
        7. Step-by-step derivation
          1. associate-*r/N/A

            \[\leadsto \mathsf{neg.f64}\left(\left(\frac{\frac{t1}{t1 + u} \cdot v}{t1 + u}\right)\right) \]
          2. /-lowering-/.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{t1}{t1 + u} \cdot v\right), \left(t1 + u\right)\right)\right) \]
          3. *-commutativeN/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{t1}{t1 + u}\right), \left(t1 + u\right)\right)\right) \]
          4. clear-numN/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{1}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
          5. un-div-invN/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{v}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
          6. /-lowering-/.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(\frac{t1 + u}{t1}\right)\right), \left(t1 + u\right)\right)\right) \]
          7. /-lowering-/.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\left(t1 + u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
          8. +-lowering-+.f64N/A

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
          9. +-lowering-+.f6499.7%

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
        8. Applied egg-rr99.7%

          \[\leadsto -\color{blue}{\frac{\frac{v}{\frac{t1 + u}{t1}}}{t1 + u}} \]
        9. Taylor expanded in t1 around inf

          \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\color{blue}{v}, \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
        10. Step-by-step derivation
          1. Simplified83.7%

            \[\leadsto -\frac{\color{blue}{v}}{t1 + u} \]

          if -4.3e-138 < t1 < 9.5000000000000005e65

          1. Initial program 81.6%

            \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
          2. Add Preprocessing
          3. Taylor expanded in t1 around 0

            \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
          4. Step-by-step derivation
            1. associate-*r/N/A

              \[\leadsto \frac{-1 \cdot \left(t1 \cdot v\right)}{\color{blue}{{u}^{2}}} \]
            2. unpow2N/A

              \[\leadsto \frac{-1 \cdot \left(t1 \cdot v\right)}{u \cdot \color{blue}{u}} \]
            3. associate-/r*N/A

              \[\leadsto \frac{\frac{-1 \cdot \left(t1 \cdot v\right)}{u}}{\color{blue}{u}} \]
            4. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\left(\frac{-1 \cdot \left(t1 \cdot v\right)}{u}\right), \color{blue}{u}\right) \]
            5. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(-1 \cdot \left(t1 \cdot v\right)\right), u\right), u\right) \]
            6. mul-1-negN/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(\mathsf{neg}\left(t1 \cdot v\right)\right), u\right), u\right) \]
            7. neg-sub0N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(0 - t1 \cdot v\right), u\right), u\right) \]
            8. --lowering--.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 \cdot v\right)\right), u\right), u\right) \]
            9. *-lowering-*.f6479.0%

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(t1, v\right)\right), u\right), u\right) \]
          5. Simplified79.0%

            \[\leadsto \color{blue}{\frac{\frac{0 - t1 \cdot v}{u}}{u}} \]
          6. Step-by-step derivation
            1. sub0-negN/A

              \[\leadsto \mathsf{/.f64}\left(\left(\frac{\mathsf{neg}\left(t1 \cdot v\right)}{u}\right), u\right) \]
            2. distribute-frac-negN/A

              \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\frac{t1 \cdot v}{u}\right)\right), u\right) \]
            3. *-commutativeN/A

              \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\frac{v \cdot t1}{u}\right)\right), u\right) \]
            4. associate-/l*N/A

              \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(v \cdot \frac{t1}{u}\right)\right), u\right) \]
            5. distribute-rgt-neg-inN/A

              \[\leadsto \mathsf{/.f64}\left(\left(v \cdot \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)\right), u\right) \]
            6. *-lowering-*.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)\right), u\right) \]
            7. neg-lowering-neg.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \mathsf{neg.f64}\left(\left(\frac{t1}{u}\right)\right)\right), u\right) \]
            8. /-lowering-/.f6481.9%

              \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \mathsf{neg.f64}\left(\mathsf{/.f64}\left(t1, u\right)\right)\right), u\right) \]
          7. Applied egg-rr81.9%

            \[\leadsto \frac{\color{blue}{v \cdot \left(-\frac{t1}{u}\right)}}{u} \]
          8. Step-by-step derivation
            1. clear-numN/A

              \[\leadsto \frac{1}{\color{blue}{\frac{u}{v \cdot \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)}}} \]
            2. associate-/r*N/A

              \[\leadsto \frac{1}{\frac{\frac{u}{v}}{\color{blue}{\mathsf{neg}\left(\frac{t1}{u}\right)}}} \]
            3. clear-numN/A

              \[\leadsto \frac{\mathsf{neg}\left(\frac{t1}{u}\right)}{\color{blue}{\frac{u}{v}}} \]
            4. distribute-frac-negN/A

              \[\leadsto \mathsf{neg}\left(\frac{\frac{t1}{u}}{\frac{u}{v}}\right) \]
            5. neg-lowering-neg.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\left(\frac{\frac{t1}{u}}{\frac{u}{v}}\right)\right) \]
            6. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{t1}{u}\right), \left(\frac{u}{v}\right)\right)\right) \]
            7. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(t1, u\right), \left(\frac{u}{v}\right)\right)\right) \]
            8. /-lowering-/.f6484.6%

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(t1, u\right), \mathsf{/.f64}\left(u, v\right)\right)\right) \]
          9. Applied egg-rr84.6%

            \[\leadsto \color{blue}{-\frac{\frac{t1}{u}}{\frac{u}{v}}} \]
        11. Recombined 2 regimes into one program.
        12. Final simplification84.1%

          \[\leadsto \begin{array}{l} \mathbf{if}\;t1 \leq -4.3 \cdot 10^{-138}:\\ \;\;\;\;0 - \frac{v}{t1 + u}\\ \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\ \;\;\;\;\frac{0 - \frac{t1}{u}}{\frac{u}{v}}\\ \mathbf{else}:\\ \;\;\;\;0 - \frac{v}{t1 + u}\\ \end{array} \]
        13. Add Preprocessing

        Alternative 4: 75.5% accurate, 0.6× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_1 := 0 - \frac{v}{t1 + u}\\ \mathbf{if}\;t1 \leq -3.8 \cdot 10^{-138}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\ \;\;\;\;0 - \frac{v}{\frac{u}{\frac{t1}{u}}}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
        (FPCore (u v t1)
         :precision binary64
         (let* ((t_1 (- 0.0 (/ v (+ t1 u)))))
           (if (<= t1 -3.8e-138)
             t_1
             (if (<= t1 9.5e+65) (- 0.0 (/ v (/ u (/ t1 u)))) t_1))))
        double code(double u, double v, double t1) {
        	double t_1 = 0.0 - (v / (t1 + u));
        	double tmp;
        	if (t1 <= -3.8e-138) {
        		tmp = t_1;
        	} else if (t1 <= 9.5e+65) {
        		tmp = 0.0 - (v / (u / (t1 / u)));
        	} else {
        		tmp = t_1;
        	}
        	return tmp;
        }
        
        real(8) function code(u, v, t1)
            real(8), intent (in) :: u
            real(8), intent (in) :: v
            real(8), intent (in) :: t1
            real(8) :: t_1
            real(8) :: tmp
            t_1 = 0.0d0 - (v / (t1 + u))
            if (t1 <= (-3.8d-138)) then
                tmp = t_1
            else if (t1 <= 9.5d+65) then
                tmp = 0.0d0 - (v / (u / (t1 / u)))
            else
                tmp = t_1
            end if
            code = tmp
        end function
        
        public static double code(double u, double v, double t1) {
        	double t_1 = 0.0 - (v / (t1 + u));
        	double tmp;
        	if (t1 <= -3.8e-138) {
        		tmp = t_1;
        	} else if (t1 <= 9.5e+65) {
        		tmp = 0.0 - (v / (u / (t1 / u)));
        	} else {
        		tmp = t_1;
        	}
        	return tmp;
        }
        
        def code(u, v, t1):
        	t_1 = 0.0 - (v / (t1 + u))
        	tmp = 0
        	if t1 <= -3.8e-138:
        		tmp = t_1
        	elif t1 <= 9.5e+65:
        		tmp = 0.0 - (v / (u / (t1 / u)))
        	else:
        		tmp = t_1
        	return tmp
        
        function code(u, v, t1)
        	t_1 = Float64(0.0 - Float64(v / Float64(t1 + u)))
        	tmp = 0.0
        	if (t1 <= -3.8e-138)
        		tmp = t_1;
        	elseif (t1 <= 9.5e+65)
        		tmp = Float64(0.0 - Float64(v / Float64(u / Float64(t1 / u))));
        	else
        		tmp = t_1;
        	end
        	return tmp
        end
        
        function tmp_2 = code(u, v, t1)
        	t_1 = 0.0 - (v / (t1 + u));
        	tmp = 0.0;
        	if (t1 <= -3.8e-138)
        		tmp = t_1;
        	elseif (t1 <= 9.5e+65)
        		tmp = 0.0 - (v / (u / (t1 / u)));
        	else
        		tmp = t_1;
        	end
        	tmp_2 = tmp;
        end
        
        code[u_, v_, t1_] := Block[{t$95$1 = N[(0.0 - N[(v / N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t1, -3.8e-138], t$95$1, If[LessEqual[t1, 9.5e+65], N[(0.0 - N[(v / N[(u / N[(t1 / u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_1 := 0 - \frac{v}{t1 + u}\\
        \mathbf{if}\;t1 \leq -3.8 \cdot 10^{-138}:\\
        \;\;\;\;t\_1\\
        
        \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\
        \;\;\;\;0 - \frac{v}{\frac{u}{\frac{t1}{u}}}\\
        
        \mathbf{else}:\\
        \;\;\;\;t\_1\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if t1 < -3.8000000000000002e-138 or 9.5000000000000005e65 < t1

          1. Initial program 70.9%

            \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. *-commutativeN/A

              \[\leadsto \frac{v \cdot \left(\mathsf{neg}\left(t1\right)\right)}{\color{blue}{\left(t1 + u\right)} \cdot \left(t1 + u\right)} \]
            2. times-fracN/A

              \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\frac{\mathsf{neg}\left(t1\right)}{t1 + u}} \]
            3. clear-numN/A

              \[\leadsto \frac{v}{t1 + u} \cdot \frac{1}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
            4. un-div-invN/A

              \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
            5. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\left(\frac{v}{t1 + u}\right), \color{blue}{\left(\frac{t1 + u}{\mathsf{neg}\left(t1\right)}\right)}\right) \]
            6. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(t1 + u\right)\right), \left(\frac{\color{blue}{t1 + u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
            7. +-lowering-+.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{t1 + \color{blue}{u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
            8. frac-2negN/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(t1\right)\right)\right)}}\right)\right) \]
            9. remove-double-negN/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}\right)\right) \]
            10. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right), \color{blue}{t1}\right)\right) \]
            11. neg-sub0N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(0 - \left(t1 + u\right)\right), t1\right)\right) \]
            12. --lowering--.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 + u\right)\right), t1\right)\right) \]
            13. +-lowering-+.f6499.3%

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right), t1\right)\right) \]
          4. Applied egg-rr99.3%

            \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{0 - \left(t1 + u\right)}{t1}}} \]
          5. Step-by-step derivation
            1. clear-numN/A

              \[\leadsto \frac{1}{\color{blue}{\frac{\frac{0 - \left(t1 + u\right)}{t1}}{\frac{v}{t1 + u}}}} \]
            2. associate-/r/N/A

              \[\leadsto \frac{1}{\frac{0 - \left(t1 + u\right)}{t1}} \cdot \color{blue}{\frac{v}{t1 + u}} \]
            3. clear-numN/A

              \[\leadsto \frac{t1}{0 - \left(t1 + u\right)} \cdot \frac{\color{blue}{v}}{t1 + u} \]
            4. sub0-negN/A

              \[\leadsto \frac{t1}{\mathsf{neg}\left(\left(t1 + u\right)\right)} \cdot \frac{v}{t1 + u} \]
            5. distribute-frac-neg2N/A

              \[\leadsto \left(\mathsf{neg}\left(\frac{t1}{t1 + u}\right)\right) \cdot \frac{\color{blue}{v}}{t1 + u} \]
            6. distribute-lft-neg-outN/A

              \[\leadsto \mathsf{neg}\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right) \]
            7. neg-lowering-neg.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right)\right) \]
            8. *-lowering-*.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\left(\frac{t1}{t1 + u}\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
            9. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \left(t1 + u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
            10. +-lowering-+.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
            11. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \left(t1 + u\right)\right)\right)\right) \]
            12. +-lowering-+.f6499.4%

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right)\right)\right) \]
          6. Applied egg-rr99.4%

            \[\leadsto \color{blue}{-\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
          7. Step-by-step derivation
            1. associate-*r/N/A

              \[\leadsto \mathsf{neg.f64}\left(\left(\frac{\frac{t1}{t1 + u} \cdot v}{t1 + u}\right)\right) \]
            2. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{t1}{t1 + u} \cdot v\right), \left(t1 + u\right)\right)\right) \]
            3. *-commutativeN/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{t1}{t1 + u}\right), \left(t1 + u\right)\right)\right) \]
            4. clear-numN/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{1}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
            5. un-div-invN/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{v}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
            6. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(\frac{t1 + u}{t1}\right)\right), \left(t1 + u\right)\right)\right) \]
            7. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\left(t1 + u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
            8. +-lowering-+.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
            9. +-lowering-+.f6499.7%

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
          8. Applied egg-rr99.7%

            \[\leadsto -\color{blue}{\frac{\frac{v}{\frac{t1 + u}{t1}}}{t1 + u}} \]
          9. Taylor expanded in t1 around inf

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\color{blue}{v}, \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
          10. Step-by-step derivation
            1. Simplified83.7%

              \[\leadsto -\frac{\color{blue}{v}}{t1 + u} \]

            if -3.8000000000000002e-138 < t1 < 9.5000000000000005e65

            1. Initial program 81.6%

              \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
            2. Add Preprocessing
            3. Taylor expanded in t1 around 0

              \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
            4. Step-by-step derivation
              1. associate-*r/N/A

                \[\leadsto \frac{-1 \cdot \left(t1 \cdot v\right)}{\color{blue}{{u}^{2}}} \]
              2. unpow2N/A

                \[\leadsto \frac{-1 \cdot \left(t1 \cdot v\right)}{u \cdot \color{blue}{u}} \]
              3. associate-/r*N/A

                \[\leadsto \frac{\frac{-1 \cdot \left(t1 \cdot v\right)}{u}}{\color{blue}{u}} \]
              4. /-lowering-/.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\left(\frac{-1 \cdot \left(t1 \cdot v\right)}{u}\right), \color{blue}{u}\right) \]
              5. /-lowering-/.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(-1 \cdot \left(t1 \cdot v\right)\right), u\right), u\right) \]
              6. mul-1-negN/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(\mathsf{neg}\left(t1 \cdot v\right)\right), u\right), u\right) \]
              7. neg-sub0N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\left(0 - t1 \cdot v\right), u\right), u\right) \]
              8. --lowering--.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 \cdot v\right)\right), u\right), u\right) \]
              9. *-lowering-*.f6479.0%

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(t1, v\right)\right), u\right), u\right) \]
            5. Simplified79.0%

              \[\leadsto \color{blue}{\frac{\frac{0 - t1 \cdot v}{u}}{u}} \]
            6. Step-by-step derivation
              1. sub0-negN/A

                \[\leadsto \mathsf{/.f64}\left(\left(\frac{\mathsf{neg}\left(t1 \cdot v\right)}{u}\right), u\right) \]
              2. distribute-frac-negN/A

                \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\frac{t1 \cdot v}{u}\right)\right), u\right) \]
              3. *-commutativeN/A

                \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\frac{v \cdot t1}{u}\right)\right), u\right) \]
              4. associate-/l*N/A

                \[\leadsto \mathsf{/.f64}\left(\left(\mathsf{neg}\left(v \cdot \frac{t1}{u}\right)\right), u\right) \]
              5. distribute-rgt-neg-inN/A

                \[\leadsto \mathsf{/.f64}\left(\left(v \cdot \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)\right), u\right) \]
              6. *-lowering-*.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)\right), u\right) \]
              7. neg-lowering-neg.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \mathsf{neg.f64}\left(\left(\frac{t1}{u}\right)\right)\right), u\right) \]
              8. /-lowering-/.f6481.9%

                \[\leadsto \mathsf{/.f64}\left(\mathsf{*.f64}\left(v, \mathsf{neg.f64}\left(\mathsf{/.f64}\left(t1, u\right)\right)\right), u\right) \]
            7. Applied egg-rr81.9%

              \[\leadsto \frac{\color{blue}{v \cdot \left(-\frac{t1}{u}\right)}}{u} \]
            8. Step-by-step derivation
              1. associate-*l/N/A

                \[\leadsto \frac{v}{u} \cdot \color{blue}{\left(\mathsf{neg}\left(\frac{t1}{u}\right)\right)} \]
              2. distribute-neg-frac2N/A

                \[\leadsto \frac{v}{u} \cdot \frac{t1}{\color{blue}{\mathsf{neg}\left(u\right)}} \]
              3. clear-numN/A

                \[\leadsto \frac{v}{u} \cdot \frac{1}{\color{blue}{\frac{\mathsf{neg}\left(u\right)}{t1}}} \]
              4. sub0-negN/A

                \[\leadsto \frac{v}{u} \cdot \frac{1}{\frac{0 - u}{t1}} \]
              5. div-invN/A

                \[\leadsto \frac{\frac{v}{u}}{\color{blue}{\frac{0 - u}{t1}}} \]
              6. associate-/l/N/A

                \[\leadsto \frac{v}{\color{blue}{\frac{0 - u}{t1} \cdot u}} \]
              7. frac-2negN/A

                \[\leadsto \frac{\mathsf{neg}\left(v\right)}{\color{blue}{\mathsf{neg}\left(\frac{0 - u}{t1} \cdot u\right)}} \]
              8. distribute-lft-neg-inN/A

                \[\leadsto \frac{\mathsf{neg}\left(v\right)}{\left(\mathsf{neg}\left(\frac{0 - u}{t1}\right)\right) \cdot \color{blue}{u}} \]
              9. sub0-negN/A

                \[\leadsto \frac{\mathsf{neg}\left(v\right)}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(u\right)}{t1}\right)\right) \cdot u} \]
              10. distribute-neg-frac2N/A

                \[\leadsto \frac{\mathsf{neg}\left(v\right)}{\frac{\mathsf{neg}\left(u\right)}{\mathsf{neg}\left(t1\right)} \cdot u} \]
              11. frac-2negN/A

                \[\leadsto \frac{\mathsf{neg}\left(v\right)}{\frac{u}{t1} \cdot u} \]
              12. distribute-frac-negN/A

                \[\leadsto \mathsf{neg}\left(\frac{v}{\frac{u}{t1} \cdot u}\right) \]
              13. neg-lowering-neg.f64N/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{\frac{u}{t1} \cdot u}\right)\right) \]
              14. frac-2negN/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{\frac{\mathsf{neg}\left(u\right)}{\mathsf{neg}\left(t1\right)} \cdot u}\right)\right) \]
              15. distribute-neg-frac2N/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{\left(\mathsf{neg}\left(\frac{\mathsf{neg}\left(u\right)}{t1}\right)\right) \cdot u}\right)\right) \]
              16. sub0-negN/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{\left(\mathsf{neg}\left(\frac{0 - u}{t1}\right)\right) \cdot u}\right)\right) \]
              17. distribute-lft-neg-inN/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{\mathsf{neg}\left(\frac{0 - u}{t1} \cdot u\right)}\right)\right) \]
              18. *-commutativeN/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{\mathsf{neg}\left(u \cdot \frac{0 - u}{t1}\right)}\right)\right) \]
              19. distribute-rgt-neg-inN/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{u \cdot \left(\mathsf{neg}\left(\frac{0 - u}{t1}\right)\right)}\right)\right) \]
              20. div-invN/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{u \cdot \left(\mathsf{neg}\left(\left(0 - u\right) \cdot \frac{1}{t1}\right)\right)}\right)\right) \]
              21. sub0-negN/A

                \[\leadsto \mathsf{neg.f64}\left(\left(\frac{v}{u \cdot \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(u\right)\right) \cdot \frac{1}{t1}\right)\right)}\right)\right) \]
            9. Applied egg-rr79.1%

              \[\leadsto \color{blue}{-\frac{v}{\frac{u}{\frac{t1}{u}}}} \]
          11. Recombined 2 regimes into one program.
          12. Final simplification81.9%

            \[\leadsto \begin{array}{l} \mathbf{if}\;t1 \leq -3.8 \cdot 10^{-138}:\\ \;\;\;\;0 - \frac{v}{t1 + u}\\ \mathbf{elif}\;t1 \leq 9.5 \cdot 10^{+65}:\\ \;\;\;\;0 - \frac{v}{\frac{u}{\frac{t1}{u}}}\\ \mathbf{else}:\\ \;\;\;\;0 - \frac{v}{t1 + u}\\ \end{array} \]
          13. Add Preprocessing

          Alternative 5: 57.6% accurate, 0.8× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} t_1 := v \cdot \frac{-1}{u}\\ \mathbf{if}\;u \leq -1.6 \cdot 10^{+175}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;u \leq 2.1 \cdot 10^{+234}:\\ \;\;\;\;0 - \frac{v}{t1}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
          (FPCore (u v t1)
           :precision binary64
           (let* ((t_1 (* v (/ -1.0 u))))
             (if (<= u -1.6e+175) t_1 (if (<= u 2.1e+234) (- 0.0 (/ v t1)) t_1))))
          double code(double u, double v, double t1) {
          	double t_1 = v * (-1.0 / u);
          	double tmp;
          	if (u <= -1.6e+175) {
          		tmp = t_1;
          	} else if (u <= 2.1e+234) {
          		tmp = 0.0 - (v / t1);
          	} else {
          		tmp = t_1;
          	}
          	return tmp;
          }
          
          real(8) function code(u, v, t1)
              real(8), intent (in) :: u
              real(8), intent (in) :: v
              real(8), intent (in) :: t1
              real(8) :: t_1
              real(8) :: tmp
              t_1 = v * ((-1.0d0) / u)
              if (u <= (-1.6d+175)) then
                  tmp = t_1
              else if (u <= 2.1d+234) then
                  tmp = 0.0d0 - (v / t1)
              else
                  tmp = t_1
              end if
              code = tmp
          end function
          
          public static double code(double u, double v, double t1) {
          	double t_1 = v * (-1.0 / u);
          	double tmp;
          	if (u <= -1.6e+175) {
          		tmp = t_1;
          	} else if (u <= 2.1e+234) {
          		tmp = 0.0 - (v / t1);
          	} else {
          		tmp = t_1;
          	}
          	return tmp;
          }
          
          def code(u, v, t1):
          	t_1 = v * (-1.0 / u)
          	tmp = 0
          	if u <= -1.6e+175:
          		tmp = t_1
          	elif u <= 2.1e+234:
          		tmp = 0.0 - (v / t1)
          	else:
          		tmp = t_1
          	return tmp
          
          function code(u, v, t1)
          	t_1 = Float64(v * Float64(-1.0 / u))
          	tmp = 0.0
          	if (u <= -1.6e+175)
          		tmp = t_1;
          	elseif (u <= 2.1e+234)
          		tmp = Float64(0.0 - Float64(v / t1));
          	else
          		tmp = t_1;
          	end
          	return tmp
          end
          
          function tmp_2 = code(u, v, t1)
          	t_1 = v * (-1.0 / u);
          	tmp = 0.0;
          	if (u <= -1.6e+175)
          		tmp = t_1;
          	elseif (u <= 2.1e+234)
          		tmp = 0.0 - (v / t1);
          	else
          		tmp = t_1;
          	end
          	tmp_2 = tmp;
          end
          
          code[u_, v_, t1_] := Block[{t$95$1 = N[(v * N[(-1.0 / u), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[u, -1.6e+175], t$95$1, If[LessEqual[u, 2.1e+234], N[(0.0 - N[(v / t1), $MachinePrecision]), $MachinePrecision], t$95$1]]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          t_1 := v \cdot \frac{-1}{u}\\
          \mathbf{if}\;u \leq -1.6 \cdot 10^{+175}:\\
          \;\;\;\;t\_1\\
          
          \mathbf{elif}\;u \leq 2.1 \cdot 10^{+234}:\\
          \;\;\;\;0 - \frac{v}{t1}\\
          
          \mathbf{else}:\\
          \;\;\;\;t\_1\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if u < -1.60000000000000011e175 or 2.1e234 < u

            1. Initial program 81.5%

              \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. *-commutativeN/A

                \[\leadsto \frac{v \cdot \left(\mathsf{neg}\left(t1\right)\right)}{\color{blue}{\left(t1 + u\right)} \cdot \left(t1 + u\right)} \]
              2. times-fracN/A

                \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\frac{\mathsf{neg}\left(t1\right)}{t1 + u}} \]
              3. clear-numN/A

                \[\leadsto \frac{v}{t1 + u} \cdot \frac{1}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
              4. un-div-invN/A

                \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
              5. /-lowering-/.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\left(\frac{v}{t1 + u}\right), \color{blue}{\left(\frac{t1 + u}{\mathsf{neg}\left(t1\right)}\right)}\right) \]
              6. /-lowering-/.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(t1 + u\right)\right), \left(\frac{\color{blue}{t1 + u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
              7. +-lowering-+.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{t1 + \color{blue}{u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
              8. frac-2negN/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(t1\right)\right)\right)}}\right)\right) \]
              9. remove-double-negN/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}\right)\right) \]
              10. /-lowering-/.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right), \color{blue}{t1}\right)\right) \]
              11. neg-sub0N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(0 - \left(t1 + u\right)\right), t1\right)\right) \]
              12. --lowering--.f64N/A

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 + u\right)\right), t1\right)\right) \]
              13. +-lowering-+.f6499.9%

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right), t1\right)\right) \]
            4. Applied egg-rr99.9%

              \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{0 - \left(t1 + u\right)}{t1}}} \]
            5. Taylor expanded in t1 around 0

              \[\leadsto \mathsf{/.f64}\left(\color{blue}{\left(\frac{v}{u}\right)}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right), t1\right)\right) \]
            6. Step-by-step derivation
              1. /-lowering-/.f6493.8%

                \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, u\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right)}, t1\right)\right) \]
            7. Simplified93.8%

              \[\leadsto \frac{\color{blue}{\frac{v}{u}}}{\frac{0 - \left(t1 + u\right)}{t1}} \]
            8. Step-by-step derivation
              1. div-invN/A

                \[\leadsto \frac{v \cdot \frac{1}{u}}{\frac{\color{blue}{0 - \left(t1 + u\right)}}{t1}} \]
              2. associate-/l*N/A

                \[\leadsto v \cdot \color{blue}{\frac{\frac{1}{u}}{\frac{0 - \left(t1 + u\right)}{t1}}} \]
              3. *-lowering-*.f64N/A

                \[\leadsto \mathsf{*.f64}\left(v, \color{blue}{\left(\frac{\frac{1}{u}}{\frac{0 - \left(t1 + u\right)}{t1}}\right)}\right) \]
              4. div-invN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left(\frac{1}{u} \cdot \color{blue}{\frac{1}{\frac{0 - \left(t1 + u\right)}{t1}}}\right)\right) \]
              5. inv-powN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left({u}^{-1} \cdot \frac{\color{blue}{1}}{\frac{0 - \left(t1 + u\right)}{t1}}\right)\right) \]
              6. inv-powN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left({u}^{-1} \cdot {\left(\frac{0 - \left(t1 + u\right)}{t1}\right)}^{\color{blue}{-1}}\right)\right) \]
              7. pow-prod-downN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left({\left(u \cdot \frac{0 - \left(t1 + u\right)}{t1}\right)}^{\color{blue}{-1}}\right)\right) \]
              8. *-commutativeN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left({\left(\frac{0 - \left(t1 + u\right)}{t1} \cdot u\right)}^{-1}\right)\right) \]
              9. inv-powN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left(\frac{1}{\color{blue}{\frac{0 - \left(t1 + u\right)}{t1} \cdot u}}\right)\right) \]
              10. frac-2negN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left(\frac{\mathsf{neg}\left(1\right)}{\color{blue}{\mathsf{neg}\left(\frac{0 - \left(t1 + u\right)}{t1} \cdot u\right)}}\right)\right) \]
              11. metadata-evalN/A

                \[\leadsto \mathsf{*.f64}\left(v, \left(\frac{-1}{\mathsf{neg}\left(\color{blue}{\frac{0 - \left(t1 + u\right)}{t1} \cdot u}\right)}\right)\right) \]
              12. /-lowering-/.f64N/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \color{blue}{\left(\mathsf{neg}\left(\frac{0 - \left(t1 + u\right)}{t1} \cdot u\right)\right)}\right)\right) \]
              13. *-commutativeN/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \left(\mathsf{neg}\left(u \cdot \frac{0 - \left(t1 + u\right)}{t1}\right)\right)\right)\right) \]
              14. clear-numN/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \left(\mathsf{neg}\left(u \cdot \frac{1}{\frac{t1}{0 - \left(t1 + u\right)}}\right)\right)\right)\right) \]
              15. un-div-invN/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \left(\mathsf{neg}\left(\frac{u}{\frac{t1}{0 - \left(t1 + u\right)}}\right)\right)\right)\right) \]
              16. distribute-neg-frac2N/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \left(\frac{u}{\color{blue}{\mathsf{neg}\left(\frac{t1}{0 - \left(t1 + u\right)}\right)}}\right)\right)\right) \]
              17. distribute-frac-negN/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \left(\frac{u}{\frac{\mathsf{neg}\left(t1\right)}{\color{blue}{0 - \left(t1 + u\right)}}}\right)\right)\right) \]
              18. sub0-negN/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \left(\frac{u}{\frac{\mathsf{neg}\left(t1\right)}{\mathsf{neg}\left(\left(t1 + u\right)\right)}}\right)\right)\right) \]
              19. frac-2negN/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \left(\frac{u}{\frac{t1}{\color{blue}{t1 + u}}}\right)\right)\right) \]
              20. /-lowering-/.f64N/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \mathsf{/.f64}\left(u, \color{blue}{\left(\frac{t1}{t1 + u}\right)}\right)\right)\right) \]
              21. /-lowering-/.f64N/A

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \mathsf{/.f64}\left(u, \mathsf{/.f64}\left(t1, \color{blue}{\left(t1 + u\right)}\right)\right)\right)\right) \]
              22. +-lowering-+.f6484.5%

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \mathsf{/.f64}\left(u, \mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, \color{blue}{u}\right)\right)\right)\right)\right) \]
            9. Applied egg-rr84.5%

              \[\leadsto \color{blue}{v \cdot \frac{-1}{\frac{u}{\frac{t1}{t1 + u}}}} \]
            10. Taylor expanded in u around 0

              \[\leadsto \mathsf{*.f64}\left(v, \color{blue}{\left(\frac{-1}{u}\right)}\right) \]
            11. Step-by-step derivation
              1. /-lowering-/.f6459.0%

                \[\leadsto \mathsf{*.f64}\left(v, \mathsf{/.f64}\left(-1, \color{blue}{u}\right)\right) \]
            12. Simplified59.0%

              \[\leadsto v \cdot \color{blue}{\frac{-1}{u}} \]

            if -1.60000000000000011e175 < u < 2.1e234

            1. Initial program 73.8%

              \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
            2. Add Preprocessing
            3. Taylor expanded in t1 around inf

              \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
            4. Step-by-step derivation
              1. mul-1-negN/A

                \[\leadsto \mathsf{neg}\left(\frac{v}{t1}\right) \]
              2. distribute-neg-frac2N/A

                \[\leadsto \frac{v}{\color{blue}{\mathsf{neg}\left(t1\right)}} \]
              3. mul-1-negN/A

                \[\leadsto \frac{v}{-1 \cdot \color{blue}{t1}} \]
              4. /-lowering-/.f64N/A

                \[\leadsto \mathsf{/.f64}\left(v, \color{blue}{\left(-1 \cdot t1\right)}\right) \]
              5. mul-1-negN/A

                \[\leadsto \mathsf{/.f64}\left(v, \left(\mathsf{neg}\left(t1\right)\right)\right) \]
              6. neg-sub0N/A

                \[\leadsto \mathsf{/.f64}\left(v, \left(0 - \color{blue}{t1}\right)\right) \]
              7. --lowering--.f6462.8%

                \[\leadsto \mathsf{/.f64}\left(v, \mathsf{\_.f64}\left(0, \color{blue}{t1}\right)\right) \]
            5. Simplified62.8%

              \[\leadsto \color{blue}{\frac{v}{0 - t1}} \]
            6. Step-by-step derivation
              1. neg-sub0N/A

                \[\leadsto \mathsf{/.f64}\left(v, \left(\mathsf{neg}\left(t1\right)\right)\right) \]
              2. neg-lowering-neg.f6462.8%

                \[\leadsto \mathsf{/.f64}\left(v, \mathsf{neg.f64}\left(t1\right)\right) \]
            7. Applied egg-rr62.8%

              \[\leadsto \frac{v}{\color{blue}{-t1}} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification62.2%

            \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -1.6 \cdot 10^{+175}:\\ \;\;\;\;v \cdot \frac{-1}{u}\\ \mathbf{elif}\;u \leq 2.1 \cdot 10^{+234}:\\ \;\;\;\;0 - \frac{v}{t1}\\ \mathbf{else}:\\ \;\;\;\;v \cdot \frac{-1}{u}\\ \end{array} \]
          5. Add Preprocessing

          Alternative 6: 61.2% accurate, 1.7× speedup?

          \[\begin{array}{l} \\ 0 - \frac{v}{t1 + u} \end{array} \]
          (FPCore (u v t1) :precision binary64 (- 0.0 (/ v (+ t1 u))))
          double code(double u, double v, double t1) {
          	return 0.0 - (v / (t1 + u));
          }
          
          real(8) function code(u, v, t1)
              real(8), intent (in) :: u
              real(8), intent (in) :: v
              real(8), intent (in) :: t1
              code = 0.0d0 - (v / (t1 + u))
          end function
          
          public static double code(double u, double v, double t1) {
          	return 0.0 - (v / (t1 + u));
          }
          
          def code(u, v, t1):
          	return 0.0 - (v / (t1 + u))
          
          function code(u, v, t1)
          	return Float64(0.0 - Float64(v / Float64(t1 + u)))
          end
          
          function tmp = code(u, v, t1)
          	tmp = 0.0 - (v / (t1 + u));
          end
          
          code[u_, v_, t1_] := N[(0.0 - N[(v / N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          0 - \frac{v}{t1 + u}
          \end{array}
          
          Derivation
          1. Initial program 75.0%

            \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. *-commutativeN/A

              \[\leadsto \frac{v \cdot \left(\mathsf{neg}\left(t1\right)\right)}{\color{blue}{\left(t1 + u\right)} \cdot \left(t1 + u\right)} \]
            2. times-fracN/A

              \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\frac{\mathsf{neg}\left(t1\right)}{t1 + u}} \]
            3. clear-numN/A

              \[\leadsto \frac{v}{t1 + u} \cdot \frac{1}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
            4. un-div-invN/A

              \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{t1 + u}{\mathsf{neg}\left(t1\right)}}} \]
            5. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\left(\frac{v}{t1 + u}\right), \color{blue}{\left(\frac{t1 + u}{\mathsf{neg}\left(t1\right)}\right)}\right) \]
            6. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(t1 + u\right)\right), \left(\frac{\color{blue}{t1 + u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
            7. +-lowering-+.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{t1 + \color{blue}{u}}{\mathsf{neg}\left(t1\right)}\right)\right) \]
            8. frac-2negN/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(t1\right)\right)\right)}}\right)\right) \]
            9. remove-double-negN/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}\right)\right) \]
            10. /-lowering-/.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right), \color{blue}{t1}\right)\right) \]
            11. neg-sub0N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\left(0 - \left(t1 + u\right)\right), t1\right)\right) \]
            12. --lowering--.f64N/A

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \left(t1 + u\right)\right), t1\right)\right) \]
            13. +-lowering-+.f6498.0%

              \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(0, \mathsf{+.f64}\left(t1, u\right)\right), t1\right)\right) \]
          4. Applied egg-rr98.0%

            \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{0 - \left(t1 + u\right)}{t1}}} \]
          5. Step-by-step derivation
            1. clear-numN/A

              \[\leadsto \frac{1}{\color{blue}{\frac{\frac{0 - \left(t1 + u\right)}{t1}}{\frac{v}{t1 + u}}}} \]
            2. associate-/r/N/A

              \[\leadsto \frac{1}{\frac{0 - \left(t1 + u\right)}{t1}} \cdot \color{blue}{\frac{v}{t1 + u}} \]
            3. clear-numN/A

              \[\leadsto \frac{t1}{0 - \left(t1 + u\right)} \cdot \frac{\color{blue}{v}}{t1 + u} \]
            4. sub0-negN/A

              \[\leadsto \frac{t1}{\mathsf{neg}\left(\left(t1 + u\right)\right)} \cdot \frac{v}{t1 + u} \]
            5. distribute-frac-neg2N/A

              \[\leadsto \left(\mathsf{neg}\left(\frac{t1}{t1 + u}\right)\right) \cdot \frac{\color{blue}{v}}{t1 + u} \]
            6. distribute-lft-neg-outN/A

              \[\leadsto \mathsf{neg}\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right) \]
            7. neg-lowering-neg.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\left(\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}\right)\right) \]
            8. *-lowering-*.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\left(\frac{t1}{t1 + u}\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
            9. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \left(t1 + u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
            10. +-lowering-+.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \left(\frac{v}{t1 + u}\right)\right)\right) \]
            11. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \left(t1 + u\right)\right)\right)\right) \]
            12. +-lowering-+.f6498.1%

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t1, \mathsf{+.f64}\left(t1, u\right)\right), \mathsf{/.f64}\left(v, \mathsf{+.f64}\left(t1, u\right)\right)\right)\right) \]
          6. Applied egg-rr98.1%

            \[\leadsto \color{blue}{-\frac{t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
          7. Step-by-step derivation
            1. associate-*r/N/A

              \[\leadsto \mathsf{neg.f64}\left(\left(\frac{\frac{t1}{t1 + u} \cdot v}{t1 + u}\right)\right) \]
            2. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{t1}{t1 + u} \cdot v\right), \left(t1 + u\right)\right)\right) \]
            3. *-commutativeN/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{t1}{t1 + u}\right), \left(t1 + u\right)\right)\right) \]
            4. clear-numN/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(v \cdot \frac{1}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
            5. un-div-invN/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\left(\frac{v}{\frac{t1 + u}{t1}}\right), \left(t1 + u\right)\right)\right) \]
            6. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \left(\frac{t1 + u}{t1}\right)\right), \left(t1 + u\right)\right)\right) \]
            7. /-lowering-/.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\left(t1 + u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
            8. +-lowering-+.f64N/A

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \left(t1 + u\right)\right)\right) \]
            9. +-lowering-+.f6497.8%

              \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(v, \mathsf{/.f64}\left(\mathsf{+.f64}\left(t1, u\right), t1\right)\right), \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
          8. Applied egg-rr97.8%

            \[\leadsto -\color{blue}{\frac{\frac{v}{\frac{t1 + u}{t1}}}{t1 + u}} \]
          9. Taylor expanded in t1 around inf

            \[\leadsto \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\color{blue}{v}, \mathsf{+.f64}\left(t1, u\right)\right)\right) \]
          10. Step-by-step derivation
            1. Simplified64.5%

              \[\leadsto -\frac{\color{blue}{v}}{t1 + u} \]
            2. Final simplification64.5%

              \[\leadsto 0 - \frac{v}{t1 + u} \]
            3. Add Preprocessing

            Alternative 7: 53.6% accurate, 2.4× speedup?

            \[\begin{array}{l} \\ 0 - \frac{v}{t1} \end{array} \]
            (FPCore (u v t1) :precision binary64 (- 0.0 (/ v t1)))
            double code(double u, double v, double t1) {
            	return 0.0 - (v / t1);
            }
            
            real(8) function code(u, v, t1)
                real(8), intent (in) :: u
                real(8), intent (in) :: v
                real(8), intent (in) :: t1
                code = 0.0d0 - (v / t1)
            end function
            
            public static double code(double u, double v, double t1) {
            	return 0.0 - (v / t1);
            }
            
            def code(u, v, t1):
            	return 0.0 - (v / t1)
            
            function code(u, v, t1)
            	return Float64(0.0 - Float64(v / t1))
            end
            
            function tmp = code(u, v, t1)
            	tmp = 0.0 - (v / t1);
            end
            
            code[u_, v_, t1_] := N[(0.0 - N[(v / t1), $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            0 - \frac{v}{t1}
            \end{array}
            
            Derivation
            1. Initial program 75.0%

              \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
            2. Add Preprocessing
            3. Taylor expanded in t1 around inf

              \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
            4. Step-by-step derivation
              1. mul-1-negN/A

                \[\leadsto \mathsf{neg}\left(\frac{v}{t1}\right) \]
              2. distribute-neg-frac2N/A

                \[\leadsto \frac{v}{\color{blue}{\mathsf{neg}\left(t1\right)}} \]
              3. mul-1-negN/A

                \[\leadsto \frac{v}{-1 \cdot \color{blue}{t1}} \]
              4. /-lowering-/.f64N/A

                \[\leadsto \mathsf{/.f64}\left(v, \color{blue}{\left(-1 \cdot t1\right)}\right) \]
              5. mul-1-negN/A

                \[\leadsto \mathsf{/.f64}\left(v, \left(\mathsf{neg}\left(t1\right)\right)\right) \]
              6. neg-sub0N/A

                \[\leadsto \mathsf{/.f64}\left(v, \left(0 - \color{blue}{t1}\right)\right) \]
              7. --lowering--.f6456.0%

                \[\leadsto \mathsf{/.f64}\left(v, \mathsf{\_.f64}\left(0, \color{blue}{t1}\right)\right) \]
            5. Simplified56.0%

              \[\leadsto \color{blue}{\frac{v}{0 - t1}} \]
            6. Step-by-step derivation
              1. neg-sub0N/A

                \[\leadsto \mathsf{/.f64}\left(v, \left(\mathsf{neg}\left(t1\right)\right)\right) \]
              2. neg-lowering-neg.f6456.0%

                \[\leadsto \mathsf{/.f64}\left(v, \mathsf{neg.f64}\left(t1\right)\right) \]
            7. Applied egg-rr56.0%

              \[\leadsto \frac{v}{\color{blue}{-t1}} \]
            8. Final simplification56.0%

              \[\leadsto 0 - \frac{v}{t1} \]
            9. Add Preprocessing

            Reproduce

            ?
            herbie shell --seed 2024161 
            (FPCore (u v t1)
              :name "Rosa's DopplerBench"
              :precision binary64
              (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))