Toniolo and Linder, Equation (13)

Average Error: 34.8 → 29.4

Time: 1.4min

Precision: binary64

Cost: 40992

Math

\[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

↓

\[\begin{array}{l} t_1 := \frac{n}{\frac{Om}{U \cdot \ell}}\\ t_2 := n \cdot \left(U \cdot 2\right)\\ t_3 := \sqrt{n \cdot 2}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(t_2, t, \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(t_2 \cdot \frac{\ell}{Om}\right)\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t \cdot \left(n \cdot U\right), \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 2.7 \cdot 10^{-256}:\\ \;\;\;\;t_3 \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{elif}\;n \leq 1.2 \cdot 10^{-195}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \mathbf{elif}\;n \leq 1.5 \cdot 10^{-85}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 3.1 \cdot 10^{-27}:\\ \;\;\;\;t_3 \cdot \left(\sqrt{\mathsf{fma}\left(\frac{\ell}{Om}, \mathsf{fma}\left(\ell, -2, \frac{\ell}{\frac{Om}{n \cdot U*}}\right), t\right)} \cdot \sqrt{U}\right)\\ \mathbf{elif}\;n \leq 1.4 \cdot 10^{+133}:\\ \;\;\;\;t_3 \cdot \sqrt{U \cdot \left(t - \mathsf{fma}\left(2, \ell \cdot \frac{\ell}{Om}, n \cdot \left({\left(\frac{\ell}{Om}\right)}^{2} \cdot \left(U - U*\right)\right)\right)\right)}\\ \mathbf{elif}\;n \leq 2.7 \cdot 10^{+160}:\\ \;\;\;\;\sqrt{2 \cdot \left(t_1 \cdot \left(\ell \cdot -2 - t_1\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_3 \cdot \sqrt{U \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell \cdot U*}{{\left(\sqrt[3]{Om}\right)}^{2}} \cdot \frac{n}{\sqrt[3]{Om}}\right)\right)}\\ \end{array} \]

FPCore

(FPCore (n U t l Om U*)
 :precision binary64
 (sqrt
  (*
   (* (* 2.0 n) U)
   (- (- t (* 2.0 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2.0)) (- U U*))))))

↓

(FPCore (n U t l Om U*)
 :precision binary64
 (let* ((t_1 (/ n (/ Om (* U l))))
        (t_2 (* n (* U 2.0)))
        (t_3 (sqrt (* n 2.0))))
   (if (<= n -8e-145)
     (sqrt
      (fma
       t_2
       t
       (* (fma l -2.0 (* n (* (/ l Om) (- U* U)))) (* t_2 (/ l Om)))))
     (if (<= n 1.55e-291)
       (sqrt (fma 2.0 (* t (* n U)) (/ -4.0 (/ Om (* U (* l (* n l)))))))
       (if (<= n 2.7e-256)
         (*
          t_3
          (sqrt (+ (* U t) (* (* l l) (* (/ U Om) (+ -2.0 (* n (/ U* Om))))))))
         (if (<= n 1.2e-195)
           (sqrt (* 2.0 (* U (* n (fma -2.0 (/ l (/ Om l)) t)))))
           (if (<= n 1.5e-85)
             (sqrt
              (+
               (* 2.0 (* n (* U t)))
               (*
                -2.0
                (/
                 (* (* n (* U l)) (- (* 2.0 l) (/ (* n (* l (- U* U))) Om)))
                 Om))))
             (if (<= n 3.1e-27)
               (*
                t_3
                (*
                 (sqrt (fma (/ l Om) (fma l -2.0 (/ l (/ Om (* n U*)))) t))
                 (sqrt U)))
               (if (<= n 1.4e+133)
                 (*
                  t_3
                  (sqrt
                   (*
                    U
                    (-
                     t
                     (fma
                      2.0
                      (* l (/ l Om))
                      (* n (* (pow (/ l Om) 2.0) (- U U*))))))))
                 (if (<= n 2.7e+160)
                   (sqrt (* 2.0 (* t_1 (- (* l -2.0) t_1))))
                   (*
                    t_3
                    (sqrt
                     (*
                      U
                      (+
                       t
                       (*
                        (/ l Om)
                        (fma
                         l
                         -2.0
                         (*
                          (/ (* l U*) (pow (cbrt Om) 2.0))
                          (/ n (cbrt Om)))))))))))))))))))

C

double code(double n, double U, double t, double l, double Om, double U_42_) {
	return sqrt((((2.0 * n) * U) * ((t - (2.0 * ((l * l) / Om))) - ((n * pow((l / Om), 2.0)) * (U - U_42_)))));
}

↓

double code(double n, double U, double t, double l, double Om, double U_42_) {
	double t_1 = n / (Om / (U * l));
	double t_2 = n * (U * 2.0);
	double t_3 = sqrt((n * 2.0));
	double tmp;
	if (n <= -8e-145) {
		tmp = sqrt(fma(t_2, t, (fma(l, -2.0, (n * ((l / Om) * (U_42_ - U)))) * (t_2 * (l / Om)))));
	} else if (n <= 1.55e-291) {
		tmp = sqrt(fma(2.0, (t * (n * U)), (-4.0 / (Om / (U * (l * (n * l)))))));
	} else if (n <= 2.7e-256) {
		tmp = t_3 * sqrt(((U * t) + ((l * l) * ((U / Om) * (-2.0 + (n * (U_42_ / Om)))))));
	} else if (n <= 1.2e-195) {
		tmp = sqrt((2.0 * (U * (n * fma(-2.0, (l / (Om / l)), t)))));
	} else if (n <= 1.5e-85) {
		tmp = sqrt(((2.0 * (n * (U * t))) + (-2.0 * (((n * (U * l)) * ((2.0 * l) - ((n * (l * (U_42_ - U))) / Om))) / Om))));
	} else if (n <= 3.1e-27) {
		tmp = t_3 * (sqrt(fma((l / Om), fma(l, -2.0, (l / (Om / (n * U_42_)))), t)) * sqrt(U));
	} else if (n <= 1.4e+133) {
		tmp = t_3 * sqrt((U * (t - fma(2.0, (l * (l / Om)), (n * (pow((l / Om), 2.0) * (U - U_42_)))))));
	} else if (n <= 2.7e+160) {
		tmp = sqrt((2.0 * (t_1 * ((l * -2.0) - t_1))));
	} else {
		tmp = t_3 * sqrt((U * (t + ((l / Om) * fma(l, -2.0, (((l * U_42_) / pow(cbrt(Om), 2.0)) * (n / cbrt(Om))))))));
	}
	return tmp;
}

Julia

function code(n, U, t, l, Om, U_42_)
	return sqrt(Float64(Float64(Float64(2.0 * n) * U) * Float64(Float64(t - Float64(2.0 * Float64(Float64(l * l) / Om))) - Float64(Float64(n * (Float64(l / Om) ^ 2.0)) * Float64(U - U_42_)))))
end

↓

function code(n, U, t, l, Om, U_42_)
	t_1 = Float64(n / Float64(Om / Float64(U * l)))
	t_2 = Float64(n * Float64(U * 2.0))
	t_3 = sqrt(Float64(n * 2.0))
	tmp = 0.0
	if (n <= -8e-145)
		tmp = sqrt(fma(t_2, t, Float64(fma(l, -2.0, Float64(n * Float64(Float64(l / Om) * Float64(U_42_ - U)))) * Float64(t_2 * Float64(l / Om)))));
	elseif (n <= 1.55e-291)
		tmp = sqrt(fma(2.0, Float64(t * Float64(n * U)), Float64(-4.0 / Float64(Om / Float64(U * Float64(l * Float64(n * l)))))));
	elseif (n <= 2.7e-256)
		tmp = Float64(t_3 * sqrt(Float64(Float64(U * t) + Float64(Float64(l * l) * Float64(Float64(U / Om) * Float64(-2.0 + Float64(n * Float64(U_42_ / Om))))))));
	elseif (n <= 1.2e-195)
		tmp = sqrt(Float64(2.0 * Float64(U * Float64(n * fma(-2.0, Float64(l / Float64(Om / l)), t)))));
	elseif (n <= 1.5e-85)
		tmp = sqrt(Float64(Float64(2.0 * Float64(n * Float64(U * t))) + Float64(-2.0 * Float64(Float64(Float64(n * Float64(U * l)) * Float64(Float64(2.0 * l) - Float64(Float64(n * Float64(l * Float64(U_42_ - U))) / Om))) / Om))));
	elseif (n <= 3.1e-27)
		tmp = Float64(t_3 * Float64(sqrt(fma(Float64(l / Om), fma(l, -2.0, Float64(l / Float64(Om / Float64(n * U_42_)))), t)) * sqrt(U)));
	elseif (n <= 1.4e+133)
		tmp = Float64(t_3 * sqrt(Float64(U * Float64(t - fma(2.0, Float64(l * Float64(l / Om)), Float64(n * Float64((Float64(l / Om) ^ 2.0) * Float64(U - U_42_))))))));
	elseif (n <= 2.7e+160)
		tmp = sqrt(Float64(2.0 * Float64(t_1 * Float64(Float64(l * -2.0) - t_1))));
	else
		tmp = Float64(t_3 * sqrt(Float64(U * Float64(t + Float64(Float64(l / Om) * fma(l, -2.0, Float64(Float64(Float64(l * U_42_) / (cbrt(Om) ^ 2.0)) * Float64(n / cbrt(Om)))))))));
	end
	return tmp
end

Wolfram

code[n_, U_, t_, l_, Om_, U$42$_] := N[Sqrt[N[(N[(N[(2.0 * n), $MachinePrecision] * U), $MachinePrecision] * N[(N[(t - N[(2.0 * N[(N[(l * l), $MachinePrecision] / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(N[(n * N[Power[N[(l / Om), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] * N[(U - U$42$), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]

↓

code[n_, U_, t_, l_, Om_, U$42$_] := Block[{t$95$1 = N[(n / N[(Om / N[(U * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(n * N[(U * 2.0), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[Sqrt[N[(n * 2.0), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[n, -8e-145], N[Sqrt[N[(t$95$2 * t + N[(N[(l * -2.0 + N[(n * N[(N[(l / Om), $MachinePrecision] * N[(U$42$ - U), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(t$95$2 * N[(l / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], If[LessEqual[n, 1.55e-291], N[Sqrt[N[(2.0 * N[(t * N[(n * U), $MachinePrecision]), $MachinePrecision] + N[(-4.0 / N[(Om / N[(U * N[(l * N[(n * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], If[LessEqual[n, 2.7e-256], N[(t$95$3 * N[Sqrt[N[(N[(U * t), $MachinePrecision] + N[(N[(l * l), $MachinePrecision] * N[(N[(U / Om), $MachinePrecision] * N[(-2.0 + N[(n * N[(U$42$ / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], If[LessEqual[n, 1.2e-195], N[Sqrt[N[(2.0 * N[(U * N[(n * N[(-2.0 * N[(l / N[(Om / l), $MachinePrecision]), $MachinePrecision] + t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], If[LessEqual[n, 1.5e-85], N[Sqrt[N[(N[(2.0 * N[(n * N[(U * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(-2.0 * N[(N[(N[(n * N[(U * l), $MachinePrecision]), $MachinePrecision] * N[(N[(2.0 * l), $MachinePrecision] - N[(N[(n * N[(l * N[(U$42$ - U), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], If[LessEqual[n, 3.1e-27], N[(t$95$3 * N[(N[Sqrt[N[(N[(l / Om), $MachinePrecision] * N[(l * -2.0 + N[(l / N[(Om / N[(n * U$42$), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t), $MachinePrecision]], $MachinePrecision] * N[Sqrt[U], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[n, 1.4e+133], N[(t$95$3 * N[Sqrt[N[(U * N[(t - N[(2.0 * N[(l * N[(l / Om), $MachinePrecision]), $MachinePrecision] + N[(n * N[(N[Power[N[(l / Om), $MachinePrecision], 2.0], $MachinePrecision] * N[(U - U$42$), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], If[LessEqual[n, 2.7e+160], N[Sqrt[N[(2.0 * N[(t$95$1 * N[(N[(l * -2.0), $MachinePrecision] - t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[(t$95$3 * N[Sqrt[N[(U * N[(t + N[(N[(l / Om), $MachinePrecision] * N[(l * -2.0 + N[(N[(N[(l * U$42$), $MachinePrecision] / N[Power[N[Power[Om, 1/3], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] * N[(n / N[Power[Om, 1/3], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]]]]]]]]]

Derivation

1. Split input into 9 regimes

2. if n < -7.99999999999999932e-145

   1. Initial program 32.9

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 30.6

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Applied egg-rr 27.0

      \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(n \cdot \left(U \cdot 2\right), t, \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(\frac{\ell}{Om} \cdot \left(n \cdot \left(U \cdot 2\right)\right)\right)\right)}} \]

   if -7.99999999999999932e-145 < n < 1.55000000000000006e-291

   1. Initial program 38.8

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 39.0

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in U* around 0 38.0

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

   4. Simplified 38.8

      \[\leadsto \sqrt{\color{blue}{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - \frac{n}{\frac{Om}{\ell \cdot U}}\right)\right)}} \]
      Proof
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 l -2) (/.f64 n (/.f64 Om (*.f64 l U))))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 -2 l)) (/.f64 n (/.f64 Om (*.f64 l U))))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 -2 l) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 n (*.f64 l U)) Om)))))): 0 points increase in error, 3 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -2 l) (neg.f64 (/.f64 (*.f64 n (*.f64 l U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (+.f64 (*.f64 -2 l) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= associate-/r/_binary64 (/.f64 l (/.f64 Om (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))))))): 8 points increase in error, 9 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 l (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))) Om)))): 22 points increase in error, 5 points decrease in error
      (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 l (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))) Om) t))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 2 n) (*.f64 U (+.f64 (/.f64 (*.f64 l (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))) Om) t)))): 34 points increase in error, 37 points decrease in error
      (*.f64 (*.f64 2 n) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (/.f64 (*.f64 l (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))) Om) t) U))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 n (*.f64 (+.f64 (/.f64 (*.f64 l (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))) Om) t) U)))): 0 points increase in error, 0 points decrease in error

   5. Taylor expanded in Om around inf 38.3

      \[\leadsto \sqrt{\color{blue}{2 \cdot \left(n \cdot \left(t \cdot U\right)\right) + -4 \cdot \frac{n \cdot \left({\ell}^{2} \cdot U\right)}{Om}}} \]

   6. Simplified 31.0

      \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(2, t \cdot \left(n \cdot U\right), \frac{-4}{\frac{Om}{U \cdot \left(\left(n \cdot \ell\right) \cdot \ell\right)}}\right)}} \]
      Proof
      (fma.f64 2 (*.f64 t (*.f64 n U)) (/.f64 -4 (/.f64 Om (*.f64 U (*.f64 (*.f64 n l) l))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 2 (*.f64 t (Rewrite=> *-commutative_binary64 (*.f64 U n))) (/.f64 -4 (/.f64 Om (*.f64 U (*.f64 (*.f64 n l) l))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 2 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 t U) n)) (/.f64 -4 (/.f64 Om (*.f64 U (*.f64 (*.f64 n l) l))))): 36 points increase in error, 31 points decrease in error
      (fma.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 t U))) (/.f64 -4 (/.f64 Om (*.f64 U (*.f64 (*.f64 n l) l))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 2 (*.f64 n (*.f64 t U)) (/.f64 -4 (/.f64 Om (*.f64 U (Rewrite<= associate-*r*_binary64 (*.f64 n (*.f64 l l))))))): 19 points increase in error, 3 points decrease in error
      (fma.f64 2 (*.f64 n (*.f64 t U)) (/.f64 -4 (/.f64 Om (*.f64 U (*.f64 n (Rewrite<= unpow2_binary64 (pow.f64 l 2))))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 2 (*.f64 n (*.f64 t U)) (/.f64 -4 (/.f64 Om (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 n (pow.f64 l 2)) U))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 2 (*.f64 n (*.f64 t U)) (/.f64 -4 (/.f64 Om (Rewrite<= associate-*r*_binary64 (*.f64 n (*.f64 (pow.f64 l 2) U)))))): 4 points increase in error, 7 points decrease in error
      (fma.f64 2 (*.f64 n (*.f64 t U)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -4 (*.f64 n (*.f64 (pow.f64 l 2) U))) Om))): 6 points increase in error, 7 points decrease in error
      (fma.f64 2 (*.f64 n (*.f64 t U)) (Rewrite<= associate-*r/_binary64 (*.f64 -4 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U)) Om)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 (*.f64 n (*.f64 t U))) (*.f64 -4 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U)) Om)))): 0 points increase in error, 0 points decrease in error

   if 1.55000000000000006e-291 < n < 2.7000000000000002e-256

   1. Initial program 38.6

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 39.7

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in U around 0 37.0

      \[\leadsto \sqrt{\color{blue}{2 \cdot \left(n \cdot \left(\left(t + \frac{\ell \cdot \left(-2 \cdot \ell + \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)}{Om}\right) \cdot U\right)\right)}} \]

   4. Applied egg-rr 21.3

      \[\leadsto \color{blue}{\sqrt{2 \cdot n} \cdot \sqrt{\left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell \cdot \left(U* \cdot n\right)}{Om}\right)\right) \cdot U}} \]

   5. Taylor expanded in l around -inf 25.5

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

   6. Simplified 26.7

      \[\leadsto \sqrt{2 \cdot n} \cdot \sqrt{\color{blue}{U \cdot t - \left(\frac{U}{Om} \cdot \left(2 - \frac{U*}{Om} \cdot n\right)\right) \cdot \left(\ell \cdot \ell\right)}} \]
      Proof
      (-.f64 (*.f64 U t) (*.f64 (*.f64 (/.f64 U Om) (-.f64 2 (*.f64 (/.f64 U* Om) n))) (*.f64 l l))): 0 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 t U)) (*.f64 (*.f64 (/.f64 U Om) (-.f64 2 (*.f64 (/.f64 U* Om) n))) (*.f64 l l))): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (*.f64 (/.f64 U Om) (-.f64 2 (Rewrite<= associate-/r/_binary64 (/.f64 U* (/.f64 Om n))))) (*.f64 l l))): 7 points increase in error, 10 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (*.f64 (/.f64 U Om) (-.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 U* n) Om)))) (*.f64 l l))): 14 points increase in error, 7 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (*.f64 (/.f64 U Om) (-.f64 2 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 n U*)) Om))) (*.f64 l l))): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (*.f64 (/.f64 U Om) (Rewrite<= unsub-neg_binary64 (+.f64 2 (neg.f64 (/.f64 (*.f64 n U*) Om))))) (*.f64 l l))): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (*.f64 (/.f64 U Om) (+.f64 2 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 n U*) Om))))) (*.f64 l l))): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (Rewrite<= associate-/r/_binary64 (/.f64 U (/.f64 Om (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om)))))) (*.f64 l l))): 9 points increase in error, 2 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 U (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om)))) Om)) (*.f64 l l))): 2 points increase in error, 11 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) U)) Om) (*.f64 l l))): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (Rewrite=> associate-/l*_binary64 (/.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) (/.f64 Om U))) (*.f64 l l))): 2 points increase in error, 3 points decrease in error
      (-.f64 (*.f64 t U) (*.f64 (/.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) (/.f64 Om U)) (Rewrite<= unpow2_binary64 (pow.f64 l 2)))): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 t U) (Rewrite<= associate-/r/_binary64 (/.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) (/.f64 (/.f64 Om U) (pow.f64 l 2))))): 4 points increase in error, 11 points decrease in error
      (-.f64 (*.f64 t U) (/.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) (Rewrite=> associate-/l/_binary64 (/.f64 Om (*.f64 (pow.f64 l 2) U))))): 9 points increase in error, 6 points decrease in error
      (-.f64 (*.f64 t U) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) (*.f64 (pow.f64 l 2) U)) Om))): 0 points increase in error, 10 points decrease in error
      (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 t U) (neg.f64 (/.f64 (*.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) (*.f64 (pow.f64 l 2) U)) Om)))): 0 points increase in error, 0 points decrease in error
      (+.f64 (*.f64 t U) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (+.f64 2 (*.f64 -1 (/.f64 (*.f64 n U*) Om))) (*.f64 (pow.f64 l 2) U)) Om)))): 0 points increase in error, 0 points decrease in error

   if 2.7000000000000002e-256 < n < 1.2e-195

   1. Initial program 39.3

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 39.3

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in U around 0 40.2

      \[\leadsto \sqrt{\color{blue}{2 \cdot \left(n \cdot \left(\left(t + \frac{\ell \cdot \left(-2 \cdot \ell + \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)}{Om}\right) \cdot U\right)\right)}} \]

   4. Taylor expanded in n around 0 40.4

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

   5. Simplified 34.5

      \[\leadsto \sqrt{2 \cdot \color{blue}{\left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}} \]
      Proof
      (*.f64 U (*.f64 n (fma.f64 -2 (/.f64 l (/.f64 Om l)) t))): 0 points increase in error, 0 points decrease in error
      (*.f64 U (*.f64 n (fma.f64 -2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 l l) Om)) t))): 24 points increase in error, 4 points decrease in error
      (*.f64 U (*.f64 n (fma.f64 -2 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) Om) t))): 0 points increase in error, 0 points decrease in error
      (*.f64 U (*.f64 n (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -2 (/.f64 (pow.f64 l 2) Om)) t)))): 0 points increase in error, 0 points decrease in error
      (*.f64 U (*.f64 n (Rewrite<= +-commutative_binary64 (+.f64 t (*.f64 -2 (/.f64 (pow.f64 l 2) Om)))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 U n) (+.f64 t (*.f64 -2 (/.f64 (pow.f64 l 2) Om))))): 34 points increase in error, 33 points decrease in error
      (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 n U)) (+.f64 t (*.f64 -2 (/.f64 (pow.f64 l 2) Om)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 t (*.f64 -2 (/.f64 (pow.f64 l 2) Om))) (*.f64 n U))): 0 points increase in error, 0 points decrease in error

   if 1.2e-195 < n < 1.50000000000000011e-85

   1. Initial program 34.5

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 33.8

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in t around inf 29.5

      \[\leadsto \sqrt{\color{blue}{2 \cdot \left(n \cdot \left(t \cdot U\right)\right) + 2 \cdot \frac{\left(\frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om} + -2 \cdot \ell\right) \cdot \left(n \cdot \left(\ell \cdot U\right)\right)}{Om}}} \]

   if 1.50000000000000011e-85 < n < 3.0999999999999998e-27

   1. Initial program 33.2

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 30.6

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in U around 0 32.2

      \[\leadsto \sqrt{\color{blue}{2 \cdot \left(n \cdot \left(\left(t + \frac{\ell \cdot \left(-2 \cdot \ell + \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)}{Om}\right) \cdot U\right)\right)}} \]

   4. Applied egg-rr 26.6

      \[\leadsto \color{blue}{\sqrt{2 \cdot n} \cdot \sqrt{\left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell \cdot \left(U* \cdot n\right)}{Om}\right)\right) \cdot U}} \]

   5. Applied egg-rr 42.0

      \[\leadsto \sqrt{2 \cdot n} \cdot \color{blue}{\left(\sqrt{\mathsf{fma}\left(\frac{\ell}{Om}, \mathsf{fma}\left(\ell, -2, \frac{\ell}{\frac{Om}{U* \cdot n}}\right), t\right)} \cdot \sqrt{U}\right)} \]

   if 3.0999999999999998e-27 < n < 1.40000000000000008e133

   1. Initial program 29.9

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Applied egg-rr 24.2

      \[\leadsto \color{blue}{\sqrt{2 \cdot n} \cdot \sqrt{U \cdot \left(t - \mathsf{fma}\left(2, \ell \cdot \frac{\ell}{Om}, n \cdot \left({\left(\frac{\ell}{Om}\right)}^{2} \cdot \left(U - U*\right)\right)\right)\right)}} \]

   if 1.40000000000000008e133 < n < 2.7e160

   1. Initial program 32.2

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 28.0

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in t around 0 56.9

      \[\leadsto \sqrt{\color{blue}{2 \cdot \frac{n \cdot \left(\left(\frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om} + -2 \cdot \ell\right) \cdot \left(\ell \cdot U\right)\right)}{Om}}} \]

   4. Taylor expanded in U* around 0 61.8

      \[\leadsto \sqrt{2 \cdot \color{blue}{\frac{n \cdot \left(\ell \cdot \left(U \cdot \left(-1 \cdot \frac{n \cdot \left(\ell \cdot U\right)}{Om} + -2 \cdot \ell\right)\right)\right)}{Om}}} \]

   5. Simplified 60.8

      \[\leadsto \sqrt{2 \cdot \color{blue}{\left(\frac{n}{\frac{Om}{\ell \cdot U}} \cdot \left(\ell \cdot -2 - \frac{n}{\frac{Om}{\ell \cdot U}}\right)\right)}} \]
      Proof
      (*.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (-.f64 (*.f64 l -2) (/.f64 n (/.f64 Om (*.f64 l U))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 -2 l)) (/.f64 n (/.f64 Om (*.f64 l U))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (-.f64 (*.f64 -2 l) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 n (*.f64 l U)) Om)))): 5 points increase in error, 11 points decrease in error
      (*.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -2 l) (neg.f64 (/.f64 (*.f64 n (*.f64 l U)) Om))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (+.f64 (*.f64 -2 l) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/r/_binary64 (/.f64 n (/.f64 (/.f64 Om (*.f64 l U)) (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))))): 26 points increase in error, 32 points decrease in error
      (/.f64 n (Rewrite<= associate-/r*_binary64 (/.f64 Om (*.f64 (*.f64 l U) (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l)))))): 27 points increase in error, 25 points decrease in error
      (/.f64 n (/.f64 Om (Rewrite<= associate-*r*_binary64 (*.f64 l (*.f64 U (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))))))): 9 points increase in error, 1 points decrease in error
      (/.f64 n (/.f64 Om (*.f64 l (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l)) U))))): 0 points increase in error, 0 points decrease in error
      (/.f64 n (/.f64 Om (*.f64 l (Rewrite=> *-commutative_binary64 (*.f64 U (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 n (*.f64 l (*.f64 U (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 l U)) Om)) (*.f64 -2 l))))) Om)): 34 points increase in error, 23 points decrease in error

   if 2.7e160 < n

   1. Initial program 38.9

      \[\sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) - \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right) \cdot \left(U - U*\right)\right)} \]

   2. Simplified 35.5

      \[\leadsto \color{blue}{\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \frac{\ell \cdot \left(U* - U\right)}{Om}\right)\right)}} \]
      Proof
      (sqrt.f64 (*.f64 (*.f64 2 (*.f64 n U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 n) U)) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l -2 (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (Rewrite<= metadata-eval (neg.f64 2)) (*.f64 n (/.f64 (*.f64 l (-.f64 U* U)) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite=> sub-neg_binary64 (+.f64 U* (neg.f64 U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 U*))) (neg.f64 U))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 U*) U)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 U (neg.f64 U*))))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (/.f64 (*.f64 l (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 U U*)))) Om))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 l Om) (neg.f64 (-.f64 U U*)))))))))): 2 points increase in error, 14 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (*.f64 n (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 n (*.f64 (/.f64 l Om) (-.f64 U U*)))))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (fma.f64 l (neg.f64 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 l (neg.f64 2)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (*.f64 (/.f64 l Om) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 2) l)) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 l Om) (*.f64 (neg.f64 2) l)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n))))))): 2 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (*.f64 (neg.f64 2) l)) Om)) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 20 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (neg.f64 2) l) l)) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 2) (*.f64 l l))) Om) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 2) (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (/.f64 l Om) (*.f64 (*.f64 (/.f64 l Om) (-.f64 U U*)) n)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (*.f64 (/.f64 l Om) (-.f64 U U*))) n)))))): 8 points increase in error, 6 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l Om) (/.f64 l Om)) (-.f64 U U*))) n))))): 6 points increase in error, 2 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)) n))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (+.f64 t (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 2 points increase in error, 8 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (neg.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 0 points increase in error, 0 points decrease in error
      (sqrt.f64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om)))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in U around 0 42.3

      \[\leadsto \sqrt{\color{blue}{2 \cdot \left(n \cdot \left(\left(t + \frac{\ell \cdot \left(-2 \cdot \ell + \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)}{Om}\right) \cdot U\right)\right)}} \]

   4. Applied egg-rr 37.0

      \[\leadsto \color{blue}{\sqrt{2 \cdot n} \cdot \sqrt{\left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell \cdot \left(U* \cdot n\right)}{Om}\right)\right) \cdot U}} \]

   5. Applied egg-rr 23.5

      \[\leadsto \sqrt{2 \cdot n} \cdot \sqrt{\left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \color{blue}{\frac{\ell \cdot U*}{{\left(\sqrt[3]{Om}\right)}^{2}} \cdot \frac{n}{\sqrt[3]{Om}}}\right)\right) \cdot U} \]
