Toniolo and Linder, Equation (3a)

Percentage Accurate: 98.5% → 99.3%
Time: 5.7s
Alternatives: 6
Speedup: 0.6×

Specification

?
\[\begin{array}{l} \\ \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \end{array} \]
(FPCore (l Om kx ky)
 :precision binary64
 (sqrt
  (*
   (/ 1.0 2.0)
   (+
    1.0
    (/
     1.0
     (sqrt
      (+
       1.0
       (*
        (pow (/ (* 2.0 l) Om) 2.0)
        (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0))))))))))
double code(double l, double Om, double kx, double ky) {
	return sqrt(((1.0 / 2.0) * (1.0 + (1.0 / sqrt((1.0 + (pow(((2.0 * l) / Om), 2.0) * (pow(sin(kx), 2.0) + pow(sin(ky), 2.0)))))))));
}
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(l, om, kx, ky)
use fmin_fmax_functions
    real(8), intent (in) :: l
    real(8), intent (in) :: om
    real(8), intent (in) :: kx
    real(8), intent (in) :: ky
    code = sqrt(((1.0d0 / 2.0d0) * (1.0d0 + (1.0d0 / sqrt((1.0d0 + ((((2.0d0 * l) / om) ** 2.0d0) * ((sin(kx) ** 2.0d0) + (sin(ky) ** 2.0d0)))))))))
end function
public static double code(double l, double Om, double kx, double ky) {
	return Math.sqrt(((1.0 / 2.0) * (1.0 + (1.0 / Math.sqrt((1.0 + (Math.pow(((2.0 * l) / Om), 2.0) * (Math.pow(Math.sin(kx), 2.0) + Math.pow(Math.sin(ky), 2.0)))))))));
}
def code(l, Om, kx, ky):
	return math.sqrt(((1.0 / 2.0) * (1.0 + (1.0 / math.sqrt((1.0 + (math.pow(((2.0 * l) / Om), 2.0) * (math.pow(math.sin(kx), 2.0) + math.pow(math.sin(ky), 2.0)))))))))
