Toniolo and Linder, Equation (3b), real

Percentage Accurate: 93.9% → 99.7%

Time: 13.5s

Alternatives: 22

Speedup: 1.2×

Specification

Math

\[\begin{array}{l} \\ \frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \end{array} \]

FPCore

(FPCore (kx ky th)
 :precision binary64
 (* (/ (sin ky) (sqrt (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0)))) (sin th)))

C

double code(double kx, double ky, double th) {
	return (sin(ky) / sqrt((pow(sin(kx), 2.0) + pow(sin(ky), 2.0)))) * sin(th);
}

Fortran

real(8) function code(kx, ky, th)
    real(8), intent (in) :: kx
    real(8), intent (in) :: ky
    real(8), intent (in) :: th
    code = (sin(ky) / sqrt(((sin(kx) ** 2.0d0) + (sin(ky) ** 2.0d0)))) * sin(th)
end function

Java

public static double code(double kx, double ky, double th) {
	return (Math.sin(ky) / Math.sqrt((Math.pow(Math.sin(kx), 2.0) + Math.pow(Math.sin(ky), 2.0)))) * Math.sin(th);
}

Python

def code(kx, ky, th):
	return (math.sin(ky) / math.sqrt((math.pow(math.sin(kx), 2.0) + math.pow(math.sin(ky), 2.0)))) * math.sin(th)

Julia

function code(kx, ky, th)
	return Float64(Float64(sin(ky) / sqrt(Float64((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))) * sin(th))
end

MATLAB

function tmp = code(kx, ky, th)
	tmp = (sin(ky) / sqrt(((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))) * sin(th);
end

Wolfram

code[kx_, ky_, th_] := N[(N[(N[Sin[ky], $MachinePrecision] / N[Sqrt[N[(N[Power[N[Sin[kx], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Sin[th], $MachinePrecision]), $MachinePrecision]

Initial Program: 93.9% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \end{array} \]

FPCore

(FPCore (kx ky th)
 :precision binary64
 (* (/ (sin ky) (sqrt (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0)))) (sin th)))

C

double code(double kx, double ky, double th) {
	return (sin(ky) / sqrt((pow(sin(kx), 2.0) + pow(sin(ky), 2.0)))) * sin(th);
}

Fortran

real(8) function code(kx, ky, th)
    real(8), intent (in) :: kx
    real(8), intent (in) :: ky
    real(8), intent (in) :: th
    code = (sin(ky) / sqrt(((sin(kx) ** 2.0d0) + (sin(ky) ** 2.0d0)))) * sin(th)
end function

Java

public static double code(double kx, double ky, double th) {
	return (Math.sin(ky) / Math.sqrt((Math.pow(Math.sin(kx), 2.0) + Math.pow(Math.sin(ky), 2.0)))) * Math.sin(th);
}

Python

def code(kx, ky, th):
	return (math.sin(ky) / math.sqrt((math.pow(math.sin(kx), 2.0) + math.pow(math.sin(ky), 2.0)))) * math.sin(th)

Julia

function code(kx, ky, th)
	return Float64(Float64(sin(ky) / sqrt(Float64((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))) * sin(th))
end

MATLAB

function tmp = code(kx, ky, th)
	tmp = (sin(ky) / sqrt(((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0)))) * sin(th);
end

Wolfram

code[kx_, ky_, th_] := N[(N[(N[Sin[ky], $MachinePrecision] / N[Sqrt[N[(N[Power[N[Sin[kx], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Sin[th], $MachinePrecision]), $MachinePrecision]

Alternative 1: 99.7% accurate, 1.2× speedup

Math

\[\begin{array}{l} \\ \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th \end{array} \]

FPCore

(FPCore (kx ky th)
 :precision binary64
 (* (/ (sin ky) (hypot (sin ky) (sin kx))) (sin th)))

C

double code(double kx, double ky, double th) {
	return (sin(ky) / hypot(sin(ky), sin(kx))) * sin(th);
}

Java

public static double code(double kx, double ky, double th) {
	return (Math.sin(ky) / Math.hypot(Math.sin(ky), Math.sin(kx))) * Math.sin(th);
}

Python

def code(kx, ky, th):
	return (math.sin(ky) / math.hypot(math.sin(ky), math.sin(kx))) * math.sin(th)

Julia

function code(kx, ky, th)
	return Float64(Float64(sin(ky) / hypot(sin(ky), sin(kx))) * sin(th))
end

MATLAB

function tmp = code(kx, ky, th)
	tmp = (sin(ky) / hypot(sin(ky), sin(kx))) * sin(th);
end

Wolfram

code[kx_, ky_, th_] := N[(N[(N[Sin[ky], $MachinePrecision] / N[Sqrt[N[Sin[ky], $MachinePrecision] ^ 2 + N[Sin[kx], $MachinePrecision] ^ 2], $MachinePrecision]), $MachinePrecision] * N[Sin[th], $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 94.6%

   \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
2. Add Preprocessing
3. Step-by-step derivation

   1. lift-sqrt.f64 N/A

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \cdot \sin th \]

   2. lift-+.f64 N/A

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}} \cdot \sin th \]

   3. +-commutative N/A

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]

   4. lift-pow.f64 N/A

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2}} + {\sin kx}^{2}}} \cdot \sin th \]

   5. unpow2 N/A

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]

   6. lift-pow.f64 N/A

      \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{{\sin kx}^{2}}}} \cdot \sin th \]

   7. unpow2 N/A

      \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]

   8. lower-hypot.f64 99.7

      \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]

4. Applied rewrites 99.7%

   \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
5. Add Preprocessing

Alternative 2: 68.3% accurate, 0.2× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := 1 - \cos \left(kx \cdot -2\right)\\ t_2 := \frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}\\ t_3 := \mathsf{fma}\left(-0.5, \cos \left(ky \cdot -2\right), 0.5\right)\\ t_4 := \left(\sin ky \cdot th\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(0.5, t\_1, t\_3\right)}}\\ \mathbf{if}\;t\_2 \leq -0.9985:\\ \;\;\;\;\frac{\sin ky \cdot \sin th}{\sqrt{t\_3}}\\ \mathbf{elif}\;t\_2 \leq -0.06:\\ \;\;\;\;t\_4\\ \mathbf{elif}\;t\_2 \leq 5 \cdot 10^{-119}:\\ \;\;\;\;\sin ky \cdot \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{t\_1}}\right)\\ \mathbf{elif}\;t\_2 \leq 5 \cdot 10^{-53}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\sin kx}\\ \mathbf{elif}\;t\_2 \leq 0.02:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\sqrt{\mathsf{fma}\left(1 - \cos \left(kx + kx\right), 0.5, ky \cdot ky\right)}}\\ \mathbf{elif}\;t\_2 \leq 0.997870194364524:\\ \;\;\;\;t\_4\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \end{array} \]