3. Recombined 9 regimes into one program.

4. Final simplification 29.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(n \cdot \left(U \cdot 2\right), t, \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(\left(n \cdot \left(U \cdot 2\right)\right) \cdot \frac{\ell}{Om}\right)\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t \cdot \left(n \cdot U\right), \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 2.7 \cdot 10^{-256}:\\ \;\;\;\;\sqrt{n \cdot 2} \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{elif}\;n \leq 1.2 \cdot 10^{-195}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \mathbf{elif}\;n \leq 1.5 \cdot 10^{-85}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 3.1 \cdot 10^{-27}:\\ \;\;\;\;\sqrt{n \cdot 2} \cdot \left(\sqrt{\mathsf{fma}\left(\frac{\ell}{Om}, \mathsf{fma}\left(\ell, -2, \frac{\ell}{\frac{Om}{n \cdot U*}}\right), t\right)} \cdot \sqrt{U}\right)\\ \mathbf{elif}\;n \leq 1.4 \cdot 10^{+133}:\\ \;\;\;\;\sqrt{n \cdot 2} \cdot \sqrt{U \cdot \left(t - \mathsf{fma}\left(2, \ell \cdot \frac{\ell}{Om}, n \cdot \left({\left(\frac{\ell}{Om}\right)}^{2} \cdot \left(U - U*\right)\right)\right)\right)}\\ \mathbf{elif}\;n \leq 2.7 \cdot 10^{+160}:\\ \;\;\;\;\sqrt{2 \cdot \left(\frac{n}{\frac{Om}{U \cdot \ell}} \cdot \left(\ell \cdot -2 - \frac{n}{\frac{Om}{U \cdot \ell}}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{n \cdot 2} \cdot \sqrt{U \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell \cdot U*}{{\left(\sqrt[3]{Om}\right)}^{2}} \cdot \frac{n}{\sqrt[3]{Om}}\right)\right)}\\ \end{array} \]

