Toniolo and Linder, Equation (13)

Percentage Accurate: 49.9% → 64.1%

Time: 21.4s

Alternatives: 8

Speedup: 2.5×

Specification

Math

\[\begin{array}{l} \\ \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)} \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*))))))

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

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(n, u, t, l, om, u_42)
use fmin_fmax_functions
    real(8), intent (in) :: n
    real(8), intent (in) :: u
    real(8), intent (in) :: t
    real(8), intent (in) :: l
    real(8), intent (in) :: om
    real(8), intent (in) :: u_42
    code = sqrt((((2.0d0 * n) * u) * ((t - (2.0d0 * ((l * l) / om))) - ((n * ((l / om) ** 2.0d0)) * (u - u_42)))))
end function

Java

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

Python

def code(n, U, t, l, Om, U_42_):
	return math.sqrt((((2.0 * n) * U) * ((t - (2.0 * ((l * l) / Om))) - ((n * math.pow((l / Om), 2.0)) * (U - U_42_)))))

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

MATLAB

function tmp = code(n, U, t, l, Om, U_42_)
	tmp = sqrt((((2.0 * n) * U) * ((t - (2.0 * ((l * l) / Om))) - ((n * ((l / Om) ^ 2.0)) * (U - U_42_)))));
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]

Initial Program: 49.9% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \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)} \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*))))))

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

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(n, u, t, l, om, u_42)
use fmin_fmax_functions
    real(8), intent (in) :: n
    real(8), intent (in) :: u
    real(8), intent (in) :: t
    real(8), intent (in) :: l
    real(8), intent (in) :: om
    real(8), intent (in) :: u_42
    code = sqrt((((2.0d0 * n) * u) * ((t - (2.0d0 * ((l * l) / om))) - ((n * ((l / om) ** 2.0d0)) * (u - u_42)))))
end function

Java

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

Python

def code(n, U, t, l, Om, U_42_):
	return math.sqrt((((2.0 * n) * U) * ((t - (2.0 * ((l * l) / Om))) - ((n * math.pow((l / Om), 2.0)) * (U - U_42_)))))

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

MATLAB

function tmp = code(n, U, t, l, Om, U_42_)
	tmp = sqrt((((2.0 * n) * U) * ((t - (2.0 * ((l * l) / Om))) - ((n * ((l / Om) ^ 2.0)) * (U - U_42_)))));
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]