FPCore

(FPCore (kx ky th)
 :precision binary64
 (let* ((t_1 (- 1.0 (cos (* kx -2.0))))
        (t_2 (/ (sin ky) (sqrt (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0)))))
        (t_3 (fma -0.5 (cos (* ky -2.0)) 0.5))
        (t_4 (* (* (sin ky) th) (sqrt (/ 1.0 (fma 0.5 t_1 t_3))))))
   (if (<= t_2 -0.9985)
     (/ (* (sin ky) (sin th)) (sqrt t_3))
     (if (<= t_2 -0.06)
       t_4
       (if (<= t_2 5e-119)
         (* (sin ky) (* (* (sin th) (sqrt 2.0)) (sqrt (/ 1.0 t_1))))
         (if (<= t_2 5e-53)
           (* (sin ky) (/ (sin th) (sin kx)))
           (if (<= t_2 0.02)
             (*
              (sin ky)
              (/ (sin th) (sqrt (fma (- 1.0 (cos (+ kx kx))) 0.5 (* ky ky)))))
             (if (<= t_2 0.997870194364524) t_4 (sin th)))))))))

C

double code(double kx, double ky, double th) {
	double t_1 = 1.0 - cos((kx * -2.0));
	double t_2 = sin(ky) / sqrt((pow(sin(kx), 2.0) + pow(sin(ky), 2.0)));
	double t_3 = fma(-0.5, cos((ky * -2.0)), 0.5);
	double t_4 = (sin(ky) * th) * sqrt((1.0 / fma(0.5, t_1, t_3)));
	double tmp;
	if (t_2 <= -0.9985) {
		tmp = (sin(ky) * sin(th)) / sqrt(t_3);
	} else if (t_2 <= -0.06) {
		tmp = t_4;
	} else if (t_2 <= 5e-119) {
		tmp = sin(ky) * ((sin(th) * sqrt(2.0)) * sqrt((1.0 / t_1)));
	} else if (t_2 <= 5e-53) {
		tmp = sin(ky) * (sin(th) / sin(kx));
	} else if (t_2 <= 0.02) {
		tmp = sin(ky) * (sin(th) / sqrt(fma((1.0 - cos((kx + kx))), 0.5, (ky * ky))));
	} else if (t_2 <= 0.997870194364524) {
		tmp = t_4;
	} else {
		tmp = sin(th);
	}
	return tmp;
}