Alternatives

Alternative 1
Error	28.5
Cost	34008

\[\begin{array}{l} t_1 := n \cdot \left(U \cdot 2\right)\\ t_2 := \sqrt{n \cdot 2}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(t_1, t, \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(t_1 \cdot \frac{\ell}{Om}\right)\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t \cdot \left(n \cdot U\right), \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 2.7 \cdot 10^{-256}:\\ \;\;\;\;t_2 \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{elif}\;n \leq 1.2 \cdot 10^{-195}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \mathbf{elif}\;n \leq 1.5 \cdot 10^{-85}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 3.1 \cdot 10^{-27}:\\ \;\;\;\;t_2 \cdot \left(\sqrt{\mathsf{fma}\left(\frac{\ell}{Om}, \mathsf{fma}\left(\ell, -2, \frac{\ell}{\frac{Om}{n \cdot U*}}\right), t\right)} \cdot \sqrt{U}\right)\\ \mathbf{else}:\\ \;\;\;\;t_2 \cdot \sqrt{U \cdot \left(t - \mathsf{fma}\left(2, \ell \cdot \frac{\ell}{Om}, n \cdot \left({\left(\frac{\ell}{Om}\right)}^{2} \cdot \left(U - U*\right)\right)\right)\right)}\\ \end{array} \]

Alternative 2
Error	28.5
Cost	28060

\[\begin{array}{l} t_1 := \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right)\\ t_2 := n \cdot \left(U \cdot 2\right)\\ t_3 := \sqrt{n \cdot 2}\\ t_4 := t_1 \cdot \left(t_2 \cdot \frac{\ell}{Om}\right)\\ t_5 := t \cdot \left(n \cdot U\right)\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(t_2, t, t_4\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t_5, \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 1.3 \cdot 10^{-259}:\\ \;\;\;\;t_3 \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{elif}\;n \leq 9.6 \cdot 10^{-58}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 3.1 \cdot 10^{-27}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(\frac{\ell}{Om}, t_1, t\right)} \cdot \sqrt{t_2}\\ \mathbf{elif}\;n \leq 1.05 \cdot 10^{+154}:\\ \;\;\;\;\sqrt{t_4 + 2 \cdot t_5}\\ \mathbf{elif}\;n \leq 1.8 \cdot 10^{+169}:\\ \;\;\;\;\left(\left(n \cdot \ell\right) \cdot \frac{\sqrt{2}}{Om}\right) \cdot \left(\sqrt{U} \cdot \sqrt{U* - U}\right)\\ \mathbf{else}:\\ \;\;\;\;t_3 \cdot \sqrt{U \cdot \left(t - \mathsf{fma}\left(2, \ell \cdot \frac{\ell}{Om}, n \cdot \left({\left(\frac{\ell}{Om}\right)}^{2} \cdot \left(U - U*\right)\right)\right)\right)}\\ \end{array} \]