Alternative 1: 64.1% accurate, 0.3× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{\ell \cdot \ell}{Om}\\ t_2 := {\left(\frac{\ell}{Om}\right)}^{2}\\ t_3 := \sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot \left(\left(t - 2 \cdot t\_1\right) - \left(n \cdot t\_2\right) \cdot \left(U - U*\right)\right)}\\ t_4 := U \cdot \left(n \cdot 2\right)\\ \mathbf{if}\;t\_3 \leq 0:\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \left(\mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right) \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \mathbf{elif}\;t\_3 \leq 2 \cdot 10^{+151}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(t - t\_1 \cdot 2, t\_4, \left(\left(\left(-n\right) \cdot t\_2\right) \cdot \left(U - U*\right)\right) \cdot t\_4\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \mathsf{fma}\left(U - U*, \frac{n}{Om} \cdot \ell, 2 \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \end{array} \end{array} \]

FPCore

(FPCore (n U t l Om U*)
 :precision binary64
 (let* ((t_1 (/ (* l l) Om))
        (t_2 (pow (/ l Om) 2.0))
        (t_3
         (sqrt
          (* (* (* 2.0 n) U) (- (- t (* 2.0 t_1)) (* (* n t_2) (- U U*))))))
        (t_4 (* U (* n 2.0))))
   (if (<= t_3 0.0)
     (sqrt
      (* (* (- t (* (/ l Om) (* (fma (/ n Om) (- U U*) 2.0) l))) U) (* n 2.0)))
     (if (<= t_3 2e+151)
       (sqrt (fma (- t (* t_1 2.0)) t_4 (* (* (* (- n) t_2) (- U U*)) t_4)))
       (sqrt
        (*
         (* (- t (* (/ l Om) (fma (- U U*) (* (/ n Om) l) (* 2.0 l)))) U)
         (* n 2.0)))))))

C

double code(double n, double U, double t, double l, double Om, double U_42_) {
	double t_1 = (l * l) / Om;
	double t_2 = pow((l / Om), 2.0);
	double t_3 = sqrt((((2.0 * n) * U) * ((t - (2.0 * t_1)) - ((n * t_2) * (U - U_42_)))));
	double t_4 = U * (n * 2.0);
	double tmp;
	if (t_3 <= 0.0) {
		tmp = sqrt((((t - ((l / Om) * (fma((n / Om), (U - U_42_), 2.0) * l))) * U) * (n * 2.0)));
	} else if (t_3 <= 2e+151) {
		tmp = sqrt(fma((t - (t_1 * 2.0)), t_4, (((-n * t_2) * (U - U_42_)) * t_4)));
	} else {
		tmp = sqrt((((t - ((l / Om) * fma((U - U_42_), ((n / Om) * l), (2.0 * l)))) * U) * (n * 2.0)));
	}
	return tmp;
}

Julia

function code(n, U, t, l, Om, U_42_)
	t_1 = Float64(Float64(l * l) / Om)
	t_2 = Float64(l / Om) ^ 2.0
	t_3 = sqrt(Float64(Float64(Float64(2.0 * n) * U) * Float64(Float64(t - Float64(2.0 * t_1)) - Float64(Float64(n * t_2) * Float64(U - U_42_)))))
	t_4 = Float64(U * Float64(n * 2.0))
	tmp = 0.0
	if (t_3 <= 0.0)
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * Float64(fma(Float64(n / Om), Float64(U - U_42_), 2.0) * l))) * U) * Float64(n * 2.0)));
	elseif (t_3 <= 2e+151)
		tmp = sqrt(fma(Float64(t - Float64(t_1 * 2.0)), t_4, Float64(Float64(Float64(Float64(-n) * t_2) * Float64(U - U_42_)) * t_4)));
	else
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * fma(Float64(U - U_42_), Float64(Float64(n / Om) * l), Float64(2.0 * l)))) * U) * Float64(n * 2.0)));
	end
	return tmp
end

Wolfram