Julia

function code(kx, ky, th)
	t_1 = Float64(1.0 - cos(Float64(kx * -2.0)))
	t_2 = Float64(sin(ky) / sqrt(Float64((sin(kx) ^ 2.0) + (sin(ky) ^ 2.0))))
	t_3 = fma(-0.5, cos(Float64(ky * -2.0)), 0.5)
	t_4 = Float64(Float64(sin(ky) * th) * sqrt(Float64(1.0 / fma(0.5, t_1, t_3))))
	tmp = 0.0
	if (t_2 <= -0.9985)
		tmp = Float64(Float64(sin(ky) * sin(th)) / sqrt(t_3));
	elseif (t_2 <= -0.06)
		tmp = t_4;
	elseif (t_2 <= 5e-119)
		tmp = Float64(sin(ky) * Float64(Float64(sin(th) * sqrt(2.0)) * sqrt(Float64(1.0 / t_1))));
	elseif (t_2 <= 5e-53)
		tmp = Float64(sin(ky) * Float64(sin(th) / sin(kx)));
	elseif (t_2 <= 0.02)
		tmp = Float64(sin(ky) * Float64(sin(th) / sqrt(fma(Float64(1.0 - cos(Float64(kx + kx))), 0.5, Float64(ky * ky)))));
	elseif (t_2 <= 0.997870194364524)
		tmp = t_4;
	else
		tmp = sin(th);
	end
	return tmp
end

Wolfram