function code(l, Om, kx, ky)
	return sqrt(Float64(Float64(1.0 / 2.0) * Float64(1.0 + Float64(1.0 / sqrt(Float64(1.0 + Float64((Float64(Float64(2.0 * l) / Om) ^ 2.0) * Float64((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))))))))
end
function tmp = code(l, Om, kx, ky)
	tmp = sqrt(((1.0 / 2.0) * (1.0 + (1.0 / sqrt((1.0 + ((((2.0 * l) / Om) ^ 2.0) * ((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))))))));
end
code[l_, Om_, kx_, ky_] := N[Sqrt[N[(N[(1.0 / 2.0), $MachinePrecision] * N[(1.0 + N[(1.0 / N[Sqrt[N[(1.0 + N[(N[Power[N[(N[(2.0 * l), $MachinePrecision] / Om), $MachinePrecision], 2.0], $MachinePrecision] * N[(N[Power[N[Sin[kx], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]
\begin{array}{l}

\\
\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)}
\end{array}

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 6 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 98.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \end{array} \]
(FPCore (l Om kx ky)
 :precision binary64
 (sqrt
  (*
   (/ 1.0 2.0)
   (+
    1.0
    (/
     1.0
     (sqrt
      (+
       1.0
       (*
        (pow (/ (* 2.0 l) Om) 2.0)
        (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0))))))))))
double code(double l, double Om, double kx, double ky) {
	return sqrt(((1.0 / 2.0) * (1.0 + (1.0 / sqrt((1.0 + (pow(((2.0 * l) / Om), 2.0) * (pow(sin(kx), 2.0) + pow(sin(ky), 2.0)))))))));
}
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(l, om, kx, ky)
use fmin_fmax_functions
    real(8), intent (in) :: l
    real(8), intent (in) :: om
    real(8), intent (in) :: kx
    real(8), intent (in) :: ky
    code = sqrt(((1.0d0 / 2.0d0) * (1.0d0 + (1.0d0 / sqrt((1.0d0 + ((((2.0d0 * l) / om) ** 2.0d0) * ((sin(kx) ** 2.0d0) + (sin(ky) ** 2.0d0)))))))))
end function
public static double code(double l, double Om, double kx, double ky) {
	return Math.sqrt(((1.0 / 2.0) * (1.0 + (1.0 / Math.sqrt((1.0 + (Math.pow(((2.0 * l) / Om), 2.0) * (Math.pow(Math.sin(kx), 2.0) + Math.pow(Math.sin(ky), 2.0)))))))));
}
def code(l, Om, kx, ky):
	return math.sqrt(((1.0 / 2.0) * (1.0 + (1.0 / math.sqrt((1.0 + (math.pow(((2.0 * l) / Om), 2.0) * (math.pow(math.sin(kx), 2.0) + math.pow(math.sin(ky), 2.0)))))))))
function code(l, Om, kx, ky)
	return sqrt(Float64(Float64(1.0 / 2.0) * Float64(1.0 + Float64(1.0 / sqrt(Float64(1.0 + Float64((Float64(Float64(2.0 * l) / Om) ^ 2.0) * Float64((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))))))))
end
function tmp = code(l, Om, kx, ky)
	tmp = sqrt(((1.0 / 2.0) * (1.0 + (1.0 / sqrt((1.0 + ((((2.0 * l) / Om) ^ 2.0) * ((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))))))));
end
code[l_, Om_, kx_, ky_] := N[Sqrt[N[(N[(1.0 / 2.0), $MachinePrecision] * N[(1.0 + N[(1.0 / N[Sqrt[N[(1.0 + N[(N[Power[N[(N[(2.0 * l), $MachinePrecision] / Om), $MachinePrecision], 2.0], $MachinePrecision] * N[(N[Power[N[Sin[kx], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]
\begin{array}{l}

\\
\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)}
\end{array}

Alternative 1: 99.3% accurate, 0.5× speedup?

\[\begin{array}{l} kx_m = \left|kx\right| \\ ky_m = \left|ky\right| \\ [l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\ \\ \begin{array}{l} t_0 := \frac{\ell + \ell}{Om}\\ \mathbf{if}\;\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)}}\right)} \leq 0.72:\\ \;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky\_m, ky\_m, 0.5 - 0.5 \cdot \cos \left(kx\_m + kx\_m\right)\right)}}\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{\mathsf{fma}\left(t\_0, t\_0 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot ky\_m\right)\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\_m\right)\right)\right), 1\right)}}\right)}\\ \end{array} \end{array} \]
kx_m = (fabs.f64 kx)
ky_m = (fabs.f64 ky)
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
(FPCore (l Om kx_m ky_m)
 :precision binary64
 (let* ((t_0 (/ (+ l l) Om)))
   (if (<=
        (sqrt
         (*
          (/ 1.0 2.0)
          (+
           1.0
           (/
            1.0
            (sqrt
             (+
              1.0
              (*
               (pow (/ (* 2.0 l) Om) 2.0)
               (+ (pow (sin kx_m) 2.0) (pow (sin ky_m) 2.0)))))))))
        0.72)
     (sqrt
      (*
       0.5
       (+
        1.0
        (/
         1.0
         (sqrt
          (+
           1.0
           (*
            (* 4.0 (* (/ l Om) (/ l Om)))
            (fma ky_m ky_m (- 0.5 (* 0.5 (cos (+ kx_m kx_m))))))))))))
     (sqrt
      (*
       0.5
       (+
        1.0
        (/
         1.0
         (sqrt
          (fma
           t_0
           (*
            t_0
            (+
             (- 0.5 (* 0.5 (cos (* 2.0 ky_m))))
             (- 0.5 (* 0.5 (cos (* 2.0 kx_m))))))
           1.0)))))))))
kx_m = fabs(kx);
ky_m = fabs(ky);
assert(l < Om && Om < kx_m && kx_m < ky_m);
double code(double l, double Om, double kx_m, double ky_m) {
	double t_0 = (l + l) / Om;
	double tmp;
	if (sqrt(((1.0 / 2.0) * (1.0 + (1.0 / sqrt((1.0 + (pow(((2.0 * l) / Om), 2.0) * (pow(sin(kx_m), 2.0) + pow(sin(ky_m), 2.0))))))))) <= 0.72) {
		tmp = sqrt((0.5 * (1.0 + (1.0 / sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * fma(ky_m, ky_m, (0.5 - (0.5 * cos((kx_m + kx_m))))))))))));
	} else {
		tmp = sqrt((0.5 * (1.0 + (1.0 / sqrt(fma(t_0, (t_0 * ((0.5 - (0.5 * cos((2.0 * ky_m)))) + (0.5 - (0.5 * cos((2.0 * kx_m)))))), 1.0))))));
	}
	return tmp;
}
kx_m = abs(kx)
ky_m = abs(ky)
l, Om, kx_m, ky_m = sort([l, Om, kx_m, ky_m])
function code(l, Om, kx_m, ky_m)
	t_0 = Float64(Float64(l + l) / Om)
	tmp = 0.0
	if (sqrt(Float64(Float64(1.0 / 2.0) * Float64(1.0 + Float64(1.0 / sqrt(Float64(1.0 + Float64((Float64(Float64(2.0 * l) / Om) ^ 2.0) * Float64((sin(kx_m) ^ 2.0) + (sin(ky_m) ^ 2.0))))))))) <= 0.72)
		tmp = sqrt(Float64(0.5 * Float64(1.0 + Float64(1.0 / sqrt(Float64(1.0 + Float64(Float64(4.0 * Float64(Float64(l / Om) * Float64(l / Om))) * fma(ky_m, ky_m, Float64(0.5 - Float64(0.5 * cos(Float64(kx_m + kx_m))))))))))));
	else
		tmp = sqrt(Float64(0.5 * Float64(1.0 + Float64(1.0 / sqrt(fma(t_0, Float64(t_0 * Float64(Float64(0.5 - Float64(0.5 * cos(Float64(2.0 * ky_m)))) + Float64(0.5 - Float64(0.5 * cos(Float64(2.0 * kx_m)))))), 1.0))))));
	end
	return tmp
end
kx_m = N[Abs[kx], $MachinePrecision]
ky_m = N[Abs[ky], $MachinePrecision]
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
code[l_, Om_, kx$95$m_, ky$95$m_] := Block[{t$95$0 = N[(N[(l + l), $MachinePrecision] / Om), $MachinePrecision]}, If[LessEqual[N[Sqrt[N[(N[(1.0 / 2.0), $MachinePrecision] * N[(1.0 + N[(1.0 / N[Sqrt[N[(1.0 + N[(N[Power[N[(N[(2.0 * l), $MachinePrecision] / Om), $MachinePrecision], 2.0], $MachinePrecision] * N[(N[Power[N[Sin[kx$95$m], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky$95$m], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 0.72], N[Sqrt[N[(0.5 * N[(1.0 + N[(1.0 / N[Sqrt[N[(1.0 + N[(N[(4.0 * N[(N[(l / Om), $MachinePrecision] * N[(l / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(ky$95$m * ky$95$m + N[(0.5 - N[(0.5 * N[Cos[N[(kx$95$m + kx$95$m), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[Sqrt[N[(0.5 * N[(1.0 + N[(1.0 / N[Sqrt[N[(t$95$0 * N[(t$95$0 * N[(N[(0.5 - N[(0.5 * N[Cos[N[(2.0 * ky$95$m), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(0.5 - N[(0.5 * N[Cos[N[(2.0 * kx$95$m), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]]
\begin{array}{l}
kx_m = \left|kx\right|
\\
ky_m = \left|ky\right|
\\
[l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\
\\
\begin{array}{l}
t_0 := \frac{\ell + \ell}{Om}\\
\mathbf{if}\;\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)}}\right)} \leq 0.72:\\
\;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky\_m, ky\_m, 0.5 - 0.5 \cdot \cos \left(kx\_m + kx\_m\right)\right)}}\right)}\\

\mathbf{else}:\\
\;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{\mathsf{fma}\left(t\_0, t\_0 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot ky\_m\right)\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\_m\right)\right)\right), 1\right)}}\right)}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (sqrt.f64 (*.f64 (/.f64 #s(literal 1 binary64) #s(literal 2 binary64)) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64)))))))))) < 0.71999999999999997

    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      5. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      8. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      9. swap-sqrN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      11. metadata-evalN/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      13. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      14. lower-*.f64N/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      16. lower-/.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    3. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    4. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \color{blue}{{\sin ky}^{2}}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \color{blue}{\sin ky \cdot \sin ky}\right)}}\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \color{blue}{\sin ky} \cdot \sin ky\right)}}\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \sin ky \cdot \color{blue}{\sin ky}\right)}}\right)} \]
      5. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}\right)}}\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot ky\right)}\right)\right)}}\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot ky\right)}\right)\right)}}\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot ky\right)}\right)\right)}}\right)} \]
      9. lift--.f6493.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot ky\right)\right)}\right)}}\right)} \]
      10. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot ky\right)}\right)\right)}}\right)} \]
      11. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot ky\right) \cdot \frac{1}{2}}\right)\right)}}\right)} \]
      12. lower-*.f6493.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(0.5 - \color{blue}{\cos \left(2 \cdot ky\right) \cdot 0.5}\right)\right)}}\right)} \]
      13. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot ky\right)} \cdot \frac{1}{2}\right)\right)}}\right)} \]
      14. count-2-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \cos \color{blue}{\left(ky + ky\right)} \cdot \frac{1}{2}\right)\right)}}\right)} \]
      15. lower-+.f6493.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(0.5 - \cos \color{blue}{\left(ky + ky\right)} \cdot 0.5\right)\right)}}\right)} \]
    5. Applied rewrites93.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \color{blue}{\left(0.5 - \cos \left(ky + ky\right) \cdot 0.5\right)}\right)}}\right)} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(\frac{1}{2} - \cos \left(ky + ky\right) \cdot \frac{1}{2}\right)\right)}}\right)} \]
      2. metadata-eval93.5

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(0.5 - \cos \left(ky + ky\right) \cdot 0.5\right)\right)}}\right)} \]
    7. Applied rewrites93.5%

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + \left(0.5 - \cos \left(ky + ky\right) \cdot 0.5\right)\right)}}\right)} \]
    8. Taylor expanded in ky around 0

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \color{blue}{\left({ky}^{2} + {\sin kx}^{2}\right)}}}\right)} \]
    9. Step-by-step derivation
      1. unpow2N/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, \color{blue}{ky}, {\sin kx}^{2}\right)}}\right)} \]
      3. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \sin kx \cdot \sin kx\right)}}\right)} \]
      4. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)}}\right)} \]
      5. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)}}\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)}}\right)} \]
      8. lift--.f6474.0

        \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, 0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)}}\right)} \]
      9. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)}}\right)} \]
      10. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)}}\right)} \]
      11. cos-2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \left(\cos kx \cdot \cos kx - \sin kx \cdot \sin kx\right)\right)}}\right)} \]
      12. cos-sumN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(kx + kx\right)\right)}}\right)} \]
      13. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, \frac{1}{2} - \frac{1}{2} \cdot \cos \left(kx + kx\right)\right)}}\right)} \]
      14. lift-+.f6474.0

        \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \mathsf{fma}\left(ky, ky, 0.5 - 0.5 \cdot \cos \left(kx + kx\right)\right)}}\right)} \]
    10. Applied rewrites74.0%

      \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \color{blue}{\mathsf{fma}\left(ky, ky, 0.5 - 0.5 \cdot \cos \left(kx + kx\right)\right)}}}\right)} \]

    if 0.71999999999999997 < (sqrt.f64 (*.f64 (/.f64 #s(literal 1 binary64) #s(literal 2 binary64)) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))))))))

    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}}\right)} \]
      2. +-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right) + 1}}}\right)} \]
      3. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)} + 1}}\right)} \]
      4. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right) + 1}}\right)} \]
      5. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right) + 1}}\right)} \]
      6. associate-*l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{\frac{2 \cdot \ell}{Om} \cdot \left(\frac{2 \cdot \ell}{Om} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)\right)} + 1}}\right)} \]
      7. lower-fma.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{2 \cdot \ell}{Om}, \frac{2 \cdot \ell}{Om} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right), 1\right)}}}\right)} \]
    3. Applied rewrites92.6%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{\color{blue}{\mathsf{fma}\left(\frac{\ell + \ell}{Om}, \frac{\ell + \ell}{Om} \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot ky\right)\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)\right), 1\right)}}}\right)} \]
    4. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{\mathsf{fma}\left(\frac{\ell + \ell}{Om}, \frac{\ell + \ell}{Om} \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot ky\right)\right) + \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)\right), 1\right)}}\right)} \]
      2. metadata-eval92.6

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{\mathsf{fma}\left(\frac{\ell + \ell}{Om}, \frac{\ell + \ell}{Om} \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot ky\right)\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)\right), 1\right)}}\right)} \]
    5. Applied rewrites92.6%

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{\mathsf{fma}\left(\frac{\ell + \ell}{Om}, \frac{\ell + \ell}{Om} \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot ky\right)\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)\right), 1\right)}}\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 2: 98.8% accurate, 0.6× speedup?