code[n_, U_, t_, l_, Om_, U$42$_] := Block[{t$95$1 = N[(N[(l * l), $MachinePrecision] / Om), $MachinePrecision]}, Block[{t$95$2 = N[Power[N[(l / Om), $MachinePrecision], 2.0], $MachinePrecision]}, Block[{t$95$3 = N[Sqrt[N[(N[(N[(2.0 * n), $MachinePrecision] * U), $MachinePrecision] * N[(N[(t - N[(2.0 * t$95$1), $MachinePrecision]), $MachinePrecision] - N[(N[(n * t$95$2), $MachinePrecision] * N[(U - U$42$), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$4 = N[(U * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$3, 0.0], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * N[(N[(N[(n / Om), $MachinePrecision] * N[(U - U$42$), $MachinePrecision] + 2.0), $MachinePrecision] * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], If[LessEqual[t$95$3, 2e+151], N[Sqrt[N[(N[(t - N[(t$95$1 * 2.0), $MachinePrecision]), $MachinePrecision] * t$95$4 + N[(N[(N[((-n) * t$95$2), $MachinePrecision] * N[(U - U$42$), $MachinePrecision]), $MachinePrecision] * t$95$4), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * N[(N[(U - U$42$), $MachinePrecision] * N[(N[(n / Om), $MachinePrecision] * l), $MachinePrecision] + N[(2.0 * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]]]]]]

Derivation

1. Split input into 3 regimes

2. if (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*))))) < 0.0

   1. Initial program 5.1%

      \[\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. Add Preprocessing

   4. Applied rewrites 43.3%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 43.3%

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

   8. Applied rewrites 43.3%

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

   10. Applied rewrites 43.3%

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

   if 0.0 < (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*))))) < 2.00000000000000003e151

   1. Initial program 99.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. Add Preprocessing

   4. Applied rewrites 99.2%

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

   if 2.00000000000000003e151 < (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*)))))

   1. Initial program 19.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. Add Preprocessing

   4. Applied rewrites 26.5%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 29.9%

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

   8. Applied rewrites 37.1%

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

   10. Applied rewrites 41.1%

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

Alternative 2: 64.1% accurate, 0.3× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \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)\\ t_2 := \sqrt{\left(\left(2 \cdot n\right) \cdot U\right) \cdot t\_1}\\ \mathbf{if}\;t\_2 \leq 0:\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \left(\mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right) \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \mathbf{elif}\;t\_2 \leq 2 \cdot 10^{+151}:\\ \;\;\;\;\sqrt{\left(\left(n + n\right) \cdot U\right) \cdot t\_1}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \mathsf{fma}\left(U - U*, \frac{n}{Om} \cdot \ell, 2 \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \end{array} \end{array} \]

FPCore

(FPCore (n U t l Om U*)
 :precision binary64
 (let* ((t_1
         (-
          (- t (* 2.0 (/ (* l l) Om)))
          (* (* n (pow (/ l Om) 2.0)) (- U U*))))
        (t_2 (sqrt (* (* (* 2.0 n) U) t_1))))
   (if (<= t_2 0.0)
     (sqrt
      (* (* (- t (* (/ l Om) (* (fma (/ n Om) (- U U*) 2.0) l))) U) (* n 2.0)))
     (if (<= t_2 2e+151)
       (sqrt (* (* (+ n n) U) t_1))
       (sqrt
        (*
         (* (- t (* (/ l Om) (fma (- U U*) (* (/ n Om) l) (* 2.0 l)))) U)
         (* n 2.0)))))))

C

double code(double n, double U, double t, double l, double Om, double U_42_) {
	double t_1 = (t - (2.0 * ((l * l) / Om))) - ((n * pow((l / Om), 2.0)) * (U - U_42_));
	double t_2 = sqrt((((2.0 * n) * U) * t_1));
	double tmp;
	if (t_2 <= 0.0) {
		tmp = sqrt((((t - ((l / Om) * (fma((n / Om), (U - U_42_), 2.0) * l))) * U) * (n * 2.0)));
	} else if (t_2 <= 2e+151) {
		tmp = sqrt((((n + n) * U) * t_1));
	} else {
		tmp = sqrt((((t - ((l / Om) * fma((U - U_42_), ((n / Om) * l), (2.0 * l)))) * U) * (n * 2.0)));
	}
	return tmp;
}

Julia

function code(n, U, t, l, Om, U_42_)
	t_1 = Float64(Float64(t - Float64(2.0 * Float64(Float64(l * l) / Om))) - Float64(Float64(n * (Float64(l / Om) ^ 2.0)) * Float64(U - U_42_)))
	t_2 = sqrt(Float64(Float64(Float64(2.0 * n) * U) * t_1))
	tmp = 0.0
	if (t_2 <= 0.0)
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * Float64(fma(Float64(n / Om), Float64(U - U_42_), 2.0) * l))) * U) * Float64(n * 2.0)));
	elseif (t_2 <= 2e+151)
		tmp = sqrt(Float64(Float64(Float64(n + n) * U) * t_1));
	else
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * fma(Float64(U - U_42_), Float64(Float64(n / Om) * l), Float64(2.0 * l)))) * U) * Float64(n * 2.0)));
	end
	return tmp
end

Wolfram