code[kx_, ky_, th_] := Block[{t$95$1 = N[(1.0 - N[Cos[N[(kx * -2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sin[ky], $MachinePrecision] / N[Sqrt[N[(N[Power[N[Sin[kx], $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[Sin[ky], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(-0.5 * N[Cos[N[(ky * -2.0), $MachinePrecision]], $MachinePrecision] + 0.5), $MachinePrecision]}, Block[{t$95$4 = N[(N[(N[Sin[ky], $MachinePrecision] * th), $MachinePrecision] * N[Sqrt[N[(1.0 / N[(0.5 * t$95$1 + t$95$3), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$2, -0.9985], N[(N[(N[Sin[ky], $MachinePrecision] * N[Sin[th], $MachinePrecision]), $MachinePrecision] / N[Sqrt[t$95$3], $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, -0.06], t$95$4, If[LessEqual[t$95$2, 5e-119], N[(N[Sin[ky], $MachinePrecision] * N[(N[(N[Sin[th], $MachinePrecision] * N[Sqrt[2.0], $MachinePrecision]), $MachinePrecision] * N[Sqrt[N[(1.0 / t$95$1), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, 5e-53], N[(N[Sin[ky], $MachinePrecision] * N[(N[Sin[th], $MachinePrecision] / N[Sin[kx], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, 0.02], N[(N[Sin[ky], $MachinePrecision] * N[(N[Sin[th], $MachinePrecision] / N[Sqrt[N[(N[(1.0 - N[Cos[N[(kx + kx), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * 0.5 + N[(ky * ky), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, 0.997870194364524], t$95$4, N[Sin[th], $MachinePrecision]]]]]]]]]]]

Derivation

1. Split input into 6 regimes

2. if (/.f64 (sin.f64 ky) (sqrt.f64 (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))) < -0.998500000000000054

   1. Initial program 85.3%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th} \]

      2. lift-/.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \cdot \sin th \]

      3. associate-*l/ N/A

         \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      4. associate-/l* N/A

         \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

      6. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

   4. Applied rewrites 62.4%

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

   5. Taylor expanded in kx around 0

      \[\leadsto \color{blue}{\left(\sin ky \cdot \sin th\right) \cdot \sqrt{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}}} \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(\sin ky \cdot \sin th\right) \cdot \sqrt{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}}} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\left(\sin th \cdot \sin ky\right)} \cdot \sqrt{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}} \]

      3. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(\sin th \cdot \sin ky\right)} \cdot \sqrt{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}} \]

      4. lower-sin.f64 N/A

         \[\leadsto \left(\color{blue}{\sin th} \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}} \]

      5. lower-sin.f64 N/A

         \[\leadsto \left(\sin th \cdot \color{blue}{\sin ky}\right) \cdot \sqrt{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}} \]

      6. lower-sqrt.f64 N/A

         \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \color{blue}{\sqrt{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}}} \]

      7. lower-/.f64 N/A

         \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\color{blue}{\frac{1}{\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)}}} \]

      8. +-commutative N/A

         \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\color{blue}{\frac{-1}{2} \cdot \cos \left(2 \cdot ky\right) + \frac{1}{2}}}} \]

      9. metadata-eval N/A

         \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\frac{-1}{2} \cdot \cos \left(\color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot ky\right) + \frac{1}{2}}} \]

      10. distribute-lft-neg-in N/A

          \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\frac{-1}{2} \cdot \cos \color{blue}{\left(\mathsf{neg}\left(-2 \cdot ky\right)\right)} + \frac{1}{2}}} \]

      11. lower-fma.f64 N/A

          \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\color{blue}{\mathsf{fma}\left(\frac{-1}{2}, \cos \left(\mathsf{neg}\left(-2 \cdot ky\right)\right), \frac{1}{2}\right)}}} \]

      12. cos-neg N/A

          \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\frac{-1}{2}, \color{blue}{\cos \left(-2 \cdot ky\right)}, \frac{1}{2}\right)}} \]

      13. lower-cos.f64 N/A

          \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\frac{-1}{2}, \color{blue}{\cos \left(-2 \cdot ky\right)}, \frac{1}{2}\right)}} \]

      14. *-commutative N/A

          \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\frac{-1}{2}, \cos \color{blue}{\left(ky \cdot -2\right)}, \frac{1}{2}\right)}} \]

      15. lower-*.f64 61.3

          \[\leadsto \left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(-0.5, \cos \color{blue}{\left(ky \cdot -2\right)}, 0.5\right)}} \]

   7. Applied rewrites 61.3%

      \[\leadsto \color{blue}{\left(\sin th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(-0.5, \cos \left(ky \cdot -2\right), 0.5\right)}}} \]
   8. Step-by-step derivation

   9. Applied rewrites 61.4%

      \[\leadsto \color{blue}{\frac{\sin th \cdot \sin ky}{\sqrt{\mathsf{fma}\left(-0.5, \cos \left(ky \cdot -2\right), 0.5\right)}}} \]

   if -0.998500000000000054 < (/.f64 (sin.f64 ky) (sqrt.f64 (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))) < -0.059999999999999998 or 0.0200000000000000004 < (/.f64 (sin.f64 ky) (sqrt.f64 (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))) < 0.997870194364523955

   1. Initial program 99.1%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th} \]

      2. lift-/.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \cdot \sin th \]

      3. associate-*l/ N/A

         \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      4. associate-/l* N/A

         \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

      6. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

   4. Applied rewrites 98.6%

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

   5. Taylor expanded in th around 0

      \[\leadsto \color{blue}{\left(th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\frac{1}{2} + \left(\frac{-1}{2} \cdot \cos \left(2 \cdot ky\right) + \frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right)\right)}}} \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\frac{1}{2} + \left(\frac{-1}{2} \cdot \cos \left(2 \cdot ky\right) + \frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right)\right)}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(th \cdot \sin ky\right)} \cdot \sqrt{\frac{1}{\frac{1}{2} + \left(\frac{-1}{2} \cdot \cos \left(2 \cdot ky\right) + \frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right)\right)}} \]

      3. lower-sin.f64 N/A

         \[\leadsto \left(th \cdot \color{blue}{\sin ky}\right) \cdot \sqrt{\frac{1}{\frac{1}{2} + \left(\frac{-1}{2} \cdot \cos \left(2 \cdot ky\right) + \frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right)\right)}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \left(th \cdot \sin ky\right) \cdot \color{blue}{\sqrt{\frac{1}{\frac{1}{2} + \left(\frac{-1}{2} \cdot \cos \left(2 \cdot ky\right) + \frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right)\right)}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \left(th \cdot \sin ky\right) \cdot \sqrt{\color{blue}{\frac{1}{\frac{1}{2} + \left(\frac{-1}{2} \cdot \cos \left(2 \cdot ky\right) + \frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right)\right)}}} \]

      6. associate-+r+ N/A

         \[\leadsto \left(th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\color{blue}{\left(\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)\right) + \frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right)}}} \]

      7. +-commutative N/A

         \[\leadsto \left(th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\color{blue}{\frac{1}{2} \cdot \left(1 - \cos \left(2 \cdot kx\right)\right) + \left(\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}}} \]

      8. lower-fma.f64 N/A

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

      9. metadata-eval N/A

         \[\leadsto \left(th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\frac{1}{2}, 1 - \cos \left(\color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot kx\right), \frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}} \]

      10. distribute-lft-neg-in N/A

          \[\leadsto \left(th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\frac{1}{2}, 1 - \cos \color{blue}{\left(\mathsf{neg}\left(-2 \cdot kx\right)\right)}, \frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}} \]

      11. lower--.f64 N/A

          \[\leadsto \left(th \cdot \sin ky\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\frac{1}{2}, \color{blue}{1 - \cos \left(\mathsf{neg}\left(-2 \cdot kx\right)\right)}, \frac{1}{2} + \frac{-1}{2} \cdot \cos \left(2 \cdot ky\right)\right)}} \]

      12. cos-neg N/A

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

      13. lower-cos.f64 N/A

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

      14. *-commutative N/A

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

      15. lower-*.f64 N/A

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

      16. +-commutative N/A

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

   7. Applied rewrites 50.8%

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

   if -0.059999999999999998 < (/.f64 (sin.f64 ky) (sqrt.f64 (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))) < 4.99999999999999993e-119

   1. Initial program 99.4%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th} \]

      2. lift-/.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \cdot \sin th \]

      3. associate-*l/ N/A

         \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      4. associate-/l* N/A

         \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

      6. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

   4. Applied rewrites 75.3%

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

   5. Taylor expanded in ky around 0

      \[\leadsto \color{blue}{\left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \left(2 \cdot kx\right)}}\right)} \cdot \sin ky \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \left(2 \cdot kx\right)}}\right)} \cdot \sin ky \]

      2. lower-*.f64 N/A

         \[\leadsto \left(\color{blue}{\left(\sin th \cdot \sqrt{2}\right)} \cdot \sqrt{\frac{1}{1 - \cos \left(2 \cdot kx\right)}}\right) \cdot \sin ky \]

      3. lower-sin.f64 N/A

         \[\leadsto \left(\left(\color{blue}{\sin th} \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \left(2 \cdot kx\right)}}\right) \cdot \sin ky \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \left(\left(\sin th \cdot \color{blue}{\sqrt{2}}\right) \cdot \sqrt{\frac{1}{1 - \cos \left(2 \cdot kx\right)}}\right) \cdot \sin ky \]

      5. lower-sqrt.f64 N/A

         \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \color{blue}{\sqrt{\frac{1}{1 - \cos \left(2 \cdot kx\right)}}}\right) \cdot \sin ky \]

      6. lower-/.f64 N/A

         \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\color{blue}{\frac{1}{1 - \cos \left(2 \cdot kx\right)}}}\right) \cdot \sin ky \]

      7. metadata-eval N/A

         \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \left(\color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot kx\right)}}\right) \cdot \sin ky \]

      8. distribute-lft-neg-in N/A

         \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \color{blue}{\left(\mathsf{neg}\left(-2 \cdot kx\right)\right)}}}\right) \cdot \sin ky \]

      9. lower--.f64 N/A

         \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{\color{blue}{1 - \cos \left(\mathsf{neg}\left(-2 \cdot kx\right)\right)}}}\right) \cdot \sin ky \]

      10. cos-neg N/A

          \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \color{blue}{\cos \left(-2 \cdot kx\right)}}}\right) \cdot \sin ky \]

      11. lower-cos.f64 N/A

          \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \color{blue}{\cos \left(-2 \cdot kx\right)}}}\right) \cdot \sin ky \]

      12. *-commutative N/A

          \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \color{blue}{\left(kx \cdot -2\right)}}}\right) \cdot \sin ky \]

      13. lower-*.f64 74.1

          \[\leadsto \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \color{blue}{\left(kx \cdot -2\right)}}}\right) \cdot \sin ky \]

   7. Applied rewrites 74.1%

      \[\leadsto \color{blue}{\left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \left(kx \cdot -2\right)}}\right)} \cdot \sin ky \]

   if 4.99999999999999993e-119 < (/.f64 (sin.f64 ky) (sqrt.f64 (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))) < 5e-53

   1. Initial program 98.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th} \]

      2. lift-/.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \cdot \sin th \]

      3. associate-*l/ N/A

         \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      4. associate-/l* N/A

         \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

      6. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

   4. Applied rewrites 66.0%

      \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{\mathsf{fma}\left(1 - \cos \left(kx + kx\right), 0.5, 0.5 + -0.5 \cdot \cos \left(ky + ky\right)\right)}} \cdot \sin ky} \]
   5. Step-by-step derivation

      1. lift-fma.f64 N/A

         \[\leadsto \frac{\sin th}{\sqrt{\color{blue}{\left(1 - \cos \left(kx + kx\right)\right) \cdot \frac{1}{2} + \left(\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(ky + ky\right)\right)}}} \cdot \sin ky \]

      2. +-commutative N/A

         \[\leadsto \frac{\sin th}{\sqrt{\color{blue}{\left(\frac{1}{2} + \frac{-1}{2} \cdot \cos \left(ky + ky\right)\right) + \left(1 - \cos \left(kx + kx\right)\right) \cdot \frac{1}{2}}}} \cdot \sin ky \]

   6. Applied rewrites 98.8%

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

   7. Taylor expanded in ky around 0

      \[\leadsto \frac{\sin th}{\color{blue}{\sin kx}} \cdot \sin ky \]
   8. Step-by-step derivation

      1. lower-sin.f64 53.5

         \[\leadsto \frac{\sin th}{\color{blue}{\sin kx}} \cdot \sin ky \]

   9. Applied rewrites 53.5%

      \[\leadsto \frac{\sin th}{\color{blue}{\sin kx}} \cdot \sin ky \]

   if 5e-53 < (/.f64 (sin.f64 ky) (sqrt.f64 (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64))))) < 0.0200000000000000004

   1. Initial program 98.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th} \]

      2. lift-/.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \cdot \sin th \]

      3. associate-*l/ N/A

         \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      4. associate-/l* N/A

         \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

      6. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin ky} \]

   4. Applied rewrites 68.1%

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

   5. Taylor expanded in ky around 0

      \[\leadsto \frac{\sin th}{\sqrt{\mathsf{fma}\left(1 - \cos \left(kx + kx\right), \frac{1}{2}, \color{blue}{{ky}^{2}}\right)}} \cdot \sin ky \]
   6. Step-by-step derivation

      1. unpow2 N/A

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

      2. lower-*.f64 63.3

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

   7. Applied rewrites 63.3%

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

   if 0.997870194364523955 < (/.f64 (sin.f64 ky) (sqrt.f64 (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64)))))

   1. Initial program 87.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
   2. Add Preprocessing

   3. Taylor expanded in kx around 0

      \[\leadsto \color{blue}{\sin th} \]
   4. Step-by-step derivation

      1. lower-sin.f64 91.7

         \[\leadsto \color{blue}{\sin th} \]

   5. Applied rewrites 91.7%

      \[\leadsto \color{blue}{\sin th} \]