\[\begin{array}{l} kx_m = \left|kx\right| \\ ky_m = \left|ky\right| \\ [l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\ \\ \begin{array}{l} \mathbf{if}\;\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)} \leq 5000000000000:\\ \;\;\;\;\sqrt{\frac{0.5}{\sqrt{\mathsf{fma}\left(\left(0.5 - \cos \left(ky\_m + ky\_m\right) \cdot 0.5\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\_m\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + 0.5}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5}\\ \end{array} \end{array} \]
kx_m = (fabs.f64 kx)
ky_m = (fabs.f64 ky)
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
(FPCore (l Om kx_m ky_m)
 :precision binary64
 (if (<=
      (sqrt
       (+
        1.0
        (*
         (pow (/ (* 2.0 l) Om) 2.0)
         (+ (pow (sin kx_m) 2.0) (pow (sin ky_m) 2.0)))))
      5000000000000.0)
   (sqrt
    (+
     (/
      0.5
      (sqrt
       (fma
        (+
         (- 0.5 (* (cos (+ ky_m ky_m)) 0.5))
         (- 0.5 (* 0.5 (cos (* 2.0 kx_m)))))
        (* 4.0 (* (/ l Om) (/ l Om)))
        1.0)))
     0.5))
   (sqrt 0.5)))
kx_m = fabs(kx);
ky_m = fabs(ky);
assert(l < Om && Om < kx_m && kx_m < ky_m);
double code(double l, double Om, double kx_m, double ky_m) {
	double tmp;
	if (sqrt((1.0 + (pow(((2.0 * l) / Om), 2.0) * (pow(sin(kx_m), 2.0) + pow(sin(ky_m), 2.0))))) <= 5000000000000.0) {
		tmp = sqrt(((0.5 / sqrt(fma(((0.5 - (cos((ky_m + ky_m)) * 0.5)) + (0.5 - (0.5 * cos((2.0 * kx_m))))), (4.0 * ((l / Om) * (l / Om))), 1.0))) + 0.5));
	} else {
		tmp = sqrt(0.5);
	}
	return tmp;
}
kx_m = abs(kx)
ky_m = abs(ky)
l, Om, kx_m, ky_m = sort([l, Om, kx_m, ky_m])
function code(l, Om, kx_m, ky_m)
	tmp = 0.0
	if (sqrt(Float64(1.0 + Float64((Float64(Float64(2.0 * l) / Om) ^ 2.0) * Float64((sin(kx_m) ^ 2.0) + (sin(ky_m) ^ 2.0))))) <= 5000000000000.0)
		tmp = sqrt(Float64(Float64(0.5 / sqrt(fma(Float64(Float64(0.5 - Float64(cos(Float64(ky_m + ky_m)) * 0.5)) + Float64(0.5 - Float64(0.5 * cos(Float64(2.0 * kx_m))))), Float64(4.0 * Float64(Float64(l / Om) * Float64(l / Om))), 1.0))) + 0.5));
	else
		tmp = sqrt(0.5);
	end
	return tmp
end
kx_m = N[Abs[kx], $MachinePrecision]
ky_m = N[Abs[ky], $MachinePrecision]
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
code[l_, Om_, kx$95$m_, ky$95$m_] := If[LessEqual[N[Sqrt[N[(1.0 + N[(N[Power[N[(N[(2.0 * l), $MachinePrecision] / Om), $MachinePrecision], 2.0], $MachinePrecision] * N[(N[Power[N[Sin[kx$95$m], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky$95$m], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 5000000000000.0], N[Sqrt[N[(N[(0.5 / N[Sqrt[N[(N[(N[(0.5 - N[(N[Cos[N[(ky$95$m + ky$95$m), $MachinePrecision]], $MachinePrecision] * 0.5), $MachinePrecision]), $MachinePrecision] + N[(0.5 - N[(0.5 * N[Cos[N[(2.0 * kx$95$m), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(4.0 * N[(N[(l / Om), $MachinePrecision] * N[(l / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] + 0.5), $MachinePrecision]], $MachinePrecision], N[Sqrt[0.5], $MachinePrecision]]
\begin{array}{l}
kx_m = \left|kx\right|
\\
ky_m = \left|ky\right|
\\
[l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\
\\
\begin{array}{l}
\mathbf{if}\;\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)} \leq 5000000000000:\\
\;\;\;\;\sqrt{\frac{0.5}{\sqrt{\mathsf{fma}\left(\left(0.5 - \cos \left(ky\_m + ky\_m\right) \cdot 0.5\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\_m\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + 0.5}\\

\mathbf{else}:\\
\;\;\;\;\sqrt{0.5}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64)))))) < 5e12

    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Applied rewrites91.6%

      \[\leadsto \color{blue}{\sqrt{\frac{0.5}{\sqrt{\mathsf{fma}\left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot ky\right)\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + 0.5}} \]
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{\frac{1}{2}}{\sqrt{\mathsf{fma}\left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot ky\right)}\right) + \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + \frac{1}{2}} \]
      2. *-commutativeN/A

        \[\leadsto \sqrt{\frac{\frac{1}{2}}{\sqrt{\mathsf{fma}\left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot ky\right) \cdot \frac{1}{2}}\right) + \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + \frac{1}{2}} \]
      3. lower-*.f6491.6

        \[\leadsto \sqrt{\frac{0.5}{\sqrt{\mathsf{fma}\left(\left(0.5 - \color{blue}{\cos \left(2 \cdot ky\right) \cdot 0.5}\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + 0.5} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{\frac{1}{2}}{\sqrt{\mathsf{fma}\left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot ky\right)} \cdot \frac{1}{2}\right) + \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + \frac{1}{2}} \]
      5. count-2-revN/A

        \[\leadsto \sqrt{\frac{\frac{1}{2}}{\sqrt{\mathsf{fma}\left(\left(\frac{1}{2} - \cos \color{blue}{\left(ky + ky\right)} \cdot \frac{1}{2}\right) + \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + \frac{1}{2}} \]
      6. lower-+.f6491.6

        \[\leadsto \sqrt{\frac{0.5}{\sqrt{\mathsf{fma}\left(\left(0.5 - \cos \color{blue}{\left(ky + ky\right)} \cdot 0.5\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + 0.5} \]
    4. Applied rewrites91.6%

      \[\leadsto \sqrt{\frac{0.5}{\sqrt{\mathsf{fma}\left(\left(0.5 - \color{blue}{\cos \left(ky + ky\right) \cdot 0.5}\right) + \left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right), 4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right), 1\right)}} + 0.5} \]

    if 5e12 < (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))))

    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      5. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      8. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      9. swap-sqrN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      11. metadata-evalN/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      13. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      14. lower-*.f64N/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      16. lower-/.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    3. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    4. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{{\sin kx}^{2}} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx} \cdot \sin kx + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin kx \cdot \color{blue}{\sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      5. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      9. lift--.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      10. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      11. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot kx\right) \cdot \frac{1}{2}}\right) + {\sin ky}^{2}\right)}}\right)} \]
      12. lower-*.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \color{blue}{\cos \left(2 \cdot kx\right) \cdot 0.5}\right) + {\sin ky}^{2}\right)}}\right)} \]
      13. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      14. count-2-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(kx + kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      15. lower-+.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \color{blue}{\left(kx + kx\right)} \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    5. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right)} + {\sin ky}^{2}\right)}}\right)} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \left(kx + kx\right) \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      2. metadata-eval98.5

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    7. Applied rewrites98.5%

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    8. Taylor expanded in l around inf

      \[\leadsto \color{blue}{\sqrt{\frac{1}{2}}} \]
    9. Step-by-step derivation
      1. lower-sqrt.f6456.1

        \[\leadsto \sqrt{0.5} \]
    10. Applied rewrites56.1%

      \[\leadsto \color{blue}{\sqrt{0.5}} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 3: 98.5% accurate, 0.7× speedup?

\[\begin{array}{l} kx_m = \left|kx\right| \\ ky_m = \left|ky\right| \\ [l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\ \\ \begin{array}{l} \mathbf{if}\;\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)} \leq 5000000000000:\\ \;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(0.5 - 0.5 \cdot \cos \left(ky\_m + ky\_m\right)\right)}}\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5}\\ \end{array} \end{array} \]
kx_m = (fabs.f64 kx)
ky_m = (fabs.f64 ky)
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
(FPCore (l Om kx_m ky_m)
 :precision binary64
 (if (<=
      (sqrt
       (+
        1.0
        (*
         (pow (/ (* 2.0 l) Om) 2.0)
         (+ (pow (sin kx_m) 2.0) (pow (sin ky_m) 2.0)))))
      5000000000000.0)
   (sqrt
    (*
     0.5
     (+
      1.0
      (/
       1.0
       (sqrt
        (+
         1.0
         (*
          (* 4.0 (* (/ l Om) (/ l Om)))
          (- 0.5 (* 0.5 (cos (+ ky_m ky_m)))))))))))
   (sqrt 0.5)))
kx_m = fabs(kx);
ky_m = fabs(ky);
assert(l < Om && Om < kx_m && kx_m < ky_m);
double code(double l, double Om, double kx_m, double ky_m) {
	double tmp;
	if (sqrt((1.0 + (pow(((2.0 * l) / Om), 2.0) * (pow(sin(kx_m), 2.0) + pow(sin(ky_m), 2.0))))) <= 5000000000000.0) {
		tmp = sqrt((0.5 * (1.0 + (1.0 / sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * (0.5 - (0.5 * cos((ky_m + ky_m)))))))))));
	} else {
		tmp = sqrt(0.5);
	}
	return tmp;
}
kx_m =     private
ky_m =     private
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
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(l, om, kx_m, ky_m)
use fmin_fmax_functions
    real(8), intent (in) :: l
    real(8), intent (in) :: om
    real(8), intent (in) :: kx_m
    real(8), intent (in) :: ky_m
    real(8) :: tmp
    if (sqrt((1.0d0 + ((((2.0d0 * l) / om) ** 2.0d0) * ((sin(kx_m) ** 2.0d0) + (sin(ky_m) ** 2.0d0))))) <= 5000000000000.0d0) then
        tmp = sqrt((0.5d0 * (1.0d0 + (1.0d0 / sqrt((1.0d0 + ((4.0d0 * ((l / om) * (l / om))) * (0.5d0 - (0.5d0 * cos((ky_m + ky_m)))))))))))
    else
        tmp = sqrt(0.5d0)
    end if
    code = tmp
end function
kx_m = Math.abs(kx);
ky_m = Math.abs(ky);
assert l < Om && Om < kx_m && kx_m < ky_m;
public static double code(double l, double Om, double kx_m, double ky_m) {
	double tmp;
	if (Math.sqrt((1.0 + (Math.pow(((2.0 * l) / Om), 2.0) * (Math.pow(Math.sin(kx_m), 2.0) + Math.pow(Math.sin(ky_m), 2.0))))) <= 5000000000000.0) {
		tmp = Math.sqrt((0.5 * (1.0 + (1.0 / Math.sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * (0.5 - (0.5 * Math.cos((ky_m + ky_m)))))))))));
	} else {
		tmp = Math.sqrt(0.5);
	}
	return tmp;
}
kx_m = math.fabs(kx)
ky_m = math.fabs(ky)
[l, Om, kx_m, ky_m] = sort([l, Om, kx_m, ky_m])
def code(l, Om, kx_m, ky_m):
	tmp = 0
	if math.sqrt((1.0 + (math.pow(((2.0 * l) / Om), 2.0) * (math.pow(math.sin(kx_m), 2.0) + math.pow(math.sin(ky_m), 2.0))))) <= 5000000000000.0:
		tmp = math.sqrt((0.5 * (1.0 + (1.0 / math.sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * (0.5 - (0.5 * math.cos((ky_m + ky_m)))))))))))
	else:
		tmp = math.sqrt(0.5)
	return tmp
