Toniolo and Linder, Equation (10-)

1. Split input into 2 regimes

2. if k < -2.1999999999999998e187

   1. Initial program 35.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. Step-by-step derivation

      1. +-rgt-identity35.0%

         \[\leadsto \frac{2}{\color{blue}{\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) + 0}} \]

      2. associate-*l*35.0%

         \[\leadsto \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)} + 0} \]

      3. mul0-rgt10.3%

         \[\leadsto \frac{2}{\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) + \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot 0}} \]

      4. distribute-lft-in35.0%

         \[\leadsto \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) + 0\right)}} \]

      5. +-rgt-identity35.0%

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

      6. sub-neg35.0%

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

      7. +-commutative35.0%

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

      8. associate-+l+41.9%

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

      9. metadata-eval41.9%

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

      10. metadata-eval41.9%

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

      11. +-rgt-identity41.9%

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

   3. Simplified41.9%

      \[\leadsto \color{blue}{\frac{2}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \left(\tan k \cdot {\left(\frac{k}{t}\right)}^{2}\right)}} \]
   4. Step-by-step derivation

      1. add-sqr-sqrt21.2%

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

      2. *-un-lft-identity21.2%

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

      3. times-frac21.2%

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

      4. sqrt-pow121.2%

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

      5. metadata-eval21.2%

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

      6. sqrt-pow127.6%

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

      7. metadata-eval27.6%

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

   5. Applied egg-rr27.6%

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

   6. Taylor expanded in t around -inf 0.0%

      \[\leadsto \frac{2}{\color{blue}{-1 \cdot \frac{{k}^{2} \cdot \left({\left(\sqrt{-1}\right)}^{2} \cdot \left({\sin k}^{2} \cdot t\right)\right)}{\cos k \cdot {\ell}^{2}}}} \]
   7. Step-by-step derivation

      1. mul-1-neg0.0%

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

      2. times-frac0.0%

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

      3. unpow20.0%

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

      4. distribute-rgt-neg-in0.0%

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

      5. associate-/l*0.0%

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

      6. *-commutative0.0%

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

      7. *-commutative0.0%

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

      8. unpow20.0%

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

      9. rem-square-sqrt62.6%

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

      10. unpow262.6%

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

      11. times-frac63.6%

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

   8. Simplified63.6%

      \[\leadsto \frac{2}{\color{blue}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\frac{{\sin k}^{2}}{\frac{\ell}{t}} \cdot \frac{-1}{\ell}\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/82.5%

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

      2. distribute-rgt-neg-in82.5%

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

      3. div-inv82.5%

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

      4. clear-num82.5%

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

   10. Applied egg-rr82.5%

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

   if -2.1999999999999998e187 < k

   1. Initial program 35.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. Step-by-step derivation

      1. associate-*l*35.5%

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

      2. associate-*l*35.5%

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

      3. associate-/r*35.5%

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

      4. associate-/r/35.5%

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

      5. *-commutative35.5%

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

      6. times-frac36.0%

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

      7. +-commutative36.0%

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

      8. associate--l+42.8%

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

      9. metadata-eval42.8%

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

      10. +-rgt-identity42.8%

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

      11. times-frac46.9%

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

   3. Simplified46.9%

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

   4. Taylor expanded in t around 0 79.9%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow279.9%

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

   6. Simplified79.9%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/79.9%

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

      2. associate-*l*86.0%

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

   8. Applied egg-rr86.0%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/86.0%

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

      2. *-commutative86.0%

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

      3. associate-*l*90.2%

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

   10. Simplified90.2%

       \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
   11. Step-by-step derivation

       1. associate-*r/90.2%

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

   12. Applied egg-rr90.2%

       \[\leadsto \frac{\ell}{\sin k} \cdot \color{blue}{\frac{\frac{\ell}{\tan k} \cdot 2}{k \cdot \left(k \cdot t\right)}} \]
   13. Step-by-step derivation

       1. associate-*l/89.4%

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

       2. times-frac94.9%

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

   14. Applied egg-rr94.9%

       \[\leadsto \color{blue}{\frac{\ell \cdot \left(\frac{\frac{\ell}{\tan k}}{k} \cdot \frac{2}{k \cdot t}\right)}{\sin k}} \]
3. Recombined 2 regimes into one program.

4. Final simplification93.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;k \leq -2.2 \cdot 10^{+187}:\\ \;\;\;\;\frac{2}{\frac{k \cdot \left(\left({\sin k}^{2} \cdot \frac{t}{\ell}\right) \cdot \frac{--1}{\ell}\right)}{\frac{\cos k}{k}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\ell \cdot \left(\frac{\frac{\ell}{\tan k}}{k} \cdot \frac{2}{k \cdot t}\right)}{\sin k}\\ \end{array} \]

1. Split input into 2 regimes

2. if (*.f64 l l) < 0.0

   1. Initial program 21.6%

      \[\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. Step-by-step derivation

      1. associate-*l*21.6%

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

      2. associate-*l*21.6%

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

      3. associate-/r*21.6%

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

      4. associate-/r/21.6%

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

      5. *-commutative21.6%

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

      6. times-frac21.6%

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

      7. +-commutative21.6%

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

      8. associate--l+29.3%

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

      9. metadata-eval29.3%

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

      10. +-rgt-identity29.3%

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

      11. times-frac43.5%

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

   3. Simplified43.5%

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

   4. Taylor expanded in t around 0 77.5%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow277.5%

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

   6. Simplified77.5%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/77.5%

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

      2. associate-*l*84.3%

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

   8. Applied egg-rr84.3%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/84.2%

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

      2. *-commutative84.2%

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

      3. associate-*l*89.7%

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

   10. Simplified89.7%

       \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
   11. Step-by-step derivation

       1. associate-*r/89.8%

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

   12. Applied egg-rr89.8%

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

   13. Taylor expanded in k around 0 87.0%

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

   if 0.0 < (*.f64 l l)

   1. Initial program 40.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. Step-by-step derivation

      1. associate-*l*40.1%

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

      2. associate-*l*40.1%

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

      3. associate-/r*40.2%

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

      4. associate-/r/40.2%

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

      5. *-commutative40.2%

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

      6. times-frac40.7%

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

      7. +-commutative40.7%

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

      8. associate--l+47.3%

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

      9. metadata-eval47.3%

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

      10. +-rgt-identity47.3%

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

      11. times-frac47.3%

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

   3. Simplified47.3%

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

   4. Taylor expanded in t around 0 78.1%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow278.1%

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

   6. Simplified78.1%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
3. Recombined 2 regimes into one program.

4. Final simplification80.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \leq 0:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \frac{2 \cdot \frac{\ell}{k}}{k \cdot \left(k \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{t \cdot \left(k \cdot k\right)} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{\ell}{\sin k}\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if (*.f64 l l) < 1.00000000000000007e-68

   1. Initial program 32.3%

      \[\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. Step-by-step derivation

      1. associate-*l*32.3%

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

      2. associate-*l*32.3%

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

      3. associate-/r*32.3%

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

      4. associate-/r/32.3%

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

      5. *-commutative32.3%

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

      6. times-frac34.9%

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

      7. +-commutative34.9%

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

      8. associate--l+44.6%

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

      9. metadata-eval44.6%

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

      10. +-rgt-identity44.6%

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

      11. times-frac52.9%

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

   3. Simplified52.9%

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

   4. Taylor expanded in t around 0 85.5%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow285.5%

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

   6. Simplified85.5%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/85.5%

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

      2. associate-*l*90.8%

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

   8. Applied egg-rr90.8%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/90.8%

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

      2. *-commutative90.8%

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

      3. associate-*l*94.0%

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

   10. Simplified94.0%

       \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
   11. Step-by-step derivation

       1. associate-*r/94.0%

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

   12. Applied egg-rr94.0%

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

   13. Taylor expanded in k around 0 87.6%

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

   if 1.00000000000000007e-68 < (*.f64 l l)

   1. Initial program 37.9%

      \[\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. Step-by-step derivation

      1. +-rgt-identity21.2%

         \[\leadsto \frac{2}{\color{blue}{\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) + 0}} \]

      2. associate-*l*21.2%

         \[\leadsto \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)} + 0} \]

      3. mul0-rgt22.5%

         \[\leadsto \frac{2}{\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) + \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot 0}} \]

      4. distribute-lft-in30.9%

         \[\leadsto \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) + 0\right)}} \]

      5. +-rgt-identity37.9%

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

      6. sub-neg37.9%

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

      7. +-commutative37.9%

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

      8. associate-+l+42.6%

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

      9. metadata-eval42.6%

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

      10. metadata-eval42.6%

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

      11. +-rgt-identity42.6%

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

   3. Simplified42.6%

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

   4. Taylor expanded in k around 0 36.7%

      \[\leadsto \frac{2}{\color{blue}{\frac{k \cdot {t}^{3}}{{\ell}^{2}}} \cdot \left(\tan k \cdot {\left(\frac{k}{t}\right)}^{2}\right)} \]
   5. Step-by-step derivation

      1. associate-/l*36.7%

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

      2. unpow236.7%

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

   6. Simplified36.7%

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

   7. Taylor expanded in k around inf 63.3%

      \[\leadsto \frac{2}{\color{blue}{\frac{{k}^{3} \cdot \left(\sin k \cdot t\right)}{\cos k \cdot {\ell}^{2}}}} \]
   8. Step-by-step derivation

      1. times-frac63.8%

         \[\leadsto \frac{2}{\color{blue}{\frac{{k}^{3}}{\cos k} \cdot \frac{\sin k \cdot t}{{\ell}^{2}}}} \]

      2. associate-/l*63.7%

         \[\leadsto \frac{2}{\frac{{k}^{3}}{\cos k} \cdot \color{blue}{\frac{\sin k}{\frac{{\ell}^{2}}{t}}}} \]

      3. unpow263.7%

         \[\leadsto \frac{2}{\frac{{k}^{3}}{\cos k} \cdot \frac{\sin k}{\frac{\color{blue}{\ell \cdot \ell}}{t}}} \]

      4. associate-/l*64.0%

         \[\leadsto \frac{2}{\frac{{k}^{3}}{\cos k} \cdot \frac{\sin k}{\color{blue}{\frac{\ell}{\frac{t}{\ell}}}}} \]

   9. Simplified64.0%

      \[\leadsto \frac{2}{\color{blue}{\frac{{k}^{3}}{\cos k} \cdot \frac{\sin k}{\frac{\ell}{\frac{t}{\ell}}}}} \]

   10. Taylor expanded in k around 0 66.9%

       \[\leadsto \frac{2}{\frac{{k}^{3}}{\cos k} \cdot \color{blue}{\frac{k \cdot t}{{\ell}^{2}}}} \]
   11. Step-by-step derivation

       1. *-commutative66.9%

          \[\leadsto \frac{2}{\frac{{k}^{3}}{\cos k} \cdot \frac{\color{blue}{t \cdot k}}{{\ell}^{2}}} \]

       2. unpow266.9%

          \[\leadsto \frac{2}{\frac{{k}^{3}}{\cos k} \cdot \frac{t \cdot k}{\color{blue}{\ell \cdot \ell}}} \]

       3. times-frac67.4%

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

   12. Simplified67.4%

       \[\leadsto \frac{2}{\frac{{k}^{3}}{\cos k} \cdot \color{blue}{\left(\frac{t}{\ell} \cdot \frac{k}{\ell}\right)}} \]