Alternative 3
Error	29.1
Cost	27604

\[\begin{array}{l} t_1 := \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right)\\ t_2 := \sqrt{n \cdot 2}\\ t_3 := t \cdot \left(n \cdot U\right)\\ t_4 := n \cdot \left(U \cdot 2\right)\\ t_5 := t_1 \cdot \left(t_4 \cdot \frac{\ell}{Om}\right)\\ t_6 := t_2 \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(t_4, t, t_5\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t_3, \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 1.3 \cdot 10^{-259}:\\ \;\;\;\;t_6\\ \mathbf{elif}\;n \leq 9.6 \cdot 10^{-58}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 3.1 \cdot 10^{-27}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(\frac{\ell}{Om}, t_1, t\right)} \cdot \sqrt{t_4}\\ \mathbf{elif}\;n \leq 1.05 \cdot 10^{+154}:\\ \;\;\;\;\sqrt{t_5 + 2 \cdot t_3}\\ \mathbf{elif}\;n \leq 1.2 \cdot 10^{+223}:\\ \;\;\;\;t_2 \cdot \sqrt{U \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell}{Om} \cdot \left(n \cdot U*\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_6\\ \end{array} \]

Alternative 4
Error	29.2
Cost	27476

\[\begin{array}{l} t_1 := \sqrt{n \cdot 2}\\ t_2 := t \cdot \left(n \cdot U\right)\\ t_3 := n \cdot \left(U \cdot 2\right)\\ t_4 := \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(t_3 \cdot \frac{\ell}{Om}\right)\\ t_5 := t_1 \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(t_3, t, t_4\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t_2, \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 1.3 \cdot 10^{-259}:\\ \;\;\;\;t_5\\ \mathbf{elif}\;n \leq 9.6 \cdot 10^{-58}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 3.1 \cdot 10^{-27}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(\frac{\ell}{Om}, \mathsf{fma}\left(n, \frac{\ell \cdot U*}{Om}, \ell \cdot -2\right), t\right)} \cdot \sqrt{2 \cdot \left(n \cdot U\right)}\\ \mathbf{elif}\;n \leq 1.05 \cdot 10^{+154}:\\ \;\;\;\;\sqrt{t_4 + 2 \cdot t_2}\\ \mathbf{elif}\;n \leq 1.2 \cdot 10^{+223}:\\ \;\;\;\;t_1 \cdot \sqrt{U \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell}{Om} \cdot \left(n \cdot U*\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_5\\ \end{array} \]

Alternative 5
Error	29.3
Cost	21468

\[\begin{array}{l} t_1 := t \cdot \left(n \cdot U\right)\\ t_2 := \sqrt{\mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(\left(n \cdot \left(U \cdot 2\right)\right) \cdot \frac{\ell}{Om}\right) + 2 \cdot t_1}\\ t_3 := \sqrt{n \cdot 2}\\ t_4 := t_3 \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t_1, \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 1.3 \cdot 10^{-259}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;n \leq 4.5 \cdot 10^{-58}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 1.15 \cdot 10^{-26}:\\ \;\;\;\;\sqrt{2} \cdot \left(\sqrt{U} \cdot \sqrt{n \cdot t}\right)\\ \mathbf{elif}\;n \leq 1.05 \cdot 10^{+154}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;n \leq 1.2 \cdot 10^{+223}:\\ \;\;\;\;t_3 \cdot \sqrt{U \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell}{Om} \cdot \left(n \cdot U*\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_4\\ \end{array} \]

Alternative 6
Error	29.3
Cost	21468

\[\begin{array}{l} t_1 := \sqrt{n \cdot 2}\\ t_2 := t \cdot \left(n \cdot U\right)\\ t_3 := n \cdot \left(U \cdot 2\right)\\ t_4 := \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(t_3 \cdot \frac{\ell}{Om}\right)\\ t_5 := t_1 \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(t_3, t, t_4\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t_2, \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 1.3 \cdot 10^{-259}:\\ \;\;\;\;t_5\\ \mathbf{elif}\;n \leq 4.5 \cdot 10^{-58}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 1.15 \cdot 10^{-26}:\\ \;\;\;\;\sqrt{2} \cdot \left(\sqrt{U} \cdot \sqrt{n \cdot t}\right)\\ \mathbf{elif}\;n \leq 1.05 \cdot 10^{+154}:\\ \;\;\;\;\sqrt{t_4 + 2 \cdot t_2}\\ \mathbf{elif}\;n \leq 1.2 \cdot 10^{+223}:\\ \;\;\;\;t_1 \cdot \sqrt{U \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, \frac{\ell}{Om} \cdot \left(n \cdot U*\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_5\\ \end{array} \]

Alternative 7
Error	31.8
Cost	21088

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ t_2 := \sqrt{\mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(\left(n \cdot \left(U \cdot 2\right)\right) \cdot \frac{\ell}{Om}\right) + 2 \cdot \left(t \cdot \left(n \cdot U\right)\right)}\\ \mathbf{if}\;U* \leq -1.3 \cdot 10^{+54}:\\ \;\;\;\;\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot U*\right)\right)\right)}\\ \mathbf{elif}\;U* \leq -3.9 \cdot 10^{-218}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \mathbf{elif}\;U* \leq 10^{-293}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;U* \leq 10^{-140}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;U* \leq 10^{-12}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;U* \leq 2.5 \cdot 10^{+120}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;U* \leq 10^{+225}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;U* \leq 10^{+280}:\\ \;\;\;\;\left(\left(n \cdot \ell\right) \cdot \frac{\sqrt{2}}{Om}\right) \cdot \left(\sqrt{U} \cdot \sqrt{U* - U}\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) + \left(U* - U\right) \cdot \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right)\right)}\\ \end{array} \]

