Toniolo and Linder, Equation (7)

Percentage Accurate: 33.1% → 79.2%
Time: 14.2s
Alternatives: 8
Speedup: 85.0×

Specification

?
\[\begin{array}{l} \\ \frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \end{array} \]
(FPCore (x l t)
 :precision binary64
 (/
  (* (sqrt 2.0) t)
  (sqrt (- (* (/ (+ x 1.0) (- x 1.0)) (+ (* l l) (* 2.0 (* t t)))) (* l l)))))
double code(double x, double l, double t) {
	return (sqrt(2.0) * t) / sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)));
}
real(8) function code(x, l, t)
    real(8), intent (in) :: x
    real(8), intent (in) :: l
    real(8), intent (in) :: t
    code = (sqrt(2.0d0) * t) / sqrt(((((x + 1.0d0) / (x - 1.0d0)) * ((l * l) + (2.0d0 * (t * t)))) - (l * l)))
end function
public static double code(double x, double l, double t) {
	return (Math.sqrt(2.0) * t) / Math.sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)));
}
def code(x, l, t):
	return (math.sqrt(2.0) * t) / math.sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)))
function code(x, l, t)
	return Float64(Float64(sqrt(2.0) * t) / sqrt(Float64(Float64(Float64(Float64(x + 1.0) / Float64(x - 1.0)) * Float64(Float64(l * l) + Float64(2.0 * Float64(t * t)))) - Float64(l * l))))
end
function tmp = code(x, l, t)
	tmp = (sqrt(2.0) * t) / sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)));
