Toniolo and Linder, Equation (7)

Average Error: 43.1 → 10.5

Time: 33.9s

Precision: binary64

Cost: 28372

Math

\[\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}} \]

↓

\[\begin{array}{l} t_1 := \left(t \cdot t\right) \cdot -2 - \ell \cdot \ell\\ t_2 := 2 \cdot \left(t \cdot t\right)\\ t_3 := \ell \cdot \ell + t_2\\ t_4 := t \cdot \sqrt{2}\\ t_5 := \frac{2}{x} + \left(2 + \frac{2}{x}\right)\\ t_6 := t \cdot t + \frac{t \cdot t}{x}\\ t_7 := \sqrt{\frac{x + -1}{x + 1}}\\ t_8 := \frac{\ell \cdot \ell}{x}\\ \mathbf{if}\;t \leq -7.2 \cdot 10^{+26}:\\ \;\;\;\;-t_7\\ \mathbf{elif}\;t \leq -2.4 \cdot 10^{-215}:\\ \;\;\;\;t \cdot \frac{\sqrt{2}}{\sqrt{t_8 + \left(t_8 - t_6 \cdot -2\right)}}\\ \mathbf{elif}\;t \leq -4.4 \cdot 10^{-269}:\\ \;\;\;\;\sqrt{2} \cdot \frac{t}{-\mathsf{fma}\left(t, \sqrt{t_5}, \sqrt{\frac{1}{t_5}} \cdot \left(\frac{\ell}{x} \cdot \frac{\ell}{t}\right)\right)}\\ \mathbf{elif}\;t \leq 7.6 \cdot 10^{-294}:\\ \;\;\;\;\frac{t_4}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{elif}\;t \leq 3.3 \cdot 10^{-176}:\\ \;\;\;\;\frac{t_4}{\mathsf{fma}\left(0.5, \frac{\ell \cdot \ell + \left(t_2 + t_3\right)}{\sqrt{2} \cdot \left(t \cdot x\right)}, t_4\right)}\\ \mathbf{elif}\;t \leq 1.2 \cdot 10^{-5}:\\ \;\;\;\;\frac{t_4}{\sqrt{\left(t_8 + \mathsf{fma}\left(-1, \frac{t_1 + t_1}{x \cdot x}, 2 \cdot t_6\right)\right) + \frac{t_3}{x}}}\\ \mathbf{else}:\\ \;\;\;\;t_7\\ \end{array} \]

FPCore

(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)))))

↓

(FPCore (x l t)
 :precision binary64
 (let* ((t_1 (- (* (* t t) -2.0) (* l l)))
        (t_2 (* 2.0 (* t t)))
        (t_3 (+ (* l l) t_2))
        (t_4 (* t (sqrt 2.0)))
        (t_5 (+ (/ 2.0 x) (+ 2.0 (/ 2.0 x))))
        (t_6 (+ (* t t) (/ (* t t) x)))
        (t_7 (sqrt (/ (+ x -1.0) (+ x 1.0))))
        (t_8 (/ (* l l) x)))
   (if (<= t -7.2e+26)
     (- t_7)
     (if (<= t -2.4e-215)
       (* t (/ (sqrt 2.0) (sqrt (+ t_8 (- t_8 (* t_6 -2.0))))))
       (if (<= t -4.4e-269)
         (*
          (sqrt 2.0)
          (/
           t
           (- (fma t (sqrt t_5) (* (sqrt (/ 1.0 t_5)) (* (/ l x) (/ l t)))))))
         (if (<= t 7.6e-294)
           (/ t_4 (sqrt (* (/ l x) (+ l l))))
           (if (<= t 3.3e-176)
             (/
              t_4
              (fma 0.5 (/ (+ (* l l) (+ t_2 t_3)) (* (sqrt 2.0) (* t x))) t_4))
             (if (<= t 1.2e-5)
               (/
                t_4
                (sqrt
                 (+
                  (+ t_8 (fma -1.0 (/ (+ t_1 t_1) (* x x)) (* 2.0 t_6)))
                  (/ t_3 x))))
               t_7))))))))

C

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)));
}

↓

double code(double x, double l, double t) {
	double t_1 = ((t * t) * -2.0) - (l * l);
	double t_2 = 2.0 * (t * t);
	double t_3 = (l * l) + t_2;
	double t_4 = t * sqrt(2.0);
	double t_5 = (2.0 / x) + (2.0 + (2.0 / x));
	double t_6 = (t * t) + ((t * t) / x);
	double t_7 = sqrt(((x + -1.0) / (x + 1.0)));
	double t_8 = (l * l) / x;
	double tmp;
	if (t <= -7.2e+26) {
		tmp = -t_7;
	} else if (t <= -2.4e-215) {
		tmp = t * (sqrt(2.0) / sqrt((t_8 + (t_8 - (t_6 * -2.0)))));
	} else if (t <= -4.4e-269) {
		tmp = sqrt(2.0) * (t / -fma(t, sqrt(t_5), (sqrt((1.0 / t_5)) * ((l / x) * (l / t)))));
	} else if (t <= 7.6e-294) {
		tmp = t_4 / sqrt(((l / x) * (l + l)));
	} else if (t <= 3.3e-176) {
		tmp = t_4 / fma(0.5, (((l * l) + (t_2 + t_3)) / (sqrt(2.0) * (t * x))), t_4);
	} else if (t <= 1.2e-5) {
		tmp = t_4 / sqrt(((t_8 + fma(-1.0, ((t_1 + t_1) / (x * x)), (2.0 * t_6))) + (t_3 / x)));
	} else {
		tmp = t_7;
	}
	return tmp;
}