kx_m = abs(kx)
ky_m = abs(ky)
l, Om, kx_m, ky_m = sort([l, Om, kx_m, ky_m])
function code(l, Om, kx_m, ky_m)
	tmp = 0.0
	if (sqrt(Float64(1.0 + Float64((Float64(Float64(2.0 * l) / Om) ^ 2.0) * Float64((sin(kx_m) ^ 2.0) + (sin(ky_m) ^ 2.0))))) <= 5000000000000.0)
		tmp = sqrt(Float64(0.5 * Float64(1.0 + Float64(1.0 / sqrt(Float64(1.0 + Float64(Float64(4.0 * Float64(Float64(l / Om) * Float64(l / Om))) * Float64(0.5 - Float64(0.5 * cos(Float64(ky_m + ky_m)))))))))));
	else
		tmp = sqrt(0.5);
	end
	return tmp
end
kx_m = abs(kx);
ky_m = abs(ky);
l, Om, kx_m, ky_m = num2cell(sort([l, Om, kx_m, ky_m])){:}
function tmp_2 = code(l, Om, kx_m, ky_m)
	tmp = 0.0;
	if (sqrt((1.0 + ((((2.0 * l) / Om) ^ 2.0) * ((sin(kx_m) ^ 2.0) + (sin(ky_m) ^ 2.0))))) <= 5000000000000.0)
		tmp = sqrt((0.5 * (1.0 + (1.0 / sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * (0.5 - (0.5 * cos((ky_m + ky_m)))))))))));
	else
		tmp = sqrt(0.5);
	end
	tmp_2 = tmp;