3. Recombined 6 regimes into one program.

4. Final simplification 68.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \leq -0.9985:\\ \;\;\;\;\frac{\sin ky \cdot \sin th}{\sqrt{\mathsf{fma}\left(-0.5, \cos \left(ky \cdot -2\right), 0.5\right)}}\\ \mathbf{elif}\;\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \leq -0.06:\\ \;\;\;\;\left(\sin ky \cdot th\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(0.5, 1 - \cos \left(kx \cdot -2\right), \mathsf{fma}\left(-0.5, \cos \left(ky \cdot -2\right), 0.5\right)\right)}}\\ \mathbf{elif}\;\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \leq 5 \cdot 10^{-119}:\\ \;\;\;\;\sin ky \cdot \left(\left(\sin th \cdot \sqrt{2}\right) \cdot \sqrt{\frac{1}{1 - \cos \left(kx \cdot -2\right)}}\right)\\ \mathbf{elif}\;\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \leq 5 \cdot 10^{-53}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\sin kx}\\ \mathbf{elif}\;\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \leq 0.02:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\sqrt{\mathsf{fma}\left(1 - \cos \left(kx + kx\right), 0.5, ky \cdot ky\right)}}\\ \mathbf{elif}\;\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \leq 0.997870194364524:\\ \;\;\;\;\left(\sin ky \cdot th\right) \cdot \sqrt{\frac{1}{\mathsf{fma}\left(0.5, 1 - \cos \left(kx \cdot -2\right), \mathsf{fma}\left(-0.5, \cos \left(ky \cdot -2\right), 0.5\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
5. Add Preprocessing

Reproduce

herbie shell --seed 2024227 
(FPCore (kx ky th)
  :name "Toniolo and Linder, Equation (3b), real"
  :precision binary64
  (* (/ (sin ky) (sqrt (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0)))) (sin th)))