Alternative 8
Error	32.9
Cost	15580

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ t_2 := \sqrt{\mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot \left(U* - U\right)\right)\right) \cdot \left(\left(n \cdot \left(U \cdot 2\right)\right) \cdot \frac{\ell}{Om}\right) + 2 \cdot \left(t \cdot \left(n \cdot U\right)\right)}\\ \mathbf{if}\;U* \leq -1.3 \cdot 10^{+54}:\\ \;\;\;\;\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot U*\right)\right)\right)}\\ \mathbf{elif}\;U* \leq -3.9 \cdot 10^{-218}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \mathbf{elif}\;U* \leq 10^{-293}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;U* \leq 10^{-140}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;U* \leq 10^{-12}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;U* \leq 2.5 \cdot 10^{+120}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;U* \leq 10^{+174}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;U* \leq 10^{+280}:\\ \;\;\;\;\frac{\left(n \cdot \ell\right) \cdot \sqrt{2}}{Om} \cdot \sqrt{U \cdot U*}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(\left(t - 2 \cdot \frac{\ell \cdot \ell}{Om}\right) + \left(U* - U\right) \cdot \left(n \cdot {\left(\frac{\ell}{Om}\right)}^{2}\right)\right)}\\ \end{array} \]

Alternative 9
Error	29.7
Cost	15188