code[n_, U_, t_, l_, Om_, U$42$_] := Block[{t$95$1 = 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]}, Block[{t$95$2 = N[Sqrt[N[(N[(N[(2.0 * n), $MachinePrecision] * U), $MachinePrecision] * t$95$1), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[t$95$2, 0.0], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * N[(N[(N[(n / Om), $MachinePrecision] * N[(U - U$42$), $MachinePrecision] + 2.0), $MachinePrecision] * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], If[LessEqual[t$95$2, 2e+151], N[Sqrt[N[(N[(N[(n + n), $MachinePrecision] * U), $MachinePrecision] * t$95$1), $MachinePrecision]], $MachinePrecision], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * N[(N[(U - U$42$), $MachinePrecision] * N[(N[(n / Om), $MachinePrecision] * l), $MachinePrecision] + N[(2.0 * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]]]]

Derivation

1. Split input into 3 regimes

2. if (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*))))) < 0.0

   1. Initial program 5.1%

      \[\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. Add Preprocessing

   4. Applied rewrites 43.3%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 43.3%

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

   8. Applied rewrites 43.3%

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

   10. Applied rewrites 43.3%

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

   if 0.0 < (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*))))) < 2.00000000000000003e151

   1. Initial program 99.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. Add Preprocessing
   3. Step-by-step derivation

      1. lift-literal N/A

         \[\leadsto \sqrt{\left(\left(\color{blue}{\mathsf{impl}\left(binary64, 2\right)} \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. lift-var N/A

         \[\leadsto \sqrt{\left(\left(\mathsf{impl}\left(binary64, 2\right) \cdot \color{blue}{\mathsf{impl}\left(binary64, n\right)}\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)} \]

      3. lift-*.f64 N/A

         \[\leadsto \sqrt{\left(\color{blue}{\mathsf{impl}\left(binary64, \left(2 \cdot n\right)\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)} \]

      4. count-2-rev N/A

         \[\leadsto \sqrt{\left(\mathsf{impl}\left(binary64, \color{blue}{\left(n + n\right)}\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)} \]

      5. lower-+.f64 N/A

         \[\leadsto \sqrt{\left(\color{blue}{\left(\mathsf{impl}\left(binary64, n\right) + \mathsf{impl}\left(binary64, n\right)\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)} \]

      6. lift-var N/A

         \[\leadsto \sqrt{\left(\left(\color{blue}{n} + \mathsf{impl}\left(binary64, n\right)\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)} \]

      7. lift-var 99.2

         \[\leadsto \sqrt{\left(\left(n + \color{blue}{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)} \]

   4. Applied rewrites 99.2%

      \[\leadsto \sqrt{\left(\color{blue}{\left(n + 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)} \]

   if 2.00000000000000003e151 < (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*)))))

   1. Initial program 19.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. Add Preprocessing

   4. Applied rewrites 26.5%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 29.9%

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

   8. Applied rewrites 37.1%

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

   10. Applied rewrites 41.1%

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

Alternative 3: 61.5% accurate, 0.4× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right)\\ t_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)}\\ \mathbf{if}\;t\_2 \leq 0 \lor \neg \left(t\_2 \leq 2 \cdot 10^{+151}\right):\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \left(t\_1 \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(\left(-\ell\right) \cdot \frac{\ell}{Om}, t\_1, t\right) \cdot \left(\left(U \cdot n\right) \cdot 2\right)}\\ \end{array} \end{array} \]

FPCore

(FPCore (n U t l Om U*)
 :precision binary64
 (let* ((t_1 (fma (/ n Om) (- U U*) 2.0))
        (t_2
         (sqrt
          (*
           (* (* 2.0 n) U)
           (-
            (- t (* 2.0 (/ (* l l) Om)))
            (* (* n (pow (/ l Om) 2.0)) (- U U*)))))))
   (if (or (<= t_2 0.0) (not (<= t_2 2e+151)))
     (sqrt (* (* (- t (* (/ l Om) (* t_1 l))) U) (* n 2.0)))
     (sqrt (* (fma (* (- l) (/ l Om)) t_1 t) (* (* U n) 2.0))))))

C

double code(double n, double U, double t, double l, double Om, double U_42_) {
	double t_1 = fma((n / Om), (U - U_42_), 2.0);
	double t_2 = sqrt((((2.0 * n) * U) * ((t - (2.0 * ((l * l) / Om))) - ((n * pow((l / Om), 2.0)) * (U - U_42_)))));
	double tmp;
	if ((t_2 <= 0.0) || !(t_2 <= 2e+151)) {
		tmp = sqrt((((t - ((l / Om) * (t_1 * l))) * U) * (n * 2.0)));
	} else {
		tmp = sqrt((fma((-l * (l / Om)), t_1, t) * ((U * n) * 2.0)));
	}
	return tmp;
}

Julia

function code(n, U, t, l, Om, U_42_)
	t_1 = fma(Float64(n / Om), Float64(U - U_42_), 2.0)
	t_2 = 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_)))))
	tmp = 0.0
	if ((t_2 <= 0.0) || !(t_2 <= 2e+151))
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * Float64(t_1 * l))) * U) * Float64(n * 2.0)));
	else
		tmp = sqrt(Float64(fma(Float64(Float64(-l) * Float64(l / Om)), t_1, t) * Float64(Float64(U * n) * 2.0)));
	end
	return tmp