Julia

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 code(x, l, t)
	t_1 = Float64(Float64(Float64(t * t) * -2.0) - Float64(l * l))
	t_2 = Float64(2.0 * Float64(t * t))
	t_3 = Float64(Float64(l * l) + t_2)
	t_4 = Float64(t * sqrt(2.0))
	t_5 = Float64(Float64(2.0 / x) + Float64(2.0 + Float64(2.0 / x)))
	t_6 = Float64(Float64(t * t) + Float64(Float64(t * t) / x))
	t_7 = sqrt(Float64(Float64(x + -1.0) / Float64(x + 1.0)))
	t_8 = Float64(Float64(l * l) / x)
	tmp = 0.0
	if (t <= -7.2e+26)
		tmp = Float64(-t_7);
	elseif (t <= -2.4e-215)
		tmp = Float64(t * Float64(sqrt(2.0) / sqrt(Float64(t_8 + Float64(t_8 - Float64(t_6 * -2.0))))));
	elseif (t <= -4.4e-269)
		tmp = Float64(sqrt(2.0) * Float64(t / Float64(-fma(t, sqrt(t_5), Float64(sqrt(Float64(1.0 / t_5)) * Float64(Float64(l / x) * Float64(l / t)))))));
	elseif (t <= 7.6e-294)
		tmp = Float64(t_4 / sqrt(Float64(Float64(l / x) * Float64(l + l))));
	elseif (t <= 3.3e-176)
		tmp = Float64(t_4 / fma(0.5, Float64(Float64(Float64(l * l) + Float64(t_2 + t_3)) / Float64(sqrt(2.0) * Float64(t * x))), t_4));
	elseif (t <= 1.2e-5)
		tmp = Float64(t_4 / sqrt(Float64(Float64(t_8 + fma(-1.0, Float64(Float64(t_1 + t_1) / Float64(x * x)), Float64(2.0 * t_6))) + Float64(t_3 / x))));
	else
		tmp = t_7;
	end
	return tmp
end

Wolfram

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]

↓