\[\begin{array}{l} t_1 := t \cdot \left(n \cdot U\right)\\ t_2 := \sqrt{n \cdot 2} \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot U*\right)\right)\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t_1, \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 1.3 \cdot 10^{-259}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;n \leq 1.35 \cdot 10^{+29}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{elif}\;n \leq 1.9 \cdot 10^{+151}:\\ \;\;\;\;\sqrt{2 \cdot t_1 + \left(\left(n \cdot \left(U \cdot 2\right)\right) \cdot \frac{\ell}{Om}\right) \cdot \mathsf{fma}\left(\ell, -2, \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)}\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 10
Error	30.1
Cost	14800

\[\begin{array}{l} t_1 := \sqrt{n \cdot 2} \cdot \sqrt{U \cdot t + \left(\ell \cdot \ell\right) \cdot \left(\frac{U}{Om} \cdot \left(-2 + n \cdot \frac{U*}{Om}\right)\right)}\\ \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot U*\right)\right)\right)}\\ \mathbf{elif}\;n \leq 1.55 \cdot 10^{-291}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t \cdot \left(n \cdot U\right), \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 1.3 \cdot 10^{-259}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;n \leq 1.85 \cdot 10^{+151}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 11
Error	32.0
Cost	14556

\[\begin{array}{l} t_1 := \frac{\left(n \cdot \ell\right) \cdot \sqrt{2}}{Om}\\ t_2 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ t_3 := \sqrt{U \cdot U*}\\ \mathbf{if}\;Om \leq -1 \cdot 10^{-55}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;Om \leq -5.2 \cdot 10^{-244}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;Om \leq -1.5 \cdot 10^{-276}:\\ \;\;\;\;t_1 \cdot \left(-\sqrt{U \cdot \left(U* - U\right)}\right)\\ \mathbf{elif}\;Om \leq 3.7 \cdot 10^{-292}:\\ \;\;\;\;t_3 \cdot \frac{n \cdot \sqrt{2}}{\frac{Om}{\ell}}\\ \mathbf{elif}\;Om \leq 1.75 \cdot 10^{-264}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{\ell \cdot \left(\ell \cdot -2 + n \cdot \frac{1}{\frac{Om}{\ell \cdot U*}}\right)}{Om}\right)\right)\right)}\\ \mathbf{elif}\;Om \leq 2.9 \cdot 10^{-246}:\\ \;\;\;\;t_1 \cdot t_3\\ \mathbf{elif}\;Om \leq 6.2 \cdot 10^{+92}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \end{array} \]

Alternative 12
Error	32.0
Cost	14556

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ t_2 := \sqrt{U \cdot U*}\\ \mathbf{if}\;Om \leq -1 \cdot 10^{-55}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;Om \leq -5.2 \cdot 10^{-244}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;Om \leq -1.5 \cdot 10^{-276}:\\ \;\;\;\;\left(\left(n \cdot \ell\right) \cdot \frac{\sqrt{2}}{Om}\right) \cdot \left(-\sqrt{U \cdot \left(U* - U\right)}\right)\\ \mathbf{elif}\;Om \leq 3.7 \cdot 10^{-292}:\\ \;\;\;\;t_2 \cdot \frac{n \cdot \sqrt{2}}{\frac{Om}{\ell}}\\ \mathbf{elif}\;Om \leq 1.75 \cdot 10^{-264}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{\ell \cdot \left(\ell \cdot -2 + n \cdot \frac{1}{\frac{Om}{\ell \cdot U*}}\right)}{Om}\right)\right)\right)}\\ \mathbf{elif}\;Om \leq 2.9 \cdot 10^{-246}:\\ \;\;\;\;\frac{\left(n \cdot \ell\right) \cdot \sqrt{2}}{Om} \cdot t_2\\ \mathbf{elif}\;Om \leq 6.2 \cdot 10^{+92}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \end{array} \]

Alternative 13
Error	32.1
Cost	14556

\[\begin{array}{l} t_1 := -\sqrt{U \cdot \left(U* - U\right)}\\ t_2 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{if}\;Om \leq -1 \cdot 10^{-55}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;Om \leq -5.2 \cdot 10^{-244}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;Om \leq -1.5 \cdot 10^{-276}:\\ \;\;\;\;\left(\left(n \cdot \ell\right) \cdot \frac{\sqrt{2}}{Om}\right) \cdot t_1\\ \mathbf{elif}\;Om \leq 3.7 \cdot 10^{-292}:\\ \;\;\;\;\sqrt{U \cdot U*} \cdot \frac{n \cdot \sqrt{2}}{\frac{Om}{\ell}}\\ \mathbf{elif}\;Om \leq 1.5 \cdot 10^{-245}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{\ell \cdot \left(\ell \cdot -2 + n \cdot \frac{1}{\frac{Om}{\ell \cdot U*}}\right)}{Om}\right)\right)\right)}\\ \mathbf{elif}\;Om \leq 4.4 \cdot 10^{-228}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t_1}{\frac{\frac{Om}{\ell}}{n}}\\ \mathbf{elif}\;Om \leq 6.2 \cdot 10^{+92}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \end{array} \]