end
kx_m = N[Abs[kx], $MachinePrecision]
ky_m = N[Abs[ky], $MachinePrecision]
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
code[l_, Om_, kx$95$m_, ky$95$m_] := If[LessEqual[N[Sqrt[N[(1.0 + N[(N[Power[N[(N[(2.0 * l), $MachinePrecision] / Om), $MachinePrecision], 2.0], $MachinePrecision] * N[(N[Power[N[Sin[kx$95$m], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky$95$m], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 5000000000000.0], N[Sqrt[N[(0.5 * N[(1.0 + N[(1.0 / N[Sqrt[N[(1.0 + N[(N[(4.0 * N[(N[(l / Om), $MachinePrecision] * N[(l / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(0.5 - N[(0.5 * N[Cos[N[(ky$95$m + ky$95$m), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[Sqrt[0.5], $MachinePrecision]]
\begin{array}{l}
kx_m = \left|kx\right|
\\
ky_m = \left|ky\right|
\\
[l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\
\\
\begin{array}{l}
\mathbf{if}\;\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)} \leq 5000000000000:\\
\;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(0.5 - 0.5 \cdot \cos \left(ky\_m + ky\_m\right)\right)}}\right)}\\

\mathbf{else}:\\
\;\;\;\;\sqrt{0.5}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64)))))) < 5e12

    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      5. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      8. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      9. swap-sqrN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      11. metadata-evalN/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      13. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      14. lower-*.f64N/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      16. lower-/.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    3. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    4. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{{\sin kx}^{2}} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx} \cdot \sin kx + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin kx \cdot \color{blue}{\sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      5. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      9. lift--.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      10. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      11. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot kx\right) \cdot \frac{1}{2}}\right) + {\sin ky}^{2}\right)}}\right)} \]
      12. lower-*.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \color{blue}{\cos \left(2 \cdot kx\right) \cdot 0.5}\right) + {\sin ky}^{2}\right)}}\right)} \]
      13. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      14. count-2-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(kx + kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      15. lower-+.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \color{blue}{\left(kx + kx\right)} \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    5. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right)} + {\sin ky}^{2}\right)}}\right)} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \left(kx + kx\right) \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      2. metadata-eval98.5

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    7. Applied rewrites98.5%

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    8. Taylor expanded in kx around 0

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \color{blue}{{\sin ky}^{2}}}}\right)} \]
    9. Step-by-step derivation
      1. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin ky \cdot \color{blue}{\sin ky}\right)}}\right)} \]
      2. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot ky\right)}\right)}}\right)} \]
      3. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}}\right)} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}}\right)} \]
      5. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot ky\right)}\right)}}\right)} \]
      6. lift--.f6491.2

        \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(0.5 - \color{blue}{0.5 \cdot \cos \left(2 \cdot ky\right)}\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}}\right)} \]
      8. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}}\right)} \]
      9. cos-2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \left(\cos ky \cdot \cos ky - \color{blue}{\sin ky \cdot \sin ky}\right)\right)}}\right)} \]
      10. cos-sumN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(ky + ky\right)\right)}}\right)} \]
      11. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(ky + ky\right)\right)}}\right)} \]
      12. lift-+.f6491.2

        \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(0.5 - 0.5 \cdot \cos \left(ky + ky\right)\right)}}\right)} \]
    10. Applied rewrites91.2%

      \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \color{blue}{\left(0.5 - 0.5 \cdot \cos \left(ky + ky\right)\right)}}}\right)} \]

    if 5e12 < (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))))

    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      5. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      8. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      9. swap-sqrN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      11. metadata-evalN/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      13. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      14. lower-*.f64N/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      16. lower-/.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    3. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    4. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{{\sin kx}^{2}} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx} \cdot \sin kx + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin kx \cdot \color{blue}{\sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      5. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      9. lift--.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      10. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      11. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot kx\right) \cdot \frac{1}{2}}\right) + {\sin ky}^{2}\right)}}\right)} \]
      12. lower-*.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \color{blue}{\cos \left(2 \cdot kx\right) \cdot 0.5}\right) + {\sin ky}^{2}\right)}}\right)} \]
      13. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      14. count-2-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(kx + kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      15. lower-+.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \color{blue}{\left(kx + kx\right)} \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    5. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right)} + {\sin ky}^{2}\right)}}\right)} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \left(kx + kx\right) \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      2. metadata-eval98.5

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    7. Applied rewrites98.5%

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    8. Taylor expanded in l around inf

      \[\leadsto \color{blue}{\sqrt{\frac{1}{2}}} \]
    9. Step-by-step derivation
      1. lower-sqrt.f6456.1

        \[\leadsto \sqrt{0.5} \]
    10. Applied rewrites56.1%

      \[\leadsto \color{blue}{\sqrt{0.5}} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 4: 98.3% accurate, 1.2× speedup?

\[\begin{array}{l} kx_m = \left|kx\right| \\ ky_m = \left|ky\right| \\ [l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\ \\ \sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx\_m + kx\_m\right) \cdot 0.5\right) + {\sin ky\_m}^{2}\right)}}\right)} \end{array} \]
kx_m = (fabs.f64 kx)
ky_m = (fabs.f64 ky)
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
(FPCore (l Om kx_m ky_m)
 :precision binary64
 (sqrt
  (*
   0.5
   (+
    1.0
    (/
     1.0
     (sqrt
      (+
       1.0
       (*
        (* 4.0 (* (/ l Om) (/ l Om)))
        (+ (- 0.5 (* (cos (+ kx_m kx_m)) 0.5)) (pow (sin ky_m) 2.0))))))))))