code[x_, l_, t_] := Block[{t$95$1 = N[(N[(N[(t * t), $MachinePrecision] * -2.0), $MachinePrecision] - N[(l * l), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(2.0 * N[(t * t), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(N[(l * l), $MachinePrecision] + t$95$2), $MachinePrecision]}, Block[{t$95$4 = N[(t * N[Sqrt[2.0], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$5 = N[(N[(2.0 / x), $MachinePrecision] + N[(2.0 + N[(2.0 / x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$6 = N[(N[(t * t), $MachinePrecision] + N[(N[(t * t), $MachinePrecision] / x), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$7 = N[Sqrt[N[(N[(x + -1.0), $MachinePrecision] / N[(x + 1.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$8 = N[(N[(l * l), $MachinePrecision] / x), $MachinePrecision]}, If[LessEqual[t, -7.2e+26], (-t$95$7), If[LessEqual[t, -2.4e-215], N[(t * N[(N[Sqrt[2.0], $MachinePrecision] / N[Sqrt[N[(t$95$8 + N[(t$95$8 - N[(t$95$6 * -2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t, -4.4e-269], N[(N[Sqrt[2.0], $MachinePrecision] * N[(t / (-N[(t * N[Sqrt[t$95$5], $MachinePrecision] + N[(N[Sqrt[N[(1.0 / t$95$5), $MachinePrecision]], $MachinePrecision] * N[(N[(l / x), $MachinePrecision] * N[(l / t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision])), $MachinePrecision]), $MachinePrecision], If[LessEqual[t, 7.6e-294], N[(t$95$4 / N[Sqrt[N[(N[(l / x), $MachinePrecision] * N[(l + l), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], If[LessEqual[t, 3.3e-176], N[(t$95$4 / N[(0.5 * N[(N[(N[(l * l), $MachinePrecision] + N[(t$95$2 + t$95$3), $MachinePrecision]), $MachinePrecision] / N[(N[Sqrt[2.0], $MachinePrecision] * N[(t * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$4), $MachinePrecision]), $MachinePrecision], If[LessEqual[t, 1.2e-5], N[(t$95$4 / N[Sqrt[N[(N[(t$95$8 + N[(-1.0 * N[(N[(t$95$1 + t$95$1), $MachinePrecision] / N[(x * x), $MachinePrecision]), $MachinePrecision] + N[(2.0 * t$95$6), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(t$95$3 / x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], t$95$7]]]]]]]]]]]]]]

Derivation

1. Split input into 7 regimes

2. if t < -7.20000000000000048e26

   1. Initial program 43.2

      \[\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. Simplified 54.8

      \[\leadsto \color{blue}{\frac{\sqrt{2}}{\sqrt{\frac{\left(x + 1\right) \cdot \mathsf{fma}\left(2 \cdot t, t, \ell \cdot \ell\right)}{x + -1} - \ell \cdot \ell}} \cdot t} \]
      Proof
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (fma.f64 (*.f64 2 t) t (*.f64 l l))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 2 t) t) (*.f64 l l)))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 t t))) (*.f64 l l))) (+.f64 x -1)) (*.f64 l l)))) t): 1 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))) (*.f64 l l)))) t): 18 points increase in error, 27 points decrease in error
      (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (sqrt.f64 2) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (*.f64 l l))))): 12 points increase in error, 9 points decrease in error

   3. Taylor expanded in t around inf 53.8

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

   4. Simplified 39.5

      \[\leadsto \frac{\sqrt{2}}{\sqrt{\color{blue}{2 \cdot \left(\frac{x + 1}{-1 + x} \cdot \left(t \cdot t\right)\right)}}} \cdot t \]
      Proof
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (+.f64 -1 x)) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 x -1))) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (Rewrite<= unpow2_binary64 (pow.f64 t 2)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= associate-/r/_binary64 (/.f64 (+.f64 x 1) (/.f64 (-.f64 x 1) (pow.f64 t 2))))): 24 points increase in error, 13 points decrease in error
      (*.f64 2 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 x)) (/.f64 (-.f64 x 1) (pow.f64 t 2)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 1 x) (pow.f64 t 2)) (-.f64 x 1)))): 45 points increase in error, 25 points decrease in error

   5. Taylor expanded in t around -inf 4.1

      \[\leadsto \color{blue}{-1 \cdot \sqrt{\frac{x - 1}{1 + x}}} \]

   6. Simplified 4.1

      \[\leadsto \color{blue}{-\sqrt{\frac{x - 1}{x + 1}}} \]
      Proof
      (neg.f64 (sqrt.f64 (/.f64 (-.f64 x 1) (+.f64 x 1)))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (sqrt.f64 (/.f64 (-.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 1 x))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (sqrt.f64 (/.f64 (-.f64 x 1) (+.f64 1 x))))): 0 points increase in error, 0 points decrease in error

   if -7.20000000000000048e26 < t < -2.4000000000000001e-215

   1. Initial program 37.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. Simplified 37.4

      \[\leadsto \color{blue}{\frac{\sqrt{2}}{\sqrt{\frac{\left(x + 1\right) \cdot \mathsf{fma}\left(2 \cdot t, t, \ell \cdot \ell\right)}{x + -1} - \ell \cdot \ell}} \cdot t} \]
      Proof
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (fma.f64 (*.f64 2 t) t (*.f64 l l))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 2 t) t) (*.f64 l l)))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 t t))) (*.f64 l l))) (+.f64 x -1)) (*.f64 l l)))) t): 1 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))) (*.f64 l l)))) t): 18 points increase in error, 27 points decrease in error
      (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (sqrt.f64 2) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (*.f64 l l))))): 12 points increase in error, 9 points decrease in error

   3. Taylor expanded in x around inf 14.3

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

   4. Simplified 14.3

      \[\leadsto \frac{\sqrt{2}}{\sqrt{\color{blue}{\frac{\ell \cdot \ell}{x} + \left(2 \cdot \left(\frac{t \cdot t}{x} + t \cdot t\right) - \frac{-\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{x}\right)}}} \cdot t \]
      Proof
      (+.f64 (/.f64 (*.f64 l l) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))) (/.f64 (neg.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))) (/.f64 (neg.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 t 2)) x) (*.f64 t t))) (/.f64 (neg.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (pow.f64 t 2) x) (Rewrite<= unpow2_binary64 (pow.f64 t 2)))) (/.f64 (neg.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (/.f64 (neg.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l)))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (pow.f64 t 2)) (Rewrite<= unpow2_binary64 (pow.f64 l 2)))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))): 0 points increase in error, 0 points decrease in error

   5. Taylor expanded in t around 0 14.5

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

   6. Simplified 14.5

      \[\leadsto \frac{\sqrt{2}}{\sqrt{\frac{\ell \cdot \ell}{x} + \left(2 \cdot \left(\frac{t \cdot t}{x} + t \cdot t\right) - \color{blue}{\frac{-\ell \cdot \ell}{x}}\right)}} \cdot t \]
      Proof
      (/.f64 (neg.f64 (*.f64 l l)) x): 0 points increase in error, 0 points decrease in error
      (/.f64 (neg.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2))) x): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (pow.f64 l 2))) x): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (pow.f64 l 2) x))): 0 points increase in error, 0 points decrease in error

   if -2.4000000000000001e-215 < t < -4.39999999999999968e-269

   1. Initial program 63.2

      \[\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. Simplified 63.2

      \[\leadsto \color{blue}{\sqrt{2} \cdot \frac{t}{\sqrt{\frac{x + 1}{\frac{x + -1}{\mathsf{fma}\left(t, 2 \cdot t, \ell \cdot \ell\right)}} - \ell \cdot \ell}}} \]
      Proof
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (/.f64 (+.f64 x 1) (/.f64 (+.f64 x -1) (fma.f64 t (*.f64 2 t) (*.f64 l l)))) (*.f64 l l))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (/.f64 (+.f64 x 1) (/.f64 (+.f64 x (Rewrite<= metadata-eval (neg.f64 1))) (fma.f64 t (*.f64 2 t) (*.f64 l l)))) (*.f64 l l))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (/.f64 (+.f64 x 1) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 x 1)) (fma.f64 t (*.f64 2 t) (*.f64 l l)))) (*.f64 l l))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (/.f64 (+.f64 x 1) (/.f64 (-.f64 x 1) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (*.f64 2 t)) (*.f64 l l))))) (*.f64 l l))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (/.f64 (+.f64 x 1) (/.f64 (-.f64 x 1) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 t) t)) (*.f64 l l)))) (*.f64 l l))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (/.f64 (+.f64 x 1) (/.f64 (-.f64 x 1) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 t t))) (*.f64 l l)))) (*.f64 l l))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (/.f64 (+.f64 x 1) (/.f64 (-.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))))) (*.f64 l l))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (sqrt.f64 2) (/.f64 t (sqrt.f64 (-.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))) (*.f64 l l))))): 4 points increase in error, 18 points decrease in error
      (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (sqrt.f64 2) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (*.f64 l l))))): 2 points increase in error, 10 points decrease in error

   3. Taylor expanded in x around inf 31.5

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

   4. Simplified 31.5

      \[\leadsto \sqrt{2} \cdot \frac{t}{\sqrt{\color{blue}{\frac{\ell}{\frac{x}{\ell}} + \mathsf{fma}\left(2, \mathsf{fma}\left(t, t, \frac{t}{\frac{x}{t}}\right), \frac{\mathsf{fma}\left(2, t \cdot t, \ell \cdot \ell\right)}{x}\right)}}} \]
      Proof
      (+.f64 (/.f64 l (/.f64 x l)) (fma.f64 2 (fma.f64 t t (/.f64 t (/.f64 x t))) (/.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l)) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 l l) x)) (fma.f64 2 (fma.f64 t t (/.f64 t (/.f64 x t))) (/.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l)) x))): 3 points increase in error, 5 points decrease in error
      (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) x) (fma.f64 2 (fma.f64 t t (/.f64 t (/.f64 x t))) (/.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l)) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (fma.f64 t t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 t t) x))) (/.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l)) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (fma.f64 t t (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 t 2)) x)) (/.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l)) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t t) (/.f64 (pow.f64 t 2) x))) (/.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l)) x))): 0 points increase in error, 1 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 t 2)) (/.f64 (pow.f64 t 2) x)) (/.f64 (fma.f64 2 (*.f64 t t) (*.f64 l l)) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (+.f64 (pow.f64 t 2) (/.f64 (pow.f64 t 2) x)) (/.f64 (fma.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2)) (*.f64 l l)) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (+.f64 (pow.f64 t 2) (/.f64 (pow.f64 t 2) x)) (/.f64 (fma.f64 2 (pow.f64 t 2) (Rewrite<= unpow2_binary64 (pow.f64 l 2))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (+.f64 (pow.f64 t 2) (/.f64 (pow.f64 t 2) x)) (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 (pow.f64 t 2)) (pow.f64 l 2))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (+.f64 (pow.f64 t 2) (/.f64 (pow.f64 t 2) x)) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (+.f64 (pow.f64 t 2) (/.f64 (pow.f64 t 2) x)) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 2 (+.f64 (pow.f64 t 2) (/.f64 (pow.f64 t 2) x)) (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 2 (+.f64 (pow.f64 t 2) (/.f64 (pow.f64 t 2) x))) (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x))))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 (pow.f64 t 2)) (*.f64 2 (/.f64 (pow.f64 t 2) x)))) (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))): 0 points increase in error, 0 points decrease in error

   5. Taylor expanded in t around -inf 25.9

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

   6. Simplified 25.9

      \[\leadsto \sqrt{2} \cdot \frac{t}{\color{blue}{-\mathsf{fma}\left(t, \sqrt{\left(2 + \frac{2}{x}\right) + \frac{2}{x}}, \sqrt{\frac{1}{\left(2 + \frac{2}{x}\right) + \frac{2}{x}}} \cdot \left(\frac{\ell}{x} \cdot \frac{\ell}{t}\right)\right)}} \]
      Proof
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (+.f64 (Rewrite<= metadata-eval (*.f64 2 1)) (/.f64 2 x)) (/.f64 2 x))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (+.f64 (*.f64 2 1) (/.f64 (Rewrite<= metadata-eval (*.f64 2 1)) x)) (/.f64 2 x))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (+.f64 (*.f64 2 1) (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 1 x)))) (/.f64 2 x))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 2 (+.f64 1 (/.f64 1 x)))) (/.f64 2 x))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (/.f64 (Rewrite<= metadata-eval (*.f64 2 1)) x))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 1 x))))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 2 (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 (Rewrite<= metadata-eval (*.f64 2 1)) (/.f64 2 x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 (*.f64 2 1) (/.f64 (Rewrite<= metadata-eval (*.f64 2 1)) x)) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (+.f64 (*.f64 2 1) (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 1 x)))) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 2 (+.f64 1 (/.f64 1 x)))) (/.f64 2 x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (/.f64 (Rewrite<= metadata-eval (*.f64 2 1)) x)))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 1 x)))))) (*.f64 (/.f64 l x) (/.f64 l t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 l l) (*.f64 x t)))))): 35 points increase in error, 13 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (*.f64 x t))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (fma.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))) (/.f64 (pow.f64 l 2) (Rewrite<= *-commutative_binary64 (*.f64 t x)))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))) (/.f64 (pow.f64 l 2) (*.f64 t x)))))): 1 points increase in error, 0 points decrease in error
      (neg.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) t)) (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))) (/.f64 (pow.f64 l 2) (*.f64 t x))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))) (/.f64 (pow.f64 l 2) (*.f64 t x))) (*.f64 (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) t)))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 l 2) (*.f64 t x)) (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))))) (*.f64 (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))) t))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (+.f64 (*.f64 (/.f64 (pow.f64 l 2) (*.f64 t x)) (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))))) (Rewrite=> *-commutative_binary64 (*.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (*.f64 (/.f64 (pow.f64 l 2) (*.f64 t x)) (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))))) (*.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 -1 (*.f64 (/.f64 (pow.f64 l 2) (*.f64 t x)) (sqrt.f64 (/.f64 1 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x))))))) (*.f64 -1 (*.f64 t (sqrt.f64 (+.f64 (*.f64 2 (+.f64 1 (/.f64 1 x))) (*.f64 2 (/.f64 1 x)))))))): 0 points increase in error, 0 points decrease in error

   if -4.39999999999999968e-269 < t < 7.6e-294

   1. Initial program 62.9

      \[\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. Taylor expanded in x around inf 32.1

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

   3. Simplified 32.1

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell \cdot \ell}{x} + \left(2 \cdot \left(\frac{t \cdot t}{x} + t \cdot t\right) - \frac{-\left(2 \cdot \left(t \cdot t\right) + \ell \cdot \ell\right)}{x}\right)}}} \]
      Proof
      (+.f64 (/.f64 (*.f64 l l) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 t 2)) x) (*.f64 t t))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (pow.f64 t 2) x) (Rewrite<= unpow2_binary64 (pow.f64 t 2)))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (pow.f64 t 2))))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (*.f64 2 (pow.f64 t 2)))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))): 0 points increase in error, 0 points decrease in error

   4. Taylor expanded in t around 0 32.1

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\sqrt{\frac{{\ell}^{2}}{x} - -1 \cdot \frac{{\ell}^{2}}{x}}}} \]

   5. Simplified 31.9

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}} \]
      Proof
      (sqrt.f64 (*.f64 (/.f64 l x) (+.f64 l l))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 l x) l) (*.f64 (/.f64 l x) l)))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (Rewrite<= cancel-sign-sub_binary64 (-.f64 (*.f64 (/.f64 l x) l) (*.f64 (neg.f64 (/.f64 l x)) l)))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l l) x)) (*.f64 (neg.f64 (/.f64 l x)) l))): 21 points increase in error, 1 points decrease in error
      (sqrt.f64 (-.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) x) (*.f64 (neg.f64 (/.f64 l x)) l))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (-.f64 (/.f64 (pow.f64 l 2) x) (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l x) l))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (-.f64 (/.f64 (pow.f64 l 2) x) (neg.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l l) x))))): 3 points increase in error, 3 points decrease in error
      (sqrt.f64 (-.f64 (/.f64 (pow.f64 l 2) x) (neg.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) x)))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (-.f64 (/.f64 (pow.f64 l 2) x) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (pow.f64 l 2) x))))): 0 points increase in error, 0 points decrease in error

   if 7.6e-294 < t < 3.30000000000000013e-176

   1. Initial program 62.7

      \[\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. Taylor expanded in x around inf 34.5

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

   3. Simplified 34.5

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell \cdot \ell}{x} + \left(2 \cdot \left(\frac{t \cdot t}{x} + t \cdot t\right) - \frac{-\left(2 \cdot \left(t \cdot t\right) + \ell \cdot \ell\right)}{x}\right)}}} \]
      Proof
      (+.f64 (/.f64 (*.f64 l l) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 t 2)) x) (*.f64 t t))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (*.f64 2 (+.f64 (/.f64 (pow.f64 t 2) x) (Rewrite<= unpow2_binary64 (pow.f64 t 2)))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))) (*.f64 l l))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (pow.f64 t 2))))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (neg.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (*.f64 2 (pow.f64 t 2)))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) x))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 (pow.f64 l 2) x) (-.f64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))) (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))): 0 points increase in error, 0 points decrease in error

   4. Taylor expanded in x around inf 23.5

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

   5. Simplified 23.5

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\mathsf{fma}\left(0.5, \frac{\ell \cdot \ell + \left(2 \cdot \left(t \cdot t\right) - \left(-\left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right)\right)\right)}{\sqrt{2} \cdot \left(t \cdot x\right)}, t \cdot \sqrt{2}\right)}} \]
      Proof
      (fma.f64 1/2 (/.f64 (+.f64 (*.f64 l l) (-.f64 (*.f64 2 (*.f64 t t)) (neg.f64 (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (*.f64 t (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/2 (/.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (-.f64 (*.f64 2 (*.f64 t t)) (neg.f64 (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (*.f64 t (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/2 (/.f64 (+.f64 (pow.f64 l 2) (-.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))) (neg.f64 (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (*.f64 t (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/2 (/.f64 (+.f64 (pow.f64 l 2) (-.f64 (*.f64 2 (pow.f64 t 2)) (neg.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (*.f64 2 (*.f64 t t)))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (*.f64 t (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/2 (/.f64 (+.f64 (pow.f64 l 2) (-.f64 (*.f64 2 (pow.f64 t 2)) (neg.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (*.f64 t (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/2 (/.f64 (+.f64 (pow.f64 l 2) (-.f64 (*.f64 2 (pow.f64 t 2)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (*.f64 t (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/2 (/.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (*.f64 t (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/2 (/.f64 (-.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) (*.f64 (sqrt.f64 2) (*.f64 t x))) (Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 2) t))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (/.f64 (-.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) (*.f64 (sqrt.f64 2) (*.f64 t x)))) (*.f64 (sqrt.f64 2) t))): 0 points increase in error, 0 points decrease in error

   if 3.30000000000000013e-176 < t < 1.2e-5

   1. Initial program 34.7

      \[\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. Taylor expanded in x around -inf 13.2

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

   3. Simplified 13.2

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\left(\frac{\ell \cdot \ell}{x} + \mathsf{fma}\left(-1, \frac{\left(-\left(2 \cdot \left(t \cdot t\right) + \ell \cdot \ell\right)\right) - \left(2 \cdot \left(t \cdot t\right) + \ell \cdot \ell\right)}{x \cdot x}, 2 \cdot \left(\frac{t \cdot t}{x} + t \cdot t\right)\right)\right) - \frac{-\left(2 \cdot \left(t \cdot t\right) + \ell \cdot \ell\right)}{x}}}} \]
      Proof
      (-.f64 (+.f64 (/.f64 (*.f64 l l) x) (fma.f64 -1 (/.f64 (-.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) x) (fma.f64 -1 (/.f64 (-.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (neg.f64 (+.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))) (*.f64 l l))) (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (pow.f64 t 2))))) (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (neg.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (*.f64 2 (pow.f64 t 2)))) (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))) (*.f64 l l))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (pow.f64 t 2))))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (*.f64 2 (pow.f64 t 2)))) (*.f64 x x)) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (Rewrite<= unpow2_binary64 (pow.f64 x 2))) (*.f64 2 (+.f64 (/.f64 (*.f64 t t) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2)) (*.f64 2 (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 t 2)) x) (*.f64 t t))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2)) (*.f64 2 (+.f64 (/.f64 (pow.f64 t 2) x) (Rewrite<= unpow2_binary64 (pow.f64 t 2)))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (fma.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2)) (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2))) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2)))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2))) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))))) (/.f64 (neg.f64 (+.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 t 2))) (*.f64 l l))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2))) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))))) (/.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (pow.f64 t 2))))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2))) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))))) (/.f64 (neg.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) (*.f64 2 (pow.f64 t 2)))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2))) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))))) (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))))) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 (/.f64 (pow.f64 l 2) x) (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2)))) (pow.f64 x 2))) (+.f64 (*.f64 2 (/.f64 (pow.f64 t 2) x)) (*.f64 2 (pow.f64 t 2))))) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (+.f64 (pow.f64 l 2) (*.f64 2 (pow.f64 t 2))) x)))): 0 points increase in error, 0 points decrease in error

   if 1.2e-5 < t

   1. Initial program 40.9

      \[\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. Simplified 52.4

      \[\leadsto \color{blue}{\frac{\sqrt{2}}{\sqrt{\frac{\left(x + 1\right) \cdot \mathsf{fma}\left(2 \cdot t, t, \ell \cdot \ell\right)}{x + -1} - \ell \cdot \ell}} \cdot t} \]
      Proof
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (fma.f64 (*.f64 2 t) t (*.f64 l l))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 2 t) t) (*.f64 l l)))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 t t))) (*.f64 l l))) (+.f64 x -1)) (*.f64 l l)))) t): 1 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))) (+.f64 x -1)) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 x 1) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (*.f64 l l)))) t): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (sqrt.f64 2) (sqrt.f64 (-.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))) (*.f64 l l)))) t): 18 points increase in error, 27 points decrease in error
      (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (sqrt.f64 2) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t)))) (*.f64 l l))))): 12 points increase in error, 9 points decrease in error

   3. Taylor expanded in t around inf 50.9

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

   4. Simplified 37.2

      \[\leadsto \frac{\sqrt{2}}{\sqrt{\color{blue}{2 \cdot \left(\frac{x + 1}{-1 + x} \cdot \left(t \cdot t\right)\right)}}} \cdot t \]
      Proof
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (+.f64 -1 x)) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 x -1))) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (*.f64 t t))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)) (Rewrite<= unpow2_binary64 (pow.f64 t 2)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= associate-/r/_binary64 (/.f64 (+.f64 x 1) (/.f64 (-.f64 x 1) (pow.f64 t 2))))): 24 points increase in error, 13 points decrease in error
      (*.f64 2 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 x)) (/.f64 (-.f64 x 1) (pow.f64 t 2)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 1 x) (pow.f64 t 2)) (-.f64 x 1)))): 45 points increase in error, 25 points decrease in error

   5. Taylor expanded in t around 0 5.3

      \[\leadsto \color{blue}{\sqrt{\frac{x - 1}{1 + x}}} \]

   6. Simplified 5.3

      \[\leadsto \color{blue}{\sqrt{\frac{x - 1}{x + 1}}} \]
      Proof
      (sqrt.f64 (/.f64 (-.f64 x 1) (+.f64 x 1))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (/.f64 (-.f64 x 1) (Rewrite<= +-commutative_binary64 (+.f64 1 x)))): 0 points increase in error, 0 points decrease in error
