Rosa's DopplerBench

Percentage Accurate: 72.7% → 98.1%
Time: 7.4s
Alternatives: 12
Speedup: 0.8×

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

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

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

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

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

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

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

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

      \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}} \]
    6. lift-neg.f64N/A

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

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

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

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

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

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

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

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

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

      \[\leadsto \frac{\frac{v}{\color{blue}{u + t1}} \cdot t1}{\mathsf{neg}\left(\left(t1 + u\right)\right)} \]
    16. lower-neg.f6497.8

      \[\leadsto \frac{\frac{v}{u + t1} \cdot t1}{\color{blue}{-\left(t1 + u\right)}} \]
    17. lift-+.f64N/A

      \[\leadsto \frac{\frac{v}{u + t1} \cdot t1}{-\color{blue}{\left(t1 + u\right)}} \]
    18. +-commutativeN/A

      \[\leadsto \frac{\frac{v}{u + t1} \cdot t1}{-\color{blue}{\left(u + t1\right)}} \]
    19. lower-+.f6497.8

      \[\leadsto \frac{\frac{v}{u + t1} \cdot t1}{-\color{blue}{\left(u + t1\right)}} \]
  4. Applied rewrites97.8%

    \[\leadsto \color{blue}{\frac{\frac{v}{u + t1} \cdot t1}{-\left(u + t1\right)}} \]
  5. Final simplification97.8%

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

Alternative 2: 95.4% accurate, 0.7× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u \leq -3.45 \cdot 10^{+118}:\\ \;\;\;\;\frac{\left(\frac{-1}{u} \cdot v\right) \cdot t1}{u}\\ \mathbf{elif}\;u \leq 3.6 \cdot 10^{+202}:\\ \;\;\;\;\frac{v}{\mathsf{fma}\left(-2 - \frac{u}{t1}, u, -t1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{-v}{u} \cdot t1}{u}\\ \end{array} \end{array} \]
(FPCore (u v t1)
 :precision binary64
 (if (<= u -3.45e+118)
   (/ (* (* (/ -1.0 u) v) t1) u)
   (if (<= u 3.6e+202)
     (/ v (fma (- -2.0 (/ u t1)) u (- t1)))
     (/ (* (/ (- v) u) t1) u))))
double code(double u, double v, double t1) {
	double tmp;
	if (u <= -3.45e+118) {
		tmp = (((-1.0 / u) * v) * t1) / u;
	} else if (u <= 3.6e+202) {
		tmp = v / fma((-2.0 - (u / t1)), u, -t1);
	} else {
		tmp = ((-v / u) * t1) / u;
	}
	return tmp;
}
function code(u, v, t1)
	tmp = 0.0
	if (u <= -3.45e+118)
		tmp = Float64(Float64(Float64(Float64(-1.0 / u) * v) * t1) / u);
	elseif (u <= 3.6e+202)
		tmp = Float64(v / fma(Float64(-2.0 - Float64(u / t1)), u, Float64(-t1)));
	else
		tmp = Float64(Float64(Float64(Float64(-v) / u) * t1) / u);
	end
	return tmp