Alternative 14
Error	30.2
Cost	14276

\[\begin{array}{l} \mathbf{if}\;n \leq -8 \cdot 10^{-145}:\\ \;\;\;\;\sqrt{\left(2 \cdot \left(n \cdot U\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, -2, n \cdot \left(\frac{\ell}{Om} \cdot U*\right)\right)\right)}\\ \mathbf{elif}\;n \leq 8.3 \cdot 10^{-193}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(2, t \cdot \left(n \cdot U\right), \frac{-4}{\frac{Om}{U \cdot \left(\ell \cdot \left(n \cdot \ell\right)\right)}}\right)}\\ \mathbf{elif}\;n \leq 8.2 \cdot 10^{+143}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{n \cdot 2} \cdot \sqrt{U \cdot t}\\ \end{array} \]

Alternative 15
Error	31.9
Cost	14160

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{if}\;Om \leq -1 \cdot 10^{-55}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;Om \leq -1.65 \cdot 10^{-268}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;Om \leq 2.9 \cdot 10^{-246}:\\ \;\;\;\;\frac{\left(n \cdot \ell\right) \cdot \sqrt{2}}{Om} \cdot \sqrt{U \cdot U*}\\ \mathbf{elif}\;Om \leq 6.2 \cdot 10^{+92}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \end{array} \]

Alternative 16
Error	31.9
Cost	14160

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{if}\;Om \leq -1 \cdot 10^{-55}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;Om \leq -6.2 \cdot 10^{-271}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;Om \leq 2.9 \cdot 10^{-246}:\\ \;\;\;\;\frac{\left(n \cdot \ell\right) \cdot \sqrt{2}}{Om} \cdot \sqrt{U \cdot \left(U* - U\right)}\\ \mathbf{elif}\;Om \leq 6.2 \cdot 10^{+92}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot \mathsf{fma}\left(-2, \frac{\ell}{\frac{Om}{\ell}}, t\right)\right)\right)}\\ \end{array} \]

Alternative 17
Error	32.0
Cost	14040

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{if}\;U \leq -1 \cdot 10^{+79}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;U \leq -2 \cdot 10^{-158}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;U \leq 3.55 \cdot 10^{-264}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ \mathbf{elif}\;U \leq 1.38 \cdot 10^{-244}:\\ \;\;\;\;\sqrt{2 \cdot \left(\frac{n}{Om} \cdot \left(\left(\ell \cdot \left(U \cdot \ell\right)\right) \cdot \left(-2 + U* \cdot \frac{n}{Om}\right)\right)\right)}\\ \mathbf{elif}\;U \leq 2.35 \cdot 10^{-60}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{\ell \cdot \left(\ell \cdot -2 + n \cdot \frac{1}{\frac{Om}{\ell \cdot U*}}\right)}{Om}\right)\right)\right)}\\ \mathbf{elif}\;U \leq 2 \cdot 10^{+57}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sqrt{U} \cdot \sqrt{n \cdot \left(2 \cdot t\right)}\\ \end{array} \]

Alternative 18
Error	32.2
Cost	9176

\[\begin{array}{l} t_1 := \sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ t_2 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot t\right)\right) + -2 \cdot \frac{\left(n \cdot \left(U \cdot \ell\right)\right) \cdot \left(2 \cdot \ell - \frac{n \cdot \left(\ell \cdot \left(U* - U\right)\right)}{Om}\right)}{Om}}\\ \mathbf{if}\;U \leq -1 \cdot 10^{+79}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;U \leq -2 \cdot 10^{-158}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;U \leq 3.55 \cdot 10^{-264}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ \mathbf{elif}\;U \leq 1.38 \cdot 10^{-244}:\\ \;\;\;\;\sqrt{2 \cdot \left(\frac{n}{Om} \cdot \left(\left(\ell \cdot \left(U \cdot \ell\right)\right) \cdot \left(-2 + U* \cdot \frac{n}{Om}\right)\right)\right)}\\ \mathbf{elif}\;U \leq 2.35 \cdot 10^{-60}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{\ell \cdot \left(\ell \cdot -2 + n \cdot \frac{1}{\frac{Om}{\ell \cdot U*}}\right)}{Om}\right)\right)\right)}\\ \mathbf{elif}\;U \leq 10^{+58}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 19
Error	36.6
Cost	8928

\[\begin{array}{l} t_1 := -2 + U* \cdot \frac{n}{Om}\\ t_2 := \sqrt{2 \cdot \left(\frac{n}{Om} \cdot \left(\left(\ell \cdot \left(U \cdot \ell\right)\right) \cdot t_1\right)\right)}\\ t_3 := \sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ t_4 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ t_5 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{\ell \cdot \left(\ell \cdot -2 + \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)}{Om}\right)\right)\right)}\\ \mathbf{if}\;t \leq -180000000000:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t \leq -7 \cdot 10^{-117}:\\ \;\;\;\;t_5\\ \mathbf{elif}\;t \leq -6.9 \cdot 10^{-133}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t \leq -5.6 \cdot 10^{-241}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t \leq 1.3 \cdot 10^{-238}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;t \leq 1.55 \cdot 10^{-179}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t \leq 2.85 \cdot 10^{-30}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \left(\ell \cdot \ell\right) \cdot \frac{t_1}{Om}\right)\right)\right)}\\ \mathbf{elif}\;t \leq 2.6 \cdot 10^{+22}:\\ \;\;\;\;t_5\\ \mathbf{else}:\\ \;\;\;\;t_4\\ \end{array} \]

Alternative 20
Error	36.3
Cost	8672

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(\frac{n}{Om} \cdot \left(\left(\ell \cdot \left(U \cdot \ell\right)\right) \cdot \left(-2 + U* \cdot \frac{n}{Om}\right)\right)\right)}\\ t_2 := \sqrt{2 \cdot \left(\left(n \cdot U\right) \cdot \left(t + \frac{-2}{\frac{Om}{\ell \cdot \ell}}\right)\right)}\\ t_3 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ t_4 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{n}{Om} \cdot \frac{\ell \cdot \left(\ell \cdot U*\right)}{Om}\right)\right)\right)}\\ \mathbf{if}\;\ell \leq -1.7 \cdot 10^{+65}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;\ell \leq -1.25 \cdot 10^{+23}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\ell \leq -1.22 \cdot 10^{-172}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot t\right)\right)}\\ \mathbf{elif}\;\ell \leq 8.2 \cdot 10^{-143}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;\ell \leq 1.7 \cdot 10^{-13}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;\ell \leq 4.2 \cdot 10^{+69}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;\ell \leq 3.3 \cdot 10^{+94}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;\ell \leq 2.55 \cdot 10^{+141}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]

Alternative 21
Error	34.5
Cost	8668

