Toniolo and Linder, Equation (10+)

Average Accuracy: 55.9% → 92.4%

Time: 38.5s

Precision: binary64

Cost: 59540

• 27.5% of points produce a very large (infinite) output. You may want to add a precondition.

Math

\[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]

↓

\[\begin{array}{l} t_1 := \sin k \cdot \tan k\\ t_2 := {\left(\frac{1}{\left(\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \sin k} \cdot \sqrt[3]{\tan k}\right) \cdot \sqrt[3]{0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3}\\ \mathbf{if}\;t \leq -4.4 \cdot 10^{-20}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t \leq -6 \cdot 10^{-105}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot \left(k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\right)}\\ \mathbf{elif}\;t \leq -5.1 \cdot 10^{-160}:\\ \;\;\;\;2 \cdot \frac{\frac{\ell}{\frac{t}{\ell} \cdot \left(k \cdot k\right)}}{t_1}\\ \mathbf{elif}\;t \leq -2.15 \cdot 10^{-206}:\\ \;\;\;\;\frac{2}{t_1 \cdot \left(t \cdot \left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)\right)}\\ \mathbf{elif}\;t \leq 6.8 \cdot 10^{-87}:\\ \;\;\;\;\frac{2}{t_1 \cdot \left(k \cdot \frac{1}{\frac{\ell}{k \cdot \frac{t}{\ell}}}\right)}\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

FPCore

(FPCore (t l k)
 :precision binary64
 (/
  2.0
  (*
   (* (* (/ (pow t 3.0) (* l l)) (sin k)) (tan k))
   (+ (+ 1.0 (pow (/ k t) 2.0)) 1.0))))

↓

(FPCore (t l k)
 :precision binary64
 (let* ((t_1 (* (sin k) (tan k)))
        (t_2
         (pow
          (*
           (/
            1.0
            (*
             (* (cbrt (* (+ 2.0 (pow (/ k t) 2.0)) (sin k))) (cbrt (tan k)))
             (cbrt 0.5)))
           (/ (pow (cbrt l) 2.0) t))
          3.0)))
   (if (<= t -4.4e-20)
     t_2
     (if (<= t -6e-105)
       (/ 2.0 (* (/ k l) (* k (* (tan k) (* (sin k) (/ t l))))))
       (if (<= t -5.1e-160)
         (* 2.0 (/ (/ l (* (/ t l) (* k k))) t_1))
         (if (<= t -2.15e-206)
           (/ 2.0 (* t_1 (* t (* (/ k l) (/ k l)))))
           (if (<= t 6.8e-87)
             (/ 2.0 (* t_1 (* k (/ 1.0 (/ l (* k (/ t l)))))))
             t_2)))))))

C

double code(double t, double l, double k) {
	return 2.0 / ((((pow(t, 3.0) / (l * l)) * sin(k)) * tan(k)) * ((1.0 + pow((k / t), 2.0)) + 1.0));
}

↓

double code(double t, double l, double k) {
	double t_1 = sin(k) * tan(k);
	double t_2 = pow(((1.0 / ((cbrt(((2.0 + pow((k / t), 2.0)) * sin(k))) * cbrt(tan(k))) * cbrt(0.5))) * (pow(cbrt(l), 2.0) / t)), 3.0);
	double tmp;
	if (t <= -4.4e-20) {
		tmp = t_2;
	} else if (t <= -6e-105) {
		tmp = 2.0 / ((k / l) * (k * (tan(k) * (sin(k) * (t / l)))));
	} else if (t <= -5.1e-160) {
		tmp = 2.0 * ((l / ((t / l) * (k * k))) / t_1);
	} else if (t <= -2.15e-206) {
		tmp = 2.0 / (t_1 * (t * ((k / l) * (k / l))));
	} else if (t <= 6.8e-87) {
		tmp = 2.0 / (t_1 * (k * (1.0 / (l / (k * (t / l))))));
	} else {
		tmp = t_2;
	}
	return tmp;
}

Java

public static double code(double t, double l, double k) {
	return 2.0 / ((((Math.pow(t, 3.0) / (l * l)) * Math.sin(k)) * Math.tan(k)) * ((1.0 + Math.pow((k / t), 2.0)) + 1.0));
}

↓

public static double code(double t, double l, double k) {
	double t_1 = Math.sin(k) * Math.tan(k);
	double t_2 = Math.pow(((1.0 / ((Math.cbrt(((2.0 + Math.pow((k / t), 2.0)) * Math.sin(k))) * Math.cbrt(Math.tan(k))) * Math.cbrt(0.5))) * (Math.pow(Math.cbrt(l), 2.0) / t)), 3.0);
	double tmp;
	if (t <= -4.4e-20) {
		tmp = t_2;
	} else if (t <= -6e-105) {
		tmp = 2.0 / ((k / l) * (k * (Math.tan(k) * (Math.sin(k) * (t / l)))));
	} else if (t <= -5.1e-160) {
		tmp = 2.0 * ((l / ((t / l) * (k * k))) / t_1);
	} else if (t <= -2.15e-206) {
		tmp = 2.0 / (t_1 * (t * ((k / l) * (k / l))));
	} else if (t <= 6.8e-87) {
		tmp = 2.0 / (t_1 * (k * (1.0 / (l / (k * (t / l))))));
	} else {
		tmp = t_2;
	}
	return tmp;
}

Julia

function code(t, l, k)
	return Float64(2.0 / Float64(Float64(Float64(Float64((t ^ 3.0) / Float64(l * l)) * sin(k)) * tan(k)) * Float64(Float64(1.0 + (Float64(k / t) ^ 2.0)) + 1.0)))
end

↓

function code(t, l, k)
	t_1 = Float64(sin(k) * tan(k))
	t_2 = Float64(Float64(1.0 / Float64(Float64(cbrt(Float64(Float64(2.0 + (Float64(k / t) ^ 2.0)) * sin(k))) * cbrt(tan(k))) * cbrt(0.5))) * Float64((cbrt(l) ^ 2.0) / t)) ^ 3.0
	tmp = 0.0
	if (t <= -4.4e-20)
		tmp = t_2;
	elseif (t <= -6e-105)
		tmp = Float64(2.0 / Float64(Float64(k / l) * Float64(k * Float64(tan(k) * Float64(sin(k) * Float64(t / l))))));
	elseif (t <= -5.1e-160)
		tmp = Float64(2.0 * Float64(Float64(l / Float64(Float64(t / l) * Float64(k * k))) / t_1));
	elseif (t <= -2.15e-206)
		tmp = Float64(2.0 / Float64(t_1 * Float64(t * Float64(Float64(k / l) * Float64(k / l)))));
	elseif (t <= 6.8e-87)
		tmp = Float64(2.0 / Float64(t_1 * Float64(k * Float64(1.0 / Float64(l / Float64(k * Float64(t / l)))))));
	else
		tmp = t_2;
	end
	return tmp
end

Wolfram

code[t_, l_, k_] := N[(2.0 / N[(N[(N[(N[(N[Power[t, 3.0], $MachinePrecision] / N[(l * l), $MachinePrecision]), $MachinePrecision] * N[Sin[k], $MachinePrecision]), $MachinePrecision] * N[Tan[k], $MachinePrecision]), $MachinePrecision] * N[(N[(1.0 + N[Power[N[(k / t), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[t_, l_, k_] := Block[{t$95$1 = N[(N[Sin[k], $MachinePrecision] * N[Tan[k], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[Power[N[(N[(1.0 / N[(N[(N[Power[N[(N[(2.0 + N[Power[N[(k / t), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] * N[Sin[k], $MachinePrecision]), $MachinePrecision], 1/3], $MachinePrecision] * N[Power[N[Tan[k], $MachinePrecision], 1/3], $MachinePrecision]), $MachinePrecision] * N[Power[0.5, 1/3], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(N[Power[N[Power[l, 1/3], $MachinePrecision], 2.0], $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision], 3.0], $MachinePrecision]}, If[LessEqual[t, -4.4e-20], t$95$2, If[LessEqual[t, -6e-105], N[(2.0 / N[(N[(k / l), $MachinePrecision] * N[(k * N[(N[Tan[k], $MachinePrecision] * N[(N[Sin[k], $MachinePrecision] * N[(t / l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t, -5.1e-160], N[(2.0 * N[(N[(l / N[(N[(t / l), $MachinePrecision] * N[(k * k), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / t$95$1), $MachinePrecision]), $MachinePrecision], If[LessEqual[t, -2.15e-206], N[(2.0 / N[(t$95$1 * N[(t * N[(N[(k / l), $MachinePrecision] * N[(k / l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t, 6.8e-87], N[(2.0 / N[(t$95$1 * N[(k * N[(1.0 / N[(l / N[(k * N[(t / l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$2]]]]]]]

Derivation

1. Split input into 5 regimes

2. if t < -4.39999999999999982e-20 or 6.7999999999999997e-87 < t

   1. Initial program 64.8%

      \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]

   2. Simplified 66.9%

      \[\leadsto \color{blue}{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \left(\frac{\ell}{{t}^{3}} \cdot \ell\right)} \]
      Proof

      [Start] 64.8	\[ \frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]
      associate-*l* [=>] 65.4	\[ \frac{2}{\color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \left(\tan k \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)\right)}} \]
      associate-/l/ [<=] 65.6	\[ \color{blue}{\frac{\frac{2}{\tan k \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}}{\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k}} \]
      *-commutative [=>] 65.6	\[ \frac{\frac{2}{\tan k \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}}{\color{blue}{\sin k \cdot \frac{{t}^{3}}{\ell \cdot \ell}}} \]
      associate-*r/ [=>] 66.2	\[ \frac{\frac{2}{\tan k \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}}{\color{blue}{\frac{\sin k \cdot {t}^{3}}{\ell \cdot \ell}}} \]
      associate-/l* [=>] 65.6	\[ \frac{\frac{2}{\tan k \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}}{\color{blue}{\frac{\sin k}{\frac{\ell \cdot \ell}{{t}^{3}}}}} \]
      associate-/r/ [=>] 60.7	\[ \color{blue}{\frac{\frac{2}{\tan k \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}}{\sin k} \cdot \frac{\ell \cdot \ell}{{t}^{3}}} \]

   3. Applied egg-rr 81.7%

      \[\leadsto \color{blue}{{\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3}} \]
      Proof

      [Start] 66.9	\[ \frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \left(\frac{\ell}{{t}^{3}} \cdot \ell\right) \]
      add-cube-cbrt [=>] 66.8	\[ \color{blue}{\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \left(\frac{\ell}{{t}^{3}} \cdot \ell\right)} \cdot \sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \left(\frac{\ell}{{t}^{3}} \cdot \ell\right)}\right) \cdot \sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \left(\frac{\ell}{{t}^{3}} \cdot \ell\right)}} \]
      pow3 [=>] 66.7	\[ \color{blue}{{\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \left(\frac{\ell}{{t}^{3}} \cdot \ell\right)}\right)}^{3}} \]
      cbrt-prod [=>] 66.7	\[ {\color{blue}{\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \sqrt[3]{\frac{\ell}{{t}^{3}} \cdot \ell}\right)}}^{3} \]
      associate-*l/ [=>] 60.6	\[ {\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \sqrt[3]{\color{blue}{\frac{\ell \cdot \ell}{{t}^{3}}}}\right)}^{3} \]
      cbrt-div [=>] 60.6	\[ {\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \color{blue}{\frac{\sqrt[3]{\ell \cdot \ell}}{\sqrt[3]{{t}^{3}}}}\right)}^{3} \]
      cbrt-unprod [<=] 68.5	\[ {\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \frac{\color{blue}{\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}}}{\sqrt[3]{{t}^{3}}}\right)}^{3} \]
      pow2 [=>] 68.5	\[ {\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \frac{\color{blue}{{\left(\sqrt[3]{\ell}\right)}^{2}}}{\sqrt[3]{{t}^{3}}}\right)}^{3} \]
      rem-cbrt-cube [=>] 81.7	\[ {\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{\color{blue}{t}}\right)}^{3} \]

   4. Applied egg-rr 82.5%

      \[\leadsto {\left(\color{blue}{\frac{1}{\sqrt[3]{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)\right) \cdot 0.5}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      Proof

      [Start] 81.7	\[ {\left(\sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      clear-num [=>] 81.7	\[ {\left(\sqrt[3]{\color{blue}{\frac{1}{\frac{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}{2}}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      cbrt-div [=>] 82.5	\[ {\left(\color{blue}{\frac{\sqrt[3]{1}}{\sqrt[3]{\frac{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}{2}}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      metadata-eval [=>] 82.5	\[ {\left(\frac{\color{blue}{1}}{\sqrt[3]{\frac{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)}{2}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      div-inv [=>] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\color{blue}{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)\right) \cdot \frac{1}{2}}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      metadata-eval [=>] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)\right) \cdot \color{blue}{0.5}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]

   5. Simplified 82.5%

      \[\leadsto {\left(\color{blue}{\frac{1}{\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\left(\sin k \cdot \tan k\right) \cdot 0.5\right)}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      Proof

      [Start] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)\right) \cdot 0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      associate-*l* [=>] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\color{blue}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\left(\sin k \cdot \tan k\right) \cdot 0.5\right)}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]

   6. Applied egg-rr 82.5%

      \[\leadsto {\left(\frac{1}{\color{blue}{\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \sqrt[3]{0.5}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      Proof

      [Start] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\left(\sin k \cdot \tan k\right) \cdot 0.5\right)}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      associate-*r* [=>] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\color{blue}{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)\right) \cdot 0.5}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      cbrt-prod [=>] 82.5	\[ {\left(\frac{1}{\color{blue}{\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \sqrt[3]{0.5}}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]

   7. Applied egg-rr 96.2%

      \[\leadsto {\left(\frac{1}{\color{blue}{\left(\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \sin k} \cdot \sqrt[3]{\tan k}\right)} \cdot \sqrt[3]{0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      Proof

      [Start] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \left(\sin k \cdot \tan k\right)} \cdot \sqrt[3]{0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      associate-*r* [=>] 82.5	\[ {\left(\frac{1}{\sqrt[3]{\color{blue}{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \sin k\right) \cdot \tan k}} \cdot \sqrt[3]{0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]
      cbrt-prod [=>] 96.2	\[ {\left(\frac{1}{\color{blue}{\left(\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \sin k} \cdot \sqrt[3]{\tan k}\right)} \cdot \sqrt[3]{0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3} \]

   if -4.39999999999999982e-20 < t < -6.0000000000000002e-105

   1. Initial program 78.1%

      \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]

   2. Simplified 78.2%

      \[\leadsto \color{blue}{\frac{2}{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      Proof

      [Start] 78.1	\[ \frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]
      *-commutative [=>] 78.1	\[ \frac{2}{\color{blue}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right)}} \]
      associate-*l* [=>] 78.1	\[ \frac{2}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \left(\sin k \cdot \tan k\right)\right)}} \]
      associate-*r* [=>] 78.2	\[ \frac{2}{\color{blue}{\left(\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      +-commutative [=>] 78.2	\[ \frac{2}{\left(\color{blue}{\left(1 + \left(1 + {\left(\frac{k}{t}\right)}^{2}\right)\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-+r+ [=>] 78.2	\[ \frac{2}{\left(\color{blue}{\left(\left(1 + 1\right) + {\left(\frac{k}{t}\right)}^{2}\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      metadata-eval [=>] 78.2	\[ \frac{2}{\left(\left(\color{blue}{2} + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]

   3. Taylor expanded in k around inf 75.0%

      \[\leadsto \frac{2}{\color{blue}{\frac{{k}^{2} \cdot t}{{\ell}^{2}}} \cdot \left(\sin k \cdot \tan k\right)} \]

   4. Simplified 75.0%

      \[\leadsto \frac{2}{\color{blue}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      Proof

      [Start] 75.0	\[ \frac{2}{\frac{{k}^{2} \cdot t}{{\ell}^{2}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l* [=>] 75.0	\[ \frac{2}{\color{blue}{\frac{{k}^{2}}{\frac{{\ell}^{2}}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 75.0	\[ \frac{2}{\frac{\color{blue}{k \cdot k}}{\frac{{\ell}^{2}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 75.0	\[ \frac{2}{\frac{k \cdot k}{\frac{\color{blue}{\ell \cdot \ell}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]

   5. Applied egg-rr 79.3%

      \[\leadsto \frac{2}{\color{blue}{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right)} \cdot \left(\sin k \cdot \tan k\right)} \]
      Proof

      [Start] 75.0	\[ \frac{2}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l* [=>] 74.9	\[ \frac{2}{\frac{k \cdot k}{\color{blue}{\frac{\ell}{\frac{t}{\ell}}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/r/ [=>] 79.3	\[ \frac{2}{\color{blue}{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right)} \cdot \left(\sin k \cdot \tan k\right)} \]

   6. Applied egg-rr 57.1%

      \[\leadsto \frac{2}{\color{blue}{0 + \left(\frac{k}{\ell} \cdot k\right) \cdot \left(\left(\frac{t}{\ell} \cdot \sin k\right) \cdot \tan k\right)}} \]
      Proof

      [Start] 79.3	\[ \frac{2}{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      add-log-exp [=>] 23.5	\[ \frac{2}{\color{blue}{\log \left(e^{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right) \cdot \left(\sin k \cdot \tan k\right)}\right)}} \]
      *-un-lft-identity [=>] 23.5	\[ \frac{2}{\log \color{blue}{\left(1 \cdot e^{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right) \cdot \left(\sin k \cdot \tan k\right)}\right)}} \]
      log-prod [=>] 23.5	\[ \frac{2}{\color{blue}{\log 1 + \log \left(e^{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right) \cdot \left(\sin k \cdot \tan k\right)}\right)}} \]
      metadata-eval [=>] 23.5	\[ \frac{2}{\color{blue}{0} + \log \left(e^{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right) \cdot \left(\sin k \cdot \tan k\right)}\right)} \]
      add-log-exp [<=] 44.5	\[ \frac{2}{0 + \color{blue}{\left(\frac{k \cdot k}{\ell} \cdot \frac{t}{\ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      associate-*l* [=>] 44.5	\[ \frac{2}{0 + \color{blue}{\frac{k \cdot k}{\ell} \cdot \left(\frac{t}{\ell} \cdot \left(\sin k \cdot \tan k\right)\right)}} \]
      associate-/l* [=>] 57.0	\[ \frac{2}{0 + \color{blue}{\frac{k}{\frac{\ell}{k}}} \cdot \left(\frac{t}{\ell} \cdot \left(\sin k \cdot \tan k\right)\right)} \]
      associate-/r/ [=>] 57.2	\[ \frac{2}{0 + \color{blue}{\left(\frac{k}{\ell} \cdot k\right)} \cdot \left(\frac{t}{\ell} \cdot \left(\sin k \cdot \tan k\right)\right)} \]
      associate-*r* [=>] 57.1	\[ \frac{2}{0 + \left(\frac{k}{\ell} \cdot k\right) \cdot \color{blue}{\left(\left(\frac{t}{\ell} \cdot \sin k\right) \cdot \tan k\right)}} \]

   7. Simplified 96.0%

      \[\leadsto \frac{2}{\color{blue}{\frac{k}{\ell} \cdot \left(k \cdot \left(\left(\sin k \cdot \frac{t}{\ell}\right) \cdot \tan k\right)\right)}} \]
      Proof

      [Start] 57.1	\[ \frac{2}{0 + \left(\frac{k}{\ell} \cdot k\right) \cdot \left(\left(\frac{t}{\ell} \cdot \sin k\right) \cdot \tan k\right)} \]
      +-lft-identity [=>] 91.9	\[ \frac{2}{\color{blue}{\left(\frac{k}{\ell} \cdot k\right) \cdot \left(\left(\frac{t}{\ell} \cdot \sin k\right) \cdot \tan k\right)}} \]
      associate-*l* [=>] 96.0	\[ \frac{2}{\color{blue}{\frac{k}{\ell} \cdot \left(k \cdot \left(\left(\frac{t}{\ell} \cdot \sin k\right) \cdot \tan k\right)\right)}} \]
      *-commutative [=>] 96.0	\[ \frac{2}{\frac{k}{\ell} \cdot \left(k \cdot \left(\color{blue}{\left(\sin k \cdot \frac{t}{\ell}\right)} \cdot \tan k\right)\right)} \]

   if -6.0000000000000002e-105 < t < -5.1e-160

   1. Initial program 29.7%

      \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]

   2. Simplified 29.7%

      \[\leadsto \color{blue}{\frac{2}{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      Proof

      [Start] 29.7	\[ \frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]
      *-commutative [=>] 29.7	\[ \frac{2}{\color{blue}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right)}} \]
      associate-*l* [=>] 29.7	\[ \frac{2}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \left(\sin k \cdot \tan k\right)\right)}} \]
      associate-*r* [=>] 29.7	\[ \frac{2}{\color{blue}{\left(\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      +-commutative [=>] 29.7	\[ \frac{2}{\left(\color{blue}{\left(1 + \left(1 + {\left(\frac{k}{t}\right)}^{2}\right)\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-+r+ [=>] 29.7	\[ \frac{2}{\left(\color{blue}{\left(\left(1 + 1\right) + {\left(\frac{k}{t}\right)}^{2}\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      metadata-eval [=>] 29.7	\[ \frac{2}{\left(\left(\color{blue}{2} + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]

   3. Taylor expanded in k around inf 69.1%

      \[\leadsto \frac{2}{\color{blue}{\frac{{k}^{2} \cdot t}{{\ell}^{2}}} \cdot \left(\sin k \cdot \tan k\right)} \]

   4. Simplified 61.1%

      \[\leadsto \frac{2}{\color{blue}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      Proof

      [Start] 69.1	\[ \frac{2}{\frac{{k}^{2} \cdot t}{{\ell}^{2}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l* [=>] 61.1	\[ \frac{2}{\color{blue}{\frac{{k}^{2}}{\frac{{\ell}^{2}}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 61.1	\[ \frac{2}{\frac{\color{blue}{k \cdot k}}{\frac{{\ell}^{2}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 61.1	\[ \frac{2}{\frac{k \cdot k}{\frac{\color{blue}{\ell \cdot \ell}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]

   5. Applied egg-rr 84.6%

      \[\leadsto \color{blue}{\frac{\frac{\ell}{\left(k \cdot k\right) \cdot \frac{t}{\ell}}}{\sin k \cdot \tan k} \cdot 2} \]
      Proof

      [Start] 61.1	\[ \frac{2}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      clear-num [=>] 61.1	\[ \color{blue}{\frac{1}{\frac{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}} \cdot \left(\sin k \cdot \tan k\right)}{2}}} \]
      associate-/r/ [=>] 61.1	\[ \color{blue}{\frac{1}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}} \cdot \left(\sin k \cdot \tan k\right)} \cdot 2} \]
      associate-/r* [=>] 61.3	\[ \color{blue}{\frac{\frac{1}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}}}}{\sin k \cdot \tan k}} \cdot 2 \]
      clear-num [<=] 61.2	\[ \frac{\color{blue}{\frac{\frac{\ell \cdot \ell}{t}}{k \cdot k}}}{\sin k \cdot \tan k} \cdot 2 \]
      associate-/l* [=>] 68.9	\[ \frac{\frac{\color{blue}{\frac{\ell}{\frac{t}{\ell}}}}{k \cdot k}}{\sin k \cdot \tan k} \cdot 2 \]
      associate-/l/ [=>] 84.6	\[ \frac{\color{blue}{\frac{\ell}{\left(k \cdot k\right) \cdot \frac{t}{\ell}}}}{\sin k \cdot \tan k} \cdot 2 \]

   if -5.1e-160 < t < -2.15000000000000012e-206

   1. Initial program 25.0%

      \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]

   2. Simplified 25.0%

      \[\leadsto \color{blue}{\frac{2}{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      Proof

      [Start] 25.0	\[ \frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]
      *-commutative [=>] 25.0	\[ \frac{2}{\color{blue}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right)}} \]
      associate-*l* [=>] 25.0	\[ \frac{2}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \left(\sin k \cdot \tan k\right)\right)}} \]
      associate-*r* [=>] 25.0	\[ \frac{2}{\color{blue}{\left(\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      +-commutative [=>] 25.0	\[ \frac{2}{\left(\color{blue}{\left(1 + \left(1 + {\left(\frac{k}{t}\right)}^{2}\right)\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-+r+ [=>] 25.0	\[ \frac{2}{\left(\color{blue}{\left(\left(1 + 1\right) + {\left(\frac{k}{t}\right)}^{2}\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      metadata-eval [=>] 25.0	\[ \frac{2}{\left(\left(\color{blue}{2} + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]

   3. Taylor expanded in k around inf 37.5%

      \[\leadsto \frac{2}{\color{blue}{\frac{{k}^{2} \cdot t}{{\ell}^{2}}} \cdot \left(\sin k \cdot \tan k\right)} \]

   4. Simplified 37.5%

      \[\leadsto \frac{2}{\color{blue}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      Proof

      [Start] 37.5	\[ \frac{2}{\frac{{k}^{2} \cdot t}{{\ell}^{2}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l* [=>] 37.5	\[ \frac{2}{\color{blue}{\frac{{k}^{2}}{\frac{{\ell}^{2}}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 37.5	\[ \frac{2}{\frac{\color{blue}{k \cdot k}}{\frac{{\ell}^{2}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 37.5	\[ \frac{2}{\frac{k \cdot k}{\frac{\color{blue}{\ell \cdot \ell}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]

   5. Applied egg-rr 99.7%

      \[\leadsto \frac{2}{\color{blue}{\left(\left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right) \cdot t\right)} \cdot \left(\sin k \cdot \tan k\right)} \]
      Proof

      [Start] 37.5	\[ \frac{2}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/r/ [=>] 37.3	\[ \frac{2}{\color{blue}{\left(\frac{k \cdot k}{\ell \cdot \ell} \cdot t\right)} \cdot \left(\sin k \cdot \tan k\right)} \]
      times-frac [=>] 99.7	\[ \frac{2}{\left(\color{blue}{\left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)} \cdot t\right) \cdot \left(\sin k \cdot \tan k\right)} \]

   if -2.15000000000000012e-206 < t < 6.7999999999999997e-87

   1. Initial program 29.5%

      \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]

   2. Simplified 29.5%

      \[\leadsto \color{blue}{\frac{2}{\left(\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      Proof

      [Start] 29.5	\[ \frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)} \]
      *-commutative [=>] 29.5	\[ \frac{2}{\color{blue}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right)}} \]
      associate-*l* [=>] 29.5	\[ \frac{2}{\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \left(\sin k \cdot \tan k\right)\right)}} \]
      associate-*r* [=>] 29.5	\[ \frac{2}{\color{blue}{\left(\left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)}} \]
      +-commutative [=>] 29.5	\[ \frac{2}{\left(\color{blue}{\left(1 + \left(1 + {\left(\frac{k}{t}\right)}^{2}\right)\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-+r+ [=>] 29.5	\[ \frac{2}{\left(\color{blue}{\left(\left(1 + 1\right) + {\left(\frac{k}{t}\right)}^{2}\right)} \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      metadata-eval [=>] 29.5	\[ \frac{2}{\left(\left(\color{blue}{2} + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \frac{{t}^{3}}{\ell \cdot \ell}\right) \cdot \left(\sin k \cdot \tan k\right)} \]

   3. Taylor expanded in k around inf 67.5%

      \[\leadsto \frac{2}{\color{blue}{\frac{{k}^{2} \cdot t}{{\ell}^{2}}} \cdot \left(\sin k \cdot \tan k\right)} \]

   4. Simplified 64.5%

      \[\leadsto \frac{2}{\color{blue}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      Proof

      [Start] 67.5	\[ \frac{2}{\frac{{k}^{2} \cdot t}{{\ell}^{2}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l* [=>] 64.5	\[ \frac{2}{\color{blue}{\frac{{k}^{2}}{\frac{{\ell}^{2}}{t}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 64.5	\[ \frac{2}{\frac{\color{blue}{k \cdot k}}{\frac{{\ell}^{2}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      unpow2 [=>] 64.5	\[ \frac{2}{\frac{k \cdot k}{\frac{\color{blue}{\ell \cdot \ell}}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]

   5. Applied egg-rr 91.5%

      \[\leadsto \frac{2}{\color{blue}{\left(k \cdot \frac{1}{\frac{\ell}{k \cdot \frac{t}{\ell}}}\right)} \cdot \left(\sin k \cdot \tan k\right)} \]
      Proof

      [Start] 64.5	\[ \frac{2}{\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l* [=>] 68.0	\[ \frac{2}{\color{blue}{\frac{k}{\frac{\frac{\ell \cdot \ell}{t}}{k}}} \cdot \left(\sin k \cdot \tan k\right)} \]
      div-inv [=>] 68.0	\[ \frac{2}{\color{blue}{\left(k \cdot \frac{1}{\frac{\frac{\ell \cdot \ell}{t}}{k}}\right)} \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l* [=>] 79.8	\[ \frac{2}{\left(k \cdot \frac{1}{\frac{\color{blue}{\frac{\ell}{\frac{t}{\ell}}}}{k}}\right) \cdot \left(\sin k \cdot \tan k\right)} \]
      associate-/l/ [=>] 91.5	\[ \frac{2}{\left(k \cdot \frac{1}{\color{blue}{\frac{\ell}{k \cdot \frac{t}{\ell}}}}\right) \cdot \left(\sin k \cdot \tan k\right)} \]

3. Recombined 5 regimes into one program.

4. Final simplification 94.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq -4.4 \cdot 10^{-20}:\\ \;\;\;\;{\left(\frac{1}{\left(\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \sin k} \cdot \sqrt[3]{\tan k}\right) \cdot \sqrt[3]{0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3}\\ \mathbf{elif}\;t \leq -6 \cdot 10^{-105}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot \left(k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\right)}\\ \mathbf{elif}\;t \leq -5.1 \cdot 10^{-160}:\\ \;\;\;\;2 \cdot \frac{\frac{\ell}{\frac{t}{\ell} \cdot \left(k \cdot k\right)}}{\sin k \cdot \tan k}\\ \mathbf{elif}\;t \leq -2.15 \cdot 10^{-206}:\\ \;\;\;\;\frac{2}{\left(\sin k \cdot \tan k\right) \cdot \left(t \cdot \left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)\right)}\\ \mathbf{elif}\;t \leq 6.8 \cdot 10^{-87}:\\ \;\;\;\;\frac{2}{\left(\sin k \cdot \tan k\right) \cdot \left(k \cdot \frac{1}{\frac{\ell}{k \cdot \frac{t}{\ell}}}\right)}\\ \mathbf{else}:\\ \;\;\;\;{\left(\frac{1}{\left(\sqrt[3]{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot \sin k} \cdot \sqrt[3]{\tan k}\right) \cdot \sqrt[3]{0.5}} \cdot \frac{{\left(\sqrt[3]{\ell}\right)}^{2}}{t}\right)}^{3}\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	88.4%
Cost	46216

\[\begin{array}{l} t_1 := {\left(\sqrt[3]{\ell}\right)}^{2}\\ t_2 := \sin k \cdot \tan k\\ \mathbf{if}\;k \leq -2.2 \cdot 10^{+85}:\\ \;\;\;\;\frac{2}{t_2 \cdot \left(t \cdot \left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)\right)}\\ \mathbf{elif}\;k \leq -5 \cdot 10^{-154}:\\ \;\;\;\;{\left(\frac{t_1}{t} \cdot \sqrt[3]{\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot t_2}}\right)}^{3}\\ \mathbf{elif}\;k \leq 4.2 \cdot 10^{-25}:\\ \;\;\;\;{\left(\frac{t_1 \cdot {\left(\sqrt[3]{k}\right)}^{-2}}{t}\right)}^{3}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot \left(k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\right)}\\ \end{array} \]

Alternative 2
Accuracy	87.7%
Cost	39816

\[\begin{array}{l} t_1 := \sin k \cdot \tan k\\ t_2 := {\left(\sqrt[3]{\ell}\right)}^{2}\\ \mathbf{if}\;k \leq -1.25 \cdot 10^{+85}:\\ \;\;\;\;\frac{2}{t_1 \cdot \left(t \cdot \left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)\right)}\\ \mathbf{elif}\;k \leq -2.65 \cdot 10^{-107}:\\ \;\;\;\;\frac{2}{\left(2 + {\left(\frac{k}{t}\right)}^{2}\right) \cdot t_1} \cdot {\left(\frac{t_2}{t}\right)}^{3}\\ \mathbf{elif}\;k \leq 4.9 \cdot 10^{-24}:\\ \;\;\;\;{\left(\frac{t_2 \cdot {\left(\sqrt[3]{k}\right)}^{-2}}{t}\right)}^{3}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot \left(k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\right)}\\ \end{array} \]

Alternative 3
Accuracy	87.9%
Cost	32644

\[\begin{array}{l} t_1 := \frac{-2}{-2 - {\left(\frac{k}{t}\right)}^{2}} \cdot \left(\frac{\ell}{\frac{\tan k}{{t}^{-3}}} \cdot \frac{\ell}{\sin k}\right)\\ t_2 := k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\\ \mathbf{if}\;t \leq -2.3 \cdot 10^{+105}:\\ \;\;\;\;{\left(\frac{{\left(\sqrt[3]{\ell}\right)}^{2} \cdot {\left(\sqrt[3]{k}\right)}^{-2}}{t}\right)}^{3}\\ \mathbf{elif}\;t \leq -4.8 \cdot 10^{-20}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 1.25 \cdot 10^{-12}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot t_2}\\ \mathbf{elif}\;t \leq 8 \cdot 10^{+129}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 3.2 \cdot 10^{+165}:\\ \;\;\;\;\frac{2}{\frac{t_2}{\frac{\ell}{k}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \end{array} \]

Alternative 4
Accuracy	87.6%
Cost	27344

\[\begin{array}{l} t_1 := \frac{-2}{-2 - {\left(\frac{k}{t}\right)}^{2}} \cdot \left(\frac{\ell}{\frac{\tan k}{{t}^{-3}}} \cdot \frac{\ell}{\sin k}\right)\\ t_2 := k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\\ t_3 := \frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \mathbf{if}\;t \leq -2.4 \cdot 10^{+105}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t \leq -3.7 \cdot 10^{-19}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 2.8 \cdot 10^{-14}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot t_2}\\ \mathbf{elif}\;t \leq 3.6 \cdot 10^{+129}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 3.2 \cdot 10^{+165}:\\ \;\;\;\;\frac{2}{\frac{t_2}{\frac{\ell}{k}}}\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]

Alternative 5
Accuracy	85.9%
Cost	19912

\[\begin{array}{l} \mathbf{if}\;k \leq -1.6 \cdot 10^{-33}:\\ \;\;\;\;\frac{2}{\left(\sin k \cdot \tan k\right) \cdot \left(t \cdot \left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)\right)}\\ \mathbf{elif}\;k \leq 2.3 \cdot 10^{-25}:\\ \;\;\;\;{\left(\frac{{\left(\sqrt[3]{\frac{\ell}{k}}\right)}^{2}}{t}\right)}^{3}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot \left(k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\right)}\\ \end{array} \]

Alternative 6
Accuracy	79.9%
Cost	14025

\[\begin{array}{l} \mathbf{if}\;t \leq -3.3 \cdot 10^{-20} \lor \neg \left(t \leq 5.8 \cdot 10^{+77}\right):\\ \;\;\;\;\frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \frac{\ell}{\left(\frac{t}{\ell} \cdot \left(k \cdot k\right)\right) \cdot \left(\sin k \cdot \tan k\right)}\\ \end{array} \]

Alternative 7
Accuracy	80.2%
Cost	14025

\[\begin{array}{l} \mathbf{if}\;t \leq -4.2 \cdot 10^{-20} \lor \neg \left(t \leq 5.8 \cdot 10^{+77}\right):\\ \;\;\;\;\frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \frac{\frac{\ell}{k \cdot k}}{\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)}\\ \end{array} \]

Alternative 8
Accuracy	80.6%
Cost	14025

\[\begin{array}{l} \mathbf{if}\;t \leq -3.7 \cdot 10^{-19} \lor \neg \left(t \leq 5.8 \cdot 10^{+77}\right):\\ \;\;\;\;\frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \frac{\frac{\ell}{\frac{t}{\ell} \cdot \left(k \cdot k\right)}}{\sin k \cdot \tan k}\\ \end{array} \]

Alternative 9
Accuracy	84.5%
Cost	14025

\[\begin{array}{l} \mathbf{if}\;k \leq -1.1 \cdot 10^{-56} \lor \neg \left(k \leq 3.4 \cdot 10^{-22}\right):\\ \;\;\;\;\frac{2}{\left(\sin k \cdot \tan k\right) \cdot \left(t \cdot \left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \end{array} \]

Alternative 10
Accuracy	84.5%
Cost	14024

\[\begin{array}{l} \mathbf{if}\;k \leq -1.1 \cdot 10^{-56}:\\ \;\;\;\;\frac{2}{\left(\sin k \cdot \tan k\right) \cdot \left(t \cdot \left(\frac{k}{\ell} \cdot \frac{k}{\ell}\right)\right)}\\ \mathbf{elif}\;k \leq 2.1 \cdot 10^{-22}:\\ \;\;\;\;\frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{k}{\ell} \cdot \left(k \cdot \left(\tan k \cdot \left(\sin k \cdot \frac{t}{\ell}\right)\right)\right)}\\ \end{array} \]

Alternative 11
Accuracy	66.8%
Cost	7305

\[\begin{array}{l} \mathbf{if}\;k \leq -3.6 \cdot 10^{-57} \lor \neg \left(k \leq 3.2 \cdot 10^{-26}\right):\\ \;\;\;\;2 \cdot \frac{\frac{\ell}{\frac{t}{\ell}}}{{k}^{4}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\ell}{k} \cdot \frac{\ell}{t \cdot t}}{t \cdot k}\\ \end{array} \]

Alternative 12
Accuracy	69.2%
Cost	7305

\[\begin{array}{l} \mathbf{if}\;t \leq -1.45 \cdot 10^{-34} \lor \neg \left(t \leq 4.4 \cdot 10^{-72}\right):\\ \;\;\;\;\frac{\frac{\ell}{k} \cdot \frac{\ell}{t}}{k \cdot \left(t \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{t} \cdot \frac{\ell}{\frac{{k}^{4}}{\ell}}\\ \end{array} \]

Alternative 13
Accuracy	69.6%
Cost	7305

\[\begin{array}{l} \mathbf{if}\;t \leq -3.4 \cdot 10^{-32} \lor \neg \left(t \leq 1.35 \cdot 10^{-72}\right):\\ \;\;\;\;\frac{\frac{\ell}{k} \cdot \frac{\ell}{t}}{k \cdot \left(t \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{t}{\ell} \cdot \frac{{k}^{4}}{\ell}}\\ \end{array} \]

Alternative 14
Accuracy	73.1%
Cost	7305

\[\begin{array}{l} \mathbf{if}\;t \leq -1.6 \cdot 10^{-18} \lor \neg \left(t \leq 3.1 \cdot 10^{-68}\right):\\ \;\;\;\;\frac{\frac{\ell}{t}}{\frac{{\left(t \cdot k\right)}^{2}}{\ell}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{t}{\ell} \cdot \frac{{k}^{4}}{\ell}}\\ \end{array} \]

Alternative 15
Accuracy	58.2%
Cost	832

\[\frac{\ell}{k \cdot k} \cdot \frac{\frac{\ell}{t}}{t \cdot t} \]

Alternative 16
Accuracy	58.3%
Cost	832

\[\frac{\ell}{\left(k \cdot k\right) \cdot \left(\frac{t}{\ell} \cdot \left(t \cdot t\right)\right)} \]

Alternative 17
Accuracy	64.8%
Cost	832

\[\frac{\frac{\ell}{k} \cdot \frac{\ell}{t}}{k \cdot \left(t \cdot t\right)} \]

Alternative 18
Accuracy	64.6%
Cost	832

\[\frac{\frac{\ell}{k} \cdot \frac{\ell}{t \cdot t}}{t \cdot k} \]

Reproduce

herbie shell --seed 2023160 
(FPCore (t l k)
  :name "Toniolo and Linder, Equation (10+)"
  :precision binary64
  (/ 2.0 (* (* (* (/ (pow t 3.0) (* l l)) (sin k)) (tan k)) (+ (+ 1.0 (pow (/ k t) 2.0)) 1.0))))