end

Wolfram

code[n_, U_, t_, l_, Om_, U$42$_] := Block[{t$95$1 = N[(N[(n / Om), $MachinePrecision] * N[(U - U$42$), $MachinePrecision] + 2.0), $MachinePrecision]}, Block[{t$95$2 = 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]}, If[Or[LessEqual[t$95$2, 0.0], N[Not[LessEqual[t$95$2, 2e+151]], $MachinePrecision]], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * N[(t$95$1 * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[Sqrt[N[(N[(N[((-l) * N[(l / Om), $MachinePrecision]), $MachinePrecision] * t$95$1 + t), $MachinePrecision] * N[(N[(U * n), $MachinePrecision] * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]]]

Derivation

1. Split input into 2 regimes

2. if (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*))))) < 0.0 or 2.00000000000000003e151 < (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*)))))

   1. Initial program 17.0%

      \[\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. Add Preprocessing

   4. Applied rewrites 29.8%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 32.5%

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

   8. Applied rewrites 38.3%

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

   10. Applied rewrites 40.4%

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

   if 0.0 < (sqrt.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*))))) < 2.00000000000000003e151

   1. Initial program 99.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. Add Preprocessing

   4. Applied rewrites 81.8%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 81.8%

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

   8. Applied rewrites 85.8%

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

   10. Applied rewrites 91.6%

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

4. Final simplification 60.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\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)} \leq 0 \lor \neg \left(\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)} \leq 2 \cdot 10^{+151}\right):\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \left(\mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right) \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(\left(-\ell\right) \cdot \frac{\ell}{Om}, \mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right), t\right) \cdot \left(\left(U \cdot n\right) \cdot 2\right)}\\ \end{array} \]
5. Add Preprocessing

Alternative 4: 58.2% accurate, 0.7× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right) \cdot \ell\\ \mathbf{if}\;\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) \leq 6 \cdot 10^{+90}:\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot t\_1\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(\mathsf{fma}\left(\frac{-\ell}{Om}, t\_1, t\right) \cdot \left(n \cdot 2\right)\right) \cdot U}\\ \end{array} \end{array} \]

FPCore

(FPCore (n U t l Om U*)
 :precision binary64
 (let* ((t_1 (* (fma (/ n Om) (- U U*) 2.0) l)))
   (if (<=
        (*
         (* (* 2.0 n) U)
         (-
          (- t (* 2.0 (/ (* l l) Om)))
          (* (* n (pow (/ l Om) 2.0)) (- U U*))))
        6e+90)
     (sqrt (* (* (- t (* (/ l Om) t_1)) U) (* n 2.0)))
     (sqrt (* (* (fma (/ (- l) Om) t_1 t) (* n 2.0)) U)))))

C

double code(double n, double U, double t, double l, double Om, double U_42_) {
	double t_1 = fma((n / Om), (U - U_42_), 2.0) * l;
	double tmp;
	if ((((2.0 * n) * U) * ((t - (2.0 * ((l * l) / Om))) - ((n * pow((l / Om), 2.0)) * (U - U_42_)))) <= 6e+90) {
		tmp = sqrt((((t - ((l / Om) * t_1)) * U) * (n * 2.0)));
	} else {
		tmp = sqrt(((fma((-l / Om), t_1, t) * (n * 2.0)) * U));
	}
	return tmp;
}

Julia

function code(n, U, t, l, Om, U_42_)
	t_1 = Float64(fma(Float64(n / Om), Float64(U - U_42_), 2.0) * l)
	tmp = 0.0
	if (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_)))) <= 6e+90)
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * t_1)) * U) * Float64(n * 2.0)));
	else
		tmp = sqrt(Float64(Float64(fma(Float64(Float64(-l) / Om), t_1, t) * Float64(n * 2.0)) * U));
	end
	return tmp
end

Wolfram