3. Recombined 7 regimes into one program.

4. Final simplification 10.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq -7.2 \cdot 10^{+26}:\\ \;\;\;\;-\sqrt{\frac{x + -1}{x + 1}}\\ \mathbf{elif}\;t \leq -2.4 \cdot 10^{-215}:\\ \;\;\;\;t \cdot \frac{\sqrt{2}}{\sqrt{\frac{\ell \cdot \ell}{x} + \left(\frac{\ell \cdot \ell}{x} - \left(t \cdot t + \frac{t \cdot t}{x}\right) \cdot -2\right)}}\\ \mathbf{elif}\;t \leq -4.4 \cdot 10^{-269}:\\ \;\;\;\;\sqrt{2} \cdot \frac{t}{-\mathsf{fma}\left(t, \sqrt{\frac{2}{x} + \left(2 + \frac{2}{x}\right)}, \sqrt{\frac{1}{\frac{2}{x} + \left(2 + \frac{2}{x}\right)}} \cdot \left(\frac{\ell}{x} \cdot \frac{\ell}{t}\right)\right)}\\ \mathbf{elif}\;t \leq 7.6 \cdot 10^{-294}:\\ \;\;\;\;\frac{t \cdot \sqrt{2}}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{elif}\;t \leq 3.3 \cdot 10^{-176}:\\ \;\;\;\;\frac{t \cdot \sqrt{2}}{\mathsf{fma}\left(0.5, \frac{\ell \cdot \ell + \left(2 \cdot \left(t \cdot t\right) + \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right)\right)}{\sqrt{2} \cdot \left(t \cdot x\right)}, t \cdot \sqrt{2}\right)}\\ \mathbf{elif}\;t \leq 1.2 \cdot 10^{-5}:\\ \;\;\;\;\frac{t \cdot \sqrt{2}}{\sqrt{\left(\frac{\ell \cdot \ell}{x} + \mathsf{fma}\left(-1, \frac{\left(\left(t \cdot t\right) \cdot -2 - \ell \cdot \ell\right) + \left(\left(t \cdot t\right) \cdot -2 - \ell \cdot \ell\right)}{x \cdot x}, 2 \cdot \left(t \cdot t + \frac{t \cdot t}{x}\right)\right)\right) + \frac{\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)}{x}}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{x + -1}{x + 1}}\\ \end{array} \]