kx_m = fabs(kx);
ky_m = fabs(ky);
assert(l < Om && Om < kx_m && kx_m < ky_m);
double code(double l, double Om, double kx_m, double ky_m) {
	return sqrt((0.5 * (1.0 + (1.0 / sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * ((0.5 - (cos((kx_m + kx_m)) * 0.5)) + pow(sin(ky_m), 2.0)))))))));
}
kx_m =     private
ky_m =     private
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
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(l, om, kx_m, ky_m)
use fmin_fmax_functions
    real(8), intent (in) :: l
    real(8), intent (in) :: om
    real(8), intent (in) :: kx_m
    real(8), intent (in) :: ky_m
    code = sqrt((0.5d0 * (1.0d0 + (1.0d0 / sqrt((1.0d0 + ((4.0d0 * ((l / om) * (l / om))) * ((0.5d0 - (cos((kx_m + kx_m)) * 0.5d0)) + (sin(ky_m) ** 2.0d0)))))))))
end function
kx_m = Math.abs(kx);
ky_m = Math.abs(ky);
assert l < Om && Om < kx_m && kx_m < ky_m;
public static double code(double l, double Om, double kx_m, double ky_m) {
	return Math.sqrt((0.5 * (1.0 + (1.0 / Math.sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * ((0.5 - (Math.cos((kx_m + kx_m)) * 0.5)) + Math.pow(Math.sin(ky_m), 2.0)))))))));
}
kx_m = math.fabs(kx)
ky_m = math.fabs(ky)
[l, Om, kx_m, ky_m] = sort([l, Om, kx_m, ky_m])
def code(l, Om, kx_m, ky_m):
	return math.sqrt((0.5 * (1.0 + (1.0 / math.sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * ((0.5 - (math.cos((kx_m + kx_m)) * 0.5)) + math.pow(math.sin(ky_m), 2.0)))))))))
kx_m = abs(kx)
ky_m = abs(ky)
l, Om, kx_m, ky_m = sort([l, Om, kx_m, ky_m])
function code(l, Om, kx_m, ky_m)
	return sqrt(Float64(0.5 * Float64(1.0 + Float64(1.0 / sqrt(Float64(1.0 + Float64(Float64(4.0 * Float64(Float64(l / Om) * Float64(l / Om))) * Float64(Float64(0.5 - Float64(cos(Float64(kx_m + kx_m)) * 0.5)) + (sin(ky_m) ^ 2.0)))))))))
end
kx_m = abs(kx);
ky_m = abs(ky);
l, Om, kx_m, ky_m = num2cell(sort([l, Om, kx_m, ky_m])){:}
function tmp = code(l, Om, kx_m, ky_m)
	tmp = sqrt((0.5 * (1.0 + (1.0 / sqrt((1.0 + ((4.0 * ((l / Om) * (l / Om))) * ((0.5 - (cos((kx_m + kx_m)) * 0.5)) + (sin(ky_m) ^ 2.0)))))))));
end
kx_m = N[Abs[kx], $MachinePrecision]
ky_m = N[Abs[ky], $MachinePrecision]
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
code[l_, Om_, kx$95$m_, ky$95$m_] := N[Sqrt[N[(0.5 * N[(1.0 + N[(1.0 / N[Sqrt[N[(1.0 + N[(N[(4.0 * N[(N[(l / Om), $MachinePrecision] * N[(l / Om), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(N[(0.5 - N[(N[Cos[N[(kx$95$m + kx$95$m), $MachinePrecision]], $MachinePrecision] * 0.5), $MachinePrecision]), $MachinePrecision] + N[Power[N[Sin[ky$95$m], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]
\begin{array}{l}
kx_m = \left|kx\right|
\\
ky_m = \left|ky\right|
\\
[l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\
\\
\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx\_m + kx\_m\right) \cdot 0.5\right) + {\sin ky\_m}^{2}\right)}}\right)}
\end{array}
Derivation
  1. Initial program 98.5%

    \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
  2. Step-by-step derivation
    1. lift-pow.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. unpow2N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    3. lift-/.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    4. lift-*.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    5. associate-/l*N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    6. lift-/.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    7. lift-*.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    8. associate-/l*N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    9. swap-sqrN/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    10. metadata-evalN/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    11. metadata-evalN/A

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

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    13. metadata-evalN/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    14. lower-*.f64N/A

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

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    16. lower-/.f6498.5

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
  3. Applied rewrites98.5%

    \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
  4. Step-by-step derivation
    1. lift-pow.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{{\sin kx}^{2}} + {\sin ky}^{2}\right)}}\right)} \]
    2. unpow2N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}\right)}}\right)} \]
    3. lift-sin.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx} \cdot \sin kx + {\sin ky}^{2}\right)}}\right)} \]
    4. lift-sin.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin kx \cdot \color{blue}{\sin kx} + {\sin ky}^{2}\right)}}\right)} \]
    5. sqr-sin-a-revN/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
    6. lift-*.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
    7. lift-cos.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
    8. lift-*.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
    9. lift--.f6498.5

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
    10. lift-*.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
    11. *-commutativeN/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot kx\right) \cdot \frac{1}{2}}\right) + {\sin ky}^{2}\right)}}\right)} \]
    12. lower-*.f6498.5

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \color{blue}{\cos \left(2 \cdot kx\right) \cdot 0.5}\right) + {\sin ky}^{2}\right)}}\right)} \]
    13. lift-*.f64N/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
    14. count-2-revN/A

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(kx + kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
    15. lower-+.f6498.5

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \color{blue}{\left(kx + kx\right)} \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
  5. Applied rewrites98.5%

    \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right)} + {\sin ky}^{2}\right)}}\right)} \]
  6. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \left(kx + kx\right) \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
    2. metadata-eval98.5

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
  7. Applied rewrites98.5%

    \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
  8. Add Preprocessing

Alternative 5: 98.1% accurate, 1.1× speedup?

\[\begin{array}{l} kx_m = \left|kx\right| \\ ky_m = \left|ky\right| \\ [l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\ \\ \begin{array}{l} \mathbf{if}\;\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)} \leq 2:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5}\\ \end{array} \end{array} \]
kx_m = (fabs.f64 kx)
ky_m = (fabs.f64 ky)
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
(FPCore (l Om kx_m ky_m)
 :precision binary64
 (if (<=
      (sqrt
       (+
        1.0
        (*
         (pow (/ (* 2.0 l) Om) 2.0)
         (+ (pow (sin kx_m) 2.0) (pow (sin ky_m) 2.0)))))
      2.0)
   1.0
   (sqrt 0.5)))