code[n_, U_, t_, l_, Om_, U$42$_] := Block[{t$95$1 = N[(N[(N[(n / Om), $MachinePrecision] * N[(U - U$42$), $MachinePrecision] + 2.0), $MachinePrecision] * l), $MachinePrecision]}, If[LessEqual[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], 6e+90], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * t$95$1), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[Sqrt[N[(N[(N[(N[((-l) / Om), $MachinePrecision] * t$95$1 + t), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision]], $MachinePrecision]]]

Derivation

1. Split input into 2 regimes

2. if (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*)))) < 5.99999999999999957e90

   1. Initial program 66.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. Add Preprocessing

   4. Applied rewrites 71.5%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 72.5%

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

   8. Applied rewrites 75.2%

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

   10. Applied rewrites 76.2%

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

   if 5.99999999999999957e90 < (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) n) U) (-.f64 (-.f64 t (*.f64 #s(literal 2 binary64) (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) #s(literal 2 binary64))) (-.f64 U U*))))

   1. Initial program 39.4%

      \[\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. Add Preprocessing

   4. Applied rewrites 37.7%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 39.7%

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

   8. Applied rewrites 49.1%

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

   10. Applied rewrites 47.4%

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

Alternative 5: 62.8% accurate, 1.9× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;U \leq -1 \cdot 10^{-107}:\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, 2, \left(n \cdot \frac{\ell}{Om}\right) \cdot \left(U - U*\right)\right)\right) \cdot \left(n + n\right)\right) \cdot U}\\ \mathbf{elif}\;U \leq 1.9 \cdot 10^{+114}:\\ \;\;\;\;\sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \mathsf{fma}\left(U - U*, \frac{n}{Om} \cdot \ell, 2 \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(\left(-\ell\right) \cdot \frac{\ell}{Om}, \mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right), t\right) \cdot \left(n \cdot 2\right)} \cdot \sqrt{U}\\ \end{array} \end{array} \]

FPCore

(FPCore (n U t l Om U*)
 :precision binary64
 (if (<= U -1e-107)
   (sqrt
    (*
     (* (- t (* (/ l Om) (fma l 2.0 (* (* n (/ l Om)) (- U U*))))) (+ n n))
     U))
   (if (<= U 1.9e+114)
     (sqrt
      (*
       (* (- t (* (/ l Om) (fma (- U U*) (* (/ n Om) l) (* 2.0 l)))) U)
       (* n 2.0)))
     (*
      (sqrt
       (* (fma (* (- l) (/ l Om)) (fma (/ n Om) (- U U*) 2.0) t) (* n 2.0)))
      (sqrt U)))))

C

double code(double n, double U, double t, double l, double Om, double U_42_) {
	double tmp;
	if (U <= -1e-107) {
		tmp = sqrt((((t - ((l / Om) * fma(l, 2.0, ((n * (l / Om)) * (U - U_42_))))) * (n + n)) * U));
	} else if (U <= 1.9e+114) {
		tmp = sqrt((((t - ((l / Om) * fma((U - U_42_), ((n / Om) * l), (2.0 * l)))) * U) * (n * 2.0)));
	} else {
		tmp = sqrt((fma((-l * (l / Om)), fma((n / Om), (U - U_42_), 2.0), t) * (n * 2.0))) * sqrt(U);
	}
	return tmp;
}

Julia

function code(n, U, t, l, Om, U_42_)
	tmp = 0.0
	if (U <= -1e-107)
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * fma(l, 2.0, Float64(Float64(n * Float64(l / Om)) * Float64(U - U_42_))))) * Float64(n + n)) * U));
	elseif (U <= 1.9e+114)
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * fma(Float64(U - U_42_), Float64(Float64(n / Om) * l), Float64(2.0 * l)))) * U) * Float64(n * 2.0)));
	else
		tmp = Float64(sqrt(Float64(fma(Float64(Float64(-l) * Float64(l / Om)), fma(Float64(n / Om), Float64(U - U_42_), 2.0), t) * Float64(n * 2.0))) * sqrt(U));
	end
	return tmp
end

Wolfram