Alternatives

Alternative 1
Error	10.9
Cost	28372

\[\begin{array}{l} t_1 := \frac{2}{x} + \left(2 + \frac{2}{x}\right)\\ t_2 := t \cdot \sqrt{2}\\ t_3 := t \cdot t + \frac{t \cdot t}{x}\\ t_4 := \sqrt{\frac{x + -1}{x + 1}}\\ t_5 := \frac{\ell \cdot \ell}{x}\\ t_6 := \left(t \cdot t\right) \cdot -2 - \ell \cdot \ell\\ \mathbf{if}\;t \leq -1.1 \cdot 10^{+26}:\\ \;\;\;\;-t_4\\ \mathbf{elif}\;t \leq -2.9 \cdot 10^{-216}:\\ \;\;\;\;t \cdot \frac{\sqrt{2}}{\sqrt{t_5 + \left(t_5 - t_3 \cdot -2\right)}}\\ \mathbf{elif}\;t \leq -1 \cdot 10^{-253}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 3.5 \cdot 10^{-295}:\\ \;\;\;\;\frac{t_2}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{elif}\;t \leq 3 \cdot 10^{-180}:\\ \;\;\;\;\sqrt{2} \cdot \frac{t}{\mathsf{fma}\left(\sqrt{t_1}, t, \sqrt{\frac{1}{t_1}} \cdot \frac{\ell \cdot \ell}{t \cdot x}\right)}\\ \mathbf{elif}\;t \leq 0.042:\\ \;\;\;\;\frac{t_2}{\sqrt{\left(t_5 + \mathsf{fma}\left(-1, \frac{t_6 + t_6}{x \cdot x}, 2 \cdot t_3\right)\right) + \frac{\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)}{x}}}\\ \mathbf{else}:\\ \;\;\;\;t_4\\ \end{array} \]