kx_m = fabs(kx);
ky_m = fabs(ky);
assert(l < Om && Om < kx_m && kx_m < ky_m);
double code(double l, double Om, double kx_m, double ky_m) {
	double tmp;
	if (sqrt((1.0 + (pow(((2.0 * l) / Om), 2.0) * (pow(sin(kx_m), 2.0) + pow(sin(ky_m), 2.0))))) <= 2.0) {
		tmp = 1.0;
	} else {
		tmp = sqrt(0.5);
	}
	return tmp;
}
kx_m =     private
ky_m =     private
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
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(l, om, kx_m, ky_m)
use fmin_fmax_functions
    real(8), intent (in) :: l
    real(8), intent (in) :: om
    real(8), intent (in) :: kx_m
    real(8), intent (in) :: ky_m
    real(8) :: tmp
    if (sqrt((1.0d0 + ((((2.0d0 * l) / om) ** 2.0d0) * ((sin(kx_m) ** 2.0d0) + (sin(ky_m) ** 2.0d0))))) <= 2.0d0) then
        tmp = 1.0d0
    else
        tmp = sqrt(0.5d0)
    end if
    code = tmp
end function
kx_m = Math.abs(kx);
ky_m = Math.abs(ky);
assert l < Om && Om < kx_m && kx_m < ky_m;
public static double code(double l, double Om, double kx_m, double ky_m) {
	double tmp;
	if (Math.sqrt((1.0 + (Math.pow(((2.0 * l) / Om), 2.0) * (Math.pow(Math.sin(kx_m), 2.0) + Math.pow(Math.sin(ky_m), 2.0))))) <= 2.0) {
		tmp = 1.0;
	} else {
		tmp = Math.sqrt(0.5);
	}
	return tmp;
}
kx_m = math.fabs(kx)
ky_m = math.fabs(ky)
[l, Om, kx_m, ky_m] = sort([l, Om, kx_m, ky_m])
def code(l, Om, kx_m, ky_m):
	tmp = 0
	if math.sqrt((1.0 + (math.pow(((2.0 * l) / Om), 2.0) * (math.pow(math.sin(kx_m), 2.0) + math.pow(math.sin(ky_m), 2.0))))) <= 2.0:
		tmp = 1.0
	else:
		tmp = math.sqrt(0.5)
	return tmp
kx_m = abs(kx)
ky_m = abs(ky)
l, Om, kx_m, ky_m = sort([l, Om, kx_m, ky_m])
function code(l, Om, kx_m, ky_m)
	tmp = 0.0
	if (sqrt(Float64(1.0 + Float64((Float64(Float64(2.0 * l) / Om) ^ 2.0) * Float64((sin(kx_m) ^ 2.0) + (sin(ky_m) ^ 2.0))))) <= 2.0)
		tmp = 1.0;
	else
		tmp = sqrt(0.5);
	end
	return tmp
end
kx_m = abs(kx);
ky_m = abs(ky);
l, Om, kx_m, ky_m = num2cell(sort([l, Om, kx_m, ky_m])){:}
function tmp_2 = code(l, Om, kx_m, ky_m)
	tmp = 0.0;
	if (sqrt((1.0 + ((((2.0 * l) / Om) ^ 2.0) * ((sin(kx_m) ^ 2.0) + (sin(ky_m) ^ 2.0))))) <= 2.0)
		tmp = 1.0;
	else
		tmp = sqrt(0.5);
	end
	tmp_2 = tmp;