end
code[u_, v_, t1_] := If[LessEqual[u, -3.45e+118], N[(N[(N[(N[(-1.0 / u), $MachinePrecision] * v), $MachinePrecision] * t1), $MachinePrecision] / u), $MachinePrecision], If[LessEqual[u, 3.6e+202], N[(v / N[(N[(-2.0 - N[(u / t1), $MachinePrecision]), $MachinePrecision] * u + (-t1)), $MachinePrecision]), $MachinePrecision], N[(N[(N[((-v) / u), $MachinePrecision] * t1), $MachinePrecision] / u), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;u \leq -3.45 \cdot 10^{+118}:\\
\;\;\;\;\frac{\left(\frac{-1}{u} \cdot v\right) \cdot t1}{u}\\

\mathbf{elif}\;u \leq 3.6 \cdot 10^{+202}:\\
\;\;\;\;\frac{v}{\mathsf{fma}\left(-2 - \frac{u}{t1}, u, -t1\right)}\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if u < -3.45000000000000001e118

    1. Initial program 73.1%

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

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

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

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

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

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

        \[\leadsto \frac{t1 \cdot v}{\color{blue}{\left(-1 \cdot u\right) \cdot u}} \]
      6. times-fracN/A

        \[\leadsto \color{blue}{\frac{t1}{-1 \cdot u} \cdot \frac{v}{u}} \]
      7. neg-mul-1N/A

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

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

        \[\leadsto \color{blue}{\frac{t1}{\mathsf{neg}\left(u\right)}} \cdot \frac{v}{u} \]
      10. lower-neg.f64N/A

        \[\leadsto \frac{t1}{\color{blue}{-u}} \cdot \frac{v}{u} \]
      11. lower-/.f6490.2

        \[\leadsto \frac{t1}{-u} \cdot \color{blue}{\frac{v}{u}} \]
    5. Applied rewrites90.2%

      \[\leadsto \color{blue}{\frac{t1}{-u} \cdot \frac{v}{u}} \]
    6. Step-by-step derivation
      1. Applied rewrites75.7%

        \[\leadsto t1 \cdot \color{blue}{\frac{v}{\left(-u\right) \cdot u}} \]
      2. Step-by-step derivation
        1. Applied rewrites93.5%

          \[\leadsto \frac{\frac{-v}{u} \cdot t1}{\color{blue}{u}} \]
        2. Step-by-step derivation
          1. Applied rewrites93.6%

            \[\leadsto \frac{\left(\frac{-1}{u} \cdot v\right) \cdot t1}{u} \]

          if -3.45000000000000001e118 < u < 3.60000000000000008e202

          1. Initial program 70.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. lift-/.f64N/A

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

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

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

              \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
            5. clear-numN/A

              \[\leadsto \color{blue}{\frac{1}{\frac{t1 + u}{-t1}}} \cdot \frac{v}{t1 + u} \]
            6. frac-timesN/A

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

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

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

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

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

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

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

              \[\leadsto \frac{1 \cdot v}{\color{blue}{\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}} \cdot \left(t1 + u\right)} \]
            14. lower-neg.f6497.4

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

              \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(t1 + u\right)}}{t1} \cdot \left(t1 + u\right)} \]
            16. +-commutativeN/A

              \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(u + t1\right)}}{t1} \cdot \left(t1 + u\right)} \]
            17. lower-+.f6497.4

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

              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(t1 + u\right)}} \]
            19. +-commutativeN/A

              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
            20. lower-+.f6497.4

              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
          4. Applied rewrites97.4%

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

            \[\leadsto \frac{1 \cdot v}{\color{blue}{-2 \cdot u + -1 \cdot t1}} \]
          6. Step-by-step derivation
            1. lower-fma.f64N/A

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

              \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
            3. lower-neg.f6466.8

              \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{-t1}\right)} \]
          7. Applied rewrites66.8%

            \[\leadsto \frac{1 \cdot v}{\color{blue}{\mathsf{fma}\left(-2, u, -t1\right)}} \]
          8. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \frac{\color{blue}{1 \cdot v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
            2. *-lft-identity66.8

              \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
          9. Applied rewrites66.8%

            \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
          10. Taylor expanded in u around 0

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

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

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

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

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

              \[\leadsto \frac{v}{\mathsf{fma}\left(-1 \cdot \frac{u}{t1} + \color{blue}{-2}, u, -1 \cdot t1\right)} \]
            6. +-commutativeN/A

              \[\leadsto \frac{v}{\mathsf{fma}\left(\color{blue}{-2 + -1 \cdot \frac{u}{t1}}, u, -1 \cdot t1\right)} \]
            7. mul-1-negN/A

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

              \[\leadsto \frac{v}{\mathsf{fma}\left(\color{blue}{-2 - \frac{u}{t1}}, u, -1 \cdot t1\right)} \]
            9. lower--.f64N/A

              \[\leadsto \frac{v}{\mathsf{fma}\left(\color{blue}{-2 - \frac{u}{t1}}, u, -1 \cdot t1\right)} \]
            10. lower-/.f64N/A

              \[\leadsto \frac{v}{\mathsf{fma}\left(-2 - \color{blue}{\frac{u}{t1}}, u, -1 \cdot t1\right)} \]
            11. mul-1-negN/A

              \[\leadsto \frac{v}{\mathsf{fma}\left(-2 - \frac{u}{t1}, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
            12. lower-neg.f6497.4

              \[\leadsto \frac{v}{\mathsf{fma}\left(-2 - \frac{u}{t1}, u, \color{blue}{-t1}\right)} \]
          12. Applied rewrites97.4%

            \[\leadsto \frac{v}{\color{blue}{\mathsf{fma}\left(-2 - \frac{u}{t1}, u, -t1\right)}} \]

          if 3.60000000000000008e202 < u

          1. Initial program 61.7%

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

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

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

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

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

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

              \[\leadsto \frac{t1 \cdot v}{\color{blue}{\left(-1 \cdot u\right) \cdot u}} \]
            6. times-fracN/A

              \[\leadsto \color{blue}{\frac{t1}{-1 \cdot u} \cdot \frac{v}{u}} \]
            7. neg-mul-1N/A

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

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

              \[\leadsto \color{blue}{\frac{t1}{\mathsf{neg}\left(u\right)}} \cdot \frac{v}{u} \]
            10. lower-neg.f64N/A

              \[\leadsto \frac{t1}{\color{blue}{-u}} \cdot \frac{v}{u} \]
            11. lower-/.f6495.2

              \[\leadsto \frac{t1}{-u} \cdot \color{blue}{\frac{v}{u}} \]
          5. Applied rewrites95.2%

            \[\leadsto \color{blue}{\frac{t1}{-u} \cdot \frac{v}{u}} \]
          6. Step-by-step derivation
            1. Applied rewrites62.6%

              \[\leadsto t1 \cdot \color{blue}{\frac{v}{\left(-u\right) \cdot u}} \]
            2. Step-by-step derivation
              1. Applied rewrites95.3%

                \[\leadsto \frac{\frac{-v}{u} \cdot t1}{\color{blue}{u}} \]
            3. Recombined 3 regimes into one program.
            4. Add Preprocessing

            Alternative 3: 86.3% accurate, 0.7× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\ \mathbf{if}\;t1 \leq -1.36 \cdot 10^{+78}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t1 \leq 1.6 \cdot 10^{+81}:\\ \;\;\;\;\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
            (FPCore (u v t1)
             :precision binary64
             (let* ((t_1 (/ v (fma -2.0 u (- t1)))))
               (if (<= t1 -1.36e+78)
                 t_1
                 (if (<= t1 1.6e+81) (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))) t_1))))
            double code(double u, double v, double t1) {
            	double t_1 = v / fma(-2.0, u, -t1);
            	double tmp;
            	if (t1 <= -1.36e+78) {
            		tmp = t_1;
            	} else if (t1 <= 1.6e+81) {
            		tmp = (-t1 * v) / ((t1 + u) * (t1 + u));
            	} else {
            		tmp = t_1;
            	}
            	return tmp;
            }
            
            function code(u, v, t1)
            	t_1 = Float64(v / fma(-2.0, u, Float64(-t1)))
            	tmp = 0.0
            	if (t1 <= -1.36e+78)
            		tmp = t_1;
            	elseif (t1 <= 1.6e+81)
            		tmp = Float64(Float64(Float64(-t1) * v) / Float64(Float64(t1 + u) * Float64(t1 + u)));
            	else
            		tmp = t_1;
            	end
            	return tmp
            end
            
            code[u_, v_, t1_] := Block[{t$95$1 = N[(v / N[(-2.0 * u + (-t1)), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t1, -1.36e+78], t$95$1, If[LessEqual[t1, 1.6e+81], N[(N[((-t1) * v), $MachinePrecision] / N[(N[(t1 + u), $MachinePrecision] * N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\
            \mathbf{if}\;t1 \leq -1.36 \cdot 10^{+78}:\\
            \;\;\;\;t\_1\\
            
            \mathbf{elif}\;t1 \leq 1.6 \cdot 10^{+81}:\\
            \;\;\;\;\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\\
            
            \mathbf{else}:\\
            \;\;\;\;t\_1\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if t1 < -1.35999999999999999e78 or 1.6e81 < t1

              1. Initial program 49.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. lift-/.f64N/A

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

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

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

                  \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
                5. clear-numN/A

                  \[\leadsto \color{blue}{\frac{1}{\frac{t1 + u}{-t1}}} \cdot \frac{v}{t1 + u} \]
                6. frac-timesN/A

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

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

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

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

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

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

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

                  \[\leadsto \frac{1 \cdot v}{\color{blue}{\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}} \cdot \left(t1 + u\right)} \]
                14. lower-neg.f6496.2

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

                  \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(t1 + u\right)}}{t1} \cdot \left(t1 + u\right)} \]
                16. +-commutativeN/A

                  \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(u + t1\right)}}{t1} \cdot \left(t1 + u\right)} \]
                17. lower-+.f6496.2

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

                  \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(t1 + u\right)}} \]
                19. +-commutativeN/A

                  \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                20. lower-+.f6496.2

                  \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
              4. Applied rewrites96.2%

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

                \[\leadsto \frac{1 \cdot v}{\color{blue}{-2 \cdot u + -1 \cdot t1}} \]
              6. Step-by-step derivation
                1. lower-fma.f64N/A

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

                  \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
                3. lower-neg.f6487.7

                  \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{-t1}\right)} \]
              7. Applied rewrites87.7%

                \[\leadsto \frac{1 \cdot v}{\color{blue}{\mathsf{fma}\left(-2, u, -t1\right)}} \]
              8. Step-by-step derivation
                1. lift-*.f64N/A

                  \[\leadsto \frac{\color{blue}{1 \cdot v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                2. *-lft-identity87.7

                  \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
              9. Applied rewrites87.7%

                \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]

              if -1.35999999999999999e78 < t1 < 1.6e81

              1. Initial program 83.3%

                \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
              2. Add Preprocessing
            3. Recombined 2 regimes into one program.
            4. Add Preprocessing

            Alternative 4: 76.8% accurate, 0.7× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u \leq -1.6 \cdot 10^{-37}:\\ \;\;\;\;\frac{t1}{\frac{-u}{v} \cdot u}\\ \mathbf{elif}\;u \leq 5.5 \cdot 10^{+57}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{-v}{u} \cdot t1}{u}\\ \end{array} \end{array} \]
            (FPCore (u v t1)
             :precision binary64
             (if (<= u -1.6e-37)
               (/ t1 (* (/ (- u) v) u))
               (if (<= u 5.5e+57) (/ (- v) t1) (/ (* (/ (- v) u) t1) u))))
            double code(double u, double v, double t1) {
            	double tmp;
            	if (u <= -1.6e-37) {
            		tmp = t1 / ((-u / v) * u);
            	} else if (u <= 5.5e+57) {
            		tmp = -v / t1;
            	} else {
            		tmp = ((-v / u) * 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 (u <= (-1.6d-37)) then
                    tmp = t1 / ((-u / v) * u)
                else if (u <= 5.5d+57) then
                    tmp = -v / t1
                else
                    tmp = ((-v / u) * t1) / u
                end if
                code = tmp
            end function
            
            public static double code(double u, double v, double t1) {
            	double tmp;
            	if (u <= -1.6e-37) {
            		tmp = t1 / ((-u / v) * u);
            	} else if (u <= 5.5e+57) {
            		tmp = -v / t1;
            	} else {
            		tmp = ((-v / u) * t1) / u;
            	}
            	return tmp;
            }
            
            def code(u, v, t1):
            	tmp = 0
            	if u <= -1.6e-37:
            		tmp = t1 / ((-u / v) * u)
            	elif u <= 5.5e+57:
            		tmp = -v / t1
            	else:
            		tmp = ((-v / u) * t1) / u
            	return tmp
            
            function code(u, v, t1)
            	tmp = 0.0
            	if (u <= -1.6e-37)
            		tmp = Float64(t1 / Float64(Float64(Float64(-u) / v) * u));
            	elseif (u <= 5.5e+57)
            		tmp = Float64(Float64(-v) / t1);
            	else
            		tmp = Float64(Float64(Float64(Float64(-v) / u) * t1) / u);
            	end
            	return tmp
            end
            
            function tmp_2 = code(u, v, t1)
            	tmp = 0.0;
            	if (u <= -1.6e-37)
            		tmp = t1 / ((-u / v) * u);
            	elseif (u <= 5.5e+57)
            		tmp = -v / t1;
            	else
            		tmp = ((-v / u) * t1) / u;
            	end
            	tmp_2 = tmp;
            end
            
            code[u_, v_, t1_] := If[LessEqual[u, -1.6e-37], N[(t1 / N[(N[((-u) / v), $MachinePrecision] * u), $MachinePrecision]), $MachinePrecision], If[LessEqual[u, 5.5e+57], N[((-v) / t1), $MachinePrecision], N[(N[(N[((-v) / u), $MachinePrecision] * t1), $MachinePrecision] / u), $MachinePrecision]]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            \mathbf{if}\;u \leq -1.6 \cdot 10^{-37}:\\
            \;\;\;\;\frac{t1}{\frac{-u}{v} \cdot u}\\
            
            \mathbf{elif}\;u \leq 5.5 \cdot 10^{+57}:\\
            \;\;\;\;\frac{-v}{t1}\\
            
            \mathbf{else}:\\
            \;\;\;\;\frac{\frac{-v}{u} \cdot t1}{u}\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 3 regimes
            2. if u < -1.5999999999999999e-37

              1. Initial program 77.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. lift-/.f64N/A

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

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

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

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

                  \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}} \]
                6. clear-numN/A

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

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

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

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

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

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

                  \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(-1 \cdot t1\right)}}{\frac{t1 + u}{v} \cdot \left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right)} \]
                13. neg-mul-1N/A

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

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

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

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

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

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

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

                  \[\leadsto \frac{t1}{\frac{\color{blue}{u + t1}}{v} \cdot \left(\mathsf{neg}\left(\left(t1 + u\right)\right)\right)} \]
                21. lower-neg.f6491.6

                  \[\leadsto \frac{t1}{\frac{u + t1}{v} \cdot \color{blue}{\left(-\left(t1 + u\right)\right)}} \]
                22. lift-+.f64N/A

                  \[\leadsto \frac{t1}{\frac{u + t1}{v} \cdot \left(-\color{blue}{\left(t1 + u\right)}\right)} \]
                23. +-commutativeN/A

                  \[\leadsto \frac{t1}{\frac{u + t1}{v} \cdot \left(-\color{blue}{\left(u + t1\right)}\right)} \]
                24. lower-+.f6491.6

                  \[\leadsto \frac{t1}{\frac{u + t1}{v} \cdot \left(-\color{blue}{\left(u + t1\right)}\right)} \]
              4. Applied rewrites91.6%

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

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

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

                  \[\leadsto \frac{t1}{\frac{\color{blue}{u \cdot u}}{v} \cdot -1} \]
                3. associate-/l*N/A

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

                  \[\leadsto \frac{t1}{\color{blue}{u \cdot \left(\frac{u}{v} \cdot -1\right)}} \]
                5. *-commutativeN/A

                  \[\leadsto \frac{t1}{u \cdot \color{blue}{\left(-1 \cdot \frac{u}{v}\right)}} \]
                6. *-commutativeN/A

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

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

                  \[\leadsto \frac{t1}{\color{blue}{\frac{-1 \cdot u}{v}} \cdot u} \]
                9. lower-/.f64N/A

                  \[\leadsto \frac{t1}{\color{blue}{\frac{-1 \cdot u}{v}} \cdot u} \]
                10. mul-1-negN/A

                  \[\leadsto \frac{t1}{\frac{\color{blue}{\mathsf{neg}\left(u\right)}}{v} \cdot u} \]
                11. lower-neg.f6483.7

                  \[\leadsto \frac{t1}{\frac{\color{blue}{-u}}{v} \cdot u} \]
              7. Applied rewrites83.7%

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

              if -1.5999999999999999e-37 < u < 5.5000000000000002e57

              1. Initial program 65.4%

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

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

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

                  \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]
                3. mul-1-negN/A

                  \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(v\right)}}{t1} \]
                4. lower-neg.f6479.0

                  \[\leadsto \frac{\color{blue}{-v}}{t1} \]
              5. Applied rewrites79.0%

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

              if 5.5000000000000002e57 < u

              1. Initial program 72.5%

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

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

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

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

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

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

                  \[\leadsto \frac{t1 \cdot v}{\color{blue}{\left(-1 \cdot u\right) \cdot u}} \]
                6. times-fracN/A

                  \[\leadsto \color{blue}{\frac{t1}{-1 \cdot u} \cdot \frac{v}{u}} \]
                7. neg-mul-1N/A

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

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

                  \[\leadsto \color{blue}{\frac{t1}{\mathsf{neg}\left(u\right)}} \cdot \frac{v}{u} \]
                10. lower-neg.f64N/A

                  \[\leadsto \frac{t1}{\color{blue}{-u}} \cdot \frac{v}{u} \]
                11. lower-/.f6478.7

                  \[\leadsto \frac{t1}{-u} \cdot \color{blue}{\frac{v}{u}} \]
              5. Applied rewrites78.7%

                \[\leadsto \color{blue}{\frac{t1}{-u} \cdot \frac{v}{u}} \]
              6. Step-by-step derivation
                1. Applied rewrites69.1%

                  \[\leadsto t1 \cdot \color{blue}{\frac{v}{\left(-u\right) \cdot u}} \]
                2. Step-by-step derivation
                  1. Applied rewrites83.7%

                    \[\leadsto \frac{\frac{-v}{u} \cdot t1}{\color{blue}{u}} \]
                3. Recombined 3 regimes into one program.
                4. Add Preprocessing

                Alternative 5: 76.5% accurate, 0.7× speedup?

                \[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{\frac{-v}{u} \cdot t1}{u}\\ \mathbf{if}\;u \leq -1.12 \cdot 10^{-64}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;u \leq 5.5 \cdot 10^{+57}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
                (FPCore (u v t1)
                 :precision binary64
                 (let* ((t_1 (/ (* (/ (- v) u) t1) u)))
                   (if (<= u -1.12e-64) t_1 (if (<= u 5.5e+57) (/ (- v) t1) t_1))))
                double code(double u, double v, double t1) {
                	double t_1 = ((-v / u) * t1) / u;
                	double tmp;
                	if (u <= -1.12e-64) {
                		tmp = t_1;
                	} else if (u <= 5.5e+57) {
                		tmp = -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 / u) * t1) / u
                    if (u <= (-1.12d-64)) then
                        tmp = t_1
                    else if (u <= 5.5d+57) then
                        tmp = -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 / u) * t1) / u;
                	double tmp;
                	if (u <= -1.12e-64) {
                		tmp = t_1;
                	} else if (u <= 5.5e+57) {
                		tmp = -v / t1;
                	} else {
                		tmp = t_1;
                	}
                	return tmp;
                }
                
                def code(u, v, t1):
                	t_1 = ((-v / u) * t1) / u
                	tmp = 0
                	if u <= -1.12e-64:
                		tmp = t_1
                	elif u <= 5.5e+57:
                		tmp = -v / t1
                	else:
                		tmp = t_1
                	return tmp
                
                function code(u, v, t1)
                	t_1 = Float64(Float64(Float64(Float64(-v) / u) * t1) / u)
                	tmp = 0.0
                	if (u <= -1.12e-64)
                		tmp = t_1;
                	elseif (u <= 5.5e+57)
                		tmp = Float64(Float64(-v) / t1);
                	else
                		tmp = t_1;
                	end
                	return tmp
                end
                
                function tmp_2 = code(u, v, t1)
                	t_1 = ((-v / u) * t1) / u;
                	tmp = 0.0;
                	if (u <= -1.12e-64)
                		tmp = t_1;
                	elseif (u <= 5.5e+57)
                		tmp = -v / t1;
                	else
                		tmp = t_1;
                	end
                	tmp_2 = tmp;
                end
                
                code[u_, v_, t1_] := Block[{t$95$1 = N[(N[(N[((-v) / u), $MachinePrecision] * t1), $MachinePrecision] / u), $MachinePrecision]}, If[LessEqual[u, -1.12e-64], t$95$1, If[LessEqual[u, 5.5e+57], N[((-v) / t1), $MachinePrecision], t$95$1]]]
                
                \begin{array}{l}
                
                \\
                \begin{array}{l}
                t_1 := \frac{\frac{-v}{u} \cdot t1}{u}\\
                \mathbf{if}\;u \leq -1.12 \cdot 10^{-64}:\\
                \;\;\;\;t\_1\\
                
                \mathbf{elif}\;u \leq 5.5 \cdot 10^{+57}:\\
                \;\;\;\;\frac{-v}{t1}\\
                
                \mathbf{else}:\\
                \;\;\;\;t\_1\\
                
                
                \end{array}
                \end{array}
                
                Derivation
                1. Split input into 2 regimes
                2. if u < -1.12e-64 or 5.5000000000000002e57 < u

                  1. Initial program 76.0%

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

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

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

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

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

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

                      \[\leadsto \frac{t1 \cdot v}{\color{blue}{\left(-1 \cdot u\right) \cdot u}} \]
                    6. times-fracN/A

                      \[\leadsto \color{blue}{\frac{t1}{-1 \cdot u} \cdot \frac{v}{u}} \]
                    7. neg-mul-1N/A

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

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

                      \[\leadsto \color{blue}{\frac{t1}{\mathsf{neg}\left(u\right)}} \cdot \frac{v}{u} \]
                    10. lower-neg.f64N/A

                      \[\leadsto \frac{t1}{\color{blue}{-u}} \cdot \frac{v}{u} \]
                    11. lower-/.f6479.2

                      \[\leadsto \frac{t1}{-u} \cdot \color{blue}{\frac{v}{u}} \]
                  5. Applied rewrites79.2%

                    \[\leadsto \color{blue}{\frac{t1}{-u} \cdot \frac{v}{u}} \]
                  6. Step-by-step derivation
                    1. Applied rewrites69.1%

                      \[\leadsto t1 \cdot \color{blue}{\frac{v}{\left(-u\right) \cdot u}} \]
                    2. Step-by-step derivation
                      1. Applied rewrites82.6%

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

                      if -1.12e-64 < u < 5.5000000000000002e57

                      1. Initial program 64.3%

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

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

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

                          \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]
                        3. mul-1-negN/A

                          \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(v\right)}}{t1} \]
                        4. lower-neg.f6479.9

                          \[\leadsto \frac{\color{blue}{-v}}{t1} \]
                      5. Applied rewrites79.9%

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

                    Alternative 6: 79.2% accurate, 0.7× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\ \mathbf{if}\;t1 \leq -1.4 \cdot 10^{-62}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t1 \leq 1.9 \cdot 10^{+26}:\\ \;\;\;\;\frac{\frac{-t1}{u} \cdot v}{u}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
                    (FPCore (u v t1)
                     :precision binary64
                     (let* ((t_1 (/ v (fma -2.0 u (- t1)))))
                       (if (<= t1 -1.4e-62)
                         t_1
                         (if (<= t1 1.9e+26) (/ (* (/ (- t1) u) v) u) t_1))))
                    double code(double u, double v, double t1) {
                    	double t_1 = v / fma(-2.0, u, -t1);
                    	double tmp;
                    	if (t1 <= -1.4e-62) {
                    		tmp = t_1;
                    	} else if (t1 <= 1.9e+26) {
                    		tmp = ((-t1 / u) * v) / u;
                    	} else {
                    		tmp = t_1;
                    	}
                    	return tmp;
                    }
                    
                    function code(u, v, t1)
                    	t_1 = Float64(v / fma(-2.0, u, Float64(-t1)))
                    	tmp = 0.0
                    	if (t1 <= -1.4e-62)
                    		tmp = t_1;
                    	elseif (t1 <= 1.9e+26)
                    		tmp = Float64(Float64(Float64(Float64(-t1) / u) * v) / u);
                    	else
                    		tmp = t_1;
                    	end
                    	return tmp
                    end
                    
                    code[u_, v_, t1_] := Block[{t$95$1 = N[(v / N[(-2.0 * u + (-t1)), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t1, -1.4e-62], t$95$1, If[LessEqual[t1, 1.9e+26], N[(N[(N[((-t1) / u), $MachinePrecision] * v), $MachinePrecision] / u), $MachinePrecision], t$95$1]]]
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\
                    \mathbf{if}\;t1 \leq -1.4 \cdot 10^{-62}:\\
                    \;\;\;\;t\_1\\
                    
                    \mathbf{elif}\;t1 \leq 1.9 \cdot 10^{+26}:\\
                    \;\;\;\;\frac{\frac{-t1}{u} \cdot v}{u}\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;t\_1\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 2 regimes
                    2. if t1 < -1.40000000000000001e-62 or 1.9000000000000001e26 < t1

                      1. Initial program 58.2%

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

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

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

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

                          \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
                        5. clear-numN/A

                          \[\leadsto \color{blue}{\frac{1}{\frac{t1 + u}{-t1}}} \cdot \frac{v}{t1 + u} \]
                        6. frac-timesN/A

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

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

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

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

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

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

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

                          \[\leadsto \frac{1 \cdot v}{\color{blue}{\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}} \cdot \left(t1 + u\right)} \]
                        14. lower-neg.f6493.7

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

                          \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(t1 + u\right)}}{t1} \cdot \left(t1 + u\right)} \]
                        16. +-commutativeN/A

                          \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(u + t1\right)}}{t1} \cdot \left(t1 + u\right)} \]
                        17. lower-+.f6493.7

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

                          \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(t1 + u\right)}} \]
                        19. +-commutativeN/A

                          \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                        20. lower-+.f6493.7

                          \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                      4. Applied rewrites93.7%

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

                        \[\leadsto \frac{1 \cdot v}{\color{blue}{-2 \cdot u + -1 \cdot t1}} \]
                      6. Step-by-step derivation
                        1. lower-fma.f64N/A

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

                          \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
                        3. lower-neg.f6482.6

                          \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{-t1}\right)} \]
                      7. Applied rewrites82.6%

                        \[\leadsto \frac{1 \cdot v}{\color{blue}{\mathsf{fma}\left(-2, u, -t1\right)}} \]
                      8. Step-by-step derivation
                        1. lift-*.f64N/A

                          \[\leadsto \frac{\color{blue}{1 \cdot v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                        2. *-lft-identity82.6

                          \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                      9. Applied rewrites82.6%

                        \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]

                      if -1.40000000000000001e-62 < t1 < 1.9000000000000001e26

                      1. Initial program 83.4%

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

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

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

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

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

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

                          \[\leadsto \frac{t1 \cdot v}{\color{blue}{\left(-1 \cdot u\right) \cdot u}} \]
                        6. times-fracN/A

                          \[\leadsto \color{blue}{\frac{t1}{-1 \cdot u} \cdot \frac{v}{u}} \]
                        7. neg-mul-1N/A

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

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

                          \[\leadsto \color{blue}{\frac{t1}{\mathsf{neg}\left(u\right)}} \cdot \frac{v}{u} \]
                        10. lower-neg.f64N/A

                          \[\leadsto \frac{t1}{\color{blue}{-u}} \cdot \frac{v}{u} \]
                        11. lower-/.f6475.8

                          \[\leadsto \frac{t1}{-u} \cdot \color{blue}{\frac{v}{u}} \]
                      5. Applied rewrites75.8%

                        \[\leadsto \color{blue}{\frac{t1}{-u} \cdot \frac{v}{u}} \]
                      6. Step-by-step derivation
                        1. Applied rewrites77.7%

                          \[\leadsto \frac{\frac{-t1}{u} \cdot v}{\color{blue}{u}} \]
                      7. Recombined 2 regimes into one program.
                      8. Add Preprocessing

                      Alternative 7: 77.0% accurate, 0.8× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\ \mathbf{if}\;t1 \leq -1.4 \cdot 10^{-62}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t1 \leq 4.4 \cdot 10^{-37}:\\ \;\;\;\;\frac{\left(-t1\right) \cdot v}{u \cdot u}\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
                      (FPCore (u v t1)
                       :precision binary64
                       (let* ((t_1 (/ v (fma -2.0 u (- t1)))))
                         (if (<= t1 -1.4e-62)
                           t_1
                           (if (<= t1 4.4e-37) (/ (* (- t1) v) (* u u)) t_1))))
                      double code(double u, double v, double t1) {
                      	double t_1 = v / fma(-2.0, u, -t1);
                      	double tmp;
                      	if (t1 <= -1.4e-62) {
                      		tmp = t_1;
                      	} else if (t1 <= 4.4e-37) {
                      		tmp = (-t1 * v) / (u * u);
                      	} else {
                      		tmp = t_1;
                      	}
                      	return tmp;
                      }
                      
                      function code(u, v, t1)
                      	t_1 = Float64(v / fma(-2.0, u, Float64(-t1)))
                      	tmp = 0.0
                      	if (t1 <= -1.4e-62)
                      		tmp = t_1;
                      	elseif (t1 <= 4.4e-37)
                      		tmp = Float64(Float64(Float64(-t1) * v) / Float64(u * u));
                      	else
                      		tmp = t_1;
                      	end
                      	return tmp
                      end
                      
                      code[u_, v_, t1_] := Block[{t$95$1 = N[(v / N[(-2.0 * u + (-t1)), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t1, -1.4e-62], t$95$1, If[LessEqual[t1, 4.4e-37], N[(N[((-t1) * v), $MachinePrecision] / N[(u * u), $MachinePrecision]), $MachinePrecision], t$95$1]]]
                      
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\
                      \mathbf{if}\;t1 \leq -1.4 \cdot 10^{-62}:\\
                      \;\;\;\;t\_1\\
                      
                      \mathbf{elif}\;t1 \leq 4.4 \cdot 10^{-37}:\\
                      \;\;\;\;\frac{\left(-t1\right) \cdot v}{u \cdot u}\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;t\_1\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if t1 < -1.40000000000000001e-62 or 4.40000000000000004e-37 < t1

                        1. Initial program 60.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. lift-/.f64N/A

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

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

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

                            \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
                          5. clear-numN/A

                            \[\leadsto \color{blue}{\frac{1}{\frac{t1 + u}{-t1}}} \cdot \frac{v}{t1 + u} \]
                          6. frac-timesN/A

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

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

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

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

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

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

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

                            \[\leadsto \frac{1 \cdot v}{\color{blue}{\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}} \cdot \left(t1 + u\right)} \]
                          14. lower-neg.f6493.0

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

                            \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(t1 + u\right)}}{t1} \cdot \left(t1 + u\right)} \]
                          16. +-commutativeN/A

                            \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(u + t1\right)}}{t1} \cdot \left(t1 + u\right)} \]
                          17. lower-+.f6493.0

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

                            \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(t1 + u\right)}} \]
                          19. +-commutativeN/A

                            \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                          20. lower-+.f6493.0

                            \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                        4. Applied rewrites93.0%

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

                          \[\leadsto \frac{1 \cdot v}{\color{blue}{-2 \cdot u + -1 \cdot t1}} \]
                        6. Step-by-step derivation
                          1. lower-fma.f64N/A

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

                            \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
                          3. lower-neg.f6480.2

                            \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{-t1}\right)} \]
                        7. Applied rewrites80.2%

                          \[\leadsto \frac{1 \cdot v}{\color{blue}{\mathsf{fma}\left(-2, u, -t1\right)}} \]
                        8. Step-by-step derivation
                          1. lift-*.f64N/A

                            \[\leadsto \frac{\color{blue}{1 \cdot v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                          2. *-lft-identity80.2

                            \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                        9. Applied rewrites80.2%

                          \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]

                        if -1.40000000000000001e-62 < t1 < 4.40000000000000004e-37

                        1. Initial program 83.3%

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

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

                            \[\leadsto \frac{\left(-t1\right) \cdot v}{\color{blue}{u \cdot u}} \]
                          2. lower-*.f6478.9

                            \[\leadsto \frac{\left(-t1\right) \cdot v}{\color{blue}{u \cdot u}} \]
                        5. Applied rewrites78.9%

                          \[\leadsto \frac{\left(-t1\right) \cdot v}{\color{blue}{u \cdot u}} \]
                      3. Recombined 2 regimes into one program.
                      4. Add Preprocessing

                      Alternative 8: 77.2% accurate, 0.8× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\ \mathbf{if}\;t1 \leq -1.4 \cdot 10^{-62}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;t1 \leq 4.4 \cdot 10^{-37}:\\ \;\;\;\;\frac{v}{\left(-u\right) \cdot u} \cdot t1\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
                      (FPCore (u v t1)
                       :precision binary64
                       (let* ((t_1 (/ v (fma -2.0 u (- t1)))))
                         (if (<= t1 -1.4e-62)
                           t_1
                           (if (<= t1 4.4e-37) (* (/ v (* (- u) u)) t1) t_1))))
                      double code(double u, double v, double t1) {
                      	double t_1 = v / fma(-2.0, u, -t1);
                      	double tmp;
                      	if (t1 <= -1.4e-62) {
                      		tmp = t_1;
                      	} else if (t1 <= 4.4e-37) {
                      		tmp = (v / (-u * u)) * t1;
                      	} else {
                      		tmp = t_1;
                      	}
                      	return tmp;
                      }
                      
                      function code(u, v, t1)
                      	t_1 = Float64(v / fma(-2.0, u, Float64(-t1)))
                      	tmp = 0.0
                      	if (t1 <= -1.4e-62)
                      		tmp = t_1;
                      	elseif (t1 <= 4.4e-37)
                      		tmp = Float64(Float64(v / Float64(Float64(-u) * u)) * t1);
                      	else
                      		tmp = t_1;
                      	end
                      	return tmp
                      end
                      
                      code[u_, v_, t1_] := Block[{t$95$1 = N[(v / N[(-2.0 * u + (-t1)), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t1, -1.4e-62], t$95$1, If[LessEqual[t1, 4.4e-37], N[(N[(v / N[((-u) * u), $MachinePrecision]), $MachinePrecision] * t1), $MachinePrecision], t$95$1]]]
                      
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      t_1 := \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\
                      \mathbf{if}\;t1 \leq -1.4 \cdot 10^{-62}:\\
                      \;\;\;\;t\_1\\
                      
                      \mathbf{elif}\;t1 \leq 4.4 \cdot 10^{-37}:\\
                      \;\;\;\;\frac{v}{\left(-u\right) \cdot u} \cdot t1\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;t\_1\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if t1 < -1.40000000000000001e-62 or 4.40000000000000004e-37 < t1

                        1. Initial program 60.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. lift-/.f64N/A

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

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

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

                            \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
                          5. clear-numN/A

                            \[\leadsto \color{blue}{\frac{1}{\frac{t1 + u}{-t1}}} \cdot \frac{v}{t1 + u} \]
                          6. frac-timesN/A

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

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

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

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

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

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

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

                            \[\leadsto \frac{1 \cdot v}{\color{blue}{\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}} \cdot \left(t1 + u\right)} \]
                          14. lower-neg.f6493.0

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

                            \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(t1 + u\right)}}{t1} \cdot \left(t1 + u\right)} \]
                          16. +-commutativeN/A

                            \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(u + t1\right)}}{t1} \cdot \left(t1 + u\right)} \]
                          17. lower-+.f6493.0

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

                            \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(t1 + u\right)}} \]
                          19. +-commutativeN/A

                            \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                          20. lower-+.f6493.0

                            \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                        4. Applied rewrites93.0%

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

                          \[\leadsto \frac{1 \cdot v}{\color{blue}{-2 \cdot u + -1 \cdot t1}} \]
                        6. Step-by-step derivation
                          1. lower-fma.f64N/A

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

                            \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
                          3. lower-neg.f6480.2

                            \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{-t1}\right)} \]
                        7. Applied rewrites80.2%

                          \[\leadsto \frac{1 \cdot v}{\color{blue}{\mathsf{fma}\left(-2, u, -t1\right)}} \]
                        8. Step-by-step derivation
                          1. lift-*.f64N/A

                            \[\leadsto \frac{\color{blue}{1 \cdot v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                          2. *-lft-identity80.2

                            \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                        9. Applied rewrites80.2%

                          \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]

                        if -1.40000000000000001e-62 < t1 < 4.40000000000000004e-37

                        1. Initial program 83.3%

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

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

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

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

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

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

                            \[\leadsto \frac{t1 \cdot v}{\color{blue}{\left(-1 \cdot u\right) \cdot u}} \]
                          6. times-fracN/A

                            \[\leadsto \color{blue}{\frac{t1}{-1 \cdot u} \cdot \frac{v}{u}} \]
                          7. neg-mul-1N/A

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

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

                            \[\leadsto \color{blue}{\frac{t1}{\mathsf{neg}\left(u\right)}} \cdot \frac{v}{u} \]
                          10. lower-neg.f64N/A

                            \[\leadsto \frac{t1}{\color{blue}{-u}} \cdot \frac{v}{u} \]
                          11. lower-/.f6478.2

                            \[\leadsto \frac{t1}{-u} \cdot \color{blue}{\frac{v}{u}} \]
                        5. Applied rewrites78.2%

                          \[\leadsto \color{blue}{\frac{t1}{-u} \cdot \frac{v}{u}} \]
                        6. Step-by-step derivation
                          1. Applied rewrites77.3%

                            \[\leadsto t1 \cdot \color{blue}{\frac{v}{\left(-u\right) \cdot u}} \]
                        7. Recombined 2 regimes into one program.
                        8. Final simplification78.9%

                          \[\leadsto \begin{array}{l} \mathbf{if}\;t1 \leq -1.4 \cdot 10^{-62}:\\ \;\;\;\;\frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\ \mathbf{elif}\;t1 \leq 4.4 \cdot 10^{-37}:\\ \;\;\;\;\frac{v}{\left(-u\right) \cdot u} \cdot t1\\ \mathbf{else}:\\ \;\;\;\;\frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}\\ \end{array} \]
                        9. Add Preprocessing

                        Alternative 9: 98.2% accurate, 0.8× speedup?

                        \[\begin{array}{l} \\ \frac{\frac{t1}{t1 + u} \cdot v}{-\left(t1 + u\right)} \end{array} \]
                        (FPCore (u v t1) :precision binary64 (/ (* (/ t1 (+ t1 u)) v) (- (+ t1 u))))
                        double code(double u, double v, double t1) {
                        	return ((t1 / (t1 + u)) * 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)) * v) / -(t1 + u)
                        end function
                        
                        public static double code(double u, double v, double t1) {
                        	return ((t1 / (t1 + u)) * v) / -(t1 + u);
                        }
                        
                        def code(u, v, t1):
                        	return ((t1 / (t1 + u)) * v) / -(t1 + u)
                        
                        function code(u, v, t1)
                        	return Float64(Float64(Float64(t1 / Float64(t1 + u)) * v) / Float64(-Float64(t1 + u)))
                        end
                        
                        function tmp = code(u, v, t1)
                        	tmp = ((t1 / (t1 + u)) * v) / -(t1 + u);
                        end
                        
                        code[u_, v_, t1_] := N[(N[(N[(t1 / N[(t1 + u), $MachinePrecision]), $MachinePrecision] * v), $MachinePrecision] / (-N[(t1 + u), $MachinePrecision])), $MachinePrecision]
                        
                        \begin{array}{l}
                        
                        \\
                        \frac{\frac{t1}{t1 + u} \cdot v}{-\left(t1 + u\right)}
                        \end{array}
                        
                        Derivation
                        1. Initial program 70.1%

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

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

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

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

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

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

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

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

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

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

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

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

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

                            \[\leadsto \frac{\color{blue}{\left(-v\right)} \cdot \frac{t1}{t1 + u}}{t1 + u} \]
                          14. lower-/.f6497.5

                            \[\leadsto \frac{\left(-v\right) \cdot \color{blue}{\frac{t1}{t1 + u}}}{t1 + u} \]
                          15. lift-+.f64N/A

                            \[\leadsto \frac{\left(-v\right) \cdot \frac{t1}{\color{blue}{t1 + u}}}{t1 + u} \]
                          16. +-commutativeN/A

                            \[\leadsto \frac{\left(-v\right) \cdot \frac{t1}{\color{blue}{u + t1}}}{t1 + u} \]
                          17. lower-+.f6497.5

                            \[\leadsto \frac{\left(-v\right) \cdot \frac{t1}{\color{blue}{u + t1}}}{t1 + u} \]
                          18. lift-+.f64N/A

                            \[\leadsto \frac{\left(-v\right) \cdot \frac{t1}{u + t1}}{\color{blue}{t1 + u}} \]
                          19. +-commutativeN/A

                            \[\leadsto \frac{\left(-v\right) \cdot \frac{t1}{u + t1}}{\color{blue}{u + t1}} \]
                          20. lower-+.f6497.5

                            \[\leadsto \frac{\left(-v\right) \cdot \frac{t1}{u + t1}}{\color{blue}{u + t1}} \]
                        4. Applied rewrites97.5%

                          \[\leadsto \color{blue}{\frac{\left(-v\right) \cdot \frac{t1}{u + t1}}{u + t1}} \]
                        5. Final simplification97.5%

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

                        Alternative 10: 56.4% accurate, 1.3× speedup?

                        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u \leq -1.35 \cdot 10^{+118}:\\ \;\;\;\;\frac{v}{-2 \cdot u}\\ \mathbf{else}:\\ \;\;\;\;\frac{-v}{t1}\\ \end{array} \end{array} \]
                        (FPCore (u v t1)
                         :precision binary64
                         (if (<= u -1.35e+118) (/ v (* -2.0 u)) (/ (- v) t1)))
                        double code(double u, double v, double t1) {
                        	double tmp;
                        	if (u <= -1.35e+118) {
                        		tmp = v / (-2.0 * u);
                        	} else {
                        		tmp = -v / t1;
                        	}
                        	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 (u <= (-1.35d+118)) then
                                tmp = v / ((-2.0d0) * u)
                            else
                                tmp = -v / t1
                            end if
                            code = tmp
                        end function
                        
                        public static double code(double u, double v, double t1) {
                        	double tmp;
                        	if (u <= -1.35e+118) {
                        		tmp = v / (-2.0 * u);
                        	} else {
                        		tmp = -v / t1;
                        	}
                        	return tmp;
                        }
                        
                        def code(u, v, t1):
                        	tmp = 0
                        	if u <= -1.35e+118:
                        		tmp = v / (-2.0 * u)
                        	else:
                        		tmp = -v / t1
                        	return tmp
                        
                        function code(u, v, t1)
                        	tmp = 0.0
                        	if (u <= -1.35e+118)
                        		tmp = Float64(v / Float64(-2.0 * u));
                        	else
                        		tmp = Float64(Float64(-v) / t1);
                        	end
                        	return tmp
                        end
                        
                        function tmp_2 = code(u, v, t1)
                        	tmp = 0.0;
                        	if (u <= -1.35e+118)
                        		tmp = v / (-2.0 * u);
                        	else
                        		tmp = -v / t1;
                        	end
                        	tmp_2 = tmp;
                        end
                        
                        code[u_, v_, t1_] := If[LessEqual[u, -1.35e+118], N[(v / N[(-2.0 * u), $MachinePrecision]), $MachinePrecision], N[((-v) / t1), $MachinePrecision]]
                        
                        \begin{array}{l}
                        
                        \\
                        \begin{array}{l}
                        \mathbf{if}\;u \leq -1.35 \cdot 10^{+118}:\\
                        \;\;\;\;\frac{v}{-2 \cdot u}\\
                        
                        \mathbf{else}:\\
                        \;\;\;\;\frac{-v}{t1}\\
                        
                        
                        \end{array}
                        \end{array}
                        
                        Derivation
                        1. Split input into 2 regimes
                        2. if u < -1.35e118

                          1. Initial program 73.1%

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

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

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

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

                              \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
                            5. clear-numN/A

                              \[\leadsto \color{blue}{\frac{1}{\frac{t1 + u}{-t1}}} \cdot \frac{v}{t1 + u} \]
                            6. frac-timesN/A

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

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

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

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

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

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

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

                              \[\leadsto \frac{1 \cdot v}{\color{blue}{\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}} \cdot \left(t1 + u\right)} \]
                            14. lower-neg.f6483.2

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

                              \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(t1 + u\right)}}{t1} \cdot \left(t1 + u\right)} \]
                            16. +-commutativeN/A

                              \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(u + t1\right)}}{t1} \cdot \left(t1 + u\right)} \]
                            17. lower-+.f6483.2

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

                              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(t1 + u\right)}} \]
                            19. +-commutativeN/A

                              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                            20. lower-+.f6483.2

                              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                          4. Applied rewrites83.2%

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

                            \[\leadsto \frac{1 \cdot v}{\color{blue}{-2 \cdot u + -1 \cdot t1}} \]
                          6. Step-by-step derivation
                            1. lower-fma.f64N/A

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

                              \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
                            3. lower-neg.f6444.0

                              \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{-t1}\right)} \]
                          7. Applied rewrites44.0%

                            \[\leadsto \frac{1 \cdot v}{\color{blue}{\mathsf{fma}\left(-2, u, -t1\right)}} \]
                          8. Step-by-step derivation
                            1. lift-*.f64N/A

                              \[\leadsto \frac{\color{blue}{1 \cdot v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                            2. *-lft-identity44.0

                              \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                          9. Applied rewrites44.0%

                            \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                          10. Taylor expanded in u around inf

                            \[\leadsto \frac{v}{-2 \cdot \color{blue}{u}} \]
                          11. Step-by-step derivation
                            1. Applied rewrites37.7%

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

                            if -1.35e118 < u

                            1. Initial program 69.5%

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

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

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

                                \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]
                              3. mul-1-negN/A

                                \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(v\right)}}{t1} \]
                              4. lower-neg.f6460.8

                                \[\leadsto \frac{\color{blue}{-v}}{t1} \]
                            5. Applied rewrites60.8%

                              \[\leadsto \color{blue}{\frac{-v}{t1}} \]
                          12. Recombined 2 regimes into one program.
                          13. Add Preprocessing

                          Alternative 11: 62.1% accurate, 1.5× speedup?

                          \[\begin{array}{l} \\ \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)} \end{array} \]
                          (FPCore (u v t1) :precision binary64 (/ v (fma -2.0 u (- t1))))
                          double code(double u, double v, double t1) {
                          	return v / fma(-2.0, u, -t1);
                          }
                          
                          function code(u, v, t1)
                          	return Float64(v / fma(-2.0, u, Float64(-t1)))
                          end
                          
                          code[u_, v_, t1_] := N[(v / N[(-2.0 * u + (-t1)), $MachinePrecision]), $MachinePrecision]
                          
                          \begin{array}{l}
                          
                          \\
                          \frac{v}{\mathsf{fma}\left(-2, u, -t1\right)}
                          \end{array}
                          
                          Derivation
                          1. Initial program 70.1%

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

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

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

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

                              \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
                            5. clear-numN/A

                              \[\leadsto \color{blue}{\frac{1}{\frac{t1 + u}{-t1}}} \cdot \frac{v}{t1 + u} \]
                            6. frac-timesN/A

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

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

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

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

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

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

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

                              \[\leadsto \frac{1 \cdot v}{\color{blue}{\frac{\mathsf{neg}\left(\left(t1 + u\right)\right)}{t1}} \cdot \left(t1 + u\right)} \]
                            14. lower-neg.f6492.9

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

                              \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(t1 + u\right)}}{t1} \cdot \left(t1 + u\right)} \]
                            16. +-commutativeN/A

                              \[\leadsto \frac{1 \cdot v}{\frac{-\color{blue}{\left(u + t1\right)}}{t1} \cdot \left(t1 + u\right)} \]
                            17. lower-+.f6492.9

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

                              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(t1 + u\right)}} \]
                            19. +-commutativeN/A

                              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                            20. lower-+.f6492.9

                              \[\leadsto \frac{1 \cdot v}{\frac{-\left(u + t1\right)}{t1} \cdot \color{blue}{\left(u + t1\right)}} \]
                          4. Applied rewrites92.9%

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

                            \[\leadsto \frac{1 \cdot v}{\color{blue}{-2 \cdot u + -1 \cdot t1}} \]
                          6. Step-by-step derivation
                            1. lower-fma.f64N/A

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

                              \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{\mathsf{neg}\left(t1\right)}\right)} \]
                            3. lower-neg.f6460.4

                              \[\leadsto \frac{1 \cdot v}{\mathsf{fma}\left(-2, u, \color{blue}{-t1}\right)} \]
                          7. Applied rewrites60.4%

                            \[\leadsto \frac{1 \cdot v}{\color{blue}{\mathsf{fma}\left(-2, u, -t1\right)}} \]
                          8. Step-by-step derivation
                            1. lift-*.f64N/A

                              \[\leadsto \frac{\color{blue}{1 \cdot v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                            2. *-lft-identity60.4

                              \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                          9. Applied rewrites60.4%

                            \[\leadsto \frac{\color{blue}{v}}{\mathsf{fma}\left(-2, u, -t1\right)} \]
                          10. Add Preprocessing

                          Alternative 12: 54.2% accurate, 2.1× speedup?

                          \[\begin{array}{l} \\ \frac{-v}{t1} \end{array} \]
                          (FPCore (u v t1) :precision binary64 (/ (- v) t1))
                          double code(double u, double v, double t1) {
                          	return -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 = -v / t1
                          end function
                          
                          public static double code(double u, double v, double t1) {
                          	return -v / t1;
                          }
                          
                          def code(u, v, t1):
                          	return -v / t1
                          
                          function code(u, v, t1)
                          	return Float64(Float64(-v) / t1)
                          end
                          
                          function tmp = code(u, v, t1)
                          	tmp = -v / t1;
                          end
                          
                          code[u_, v_, t1_] := N[((-v) / t1), $MachinePrecision]
                          
                          \begin{array}{l}
                          
                          \\
                          \frac{-v}{t1}
                          \end{array}
                          
                          Derivation
                          1. Initial program 70.1%

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

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

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

                              \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]
                            3. mul-1-negN/A

                              \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(v\right)}}{t1} \]
                            4. lower-neg.f6453.9

                              \[\leadsto \frac{\color{blue}{-v}}{t1} \]
                          5. Applied rewrites53.9%

                            \[\leadsto \color{blue}{\frac{-v}{t1}} \]
                          6. Add Preprocessing

                          Reproduce

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