Alternative 2
Error	10.4
Cost	28372

\[\begin{array}{l} t_1 := t \cdot \sqrt{2}\\ t_2 := \frac{2}{x} + \left(2 + \frac{2}{x}\right)\\ t_3 := \sqrt{\frac{x + -1}{x + 1}}\\ t_4 := \frac{\ell \cdot \ell}{x}\\ t_5 := \sqrt{t_2}\\ t_6 := t \cdot t + \frac{t \cdot t}{x}\\ t_7 := \sqrt{\frac{1}{t_2}}\\ t_8 := \left(t \cdot t\right) \cdot -2 - \ell \cdot \ell\\ \mathbf{if}\;t \leq -7.5 \cdot 10^{+26}:\\ \;\;\;\;-t_3\\ \mathbf{elif}\;t \leq -3.9 \cdot 10^{-215}:\\ \;\;\;\;t \cdot \frac{\sqrt{2}}{\sqrt{t_4 + \left(t_4 - t_6 \cdot -2\right)}}\\ \mathbf{elif}\;t \leq -6 \cdot 10^{-270}:\\ \;\;\;\;\sqrt{2} \cdot \frac{t}{-\mathsf{fma}\left(t, t_5, t_7 \cdot \left(\frac{\ell}{x} \cdot \frac{\ell}{t}\right)\right)}\\ \mathbf{elif}\;t \leq 4 \cdot 10^{-295}:\\ \;\;\;\;\frac{t_1}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{elif}\;t \leq 4.9 \cdot 10^{-175}:\\ \;\;\;\;\sqrt{2} \cdot \frac{t}{\mathsf{fma}\left(t_5, t, t_7 \cdot \frac{\ell \cdot \ell}{t \cdot x}\right)}\\ \mathbf{elif}\;t \leq 0.042:\\ \;\;\;\;\frac{t_1}{\sqrt{\left(t_4 + \mathsf{fma}\left(-1, \frac{t_8 + t_8}{x \cdot x}, 2 \cdot t_6\right)\right) + \frac{\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)}{x}}}\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]