end
kx_m = N[Abs[kx], $MachinePrecision]
ky_m = N[Abs[ky], $MachinePrecision]
NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
code[l_, Om_, kx$95$m_, ky$95$m_] := If[LessEqual[N[Sqrt[N[(1.0 + N[(N[Power[N[(N[(2.0 * l), $MachinePrecision] / Om), $MachinePrecision], 2.0], $MachinePrecision] * N[(N[Power[N[Sin[kx$95$m], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky$95$m], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 2.0], 1.0, N[Sqrt[0.5], $MachinePrecision]]
\begin{array}{l}
kx_m = \left|kx\right|
\\
ky_m = \left|ky\right|
\\
[l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\
\\
\begin{array}{l}
\mathbf{if}\;\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx\_m}^{2} + {\sin ky\_m}^{2}\right)} \leq 2:\\
\;\;\;\;1\\

\mathbf{else}:\\
\;\;\;\;\sqrt{0.5}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64)))))) < 2

    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      5. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      8. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      9. swap-sqrN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      11. metadata-evalN/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      13. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      14. lower-*.f64N/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      16. lower-/.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    3. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    4. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{{\sin kx}^{2}} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx} \cdot \sin kx + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin kx \cdot \color{blue}{\sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      5. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      9. lift--.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      10. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      11. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot kx\right) \cdot \frac{1}{2}}\right) + {\sin ky}^{2}\right)}}\right)} \]
      12. lower-*.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \color{blue}{\cos \left(2 \cdot kx\right) \cdot 0.5}\right) + {\sin ky}^{2}\right)}}\right)} \]
      13. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      14. count-2-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(kx + kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      15. lower-+.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \color{blue}{\left(kx + kx\right)} \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    5. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right)} + {\sin ky}^{2}\right)}}\right)} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \left(kx + kx\right) \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      2. metadata-eval98.5

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    7. Applied rewrites98.5%

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    8. Taylor expanded in l around 0

      \[\leadsto \color{blue}{1} \]
    9. Step-by-step derivation
      1. Applied rewrites62.4%

        \[\leadsto \color{blue}{1} \]

      if 2 < (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))))

      1. Initial program 98.5%

        \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      2. Step-by-step derivation
        1. lift-pow.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        2. unpow2N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        3. lift-/.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        4. lift-*.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        5. associate-/l*N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        6. lift-/.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        7. lift-*.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        8. associate-/l*N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        9. swap-sqrN/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        10. metadata-evalN/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        11. metadata-evalN/A

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

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        13. metadata-evalN/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        14. lower-*.f64N/A

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

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
        16. lower-/.f6498.5

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      3. Applied rewrites98.5%

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      4. Step-by-step derivation
        1. lift-pow.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{{\sin kx}^{2}} + {\sin ky}^{2}\right)}}\right)} \]
        2. unpow2N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}\right)}}\right)} \]
        3. lift-sin.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx} \cdot \sin kx + {\sin ky}^{2}\right)}}\right)} \]
        4. lift-sin.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin kx \cdot \color{blue}{\sin kx} + {\sin ky}^{2}\right)}}\right)} \]
        5. sqr-sin-a-revN/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
        6. lift-*.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
        7. lift-cos.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
        8. lift-*.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
        9. lift--.f6498.5

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
        10. lift-*.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
        11. *-commutativeN/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot kx\right) \cdot \frac{1}{2}}\right) + {\sin ky}^{2}\right)}}\right)} \]
        12. lower-*.f6498.5

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \color{blue}{\cos \left(2 \cdot kx\right) \cdot 0.5}\right) + {\sin ky}^{2}\right)}}\right)} \]
        13. lift-*.f64N/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
        14. count-2-revN/A

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(kx + kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
        15. lower-+.f6498.5

          \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \color{blue}{\left(kx + kx\right)} \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
      5. Applied rewrites98.5%

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right)} + {\sin ky}^{2}\right)}}\right)} \]
      6. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \left(kx + kx\right) \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
        2. metadata-eval98.5

          \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
      7. Applied rewrites98.5%

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
      8. Taylor expanded in l around inf

        \[\leadsto \color{blue}{\sqrt{\frac{1}{2}}} \]
      9. Step-by-step derivation
        1. lower-sqrt.f6456.1

          \[\leadsto \sqrt{0.5} \]
      10. Applied rewrites56.1%

        \[\leadsto \color{blue}{\sqrt{0.5}} \]
    10. Recombined 2 regimes into one program.
    11. Add Preprocessing

    Alternative 6: 62.4% accurate, 142.7× speedup?

    \[\begin{array}{l} kx_m = \left|kx\right| \\ ky_m = \left|ky\right| \\ [l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\ \\ 1 \end{array} \]
    kx_m = (fabs.f64 kx)
    ky_m = (fabs.f64 ky)
    NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
    (FPCore (l Om kx_m ky_m) :precision binary64 1.0)
    kx_m = fabs(kx);
    ky_m = fabs(ky);
    assert(l < Om && Om < kx_m && kx_m < ky_m);
    double code(double l, double Om, double kx_m, double ky_m) {
    	return 1.0;
    }
    
    kx_m =     private
    ky_m =     private
    NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
    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(l, om, kx_m, ky_m)
    use fmin_fmax_functions
        real(8), intent (in) :: l
        real(8), intent (in) :: om
        real(8), intent (in) :: kx_m
        real(8), intent (in) :: ky_m
        code = 1.0d0
    end function
    
    kx_m = Math.abs(kx);
    ky_m = Math.abs(ky);
    assert l < Om && Om < kx_m && kx_m < ky_m;
    public static double code(double l, double Om, double kx_m, double ky_m) {
    	return 1.0;
    }
    
    kx_m = math.fabs(kx)
    ky_m = math.fabs(ky)
    [l, Om, kx_m, ky_m] = sort([l, Om, kx_m, ky_m])
    def code(l, Om, kx_m, ky_m):
    	return 1.0
    
    kx_m = abs(kx)
    ky_m = abs(ky)
    l, Om, kx_m, ky_m = sort([l, Om, kx_m, ky_m])
    function code(l, Om, kx_m, ky_m)
    	return 1.0
    end
    
    kx_m = abs(kx);
    ky_m = abs(ky);
    l, Om, kx_m, ky_m = num2cell(sort([l, Om, kx_m, ky_m])){:}
    function tmp = code(l, Om, kx_m, ky_m)
    	tmp = 1.0;
    end
    
    kx_m = N[Abs[kx], $MachinePrecision]
    ky_m = N[Abs[ky], $MachinePrecision]
    NOTE: l, Om, kx_m, and ky_m should be sorted in increasing order before calling this function.
    code[l_, Om_, kx$95$m_, ky$95$m_] := 1.0
    
    \begin{array}{l}
    kx_m = \left|kx\right|
    \\
    ky_m = \left|ky\right|
    \\
    [l, Om, kx_m, ky_m] = \mathsf{sort}([l, Om, kx_m, ky_m])\\
    \\
    1
    \end{array}
    
    Derivation
    1. Initial program 98.5%

      \[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    2. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{{\left(\frac{2 \cdot \ell}{Om}\right)}^{2}} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\frac{2 \cdot \ell}{Om} \cdot \frac{2 \cdot \ell}{Om}\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\frac{2 \cdot \ell}{Om}} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\frac{\color{blue}{2 \cdot \ell}}{Om} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      5. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)} \cdot \frac{2 \cdot \ell}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-/.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\frac{2 \cdot \ell}{Om}}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \frac{\color{blue}{2 \cdot \ell}}{Om}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      8. associate-/l*N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\left(2 \cdot \frac{\ell}{Om}\right) \cdot \color{blue}{\left(2 \cdot \frac{\ell}{Om}\right)}\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      9. swap-sqrN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(\left(2 \cdot 2\right) \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      11. metadata-evalN/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left({2}^{2} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      13. metadata-evalN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(\color{blue}{4} \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      14. lower-*.f64N/A

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

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\color{blue}{\frac{\ell}{Om}} \cdot \frac{\ell}{Om}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
      16. lower-/.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \color{blue}{\frac{\ell}{Om}}\right)\right) \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    3. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \color{blue}{\left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right)} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)} \]
    4. Step-by-step derivation
      1. lift-pow.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{{\sin kx}^{2}} + {\sin ky}^{2}\right)}}\right)} \]
      2. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\sin kx} \cdot \sin kx + {\sin ky}^{2}\right)}}\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\sin kx \cdot \color{blue}{\sin kx} + {\sin ky}^{2}\right)}}\right)} \]
      5. sqr-sin-a-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \cos \color{blue}{\left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \frac{1}{2} \cdot \color{blue}{\cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      9. lift--.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot kx\right)\right)} + {\sin ky}^{2}\right)}}\right)} \]
      10. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\frac{1}{2} \cdot \cos \left(2 \cdot kx\right)}\right) + {\sin ky}^{2}\right)}}\right)} \]
      11. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \color{blue}{\cos \left(2 \cdot kx\right) \cdot \frac{1}{2}}\right) + {\sin ky}^{2}\right)}}\right)} \]
      12. lower-*.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \color{blue}{\cos \left(2 \cdot kx\right) \cdot 0.5}\right) + {\sin ky}^{2}\right)}}\right)} \]
      13. lift-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(2 \cdot kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      14. count-2-revN/A

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \color{blue}{\left(kx + kx\right)} \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      15. lower-+.f6498.5

        \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \color{blue}{\left(kx + kx\right)} \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    5. Applied rewrites98.5%

      \[\leadsto \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\color{blue}{\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right)} + {\sin ky}^{2}\right)}}\right)} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{2}} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(\frac{1}{2} - \cos \left(kx + kx\right) \cdot \frac{1}{2}\right) + {\sin ky}^{2}\right)}}\right)} \]
      2. metadata-eval98.5

        \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    7. Applied rewrites98.5%

      \[\leadsto \sqrt{\color{blue}{0.5} \cdot \left(1 + \frac{1}{\sqrt{1 + \left(4 \cdot \left(\frac{\ell}{Om} \cdot \frac{\ell}{Om}\right)\right) \cdot \left(\left(0.5 - \cos \left(kx + kx\right) \cdot 0.5\right) + {\sin ky}^{2}\right)}}\right)} \]
    8. Taylor expanded in l around 0

      \[\leadsto \color{blue}{1} \]
    9. Step-by-step derivation
      1. Applied rewrites62.4%

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

      Reproduce

      ?
      herbie shell --seed 2025140 
      (FPCore (l Om kx ky)
        :name "Toniolo and Linder, Equation (3a)"
        :precision binary64
        (sqrt (* (/ 1.0 2.0) (+ 1.0 (/ 1.0 (sqrt (+ 1.0 (* (pow (/ (* 2.0 l) Om) 2.0) (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0))))))))))