end
code[x_, l_, t_] := N[(N[(N[Sqrt[2.0], $MachinePrecision] * t), $MachinePrecision] / N[Sqrt[N[(N[(N[(N[(x + 1.0), $MachinePrecision] / N[(x - 1.0), $MachinePrecision]), $MachinePrecision] * N[(N[(l * l), $MachinePrecision] + N[(2.0 * N[(t * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(l * l), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}
\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 8 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: 33.1% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \end{array} \]
(FPCore (x l t)
 :precision binary64
 (/
  (* (sqrt 2.0) t)
  (sqrt (- (* (/ (+ x 1.0) (- x 1.0)) (+ (* l l) (* 2.0 (* t t)))) (* l l)))))
double code(double x, double l, double t) {
	return (sqrt(2.0) * t) / sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)));
}
real(8) function code(x, l, t)
    real(8), intent (in) :: x
    real(8), intent (in) :: l
    real(8), intent (in) :: t
    code = (sqrt(2.0d0) * t) / sqrt(((((x + 1.0d0) / (x - 1.0d0)) * ((l * l) + (2.0d0 * (t * t)))) - (l * l)))
end function
public static double code(double x, double l, double t) {
	return (Math.sqrt(2.0) * t) / Math.sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)));
}
def code(x, l, t):
	return (math.sqrt(2.0) * t) / math.sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)))
function code(x, l, t)
	return Float64(Float64(sqrt(2.0) * t) / sqrt(Float64(Float64(Float64(Float64(x + 1.0) / Float64(x - 1.0)) * Float64(Float64(l * l) + Float64(2.0 * Float64(t * t)))) - Float64(l * l))))
end
function tmp = code(x, l, t)
	tmp = (sqrt(2.0) * t) / sqrt(((((x + 1.0) / (x - 1.0)) * ((l * l) + (2.0 * (t * t)))) - (l * l)));
end
code[x_, l_, t_] := N[(N[(N[Sqrt[2.0], $MachinePrecision] * t), $MachinePrecision] / N[Sqrt[N[(N[(N[(N[(x + 1.0), $MachinePrecision] / N[(x - 1.0), $MachinePrecision]), $MachinePrecision] * N[(N[(l * l), $MachinePrecision] + N[(2.0 * N[(t * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(l * l), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}
\end{array}

Alternative 1: 79.2% accurate, 1.0× speedup?

\[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ \begin{array}{l} t_2 := \sqrt{2} \cdot t\_m\\ t\_s \cdot \begin{array}{l} \mathbf{if}\;l\_m \cdot l\_m \leq 10^{+276}:\\ \;\;\;\;\frac{t\_2}{t\_2 \cdot \sqrt{\frac{x + 1}{x + -1}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_2}{l\_m \cdot \sqrt{\frac{2}{x}}}\\ \end{array} \end{array} \end{array} \]
l_m = (fabs.f64 l)
t\_m = (fabs.f64 t)
t\_s = (copysign.f64 #s(literal 1 binary64) t)
(FPCore (t_s x l_m t_m)
 :precision binary64
 (let* ((t_2 (* (sqrt 2.0) t_m)))
   (*
    t_s
    (if (<= (* l_m l_m) 1e+276)
      (/ t_2 (* t_2 (sqrt (/ (+ x 1.0) (+ x -1.0)))))
      (/ t_2 (* l_m (sqrt (/ 2.0 x))))))))
l_m = fabs(l);
t\_m = fabs(t);
t\_s = copysign(1.0, t);
double code(double t_s, double x, double l_m, double t_m) {
	double t_2 = sqrt(2.0) * t_m;
	double tmp;
	if ((l_m * l_m) <= 1e+276) {
		tmp = t_2 / (t_2 * sqrt(((x + 1.0) / (x + -1.0))));
	} else {
		tmp = t_2 / (l_m * sqrt((2.0 / x)));
	}
	return t_s * tmp;
}
l_m = abs(l)
t\_m = abs(t)
t\_s = copysign(1.0d0, t)
real(8) function code(t_s, x, l_m, t_m)
    real(8), intent (in) :: t_s
    real(8), intent (in) :: x
    real(8), intent (in) :: l_m
    real(8), intent (in) :: t_m
    real(8) :: t_2
    real(8) :: tmp
    t_2 = sqrt(2.0d0) * t_m
    if ((l_m * l_m) <= 1d+276) then
        tmp = t_2 / (t_2 * sqrt(((x + 1.0d0) / (x + (-1.0d0)))))
    else
        tmp = t_2 / (l_m * sqrt((2.0d0 / x)))
    end if
    code = t_s * tmp
end function
l_m = Math.abs(l);
t\_m = Math.abs(t);
t\_s = Math.copySign(1.0, t);
public static double code(double t_s, double x, double l_m, double t_m) {
	double t_2 = Math.sqrt(2.0) * t_m;
	double tmp;
	if ((l_m * l_m) <= 1e+276) {
		tmp = t_2 / (t_2 * Math.sqrt(((x + 1.0) / (x + -1.0))));
	} else {
		tmp = t_2 / (l_m * Math.sqrt((2.0 / x)));
	}
	return t_s * tmp;
}
l_m = math.fabs(l)
t\_m = math.fabs(t)
t\_s = math.copysign(1.0, t)
def code(t_s, x, l_m, t_m):
	t_2 = math.sqrt(2.0) * t_m
	tmp = 0
	if (l_m * l_m) <= 1e+276:
		tmp = t_2 / (t_2 * math.sqrt(((x + 1.0) / (x + -1.0))))
	else:
		tmp = t_2 / (l_m * math.sqrt((2.0 / x)))
	return t_s * tmp
l_m = abs(l)
t\_m = abs(t)
t\_s = copysign(1.0, t)
function code(t_s, x, l_m, t_m)
	t_2 = Float64(sqrt(2.0) * t_m)
	tmp = 0.0
	if (Float64(l_m * l_m) <= 1e+276)
		tmp = Float64(t_2 / Float64(t_2 * sqrt(Float64(Float64(x + 1.0) / Float64(x + -1.0)))));
	else
		tmp = Float64(t_2 / Float64(l_m * sqrt(Float64(2.0 / x))));
	end
	return Float64(t_s * tmp)
end
l_m = abs(l);
t\_m = abs(t);
t\_s = sign(t) * abs(1.0);
function tmp_2 = code(t_s, x, l_m, t_m)
	t_2 = sqrt(2.0) * t_m;
	tmp = 0.0;
	if ((l_m * l_m) <= 1e+276)
		tmp = t_2 / (t_2 * sqrt(((x + 1.0) / (x + -1.0))));
	else
		tmp = t_2 / (l_m * sqrt((2.0 / x)));
	end
	tmp_2 = t_s * tmp;
end
l_m = N[Abs[l], $MachinePrecision]
t\_m = N[Abs[t], $MachinePrecision]
t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[t$95$s_, x_, l$95$m_, t$95$m_] := Block[{t$95$2 = N[(N[Sqrt[2.0], $MachinePrecision] * t$95$m), $MachinePrecision]}, N[(t$95$s * If[LessEqual[N[(l$95$m * l$95$m), $MachinePrecision], 1e+276], N[(t$95$2 / N[(t$95$2 * N[Sqrt[N[(N[(x + 1.0), $MachinePrecision] / N[(x + -1.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(t$95$2 / N[(l$95$m * N[Sqrt[N[(2.0 / x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]]
\begin{array}{l}
l_m = \left|\ell\right|
\\
t\_m = \left|t\right|
\\
t\_s = \mathsf{copysign}\left(1, t\right)

\\
\begin{array}{l}
t_2 := \sqrt{2} \cdot t\_m\\
t\_s \cdot \begin{array}{l}
\mathbf{if}\;l\_m \cdot l\_m \leq 10^{+276}:\\
\;\;\;\;\frac{t\_2}{t\_2 \cdot \sqrt{\frac{x + 1}{x + -1}}}\\

\mathbf{else}:\\
\;\;\;\;\frac{t\_2}{l\_m \cdot \sqrt{\frac{2}{x}}}\\


\end{array}
\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 l l) < 1.0000000000000001e276

    1. Initial program 40.1%

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

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x - 1}}}} \]
    4. Step-by-step derivation
      1. lower-*.f64N/A

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

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

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

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

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

        \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{\color{blue}{1 + x}}{x - 1}}} \]
      7. sub-negN/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{\color{blue}{x + \left(\mathsf{neg}\left(1\right)\right)}}}} \]
      8. metadata-evalN/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x + \color{blue}{-1}}}} \]
      9. lower-+.f6443.2

        \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{\color{blue}{x + -1}}}} \]
    5. Applied rewrites43.2%

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x + -1}}}} \]

    if 1.0000000000000001e276 < (*.f64 l l)

    1. Initial program 0.0%

      \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
    2. Add Preprocessing
    3. Applied rewrites0.0%

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
    4. Taylor expanded in l around inf

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
    5. Step-by-step derivation
      1. lower-*.f64N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
      2. lower-sqrt.f64N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \color{blue}{\sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
      3. sub-negN/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + \left(\mathsf{neg}\left(1\right)\right)}}} \]
      4. metadata-evalN/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + \color{blue}{-1}}} \]
      5. lower-+.f64N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + -1}}} \]
      6. lower-/.f64N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1}} + -1}} \]
      7. unpow2N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right) \cdot \left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
      8. lower-*.f64N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right) \cdot \left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
      9. lower-+.f64N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right)} \cdot \left(1 + x\right)}{{x}^{2} - 1} + -1}} \]
      10. lower-+.f64N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \color{blue}{\left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
      11. sub-negN/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} + -1}} \]
      12. unpow2N/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} + -1}} \]
      13. metadata-evalN/A

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{x \cdot x + \color{blue}{-1}} + -1}} \]
      14. lower-fma.f642.9

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} + -1}} \]
    6. Applied rewrites2.9%

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\mathsf{fma}\left(x, x, -1\right)} + -1}}} \]
    7. Taylor expanded in x around inf

      \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}} \]
    8. Step-by-step derivation
      1. Applied rewrites50.1%

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}} \]
    9. Recombined 2 regimes into one program.
    10. Final simplification44.4%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \leq 10^{+276}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\left(\sqrt{2} \cdot t\right) \cdot \sqrt{\frac{x + 1}{x + -1}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}}\\ \end{array} \]
    11. Add Preprocessing

    Alternative 2: 79.1% accurate, 1.2× speedup?

    \[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ \begin{array}{l} t_2 := \sqrt{2} \cdot t\_m\\ t\_s \cdot \begin{array}{l} \mathbf{if}\;l\_m \cdot l\_m \leq 10^{+276}:\\ \;\;\;\;\frac{t\_2}{t\_m \cdot \sqrt{\frac{\mathsf{fma}\left(x, 2, 2\right)}{x + -1}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_2}{l\_m \cdot \sqrt{\frac{2}{x}}}\\ \end{array} \end{array} \end{array} \]
    l_m = (fabs.f64 l)
    t\_m = (fabs.f64 t)
    t\_s = (copysign.f64 #s(literal 1 binary64) t)
    (FPCore (t_s x l_m t_m)
     :precision binary64
     (let* ((t_2 (* (sqrt 2.0) t_m)))
       (*
        t_s
        (if (<= (* l_m l_m) 1e+276)
          (/ t_2 (* t_m (sqrt (/ (fma x 2.0 2.0) (+ x -1.0)))))
          (/ t_2 (* l_m (sqrt (/ 2.0 x))))))))
    l_m = fabs(l);
    t\_m = fabs(t);
    t\_s = copysign(1.0, t);
    double code(double t_s, double x, double l_m, double t_m) {
    	double t_2 = sqrt(2.0) * t_m;
    	double tmp;
    	if ((l_m * l_m) <= 1e+276) {
    		tmp = t_2 / (t_m * sqrt((fma(x, 2.0, 2.0) / (x + -1.0))));
    	} else {
    		tmp = t_2 / (l_m * sqrt((2.0 / x)));
    	}
    	return t_s * tmp;
    }
    
    l_m = abs(l)
    t\_m = abs(t)
    t\_s = copysign(1.0, t)
    function code(t_s, x, l_m, t_m)
    	t_2 = Float64(sqrt(2.0) * t_m)
    	tmp = 0.0
    	if (Float64(l_m * l_m) <= 1e+276)
    		tmp = Float64(t_2 / Float64(t_m * sqrt(Float64(fma(x, 2.0, 2.0) / Float64(x + -1.0)))));
    	else
    		tmp = Float64(t_2 / Float64(l_m * sqrt(Float64(2.0 / x))));
    	end
    	return Float64(t_s * tmp)
    end
    
    l_m = N[Abs[l], $MachinePrecision]
    t\_m = N[Abs[t], $MachinePrecision]
    t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
    code[t$95$s_, x_, l$95$m_, t$95$m_] := Block[{t$95$2 = N[(N[Sqrt[2.0], $MachinePrecision] * t$95$m), $MachinePrecision]}, N[(t$95$s * If[LessEqual[N[(l$95$m * l$95$m), $MachinePrecision], 1e+276], N[(t$95$2 / N[(t$95$m * N[Sqrt[N[(N[(x * 2.0 + 2.0), $MachinePrecision] / N[(x + -1.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(t$95$2 / N[(l$95$m * N[Sqrt[N[(2.0 / x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]]
    
    \begin{array}{l}
    l_m = \left|\ell\right|
    \\
    t\_m = \left|t\right|
    \\
    t\_s = \mathsf{copysign}\left(1, t\right)
    
    \\
    \begin{array}{l}
    t_2 := \sqrt{2} \cdot t\_m\\
    t\_s \cdot \begin{array}{l}
    \mathbf{if}\;l\_m \cdot l\_m \leq 10^{+276}:\\
    \;\;\;\;\frac{t\_2}{t\_m \cdot \sqrt{\frac{\mathsf{fma}\left(x, 2, 2\right)}{x + -1}}}\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{t\_2}{l\_m \cdot \sqrt{\frac{2}{x}}}\\
    
    
    \end{array}
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (*.f64 l l) < 1.0000000000000001e276

      1. Initial program 40.1%

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

        \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x - 1}}}} \]
      4. Step-by-step derivation
        1. lower-*.f64N/A

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

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

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

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

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

          \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{\color{blue}{1 + x}}{x - 1}}} \]
        7. sub-negN/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{\color{blue}{x + \left(\mathsf{neg}\left(1\right)\right)}}}} \]
        8. metadata-evalN/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x + \color{blue}{-1}}}} \]
        9. lower-+.f6443.2

          \[\leadsto \frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{\color{blue}{x + -1}}}} \]
      5. Applied rewrites43.2%

        \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x + -1}}}} \]
      6. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\sqrt{2} \cdot t}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x + -1}}}} \]
        2. clear-numN/A

          \[\leadsto \color{blue}{\frac{1}{\frac{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x + -1}}}{\sqrt{2} \cdot t}}} \]
        3. associate-/r/N/A

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

          \[\leadsto \color{blue}{\frac{1}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1 + x}{x + -1}}} \cdot \left(\sqrt{2} \cdot t\right)} \]
      7. Applied rewrites43.1%

        \[\leadsto \color{blue}{\frac{1}{t \cdot \sqrt{2 \cdot \frac{x + 1}{x + -1}}} \cdot \left(\sqrt{2} \cdot t\right)} \]
      8. Applied rewrites43.2%

        \[\leadsto \color{blue}{\frac{t \cdot \sqrt{2}}{t \cdot \sqrt{\frac{\mathsf{fma}\left(x, 2, 2\right)}{x + -1}}}} \]

      if 1.0000000000000001e276 < (*.f64 l l)

      1. Initial program 0.0%

        \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
      2. Add Preprocessing
      3. Applied rewrites0.0%

        \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
      4. Taylor expanded in l around inf

        \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
      5. Step-by-step derivation
        1. lower-*.f64N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
        2. lower-sqrt.f64N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \color{blue}{\sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
        3. sub-negN/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + \left(\mathsf{neg}\left(1\right)\right)}}} \]
        4. metadata-evalN/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + \color{blue}{-1}}} \]
        5. lower-+.f64N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + -1}}} \]
        6. lower-/.f64N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1}} + -1}} \]
        7. unpow2N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right) \cdot \left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
        8. lower-*.f64N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right) \cdot \left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
        9. lower-+.f64N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right)} \cdot \left(1 + x\right)}{{x}^{2} - 1} + -1}} \]
        10. lower-+.f64N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \color{blue}{\left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
        11. sub-negN/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} + -1}} \]
        12. unpow2N/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} + -1}} \]
        13. metadata-evalN/A

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{x \cdot x + \color{blue}{-1}} + -1}} \]
        14. lower-fma.f642.9

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} + -1}} \]
      6. Applied rewrites2.9%

        \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\mathsf{fma}\left(x, x, -1\right)} + -1}}} \]
      7. Taylor expanded in x around inf

        \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}} \]
      8. Step-by-step derivation
        1. Applied rewrites50.1%

          \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}} \]
      9. Recombined 2 regimes into one program.
      10. Final simplification44.4%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \leq 10^{+276}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{t \cdot \sqrt{\frac{\mathsf{fma}\left(x, 2, 2\right)}{x + -1}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}}\\ \end{array} \]
      11. Add Preprocessing

      Alternative 3: 79.0% accurate, 1.3× speedup?

      \[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ t\_s \cdot \begin{array}{l} \mathbf{if}\;l\_m \cdot l\_m \leq 10^{+276}:\\ \;\;\;\;\frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t\_m}{l\_m \cdot \sqrt{\frac{2}{x}}}\\ \end{array} \end{array} \]
      l_m = (fabs.f64 l)
      t\_m = (fabs.f64 t)
      t\_s = (copysign.f64 #s(literal 1 binary64) t)
      (FPCore (t_s x l_m t_m)
       :precision binary64
       (*
        t_s
        (if (<= (* l_m l_m) 1e+276)
          (/ (* x (- 1.0 (/ 0.5 (* x x)))) (+ x 1.0))
          (/ (* (sqrt 2.0) t_m) (* l_m (sqrt (/ 2.0 x)))))))
      l_m = fabs(l);
      t\_m = fabs(t);
      t\_s = copysign(1.0, t);
      double code(double t_s, double x, double l_m, double t_m) {
      	double tmp;
      	if ((l_m * l_m) <= 1e+276) {
      		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0);
      	} else {
      		tmp = (sqrt(2.0) * t_m) / (l_m * sqrt((2.0 / x)));
      	}
      	return t_s * tmp;
      }
      
      l_m = abs(l)
      t\_m = abs(t)
      t\_s = copysign(1.0d0, t)
      real(8) function code(t_s, x, l_m, t_m)
          real(8), intent (in) :: t_s
          real(8), intent (in) :: x
          real(8), intent (in) :: l_m
          real(8), intent (in) :: t_m
          real(8) :: tmp
          if ((l_m * l_m) <= 1d+276) then
              tmp = (x * (1.0d0 - (0.5d0 / (x * x)))) / (x + 1.0d0)
          else
              tmp = (sqrt(2.0d0) * t_m) / (l_m * sqrt((2.0d0 / x)))
          end if
          code = t_s * tmp
      end function
      
      l_m = Math.abs(l);
      t\_m = Math.abs(t);
      t\_s = Math.copySign(1.0, t);
      public static double code(double t_s, double x, double l_m, double t_m) {
      	double tmp;
      	if ((l_m * l_m) <= 1e+276) {
      		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0);
      	} else {
      		tmp = (Math.sqrt(2.0) * t_m) / (l_m * Math.sqrt((2.0 / x)));
      	}
      	return t_s * tmp;
      }
      
      l_m = math.fabs(l)
      t\_m = math.fabs(t)
      t\_s = math.copysign(1.0, t)
      def code(t_s, x, l_m, t_m):
      	tmp = 0
      	if (l_m * l_m) <= 1e+276:
      		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0)
      	else:
      		tmp = (math.sqrt(2.0) * t_m) / (l_m * math.sqrt((2.0 / x)))
      	return t_s * tmp
      
      l_m = abs(l)
      t\_m = abs(t)
      t\_s = copysign(1.0, t)
      function code(t_s, x, l_m, t_m)
      	tmp = 0.0
      	if (Float64(l_m * l_m) <= 1e+276)
      		tmp = Float64(Float64(x * Float64(1.0 - Float64(0.5 / Float64(x * x)))) / Float64(x + 1.0));
      	else
      		tmp = Float64(Float64(sqrt(2.0) * t_m) / Float64(l_m * sqrt(Float64(2.0 / x))));
      	end
      	return Float64(t_s * tmp)
      end
      
      l_m = abs(l);
      t\_m = abs(t);
      t\_s = sign(t) * abs(1.0);
      function tmp_2 = code(t_s, x, l_m, t_m)
      	tmp = 0.0;
      	if ((l_m * l_m) <= 1e+276)
      		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0);
      	else
      		tmp = (sqrt(2.0) * t_m) / (l_m * sqrt((2.0 / x)));
      	end
      	tmp_2 = t_s * tmp;
      end
      
      l_m = N[Abs[l], $MachinePrecision]
      t\_m = N[Abs[t], $MachinePrecision]
      t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      code[t$95$s_, x_, l$95$m_, t$95$m_] := N[(t$95$s * If[LessEqual[N[(l$95$m * l$95$m), $MachinePrecision], 1e+276], N[(N[(x * N[(1.0 - N[(0.5 / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(x + 1.0), $MachinePrecision]), $MachinePrecision], N[(N[(N[Sqrt[2.0], $MachinePrecision] * t$95$m), $MachinePrecision] / N[(l$95$m * N[Sqrt[N[(2.0 / x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]
      
      \begin{array}{l}
      l_m = \left|\ell\right|
      \\
      t\_m = \left|t\right|
      \\
      t\_s = \mathsf{copysign}\left(1, t\right)
      
      \\
      t\_s \cdot \begin{array}{l}
      \mathbf{if}\;l\_m \cdot l\_m \leq 10^{+276}:\\
      \;\;\;\;\frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1}\\
      
      \mathbf{else}:\\
      \;\;\;\;\frac{\sqrt{2} \cdot t\_m}{l\_m \cdot \sqrt{\frac{2}{x}}}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (*.f64 l l) < 1.0000000000000001e276

        1. Initial program 40.1%

          \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
        2. Add Preprocessing
        3. Applied rewrites22.2%

          \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
        4. Taylor expanded in t around inf

          \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
        5. Step-by-step derivation
          1. lower-*.f64N/A

            \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
          2. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
          3. *-commutativeN/A

            \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
          4. lower-*.f64N/A

            \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
          5. lower-sqrt.f64N/A

            \[\leadsto \frac{\color{blue}{\sqrt{2}} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
          6. lower-sqrt.f64N/A

            \[\leadsto \frac{\sqrt{2} \cdot \color{blue}{\sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
          7. lower-+.f64N/A

            \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{\color{blue}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
          8. lower-sqrt.f64N/A

            \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \color{blue}{\sqrt{{x}^{2} - 1}} \]
          9. sub-negN/A

            \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} \]
          10. unpow2N/A

            \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} \]
          11. metadata-evalN/A

            \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{x \cdot x + \color{blue}{-1}} \]
          12. lower-fma.f6421.1

            \[\leadsto \frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} \]
        6. Applied rewrites21.1%

          \[\leadsto \color{blue}{\frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\mathsf{fma}\left(x, x, -1\right)}} \]
        7. Applied rewrites21.4%

          \[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(x, x, -1\right)}}{1 + x}} \]
        8. Taylor expanded in x around inf

          \[\leadsto \frac{x \cdot \left(1 - \frac{1}{2} \cdot \frac{1}{{x}^{2}}\right)}{\color{blue}{1} + x} \]
        9. Step-by-step derivation
          1. Applied rewrites42.9%

            \[\leadsto \frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{\color{blue}{1} + x} \]

          if 1.0000000000000001e276 < (*.f64 l l)

          1. Initial program 0.0%

            \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
          2. Add Preprocessing
          3. Applied rewrites0.0%

            \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
          4. Taylor expanded in l around inf

            \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
          5. Step-by-step derivation
            1. lower-*.f64N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
            2. lower-sqrt.f64N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \color{blue}{\sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} - 1}}} \]
            3. sub-negN/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + \left(\mathsf{neg}\left(1\right)\right)}}} \]
            4. metadata-evalN/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + \color{blue}{-1}}} \]
            5. lower-+.f64N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1} + -1}}} \]
            6. lower-/.f64N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\color{blue}{\frac{{\left(1 + x\right)}^{2}}{{x}^{2} - 1}} + -1}} \]
            7. unpow2N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right) \cdot \left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
            8. lower-*.f64N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right) \cdot \left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
            9. lower-+.f64N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\color{blue}{\left(1 + x\right)} \cdot \left(1 + x\right)}{{x}^{2} - 1} + -1}} \]
            10. lower-+.f64N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \color{blue}{\left(1 + x\right)}}{{x}^{2} - 1} + -1}} \]
            11. sub-negN/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} + -1}} \]
            12. unpow2N/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} + -1}} \]
            13. metadata-evalN/A

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{x \cdot x + \color{blue}{-1}} + -1}} \]
            14. lower-fma.f642.9

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} + -1}} \]
          6. Applied rewrites2.9%

            \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\ell \cdot \sqrt{\frac{\left(1 + x\right) \cdot \left(1 + x\right)}{\mathsf{fma}\left(x, x, -1\right)} + -1}}} \]
          7. Taylor expanded in x around inf

            \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}} \]
          8. Step-by-step derivation
            1. Applied rewrites50.1%

              \[\leadsto \frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}} \]
          9. Recombined 2 regimes into one program.
          10. Final simplification44.2%

            \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \leq 10^{+276}:\\ \;\;\;\;\frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\ell \cdot \sqrt{\frac{2}{x}}}\\ \end{array} \]
          11. Add Preprocessing

          Alternative 4: 76.5% accurate, 1.6× speedup?

          \[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ t\_s \cdot \begin{array}{l} \mathbf{if}\;l\_m \leq 7.5 \cdot 10^{+256}:\\ \;\;\;\;\frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{2} \cdot t\_m\right) \cdot \sqrt{\frac{-0.5}{l\_m \cdot l\_m}}\\ \end{array} \end{array} \]
          l_m = (fabs.f64 l)
          t\_m = (fabs.f64 t)
          t\_s = (copysign.f64 #s(literal 1 binary64) t)
          (FPCore (t_s x l_m t_m)
           :precision binary64
           (*
            t_s
            (if (<= l_m 7.5e+256)
              (/ (* x (- 1.0 (/ 0.5 (* x x)))) (+ x 1.0))
              (* (* (sqrt 2.0) t_m) (sqrt (/ -0.5 (* l_m l_m)))))))
          l_m = fabs(l);
          t\_m = fabs(t);
          t\_s = copysign(1.0, t);
          double code(double t_s, double x, double l_m, double t_m) {
          	double tmp;
          	if (l_m <= 7.5e+256) {
          		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0);
          	} else {
          		tmp = (sqrt(2.0) * t_m) * sqrt((-0.5 / (l_m * l_m)));
          	}
          	return t_s * tmp;
          }
          
          l_m = abs(l)
          t\_m = abs(t)
          t\_s = copysign(1.0d0, t)
          real(8) function code(t_s, x, l_m, t_m)
              real(8), intent (in) :: t_s
              real(8), intent (in) :: x
              real(8), intent (in) :: l_m
              real(8), intent (in) :: t_m
              real(8) :: tmp
              if (l_m <= 7.5d+256) then
                  tmp = (x * (1.0d0 - (0.5d0 / (x * x)))) / (x + 1.0d0)
              else
                  tmp = (sqrt(2.0d0) * t_m) * sqrt(((-0.5d0) / (l_m * l_m)))
              end if
              code = t_s * tmp
          end function
          
          l_m = Math.abs(l);
          t\_m = Math.abs(t);
          t\_s = Math.copySign(1.0, t);
          public static double code(double t_s, double x, double l_m, double t_m) {
          	double tmp;
          	if (l_m <= 7.5e+256) {
          		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0);
          	} else {
          		tmp = (Math.sqrt(2.0) * t_m) * Math.sqrt((-0.5 / (l_m * l_m)));
          	}
          	return t_s * tmp;
          }
          
          l_m = math.fabs(l)
          t\_m = math.fabs(t)
          t\_s = math.copysign(1.0, t)
          def code(t_s, x, l_m, t_m):
          	tmp = 0
          	if l_m <= 7.5e+256:
          		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0)
          	else:
          		tmp = (math.sqrt(2.0) * t_m) * math.sqrt((-0.5 / (l_m * l_m)))
          	return t_s * tmp
          
          l_m = abs(l)
          t\_m = abs(t)
          t\_s = copysign(1.0, t)
          function code(t_s, x, l_m, t_m)
          	tmp = 0.0
          	if (l_m <= 7.5e+256)
          		tmp = Float64(Float64(x * Float64(1.0 - Float64(0.5 / Float64(x * x)))) / Float64(x + 1.0));
          	else
          		tmp = Float64(Float64(sqrt(2.0) * t_m) * sqrt(Float64(-0.5 / Float64(l_m * l_m))));
          	end
          	return Float64(t_s * tmp)
          end
          
          l_m = abs(l);
          t\_m = abs(t);
          t\_s = sign(t) * abs(1.0);
          function tmp_2 = code(t_s, x, l_m, t_m)
          	tmp = 0.0;
          	if (l_m <= 7.5e+256)
          		tmp = (x * (1.0 - (0.5 / (x * x)))) / (x + 1.0);
          	else
          		tmp = (sqrt(2.0) * t_m) * sqrt((-0.5 / (l_m * l_m)));
          	end
          	tmp_2 = t_s * tmp;
          end
          
          l_m = N[Abs[l], $MachinePrecision]
          t\_m = N[Abs[t], $MachinePrecision]
          t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
          code[t$95$s_, x_, l$95$m_, t$95$m_] := N[(t$95$s * If[LessEqual[l$95$m, 7.5e+256], N[(N[(x * N[(1.0 - N[(0.5 / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(x + 1.0), $MachinePrecision]), $MachinePrecision], N[(N[(N[Sqrt[2.0], $MachinePrecision] * t$95$m), $MachinePrecision] * N[Sqrt[N[(-0.5 / N[(l$95$m * l$95$m), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]
          
          \begin{array}{l}
          l_m = \left|\ell\right|
          \\
          t\_m = \left|t\right|
          \\
          t\_s = \mathsf{copysign}\left(1, t\right)
          
          \\
          t\_s \cdot \begin{array}{l}
          \mathbf{if}\;l\_m \leq 7.5 \cdot 10^{+256}:\\
          \;\;\;\;\frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1}\\
          
          \mathbf{else}:\\
          \;\;\;\;\left(\sqrt{2} \cdot t\_m\right) \cdot \sqrt{\frac{-0.5}{l\_m \cdot l\_m}}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if l < 7.4999999999999999e256

            1. Initial program 34.3%

              \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
            2. Add Preprocessing
            3. Applied rewrites18.9%

              \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
            4. Taylor expanded in t around inf

              \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
            5. Step-by-step derivation
              1. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
              2. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
              3. *-commutativeN/A

                \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
              4. lower-*.f64N/A

                \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
              5. lower-sqrt.f64N/A

                \[\leadsto \frac{\color{blue}{\sqrt{2}} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
              6. lower-sqrt.f64N/A

                \[\leadsto \frac{\sqrt{2} \cdot \color{blue}{\sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
              7. lower-+.f64N/A

                \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{\color{blue}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
              8. lower-sqrt.f64N/A

                \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \color{blue}{\sqrt{{x}^{2} - 1}} \]
              9. sub-negN/A

                \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} \]
              10. unpow2N/A

                \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} \]
              11. metadata-evalN/A

                \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{x \cdot x + \color{blue}{-1}} \]
              12. lower-fma.f6418.8

                \[\leadsto \frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} \]
            6. Applied rewrites18.8%

              \[\leadsto \color{blue}{\frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\mathsf{fma}\left(x, x, -1\right)}} \]
            7. Applied rewrites19.0%

              \[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(x, x, -1\right)}}{1 + x}} \]
            8. Taylor expanded in x around inf

              \[\leadsto \frac{x \cdot \left(1 - \frac{1}{2} \cdot \frac{1}{{x}^{2}}\right)}{\color{blue}{1} + x} \]
            9. Step-by-step derivation
              1. Applied rewrites40.3%

                \[\leadsto \frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{\color{blue}{1} + x} \]

              if 7.4999999999999999e256 < l

              1. Initial program 0.0%

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

                \[\leadsto \color{blue}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{-1 \cdot \left(2 \cdot {t}^{2} + {\ell}^{2}\right) - {\ell}^{2}}}} \]
              4. Step-by-step derivation
                1. lower-*.f64N/A

                  \[\leadsto \color{blue}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{-1 \cdot \left(2 \cdot {t}^{2} + {\ell}^{2}\right) - {\ell}^{2}}}} \]
                2. lower-*.f64N/A

                  \[\leadsto \color{blue}{\left(t \cdot \sqrt{2}\right)} \cdot \sqrt{\frac{1}{-1 \cdot \left(2 \cdot {t}^{2} + {\ell}^{2}\right) - {\ell}^{2}}} \]
                3. lower-sqrt.f64N/A

                  \[\leadsto \left(t \cdot \color{blue}{\sqrt{2}}\right) \cdot \sqrt{\frac{1}{-1 \cdot \left(2 \cdot {t}^{2} + {\ell}^{2}\right) - {\ell}^{2}}} \]
                4. lower-sqrt.f64N/A

                  \[\leadsto \left(t \cdot \sqrt{2}\right) \cdot \color{blue}{\sqrt{\frac{1}{-1 \cdot \left(2 \cdot {t}^{2} + {\ell}^{2}\right) - {\ell}^{2}}}} \]
                5. lower-/.f64N/A

                  \[\leadsto \left(t \cdot \sqrt{2}\right) \cdot \sqrt{\color{blue}{\frac{1}{-1 \cdot \left(2 \cdot {t}^{2} + {\ell}^{2}\right) - {\ell}^{2}}}} \]
                6. lower--.f64N/A

                  \[\leadsto \left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{\color{blue}{-1 \cdot \left(2 \cdot {t}^{2} + {\ell}^{2}\right) - {\ell}^{2}}}} \]
              5. Applied rewrites37.0%

                \[\leadsto \color{blue}{\left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\ell, -\ell, -2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}} \]
              6. Taylor expanded in l around inf

                \[\leadsto \left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{\frac{-1}{2}}{{\ell}^{2}}} \]
              7. Step-by-step derivation
                1. Applied rewrites37.0%

                  \[\leadsto \left(t \cdot \sqrt{2}\right) \cdot \sqrt{\frac{-0.5}{\ell \cdot \ell}} \]
              8. Recombined 2 regimes into one program.
              9. Final simplification40.2%

                \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \leq 7.5 \cdot 10^{+256}:\\ \;\;\;\;\frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{2} \cdot t\right) \cdot \sqrt{\frac{-0.5}{\ell \cdot \ell}}\\ \end{array} \]
              10. Add Preprocessing

              Alternative 5: 76.5% accurate, 2.2× speedup?

              \[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ t\_s \cdot \frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1} \end{array} \]
              l_m = (fabs.f64 l)
              t\_m = (fabs.f64 t)
              t\_s = (copysign.f64 #s(literal 1 binary64) t)
              (FPCore (t_s x l_m t_m)
               :precision binary64
               (* t_s (/ (* x (- 1.0 (/ 0.5 (* x x)))) (+ x 1.0))))
              l_m = fabs(l);
              t\_m = fabs(t);
              t\_s = copysign(1.0, t);
              double code(double t_s, double x, double l_m, double t_m) {
              	return t_s * ((x * (1.0 - (0.5 / (x * x)))) / (x + 1.0));
              }
              
              l_m = abs(l)
              t\_m = abs(t)
              t\_s = copysign(1.0d0, t)
              real(8) function code(t_s, x, l_m, t_m)
                  real(8), intent (in) :: t_s
                  real(8), intent (in) :: x
                  real(8), intent (in) :: l_m
                  real(8), intent (in) :: t_m
                  code = t_s * ((x * (1.0d0 - (0.5d0 / (x * x)))) / (x + 1.0d0))
              end function
              
              l_m = Math.abs(l);
              t\_m = Math.abs(t);
              t\_s = Math.copySign(1.0, t);
              public static double code(double t_s, double x, double l_m, double t_m) {
              	return t_s * ((x * (1.0 - (0.5 / (x * x)))) / (x + 1.0));
              }
              
              l_m = math.fabs(l)
              t\_m = math.fabs(t)
              t\_s = math.copysign(1.0, t)
              def code(t_s, x, l_m, t_m):
              	return t_s * ((x * (1.0 - (0.5 / (x * x)))) / (x + 1.0))
              
              l_m = abs(l)
              t\_m = abs(t)
              t\_s = copysign(1.0, t)
              function code(t_s, x, l_m, t_m)
              	return Float64(t_s * Float64(Float64(x * Float64(1.0 - Float64(0.5 / Float64(x * x)))) / Float64(x + 1.0)))
              end
              
              l_m = abs(l);
              t\_m = abs(t);
              t\_s = sign(t) * abs(1.0);
              function tmp = code(t_s, x, l_m, t_m)
              	tmp = t_s * ((x * (1.0 - (0.5 / (x * x)))) / (x + 1.0));
              end
              
              l_m = N[Abs[l], $MachinePrecision]
              t\_m = N[Abs[t], $MachinePrecision]
              t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
              code[t$95$s_, x_, l$95$m_, t$95$m_] := N[(t$95$s * N[(N[(x * N[(1.0 - N[(0.5 / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(x + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
              
              \begin{array}{l}
              l_m = \left|\ell\right|
              \\
              t\_m = \left|t\right|
              \\
              t\_s = \mathsf{copysign}\left(1, t\right)
              
              \\
              t\_s \cdot \frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1}
              \end{array}
              
              Derivation
              1. Initial program 33.1%

                \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
              2. Add Preprocessing
              3. Applied rewrites18.3%

                \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
              4. Taylor expanded in t around inf

                \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
              5. Step-by-step derivation
                1. lower-*.f64N/A

                  \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
                2. lower-/.f64N/A

                  \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
                3. *-commutativeN/A

                  \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                4. lower-*.f64N/A

                  \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                5. lower-sqrt.f64N/A

                  \[\leadsto \frac{\color{blue}{\sqrt{2}} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                6. lower-sqrt.f64N/A

                  \[\leadsto \frac{\sqrt{2} \cdot \color{blue}{\sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                7. lower-+.f64N/A

                  \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{\color{blue}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
                8. lower-sqrt.f64N/A

                  \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \color{blue}{\sqrt{{x}^{2} - 1}} \]
                9. sub-negN/A

                  \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} \]
                10. unpow2N/A

                  \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} \]
                11. metadata-evalN/A

                  \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{x \cdot x + \color{blue}{-1}} \]
                12. lower-fma.f6418.6

                  \[\leadsto \frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} \]
              6. Applied rewrites18.6%

                \[\leadsto \color{blue}{\frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\mathsf{fma}\left(x, x, -1\right)}} \]
              7. Applied rewrites18.8%

                \[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(x, x, -1\right)}}{1 + x}} \]
              8. Taylor expanded in x around inf

                \[\leadsto \frac{x \cdot \left(1 - \frac{1}{2} \cdot \frac{1}{{x}^{2}}\right)}{\color{blue}{1} + x} \]
              9. Step-by-step derivation
                1. Applied rewrites39.0%

                  \[\leadsto \frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{\color{blue}{1} + x} \]
                2. Final simplification39.0%

                  \[\leadsto \frac{x \cdot \left(1 - \frac{0.5}{x \cdot x}\right)}{x + 1} \]
                3. Add Preprocessing

                Alternative 6: 76.4% accurate, 2.5× speedup?

                \[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ t\_s \cdot \left(\left(1 + \frac{0.5}{x \cdot x}\right) + \frac{-1}{x}\right) \end{array} \]
                l_m = (fabs.f64 l)
                t\_m = (fabs.f64 t)
                t\_s = (copysign.f64 #s(literal 1 binary64) t)
                (FPCore (t_s x l_m t_m)
                 :precision binary64
                 (* t_s (+ (+ 1.0 (/ 0.5 (* x x))) (/ -1.0 x))))
                l_m = fabs(l);
                t\_m = fabs(t);
                t\_s = copysign(1.0, t);
                double code(double t_s, double x, double l_m, double t_m) {
                	return t_s * ((1.0 + (0.5 / (x * x))) + (-1.0 / x));
                }
                
                l_m = abs(l)
                t\_m = abs(t)
                t\_s = copysign(1.0d0, t)
                real(8) function code(t_s, x, l_m, t_m)
                    real(8), intent (in) :: t_s
                    real(8), intent (in) :: x
                    real(8), intent (in) :: l_m
                    real(8), intent (in) :: t_m
                    code = t_s * ((1.0d0 + (0.5d0 / (x * x))) + ((-1.0d0) / x))
                end function
                
                l_m = Math.abs(l);
                t\_m = Math.abs(t);
                t\_s = Math.copySign(1.0, t);
                public static double code(double t_s, double x, double l_m, double t_m) {
                	return t_s * ((1.0 + (0.5 / (x * x))) + (-1.0 / x));
                }
                
                l_m = math.fabs(l)
                t\_m = math.fabs(t)
                t\_s = math.copysign(1.0, t)
                def code(t_s, x, l_m, t_m):
                	return t_s * ((1.0 + (0.5 / (x * x))) + (-1.0 / x))
                
                l_m = abs(l)
                t\_m = abs(t)
                t\_s = copysign(1.0, t)
                function code(t_s, x, l_m, t_m)
                	return Float64(t_s * Float64(Float64(1.0 + Float64(0.5 / Float64(x * x))) + Float64(-1.0 / x)))
                end
                
                l_m = abs(l);
                t\_m = abs(t);
                t\_s = sign(t) * abs(1.0);
                function tmp = code(t_s, x, l_m, t_m)
                	tmp = t_s * ((1.0 + (0.5 / (x * x))) + (-1.0 / x));
                end
                
                l_m = N[Abs[l], $MachinePrecision]
                t\_m = N[Abs[t], $MachinePrecision]
                t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                code[t$95$s_, x_, l$95$m_, t$95$m_] := N[(t$95$s * N[(N[(1.0 + N[(0.5 / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(-1.0 / x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
                
                \begin{array}{l}
                l_m = \left|\ell\right|
                \\
                t\_m = \left|t\right|
                \\
                t\_s = \mathsf{copysign}\left(1, t\right)
                
                \\
                t\_s \cdot \left(\left(1 + \frac{0.5}{x \cdot x}\right) + \frac{-1}{x}\right)
                \end{array}
                
                Derivation
                1. Initial program 33.1%

                  \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
                2. Add Preprocessing
                3. Applied rewrites18.3%

                  \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
                4. Taylor expanded in t around inf

                  \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
                5. Step-by-step derivation
                  1. lower-*.f64N/A

                    \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
                  2. lower-/.f64N/A

                    \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
                  3. *-commutativeN/A

                    \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                  4. lower-*.f64N/A

                    \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                  5. lower-sqrt.f64N/A

                    \[\leadsto \frac{\color{blue}{\sqrt{2}} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                  6. lower-sqrt.f64N/A

                    \[\leadsto \frac{\sqrt{2} \cdot \color{blue}{\sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                  7. lower-+.f64N/A

                    \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{\color{blue}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
                  8. lower-sqrt.f64N/A

                    \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \color{blue}{\sqrt{{x}^{2} - 1}} \]
                  9. sub-negN/A

                    \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} \]
                  10. unpow2N/A

                    \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} \]
                  11. metadata-evalN/A

                    \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{x \cdot x + \color{blue}{-1}} \]
                  12. lower-fma.f6418.6

                    \[\leadsto \frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} \]
                6. Applied rewrites18.6%

                  \[\leadsto \color{blue}{\frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\mathsf{fma}\left(x, x, -1\right)}} \]
                7. Applied rewrites18.8%

                  \[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(x, x, -1\right)}}{1 + x}} \]
                8. Taylor expanded in x around inf

                  \[\leadsto \left(1 + \frac{\frac{1}{2}}{{x}^{2}}\right) - \color{blue}{\frac{1}{x}} \]
                9. Step-by-step derivation
                  1. Applied rewrites39.0%

                    \[\leadsto \left(1 + \frac{0.5}{x \cdot x}\right) - \color{blue}{\frac{1}{x}} \]
                  2. Final simplification39.0%

                    \[\leadsto \left(1 + \frac{0.5}{x \cdot x}\right) + \frac{-1}{x} \]
                  3. Add Preprocessing

                  Alternative 7: 76.2% accurate, 5.7× speedup?

                  \[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ t\_s \cdot \left(1 + \frac{-1}{x}\right) \end{array} \]
                  l_m = (fabs.f64 l)
                  t\_m = (fabs.f64 t)
                  t\_s = (copysign.f64 #s(literal 1 binary64) t)
                  (FPCore (t_s x l_m t_m) :precision binary64 (* t_s (+ 1.0 (/ -1.0 x))))
                  l_m = fabs(l);
                  t\_m = fabs(t);
                  t\_s = copysign(1.0, t);
                  double code(double t_s, double x, double l_m, double t_m) {
                  	return t_s * (1.0 + (-1.0 / x));
                  }
                  
                  l_m = abs(l)
                  t\_m = abs(t)
                  t\_s = copysign(1.0d0, t)
                  real(8) function code(t_s, x, l_m, t_m)
                      real(8), intent (in) :: t_s
                      real(8), intent (in) :: x
                      real(8), intent (in) :: l_m
                      real(8), intent (in) :: t_m
                      code = t_s * (1.0d0 + ((-1.0d0) / x))
                  end function
                  
                  l_m = Math.abs(l);
                  t\_m = Math.abs(t);
                  t\_s = Math.copySign(1.0, t);
                  public static double code(double t_s, double x, double l_m, double t_m) {
                  	return t_s * (1.0 + (-1.0 / x));
                  }
                  
                  l_m = math.fabs(l)
                  t\_m = math.fabs(t)
                  t\_s = math.copysign(1.0, t)
                  def code(t_s, x, l_m, t_m):
                  	return t_s * (1.0 + (-1.0 / x))
                  
                  l_m = abs(l)
                  t\_m = abs(t)
                  t\_s = copysign(1.0, t)
                  function code(t_s, x, l_m, t_m)
                  	return Float64(t_s * Float64(1.0 + Float64(-1.0 / x)))
                  end
                  
                  l_m = abs(l);
                  t\_m = abs(t);
                  t\_s = sign(t) * abs(1.0);
                  function tmp = code(t_s, x, l_m, t_m)
                  	tmp = t_s * (1.0 + (-1.0 / x));
                  end
                  
                  l_m = N[Abs[l], $MachinePrecision]
                  t\_m = N[Abs[t], $MachinePrecision]
                  t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                  code[t$95$s_, x_, l$95$m_, t$95$m_] := N[(t$95$s * N[(1.0 + N[(-1.0 / x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
                  
                  \begin{array}{l}
                  l_m = \left|\ell\right|
                  \\
                  t\_m = \left|t\right|
                  \\
                  t\_s = \mathsf{copysign}\left(1, t\right)
                  
                  \\
                  t\_s \cdot \left(1 + \frac{-1}{x}\right)
                  \end{array}
                  
                  Derivation
                  1. Initial program 33.1%

                    \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}} \]
                  2. Add Preprocessing
                  3. Applied rewrites18.3%

                    \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{\mathsf{fma}\left(x, x, -1\right)}, \left(x + 1\right) \cdot \left(x + 1\right), -\ell \cdot \ell\right)}}} \]
                  4. Taylor expanded in t around inf

                    \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
                  5. Step-by-step derivation
                    1. lower-*.f64N/A

                      \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x} \cdot \sqrt{{x}^{2} - 1}} \]
                    2. lower-/.f64N/A

                      \[\leadsto \color{blue}{\frac{\sqrt{\frac{1}{2}} \cdot \sqrt{2}}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
                    3. *-commutativeN/A

                      \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                    4. lower-*.f64N/A

                      \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                    5. lower-sqrt.f64N/A

                      \[\leadsto \frac{\color{blue}{\sqrt{2}} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                    6. lower-sqrt.f64N/A

                      \[\leadsto \frac{\sqrt{2} \cdot \color{blue}{\sqrt{\frac{1}{2}}}}{1 + x} \cdot \sqrt{{x}^{2} - 1} \]
                    7. lower-+.f64N/A

                      \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{\color{blue}{1 + x}} \cdot \sqrt{{x}^{2} - 1} \]
                    8. lower-sqrt.f64N/A

                      \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \color{blue}{\sqrt{{x}^{2} - 1}} \]
                    9. sub-negN/A

                      \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(1\right)\right)}} \]
                    10. unpow2N/A

                      \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{\color{blue}{x \cdot x} + \left(\mathsf{neg}\left(1\right)\right)} \]
                    11. metadata-evalN/A

                      \[\leadsto \frac{\sqrt{2} \cdot \sqrt{\frac{1}{2}}}{1 + x} \cdot \sqrt{x \cdot x + \color{blue}{-1}} \]
                    12. lower-fma.f6418.6

                      \[\leadsto \frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\color{blue}{\mathsf{fma}\left(x, x, -1\right)}} \]
                  6. Applied rewrites18.6%

                    \[\leadsto \color{blue}{\frac{\sqrt{2} \cdot \sqrt{0.5}}{1 + x} \cdot \sqrt{\mathsf{fma}\left(x, x, -1\right)}} \]
                  7. Applied rewrites18.8%

                    \[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(x, x, -1\right)}}{1 + x}} \]
                  8. Taylor expanded in x around inf

                    \[\leadsto 1 - \color{blue}{\frac{1}{x}} \]
                  9. Step-by-step derivation
                    1. Applied rewrites39.0%

                      \[\leadsto 1 - \color{blue}{\frac{1}{x}} \]
                    2. Final simplification39.0%

                      \[\leadsto 1 + \frac{-1}{x} \]
                    3. Add Preprocessing

                    Alternative 8: 75.5% accurate, 85.0× speedup?

                    \[\begin{array}{l} l_m = \left|\ell\right| \\ t\_m = \left|t\right| \\ t\_s = \mathsf{copysign}\left(1, t\right) \\ t\_s \cdot 1 \end{array} \]
                    l_m = (fabs.f64 l)
                    t\_m = (fabs.f64 t)
                    t\_s = (copysign.f64 #s(literal 1 binary64) t)
                    (FPCore (t_s x l_m t_m) :precision binary64 (* t_s 1.0))
                    l_m = fabs(l);
                    t\_m = fabs(t);
                    t\_s = copysign(1.0, t);
                    double code(double t_s, double x, double l_m, double t_m) {
                    	return t_s * 1.0;
                    }
                    
                    l_m = abs(l)
                    t\_m = abs(t)
                    t\_s = copysign(1.0d0, t)
                    real(8) function code(t_s, x, l_m, t_m)
                        real(8), intent (in) :: t_s
                        real(8), intent (in) :: x
                        real(8), intent (in) :: l_m
                        real(8), intent (in) :: t_m
                        code = t_s * 1.0d0
                    end function
                    
                    l_m = Math.abs(l);
                    t\_m = Math.abs(t);
                    t\_s = Math.copySign(1.0, t);
                    public static double code(double t_s, double x, double l_m, double t_m) {
                    	return t_s * 1.0;
                    }
                    
                    l_m = math.fabs(l)
                    t\_m = math.fabs(t)
                    t\_s = math.copysign(1.0, t)
                    def code(t_s, x, l_m, t_m):
                    	return t_s * 1.0
                    
                    l_m = abs(l)
                    t\_m = abs(t)
                    t\_s = copysign(1.0, t)
                    function code(t_s, x, l_m, t_m)
                    	return Float64(t_s * 1.0)
                    end
                    
                    l_m = abs(l);
                    t\_m = abs(t);
                    t\_s = sign(t) * abs(1.0);
                    function tmp = code(t_s, x, l_m, t_m)
                    	tmp = t_s * 1.0;
                    end
                    
                    l_m = N[Abs[l], $MachinePrecision]
                    t\_m = N[Abs[t], $MachinePrecision]
                    t\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[t]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                    code[t$95$s_, x_, l$95$m_, t$95$m_] := N[(t$95$s * 1.0), $MachinePrecision]
                    
                    \begin{array}{l}
                    l_m = \left|\ell\right|
                    \\
                    t\_m = \left|t\right|
                    \\
                    t\_s = \mathsf{copysign}\left(1, t\right)
                    
                    \\
                    t\_s \cdot 1
                    \end{array}
                    
                    Derivation
                    1. Initial program 33.1%

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

                      \[\leadsto \color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{2}} \]
                    4. Step-by-step derivation
                      1. *-commutativeN/A

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

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

                        \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{1}{2}} \]
                      4. lower-sqrt.f6438.3

                        \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{0.5}} \]
                    5. Applied rewrites38.3%

                      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{0.5}} \]
                    6. Step-by-step derivation
                      1. Applied rewrites38.9%

                        \[\leadsto \color{blue}{1} \]
                      2. Add Preprocessing

                      Reproduce

                      ?
                      herbie shell --seed 2024227 
                      (FPCore (x l t)
                        :name "Toniolo and Linder, Equation (7)"
                        :precision binary64
                        (/ (* (sqrt 2.0) t) (sqrt (- (* (/ (+ x 1.0) (- x 1.0)) (+ (* l l) (* 2.0 (* t t)))) (* l l)))))