3. Recombined 2 regimes into one program.

4. Final simplification76.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \leq 10^{-68}:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \frac{2 \cdot \frac{\ell}{k}}{k \cdot \left(k \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{{k}^{3}}{\cos k} \cdot \left(\frac{t}{\ell} \cdot \frac{k}{\ell}\right)}\\ \end{array} \]

1. Initial program 35.4%

   \[\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. Step-by-step derivation

   1. associate-*l*35.4%

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

   2. associate-*l*35.4%

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

   3. associate-/r*35.5%

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

   4. associate-/r/35.5%

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

   5. *-commutative35.5%

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

   6. times-frac35.8%

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

   7. +-commutative35.8%

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

   8. associate--l+42.7%

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

   9. metadata-eval42.7%

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

   10. +-rgt-identity42.7%

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

   11. times-frac46.4%

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

3. Simplified46.4%

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

4. Taylor expanded in t around 0 78.0%

   \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
5. Step-by-step derivation

   1. unpow278.0%

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

6. Simplified78.0%

   \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
7. Step-by-step derivation

   1. associate-*l/78.0%

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

   2. associate-*l*83.4%

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

8. Applied egg-rr83.4%

   \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
9. Step-by-step derivation

   1. associate-*l/83.4%

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

   2. *-commutative83.4%

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

   3. associate-*l*87.6%

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

10. Simplified87.6%

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

11. Final simplification87.6%

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

1. Initial program 35.4%

   \[\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. Step-by-step derivation

   1. associate-*l*35.4%

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

   2. associate-*l*35.4%

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

   3. associate-/r*35.5%

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

   4. associate-/r/35.5%

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

   5. *-commutative35.5%

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

   6. times-frac35.8%

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

   7. +-commutative35.8%

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

   8. associate--l+42.7%

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

   9. metadata-eval42.7%

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

   10. +-rgt-identity42.7%

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

   11. times-frac46.4%

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

3. Simplified46.4%

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

4. Taylor expanded in t around 0 78.0%

   \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
5. Step-by-step derivation

   1. unpow278.0%

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

6. Simplified78.0%

   \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
7. Step-by-step derivation

   1. associate-*l/78.0%

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

   2. associate-*l*83.4%

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

8. Applied egg-rr83.4%

   \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
9. Step-by-step derivation

   1. associate-*l/83.4%

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

   2. *-commutative83.4%

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

   3. associate-*l*87.6%

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

10. Simplified87.6%

    \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
11. Step-by-step derivation

    1. associate-*l/87.6%

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

12. Applied egg-rr87.6%

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

13. Final simplification87.6%

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

1. Initial program 35.4%

   \[\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. Step-by-step derivation

   1. associate-*l*35.4%

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

   2. associate-*l*35.4%

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

   3. associate-/r*35.5%

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

   4. associate-/r/35.5%

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

   5. *-commutative35.5%

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

   6. times-frac35.8%

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

   7. +-commutative35.8%

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

   8. associate--l+42.7%

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

   9. metadata-eval42.7%

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

   10. +-rgt-identity42.7%

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

   11. times-frac46.4%

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

3. Simplified46.4%

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

4. Taylor expanded in t around 0 78.0%

   \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
5. Step-by-step derivation

   1. unpow278.0%

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

6. Simplified78.0%

   \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
7. Step-by-step derivation

   1. associate-*l/78.0%

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

   2. associate-*l*83.4%

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

8. Applied egg-rr83.4%

   \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
9. Step-by-step derivation

   1. associate-*l/83.4%

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

   2. *-commutative83.4%

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

   3. associate-*l*87.6%

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

10. Simplified87.6%

    \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
11. Step-by-step derivation

    1. associate-*r/87.6%

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

12. Applied egg-rr87.6%

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

13. Final simplification87.6%

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

1. Initial program 35.4%

   \[\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. Step-by-step derivation

   1. associate-*l*35.4%

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

   2. associate-*l*35.4%

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

   3. associate-/r*35.5%

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

   4. associate-/r/35.5%

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

   5. *-commutative35.5%

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

   6. times-frac35.8%

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

   7. +-commutative35.8%

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

   8. associate--l+42.7%

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

   9. metadata-eval42.7%

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

   10. +-rgt-identity42.7%

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

   11. times-frac46.4%

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

3. Simplified46.4%

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

4. Taylor expanded in t around 0 78.0%

   \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
5. Step-by-step derivation

   1. unpow278.0%

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

6. Simplified78.0%

   \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
7. Step-by-step derivation

   1. associate-*l/78.0%

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

   2. associate-*l*83.4%

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

8. Applied egg-rr83.4%

   \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
9. Step-by-step derivation

   1. associate-*l/83.4%

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

   2. *-commutative83.4%

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

   3. associate-*l*87.6%

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

10. Simplified87.6%

    \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
11. Step-by-step derivation

    1. associate-*r/87.6%

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

12. Applied egg-rr87.6%

    \[\leadsto \frac{\ell}{\sin k} \cdot \color{blue}{\frac{\frac{\ell}{\tan k} \cdot 2}{k \cdot \left(k \cdot t\right)}} \]
13. Step-by-step derivation

    1. frac-times80.2%

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

14. Applied egg-rr80.2%

    \[\leadsto \color{blue}{\frac{\ell \cdot \left(\frac{\ell}{\tan k} \cdot 2\right)}{\sin k \cdot \left(k \cdot \left(k \cdot t\right)\right)}} \]
15. Step-by-step derivation

    1. *-commutative80.2%

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

    2. *-commutative80.2%

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

    3. times-frac87.6%

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

    4. times-frac92.5%

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

    5. associate-*l/92.4%

       \[\leadsto \color{blue}{\frac{\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot t}}{k}} \cdot \frac{\ell}{\sin k} \]

    6. associate-*l/91.4%

       \[\leadsto \frac{\color{blue}{\frac{\ell \cdot \frac{2}{k \cdot t}}{\tan k}}}{k} \cdot \frac{\ell}{\sin k} \]

16. Simplified91.4%

    \[\leadsto \color{blue}{\frac{\frac{\ell \cdot \frac{2}{k \cdot t}}{\tan k}}{k} \cdot \frac{\ell}{\sin k}} \]

17. Final simplification91.4%

    \[\leadsto \frac{\frac{\ell \cdot \frac{2}{k \cdot t}}{\tan k}}{k} \cdot \frac{\ell}{\sin k} \]

1. Initial program 35.4%

   \[\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. Step-by-step derivation

   1. associate-*l*35.4%

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

   2. associate-*l*35.4%

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

   3. associate-/r*35.5%

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

   4. associate-/r/35.5%

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

   5. *-commutative35.5%

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

   6. times-frac35.8%

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

   7. +-commutative35.8%

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

   8. associate--l+42.7%

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

   9. metadata-eval42.7%

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

   10. +-rgt-identity42.7%

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

   11. times-frac46.4%

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

3. Simplified46.4%

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

4. Taylor expanded in t around 0 78.0%

   \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
5. Step-by-step derivation

   1. unpow278.0%

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

6. Simplified78.0%

   \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
7. Step-by-step derivation

   1. associate-*l/78.0%

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

   2. associate-*l*83.4%

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

8. Applied egg-rr83.4%

   \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
9. Step-by-step derivation

   1. associate-*l/83.4%

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

   2. *-commutative83.4%

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

   3. associate-*l*87.6%

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

10. Simplified87.6%

    \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
11. Step-by-step derivation

    1. associate-*r/87.6%

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

12. Applied egg-rr87.6%

    \[\leadsto \frac{\ell}{\sin k} \cdot \color{blue}{\frac{\frac{\ell}{\tan k} \cdot 2}{k \cdot \left(k \cdot t\right)}} \]
13. Step-by-step derivation

    1. associate-*l/87.0%

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

    2. times-frac91.8%

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

14. Applied egg-rr91.8%

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

15. Final simplification91.8%

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

1. Split input into 2 regimes

2. if (*.f64 l l) < 1.00000000000000007e-68

   1. Initial program 32.3%

      \[\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. Step-by-step derivation

      1. associate-*l*32.3%

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

      2. associate-*l*32.3%

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

      3. associate-/r*32.3%

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

      4. associate-/r/32.3%

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

      5. *-commutative32.3%

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

      6. times-frac34.9%

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

      7. +-commutative34.9%

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

      8. associate--l+44.6%

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

      9. metadata-eval44.6%

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

      10. +-rgt-identity44.6%

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

      11. times-frac52.9%

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

   3. Simplified52.9%

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

   4. Taylor expanded in t around 0 85.5%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow285.5%

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

   6. Simplified85.5%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/85.5%

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

      2. associate-*l*90.8%

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

   8. Applied egg-rr90.8%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/90.8%

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

      2. *-commutative90.8%

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

      3. associate-*l*94.0%

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

   10. Simplified94.0%

       \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
   11. Step-by-step derivation

       1. associate-*r/94.0%

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

   12. Applied egg-rr94.0%

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

   13. Taylor expanded in k around 0 87.6%

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

   if 1.00000000000000007e-68 < (*.f64 l l)

   1. Initial program 37.9%

      \[\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. Step-by-step derivation

      1. +-rgt-identity21.2%

         \[\leadsto \frac{2}{\color{blue}{\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) + 0}} \]

      2. associate-*l*21.2%

         \[\leadsto \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)} + 0} \]

      3. mul0-rgt22.5%

         \[\leadsto \frac{2}{\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) + \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot 0}} \]

      4. distribute-lft-in30.9%

         \[\leadsto \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) + 0\right)}} \]

      5. +-rgt-identity37.9%

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

      6. sub-neg37.9%

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

      7. +-commutative37.9%

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

      8. associate-+l+42.6%

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

      9. metadata-eval42.6%

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

      10. metadata-eval42.6%

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

      11. +-rgt-identity42.6%

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

   3. Simplified42.6%

      \[\leadsto \color{blue}{\frac{2}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \left(\tan k \cdot {\left(\frac{k}{t}\right)}^{2}\right)}} \]
   4. Step-by-step derivation

      1. add-sqr-sqrt17.5%

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

      2. *-un-lft-identity17.5%

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

      3. times-frac17.5%

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

      4. sqrt-pow117.5%

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

      5. metadata-eval17.5%

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

      6. sqrt-pow119.5%

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

      7. metadata-eval19.5%

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

   5. Applied egg-rr19.5%

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

   6. Taylor expanded in t around -inf 0.0%

      \[\leadsto \frac{2}{\color{blue}{-1 \cdot \frac{{k}^{2} \cdot \left({\left(\sqrt{-1}\right)}^{2} \cdot \left({\sin k}^{2} \cdot t\right)\right)}{\cos k \cdot {\ell}^{2}}}} \]
   7. Step-by-step derivation

      1. mul-1-neg0.0%

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

      2. times-frac0.0%

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

      3. unpow20.0%

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

      4. distribute-rgt-neg-in0.0%

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

      5. associate-/l*0.0%

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

      6. *-commutative0.0%

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

      7. *-commutative0.0%

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

      8. unpow20.0%

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

      9. rem-square-sqrt73.4%

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

      10. unpow273.4%

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

      11. times-frac76.3%

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

   8. Simplified76.3%

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

   9. Taylor expanded in k around 0 66.9%

      \[\leadsto \frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\color{blue}{\frac{{k}^{2} \cdot t}{\ell}} \cdot \frac{-1}{\ell}\right)} \]
   10. Step-by-step derivation

       1. unpow266.9%

          \[\leadsto \frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\frac{\color{blue}{\left(k \cdot k\right)} \cdot t}{\ell} \cdot \frac{-1}{\ell}\right)} \]

       2. associate-*r*66.8%

          \[\leadsto \frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\frac{\color{blue}{k \cdot \left(k \cdot t\right)}}{\ell} \cdot \frac{-1}{\ell}\right)} \]

   11. Simplified66.8%

       \[\leadsto \frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\color{blue}{\frac{k \cdot \left(k \cdot t\right)}{\ell}} \cdot \frac{-1}{\ell}\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification75.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \leq 10^{-68}:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \frac{2 \cdot \frac{\ell}{k}}{k \cdot \left(k \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(\frac{-1}{\ell} \cdot \frac{k \cdot \left(k \cdot \left(-t\right)\right)}{\ell}\right)}\\ \end{array} \]

1. Split input into 2 regimes

2. if (*.f64 l l) < 1.00000000000000007e-68

   1. Initial program 32.3%

      \[\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. Step-by-step derivation

      1. associate-*l*32.3%

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

      2. associate-*l*32.3%

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

      3. associate-/r*32.3%

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

      4. associate-/r/32.3%

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

      5. *-commutative32.3%

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

      6. times-frac34.9%

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

      7. +-commutative34.9%

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

      8. associate--l+44.6%

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

      9. metadata-eval44.6%

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

      10. +-rgt-identity44.6%

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

      11. times-frac52.9%

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

   3. Simplified52.9%

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

   4. Taylor expanded in t around 0 85.5%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow285.5%

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

   6. Simplified85.5%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/85.5%

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

      2. associate-*l*90.8%

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

   8. Applied egg-rr90.8%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/90.8%

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

      2. *-commutative90.8%

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

      3. associate-*l*94.0%

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

   10. Simplified94.0%

       \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
   11. Step-by-step derivation

       1. associate-*r/94.0%

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

   12. Applied egg-rr94.0%

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

   13. Taylor expanded in k around 0 87.6%

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

   if 1.00000000000000007e-68 < (*.f64 l l)

   1. Initial program 37.9%

      \[\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. Step-by-step derivation

      1. +-rgt-identity21.2%

         \[\leadsto \frac{2}{\color{blue}{\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) + 0}} \]

      2. associate-*l*21.2%

         \[\leadsto \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)} + 0} \]

      3. mul0-rgt22.5%

         \[\leadsto \frac{2}{\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) + \color{blue}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot 0}} \]

      4. distribute-lft-in30.9%

         \[\leadsto \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) + 0\right)}} \]

      5. +-rgt-identity37.9%

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

      6. sub-neg37.9%

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

      7. +-commutative37.9%

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

      8. associate-+l+42.6%

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

      9. metadata-eval42.6%

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

      10. metadata-eval42.6%

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

      11. +-rgt-identity42.6%

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

   3. Simplified42.6%

      \[\leadsto \color{blue}{\frac{2}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \left(\tan k \cdot {\left(\frac{k}{t}\right)}^{2}\right)}} \]
   4. Step-by-step derivation

      1. add-sqr-sqrt17.5%

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

      2. *-un-lft-identity17.5%

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

      3. times-frac17.5%

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

      4. sqrt-pow117.5%

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

      5. metadata-eval17.5%

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

      6. sqrt-pow119.5%

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

      7. metadata-eval19.5%

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

   5. Applied egg-rr19.5%

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

   6. Taylor expanded in t around -inf 0.0%

      \[\leadsto \frac{2}{\color{blue}{-1 \cdot \frac{{k}^{2} \cdot \left({\left(\sqrt{-1}\right)}^{2} \cdot \left({\sin k}^{2} \cdot t\right)\right)}{\cos k \cdot {\ell}^{2}}}} \]
   7. Step-by-step derivation

      1. mul-1-neg0.0%

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

      2. times-frac0.0%

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

      3. unpow20.0%

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

      4. distribute-rgt-neg-in0.0%

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

      5. associate-/l*0.0%

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

      6. *-commutative0.0%

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

      7. *-commutative0.0%

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

      8. unpow20.0%

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

      9. rem-square-sqrt73.4%

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

      10. unpow273.4%

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

      11. times-frac76.3%

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

   8. Simplified76.3%

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

   9. Taylor expanded in k around 0 66.2%

      \[\leadsto \frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\color{blue}{-1 \cdot \frac{{k}^{2} \cdot t}{{\ell}^{2}}}\right)} \]
   10. Step-by-step derivation

       1. mul-1-neg66.2%

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

       2. associate-/l*66.8%

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

       3. unpow266.8%

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

       4. unpow266.8%

          \[\leadsto \frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\left(-\frac{k \cdot k}{\frac{\color{blue}{\ell \cdot \ell}}{t}}\right)\right)} \]

   11. Simplified66.8%

       \[\leadsto \frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \left(-\color{blue}{\left(-\frac{k \cdot k}{\frac{\ell \cdot \ell}{t}}\right)}\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification75.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \leq 10^{-68}:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \frac{2 \cdot \frac{\ell}{k}}{k \cdot \left(k \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{2}{\frac{k}{\frac{\cos k}{k}} \cdot \frac{k \cdot k}{\frac{\ell \cdot \ell}{t}}}\\ \end{array} \]

1. Split input into 2 regimes

2. if k < -2.69999999999999993e97 or -7.4e21 < k

   1. Initial program 37.2%

      \[\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. Step-by-step derivation

      1. associate-*l*37.2%

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

      2. associate-*l*37.2%

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

      3. associate-/r*37.2%

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

      4. associate-/r/37.2%

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

      5. *-commutative37.2%

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

      6. times-frac37.7%

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

      7. +-commutative37.7%

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

      8. associate--l+44.1%

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

      9. metadata-eval44.1%

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

      10. +-rgt-identity44.1%

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

      11. times-frac48.0%

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

   3. Simplified48.0%

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

   4. Taylor expanded in t around 0 77.4%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow277.4%

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

   6. Simplified77.4%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/77.4%

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

      2. associate-*l*83.2%

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

   8. Applied egg-rr83.2%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/83.2%

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

      2. *-commutative83.2%

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

      3. associate-*l*87.3%

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

   10. Simplified87.3%

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

   11. Taylor expanded in k around 0 75.1%

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

   if -2.69999999999999993e97 < k < -7.4e21

   1. Initial program 6.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. Step-by-step derivation

      1. associate-*l*6.6%

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

      2. associate-*l*6.7%

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

      3. associate-/r*6.7%

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

      4. associate-/r/6.7%

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

      5. *-commutative6.7%

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

      6. times-frac6.6%

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

      7. +-commutative6.6%

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

      8. associate--l+19.9%

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

      9. metadata-eval19.9%

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

      10. +-rgt-identity19.9%

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

      11. times-frac20.0%

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

   3. Simplified20.0%

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

   4. Taylor expanded in t around 0 87.1%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow287.1%

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

   6. Simplified87.1%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/87.1%

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

      2. associate-*l*87.1%

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

   8. Applied egg-rr87.1%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/87.1%

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

      2. *-commutative87.1%

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

      3. associate-*l*93.3%

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

   10. Simplified93.3%

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

   11. Taylor expanded in k around 0 74.9%

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

   12. Taylor expanded in k around inf 81.6%

       \[\leadsto \frac{\ell}{\sin k} \cdot \color{blue}{\left(-0.6666666666666666 \cdot \frac{\ell}{k \cdot t}\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification75.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;k \leq -2.7 \cdot 10^{+97} \lor \neg \left(k \leq -7.4 \cdot 10^{+21}\right):\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \left(\frac{2}{k \cdot \left(k \cdot t\right)} \cdot \frac{\ell}{k}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \left(-0.6666666666666666 \cdot \frac{\ell}{k \cdot t}\right)\\ \end{array} \]

1. Split input into 3 regimes

2. if k < -3.20000000000000016e97

   1. Initial program 41.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. Step-by-step derivation

      1. associate-*l*41.8%

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

      2. associate-*l*41.8%

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

      3. associate-/r*41.8%

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

      4. associate-/r/41.8%

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

      5. *-commutative41.8%

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

      6. times-frac38.2%

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

      7. +-commutative38.2%

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

      8. associate--l+45.8%

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

      9. metadata-eval45.8%

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

      10. +-rgt-identity45.8%

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

      11. times-frac45.8%

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

   3. Simplified45.8%

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

   4. Taylor expanded in t around 0 61.8%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow261.8%

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

   6. Simplified61.8%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/61.8%

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

      2. associate-*l*68.7%

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

   8. Applied egg-rr68.7%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/68.7%

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

      2. *-commutative68.7%

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

      3. associate-*l*74.9%

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

   10. Simplified74.9%

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

   11. Taylor expanded in k around 0 59.3%

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

   if -3.20000000000000016e97 < k < -7.4e21

   1. Initial program 6.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. Step-by-step derivation

      1. associate-*l*6.6%

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

      2. associate-*l*6.7%

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

      3. associate-/r*6.7%

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

      4. associate-/r/6.7%

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

      5. *-commutative6.7%

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

      6. times-frac6.6%

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

      7. +-commutative6.6%

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

      8. associate--l+19.9%

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

      9. metadata-eval19.9%

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

      10. +-rgt-identity19.9%

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

      11. times-frac20.0%

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

   3. Simplified20.0%

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

   4. Taylor expanded in t around 0 87.1%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow287.1%

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

   6. Simplified87.1%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/87.1%

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

      2. associate-*l*87.1%

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

   8. Applied egg-rr87.1%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/87.1%

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

      2. *-commutative87.1%

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

      3. associate-*l*93.3%

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

   10. Simplified93.3%

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

   11. Taylor expanded in k around 0 74.9%

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

   12. Taylor expanded in k around inf 81.6%

       \[\leadsto \frac{\ell}{\sin k} \cdot \color{blue}{\left(-0.6666666666666666 \cdot \frac{\ell}{k \cdot t}\right)} \]

   if -7.4e21 < k

   1. Initial program 35.9%

      \[\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. Step-by-step derivation

      1. associate-*l*35.9%

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

      2. associate-*l*35.9%

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

      3. associate-/r*36.0%

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

      4. associate-/r/36.0%

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

      5. *-commutative36.0%

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

      6. times-frac37.5%

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

      7. +-commutative37.5%

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

      8. associate--l+43.7%

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

      9. metadata-eval43.7%

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

      10. +-rgt-identity43.7%

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

      11. times-frac48.6%

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

   3. Simplified48.6%

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

   4. Taylor expanded in t around 0 81.8%

      \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   5. Step-by-step derivation

      1. unpow281.8%

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

   6. Simplified81.8%

      \[\leadsto \color{blue}{\frac{2}{\left(k \cdot k\right) \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
   7. Step-by-step derivation

      1. associate-*l/81.8%

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

      2. associate-*l*87.3%

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

   8. Applied egg-rr87.3%

      \[\leadsto \color{blue}{\frac{2 \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right)}{k \cdot \left(k \cdot t\right)}} \]
   9. Step-by-step derivation

      1. associate-*l/87.2%

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

      2. *-commutative87.2%

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

      3. associate-*l*90.7%

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

   10. Simplified90.7%

       \[\leadsto \color{blue}{\frac{\ell}{\sin k} \cdot \left(\frac{\ell}{\tan k} \cdot \frac{2}{k \cdot \left(k \cdot t\right)}\right)} \]
   11. Step-by-step derivation

       1. associate-*r/90.8%

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

   12. Applied egg-rr90.8%

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

   13. Taylor expanded in k around 0 79.6%

       \[\leadsto \frac{\ell}{\sin k} \cdot \frac{\color{blue}{\frac{\ell}{k}} \cdot 2}{k \cdot \left(k \cdot t\right)} \]
3. Recombined 3 regimes into one program.

4. Final simplification75.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;k \leq -3.2 \cdot 10^{+97}:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \left(\frac{2}{k \cdot \left(k \cdot t\right)} \cdot \frac{\ell}{k}\right)\\ \mathbf{elif}\;k \leq -7.4 \cdot 10^{+21}:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \left(-0.6666666666666666 \cdot \frac{\ell}{k \cdot t}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\ell}{\sin k} \cdot \frac{2 \cdot \frac{\ell}{k}}{k \cdot \left(k \cdot t\right)}\\ \end{array} \]

1. Initial program 35.4%

   \[\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. Step-by-step derivation

   1. associate-*l*35.4%

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

   2. associate-*l*35.4%

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

   3. associate-/r*35.5%

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

   4. associate-/r/35.5%

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

   5. *-commutative35.5%

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

   6. times-frac35.8%

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

   7. +-commutative35.8%

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

   8. associate--l+42.7%

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

   9. metadata-eval42.7%

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

   10. +-rgt-identity42.7%

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

   11. times-frac46.4%

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

3. Simplified46.4%

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

4. Taylor expanded in t around 0 78.0%

   \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
5. Step-by-step derivation

   1. unpow278.0%

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

6. Simplified78.0%

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

7. Taylor expanded in k around 0 69.5%

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

8. Final simplification69.5%

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

1. Initial program 35.4%

   \[\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. Step-by-step derivation

   1. associate-*l*35.4%

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

   2. associate-*l*35.4%

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

   3. associate-/r*35.5%

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

   4. associate-/r/35.5%

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

   5. *-commutative35.5%

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

   6. times-frac35.8%

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

   7. +-commutative35.8%

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

   8. associate--l+42.7%

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

   9. metadata-eval42.7%

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

   10. +-rgt-identity42.7%

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

   11. times-frac46.4%

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

3. Simplified46.4%

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

4. Taylor expanded in t around 0 78.0%

   \[\leadsto \color{blue}{\frac{2}{{k}^{2} \cdot t}} \cdot \left(\frac{\ell}{\sin k} \cdot \frac{\ell}{\tan k}\right) \]
5. Step-by-step derivation

   1. unpow278.0%

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

6. Simplified78.0%

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

7. Taylor expanded in k around 0 68.3%

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

8. Taylor expanded in k around 0 69.5%

   \[\leadsto \frac{2}{\left(k \cdot k\right) \cdot t} \cdot \left(\color{blue}{\frac{\ell}{k}} \cdot \left(-0.3333333333333333 \cdot \left(k \cdot \ell\right) + \frac{\ell}{k}\right)\right) \]

9. Final simplification69.5%

   \[\leadsto \frac{2}{t \cdot \left(k \cdot k\right)} \cdot \left(\frac{\ell}{k} \cdot \left(\frac{\ell}{k} + -0.3333333333333333 \cdot \left(k \cdot \ell\right)\right)\right) \]

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