Alternative 3
Error	11.7
Cost	23640

\[\begin{array}{l} t_1 := t \cdot \sqrt{2}\\ t_2 := t \cdot t + \frac{t \cdot t}{x}\\ t_3 := \left(t \cdot t\right) \cdot -2 - \ell \cdot \ell\\ t_4 := \sqrt{\frac{x + -1}{x + 1}}\\ t_5 := \frac{\ell \cdot \ell}{x}\\ \mathbf{if}\;t \leq -1.15 \cdot 10^{+27}:\\ \;\;\;\;-t_4\\ \mathbf{elif}\;t \leq -1.1 \cdot 10^{-218}:\\ \;\;\;\;t \cdot \frac{\sqrt{2}}{\sqrt{t_5 + \left(t_5 - t_2 \cdot -2\right)}}\\ \mathbf{elif}\;t \leq -1.5 \cdot 10^{-253}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 5.2 \cdot 10^{-291}:\\ \;\;\;\;\frac{t_1}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{elif}\;t \leq 7.6 \cdot 10^{-175}:\\ \;\;\;\;\sqrt{1 + \frac{-2}{x}}\\ \mathbf{elif}\;t \leq 0.0115:\\ \;\;\;\;\frac{t_1}{\sqrt{\left(t_5 + \mathsf{fma}\left(-1, \frac{t_3 + t_3}{x \cdot x}, 2 \cdot t_2\right)\right) + \frac{\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)}{x}}}\\ \mathbf{else}:\\ \;\;\;\;t_4\\ \end{array} \]

Alternative 4
Error	11.7
Cost	15320