code[n_, U_, t_, l_, Om_, U$42$_] := If[LessEqual[U, -1e-107], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * N[(l * 2.0 + N[(N[(n * N[(l / Om), $MachinePrecision]), $MachinePrecision] * N[(U - U$42$), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(n + n), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision]], $MachinePrecision], If[LessEqual[U, 1.9e+114], N[Sqrt[N[(N[(N[(t - N[(N[(l / Om), $MachinePrecision] * N[(N[(U - U$42$), $MachinePrecision] * N[(N[(n / Om), $MachinePrecision] * l), $MachinePrecision] + N[(2.0 * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * U), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[(N[Sqrt[N[(N[(N[((-l) * N[(l / Om), $MachinePrecision]), $MachinePrecision] * N[(N[(n / Om), $MachinePrecision] * N[(U - U$42$), $MachinePrecision] + 2.0), $MachinePrecision] + t), $MachinePrecision] * N[(n * 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * N[Sqrt[U], $MachinePrecision]), $MachinePrecision]]]

Derivation

1. Split input into 3 regimes

2. if U < -1e-107

   1. Initial program 47.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. Add Preprocessing

   4. Applied rewrites 54.1%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 54.2%

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

   8. Applied rewrites 59.0%

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

      1. lift-var N/A

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

      2. lift-literal N/A

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

      3. lift-*.f64 N/A

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

      4. *-commutative N/A

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

      5. count-2-rev N/A

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

      6. lower-+.f64 N/A

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

      7. lift-var N/A

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

      8. lift-var 59.0

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

   10. Applied rewrites 59.0%

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

   if -1e-107 < U < 1.9e114

   1. Initial program 47.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. Add Preprocessing

   4. Applied rewrites 48.2%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 50.8%

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

   8. Applied rewrites 57.2%

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

   10. Applied rewrites 61.5%

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

   if 1.9e114 < U

   1. Initial program 65.1%

      \[\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. Add Preprocessing

   4. Applied rewrites 54.8%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 54.8%

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

   8. Applied rewrites 65.1%

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

   10. Applied rewrites 80.4%

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

Alternative 6: 62.9% accurate, 2.1× speedup

Math

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

FPCore

(FPCore (n U t l Om U*)
 :precision binary64
 (if (<= n -1e-310)
   (sqrt
    (*
     (* (- t (* (/ l Om) (fma l 2.0 (* (* n (/ l Om)) (- U U*))))) (+ n n))
     U))
   (*
    (sqrt (* (fma (* (- l) (/ l Om)) (fma (/ n Om) (- U U*) 2.0) t) U))
    (sqrt (* n 2.0)))))

C

double code(double n, double U, double t, double l, double Om, double U_42_) {
	double tmp;
	if (n <= -1e-310) {
		tmp = sqrt((((t - ((l / Om) * fma(l, 2.0, ((n * (l / Om)) * (U - U_42_))))) * (n + n)) * U));
	} else {
		tmp = sqrt((fma((-l * (l / Om)), fma((n / Om), (U - U_42_), 2.0), t) * U)) * sqrt((n * 2.0));
	}
	return tmp;
}

Julia

function code(n, U, t, l, Om, U_42_)
	tmp = 0.0
	if (n <= -1e-310)
		tmp = sqrt(Float64(Float64(Float64(t - Float64(Float64(l / Om) * fma(l, 2.0, Float64(Float64(n * Float64(l / Om)) * Float64(U - U_42_))))) * Float64(n + n)) * U));
	else
		tmp = Float64(sqrt(Float64(fma(Float64(Float64(-l) * Float64(l / Om)), fma(Float64(n / Om), Float64(U - U_42_), 2.0), t) * U)) * sqrt(Float64(n * 2.0)));
	end
	return tmp
end

Wolfram

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

Derivation

1. Split input into 2 regimes

2. if n < -9.999999999999969e-311

   1. Initial program 48.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. Add Preprocessing

   4. Applied rewrites 51.2%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 51.3%

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

   8. Applied rewrites 57.2%

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

      1. lift-var N/A

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

      2. lift-literal N/A

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

      3. lift-*.f64 N/A

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

      4. *-commutative N/A

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

      5. count-2-rev N/A

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

      6. lower-+.f64 N/A

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

      7. lift-var N/A

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

      8. lift-var 57.2

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

   10. Applied rewrites 57.2%

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

   if -9.999999999999969e-311 < n

   1. Initial program 51.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. Add Preprocessing

   4. Applied rewrites 49.9%

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

      1. lift-var N/A

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

      2. lift-var N/A

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

      3. lift--.f64 N/A

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

      4. lift-var N/A

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

      5. lift-*.f64 N/A

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

      6. lift-var N/A

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

      7. lift-var N/A

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

      8. lift-/.f64 N/A

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

      9. lift-literal N/A

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

      10. lift-pow.f64 N/A

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

      11. lift-*.f64 N/A

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

      12. *-commutative N/A

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

      13. unpow2 N/A

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

      14. associate-*l* N/A

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

      15. lower-*.f64 N/A

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

      16. lift-/.f64 N/A

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

      17. lift-var N/A

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

      18. lift-var N/A

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

      19. lower-*.f64 N/A

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

      20. lift-/.f64 N/A

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

      21. lift-var N/A

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

      22. lift-var N/A

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

      23. *-commutative N/A

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

   6. Applied rewrites 53.0%

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

   8. Applied rewrites 60.2%

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

   10. Applied rewrites 65.3%

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

Alternative 7: 60.0% accurate, 2.4× speedup

Math

\[\begin{array}{l} \\ \sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \mathsf{fma}\left(\ell, 2, \left(n \cdot \frac{\ell}{Om}\right) \cdot \left(U - U*\right)\right)\right) \cdot \left(n + n\right)\right) \cdot U} \end{array} \]

FPCore

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

C

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

Julia

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

Wolfram

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

Derivation

1. Initial program 49.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. Add Preprocessing

4. Applied rewrites 50.5%

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

   1. lift-var N/A

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

   2. lift-var N/A

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

   3. lift--.f64 N/A

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

   4. lift-var N/A

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

   5. lift-*.f64 N/A

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

   6. lift-var N/A

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

   7. lift-var N/A

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

   8. lift-/.f64 N/A

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

   9. lift-literal N/A

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

   10. lift-pow.f64 N/A

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

   11. lift-*.f64 N/A

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

   12. *-commutative N/A

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

   13. unpow2 N/A

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

   14. associate-*l* N/A

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

   15. lower-*.f64 N/A

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

   16. lift-/.f64 N/A

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

   17. lift-var N/A

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

   18. lift-var N/A

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

   19. lower-*.f64 N/A

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

   20. lift-/.f64 N/A

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

   21. lift-var N/A

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

   22. lift-var N/A

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

   23. *-commutative N/A

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

6. Applied rewrites 52.1%

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

8. Applied rewrites 58.7%

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

   1. lift-var N/A

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

   2. lift-literal N/A

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

   3. lift-*.f64 N/A

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

   4. *-commutative N/A

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

   5. count-2-rev N/A

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

   6. lower-+.f64 N/A

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

   7. lift-var N/A

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

   8. lift-var 58.7

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

10. Applied rewrites 58.7%

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

Alternative 8: 57.6% accurate, 2.5× speedup

Math

\[\begin{array}{l} \\ \sqrt{\left(\left(t - \frac{\ell}{Om} \cdot \left(\mathsf{fma}\left(\frac{n}{Om}, U - U*, 2\right) \cdot \ell\right)\right) \cdot U\right) \cdot \left(n \cdot 2\right)} \end{array} \]

FPCore

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

C

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

Julia

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

Wolfram

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

Derivation

1. Initial program 49.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. Add Preprocessing

4. Applied rewrites 50.5%

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

   1. lift-var N/A

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

   2. lift-var N/A

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

   3. lift--.f64 N/A

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

   4. lift-var N/A

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

   5. lift-*.f64 N/A

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

   6. lift-var N/A

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

   7. lift-var N/A

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

   8. lift-/.f64 N/A

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

   9. lift-literal N/A

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

   10. lift-pow.f64 N/A

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

   11. lift-*.f64 N/A

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

   12. *-commutative N/A

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

   13. unpow2 N/A

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

   14. associate-*l* N/A

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

   15. lower-*.f64 N/A

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

   16. lift-/.f64 N/A

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

   17. lift-var N/A

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

   18. lift-var N/A

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

   19. lower-*.f64 N/A

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

   20. lift-/.f64 N/A

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

   21. lift-var N/A

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

   22. lift-var N/A

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

   23. *-commutative N/A

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

6. Applied rewrites 52.1%

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

8. Applied rewrites 52.5%

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

10. Applied rewrites 55.3%

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

Reproduce

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