\[\begin{array}{l} t_1 := -2 + U* \cdot \frac{n}{Om}\\ t_2 := \frac{n}{\frac{Om}{U \cdot \ell}}\\ t_3 := \sqrt{2 \cdot \left(t_2 \cdot \left(\ell \cdot -2 - t_2\right)\right)}\\ t_4 := \sqrt{2 \cdot \left(\left(n \cdot U\right) \cdot \left(t + \frac{-2}{\frac{Om}{\ell \cdot \ell}}\right)\right)}\\ \mathbf{if}\;\ell \leq -6.3 \cdot 10^{+178}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;\ell \leq -1.25 \cdot 10^{+23}:\\ \;\;\;\;\sqrt{2 \cdot \left(\frac{n}{Om} \cdot \left(\left(\ell \cdot \left(U \cdot \ell\right)\right) \cdot t_1\right)\right)}\\ \mathbf{elif}\;\ell \leq -1.22 \cdot 10^{-172}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot t\right)\right)}\\ \mathbf{elif}\;\ell \leq 8.2 \cdot 10^{-143}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;\ell \leq 1.7 \cdot 10^{-13}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{n}{Om} \cdot \frac{\ell \cdot \left(\ell \cdot U*\right)}{Om}\right)\right)\right)}\\ \mathbf{elif}\;\ell \leq 3.3 \cdot 10^{+94}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;\ell \leq 3.2 \cdot 10^{+148}:\\ \;\;\;\;\sqrt{2 \cdot \frac{\left(n \cdot \left(U \cdot \left(\ell \cdot \ell\right)\right)\right) \cdot t_1}{Om}}\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]

Alternative 22
Error	33.9
Cost	8396

\[\begin{array}{l} \mathbf{if}\;Om \leq -1.3 \cdot 10^{-90}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;Om \leq 3 \cdot 10^{-218}:\\ \;\;\;\;\sqrt{2 \cdot \frac{n \cdot \left(\ell \cdot \left(U \cdot \left(\ell \cdot -2 + \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)\right)\right)}{Om}}\\ \mathbf{elif}\;Om \leq 10^{+75}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{\ell \cdot \left(\ell \cdot -2 + n \cdot \frac{1}{\frac{Om}{\ell \cdot U*}}\right)}{Om}\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ \end{array} \]

Alternative 23
Error	34.5
Cost	8276

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(\left(n \cdot U\right) \cdot \left(t + \frac{-2}{\frac{Om}{\ell \cdot \ell}}\right)\right)}\\ t_2 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{n}{Om} \cdot \frac{\ell \cdot \left(\ell \cdot U*\right)}{Om}\right)\right)\right)}\\ t_3 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ \mathbf{if}\;\ell \leq -1.7 \cdot 10^{+65}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;\ell \leq -2.7 \cdot 10^{+46}:\\ \;\;\;\;\sqrt{2 \cdot \frac{\left(n \cdot \left(U \cdot \left(\ell \cdot \ell\right)\right)\right) \cdot \left(-2 + U* \cdot \frac{n}{Om}\right)}{Om}}\\ \mathbf{elif}\;\ell \leq -1.3 \cdot 10^{-192}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;\ell \leq 8.2 \cdot 10^{-143}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\ell \leq 1.7 \cdot 10^{-13}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;\ell \leq 5.2 \cdot 10^{+34}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]

Alternative 24
Error	31.9
Cost	8272

\[\begin{array}{l} t_1 := \frac{n}{\frac{Om}{U \cdot \ell}}\\ t_2 := \sqrt{2 \cdot \left(t_1 \cdot \left(\ell \cdot -2 - t_1\right)\right)}\\ t_3 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \left(\ell \cdot \ell\right) \cdot \frac{-2 + U* \cdot \frac{n}{Om}}{Om}\right)\right)\right)}\\ \mathbf{if}\;\ell \leq -5 \cdot 10^{+157}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;\ell \leq -1.55 \cdot 10^{-177}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;\ell \leq 1.2 \cdot 10^{-151}:\\ \;\;\;\;\sqrt{t \cdot \left(2 \cdot \left(n \cdot U\right)\right)}\\ \mathbf{elif}\;\ell \leq 3.2 \cdot 10^{+148}:\\ \;\;\;\;t_3\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 25
Error	34.8
Cost	8272

\[\begin{array}{l} \mathbf{if}\;Om \leq -1.3 \cdot 10^{-90}:\\ \;\;\;\;\sqrt{\left(U \cdot \left(n \cdot 2\right)\right) \cdot \left(t + \frac{\ell}{Om} \cdot \left(\ell \cdot -2 - U \cdot \frac{n}{\frac{Om}{\ell}}\right)\right)}\\ \mathbf{elif}\;Om \leq 3 \cdot 10^{-218}:\\ \;\;\;\;\sqrt{2 \cdot \frac{n \cdot \left(\ell \cdot \left(U \cdot \left(\ell \cdot -2 + \frac{n \cdot \left(\ell \cdot U*\right)}{Om}\right)\right)\right)}{Om}}\\ \mathbf{elif}\;Om \leq 4.9 \cdot 10^{-34}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \frac{n}{Om} \cdot \frac{\ell \cdot \left(\ell \cdot U*\right)}{Om}\right)\right)\right)}\\ \mathbf{elif}\;Om \leq 5.4 \cdot 10^{+73}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + \left(\ell \cdot \ell\right) \cdot \frac{-2 + U* \cdot \frac{n}{Om}}{Om}\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ \end{array} \]

Alternative 26
Error	36.0
Cost	7888

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ \mathbf{if}\;\ell \leq -1.7 \cdot 10^{+65}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\ell \leq -3 \cdot 10^{+41}:\\ \;\;\;\;\sqrt{2 \cdot \frac{\left(n \cdot \left(U \cdot \left(\ell \cdot \ell\right)\right)\right) \cdot \left(-2 + U* \cdot \frac{n}{Om}\right)}{Om}}\\ \mathbf{elif}\;\ell \leq -1.22 \cdot 10^{-172}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot t\right)\right)}\\ \mathbf{elif}\;\ell \leq 5.2 \cdot 10^{+34}:\\ \;\;\;\;\sqrt{2 \cdot \left(\left(n \cdot U\right) \cdot \left(t + \frac{-2}{\frac{Om}{\ell \cdot \ell}}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 27
Error	38.6
Cost	7496

\[\begin{array}{l} t_1 := \sqrt{2 \cdot \left(\frac{-2}{Om} \cdot \left(n \cdot \left(\ell \cdot \left(U \cdot \ell\right)\right)\right)\right)}\\ \mathbf{if}\;\ell \leq -7.9 \cdot 10^{+99}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\ell \leq 3.3 \cdot 10^{+94}:\\ \;\;\;\;\sqrt{t \cdot \left(2 \cdot \left(n \cdot U\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 28
Error	35.4
Cost	7492

\[\begin{array}{l} \mathbf{if}\;t \leq -1 \cdot 10^{+220}:\\ \;\;\;\;\sqrt{2 \cdot \left(U \cdot \left(n \cdot t\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{2 \cdot \left(n \cdot \left(U \cdot \left(t + -2 \cdot \frac{\ell}{\frac{Om}{\ell}}\right)\right)\right)}\\ \end{array} \]

Alternative 29
Error	40.8
Cost	6980

\[\begin{array}{l} \mathbf{if}\;n \leq 4.1 \cdot 10^{-306}:\\ \;\;\;\;\sqrt{t \cdot \left(2 \cdot \left(n \cdot U\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(n \cdot 2\right) \cdot \left(U \cdot t\right)}\\ \end{array} \]

Alternative 30
Error	40.7
Cost	6848

\[\sqrt{t \cdot \left(2 \cdot \left(n \cdot U\right)\right)} \]

Reproduce

herbie shell --seed 2022298 
(FPCore (n U t l Om U*)
  :name "Toniolo and Linder, Equation (13)"
  :precision binary64
  (sqrt (* (* (* 2.0 n) U) (- (- t (* 2.0 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2.0)) (- U U*))))))