\[\begin{array}{l} t_1 := \sqrt{\frac{x + -1}{x + 1}}\\ t_2 := \frac{\ell \cdot \ell}{x}\\ t_3 := t \cdot \frac{\sqrt{2}}{\sqrt{t_2 + \left(t_2 - \left(t \cdot t + \frac{t \cdot t}{x}\right) \cdot -2\right)}}\\ \mathbf{if}\;t \leq -1.55 \cdot 10^{+27}:\\ \;\;\;\;-t_1\\ \mathbf{elif}\;t \leq -3 \cdot 10^{-217}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t \leq -8.2 \cdot 10^{-254}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 7.2 \cdot 10^{-290}:\\ \;\;\;\;\frac{t \cdot \sqrt{2}}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{elif}\;t \leq 8.4 \cdot 10^{-175}:\\ \;\;\;\;\sqrt{1 + \frac{-2}{x}}\\ \mathbf{elif}\;t \leq 1.46 \cdot 10^{-5}:\\ \;\;\;\;t_3\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 5
Error	11.8
Cost	15320

\[\begin{array}{l} t_1 := t \cdot \sqrt{2}\\ t_2 := \sqrt{\frac{x + -1}{x + 1}}\\ t_3 := \frac{\ell \cdot \ell}{x}\\ t_4 := \sqrt{t_3 + \left(t_3 - \left(t \cdot t + \frac{t \cdot t}{x}\right) \cdot -2\right)}\\ \mathbf{if}\;t \leq -1.25 \cdot 10^{+25}:\\ \;\;\;\;-t_2\\ \mathbf{elif}\;t \leq -4.2 \cdot 10^{-216}:\\ \;\;\;\;t \cdot \frac{\sqrt{2}}{t_4}\\ \mathbf{elif}\;t \leq -2.1 \cdot 10^{-254}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 3.6 \cdot 10^{-294}:\\ \;\;\;\;\frac{t_1}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{elif}\;t \leq 5.4 \cdot 10^{-176}:\\ \;\;\;\;\sqrt{1 + \frac{-2}{x}}\\ \mathbf{elif}\;t \leq 0.042:\\ \;\;\;\;\frac{t_1}{t_4}\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 6
Error	14.2
Cost	14032

\[\begin{array}{l} t_1 := \sqrt{2} \cdot \frac{t}{\sqrt{\ell \cdot \frac{\ell + \ell}{x}}}\\ t_2 := \sqrt{\frac{x + -1}{x + 1}}\\ \mathbf{if}\;t \leq -1.08 \cdot 10^{-156}:\\ \;\;\;\;-t_2\\ \mathbf{elif}\;t \leq -2.2 \cdot 10^{-218}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq -8 \cdot 10^{-254}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 1.3 \cdot 10^{-289}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 7
Error	14.3
Cost	14032

\[\begin{array}{l} t_1 := \sqrt{\frac{x + -1}{x + 1}}\\ \mathbf{if}\;t \leq -1.85 \cdot 10^{-146}:\\ \;\;\;\;-t_1\\ \mathbf{elif}\;t \leq -7.2 \cdot 10^{-216}:\\ \;\;\;\;\sqrt{2} \cdot \frac{t}{\sqrt{\ell \cdot \frac{\ell + \ell}{x}}}\\ \mathbf{elif}\;t \leq -9 \cdot 10^{-254}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 4.8 \cdot 10^{-290}:\\ \;\;\;\;t \cdot \frac{\sqrt{2}}{\sqrt{2 \cdot \frac{\ell}{\frac{x}{\ell}}}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 8
Error	14.3
Cost	14032

\[\begin{array}{l} t_1 := \sqrt{\frac{x + -1}{x + 1}}\\ \mathbf{if}\;t \leq -1.9 \cdot 10^{-146}:\\ \;\;\;\;-t_1\\ \mathbf{elif}\;t \leq -4.3 \cdot 10^{-218}:\\ \;\;\;\;\sqrt{2} \cdot \frac{t}{\sqrt{\ell \cdot \frac{\ell + \ell}{x}}}\\ \mathbf{elif}\;t \leq -1.7 \cdot 10^{-254}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 1.7 \cdot 10^{-293}:\\ \;\;\;\;\frac{t \cdot \sqrt{2}}{\sqrt{\frac{\ell}{x} \cdot \left(\ell + \ell\right)}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 9
Error	14.6
Cost	13712

\[\begin{array}{l} t_1 := t \cdot \sqrt{x \cdot {\ell}^{-2}}\\ t_2 := \sqrt{\frac{x + -1}{x + 1}}\\ \mathbf{if}\;t \leq -2.75 \cdot 10^{-146}:\\ \;\;\;\;-t_2\\ \mathbf{elif}\;t \leq -3.2 \cdot 10^{-216}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq -3.2 \cdot 10^{-254}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{elif}\;t \leq 3.8 \cdot 10^{-292}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 10
Error	15.0
Cost	7044

\[\begin{array}{l} t_1 := \sqrt{\frac{x + -1}{x + 1}}\\ \mathbf{if}\;t \leq -5 \cdot 10^{-310}:\\ \;\;\;\;-t_1\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 11
Error	15.1
Cost	6980

\[\begin{array}{l} \mathbf{if}\;t \leq -5 \cdot 10^{-310}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{x + -1}{x + 1}}\\ \end{array} \]

Alternative 12
Error	15.3
Cost	836

\[\begin{array}{l} \mathbf{if}\;t \leq -5 \cdot 10^{-310}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\frac{0.5}{x \cdot x} + \frac{-1}{x}\right)\\ \end{array} \]

Alternative 13
Error	15.8
Cost	452

\[\begin{array}{l} \mathbf{if}\;t \leq -5 \cdot 10^{-309}:\\ \;\;\;\;t \cdot \frac{-1}{t}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 14
Error	15.5
Cost	452

\[\begin{array}{l} \mathbf{if}\;t \leq -5 \cdot 10^{-310}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 15
Error	15.3
Cost	452

\[\begin{array}{l} \mathbf{if}\;t \leq -5 \cdot 10^{-310}:\\ \;\;\;\;-1 + \frac{1}{x}\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{1}{x}\\ \end{array} \]

Alternative 16
Error	38.5
Cost	64

\[1 \]

Reproduce

herbie shell --seed 2022338 
(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)))))