Derivation

Split input into 2 regimes
if (* l l) < 3.5206845039667455e-117 or 1.774355983930986e+307 < (* l l)
1. Initial program 48.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. Initial simplification28.9
  \[\leadsto \frac{\frac{\frac{2}{\tan k}}{\frac{\sin k \cdot t}{\frac{\ell}{t} \cdot \frac{\ell}{t}}}}{\frac{k}{t} \cdot \frac{k}{t}}\]
3. Using strategy rm
4. Applied times-frac27.4
  \[\leadsto \frac{\frac{\frac{2}{\tan k}}{\color{blue}{\frac{\sin k}{\frac{\ell}{t}} \cdot \frac{t}{\frac{\ell}{t}}}}}{\frac{k}{t} \cdot \frac{k}{t}}\]
5. Applied add-cube-cbrt27.5
  \[\leadsto \frac{\frac{\color{blue}{\left(\sqrt[3]{\frac{2}{\tan k}} \cdot \sqrt[3]{\frac{2}{\tan k}}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}}}{\frac{\sin k}{\frac{\ell}{t}} \cdot \frac{t}{\frac{\ell}{t}}}}{\frac{k}{t} \cdot \frac{k}{t}}\]
6. Applied times-frac27.0
  \[\leadsto \frac{\color{blue}{\frac{\sqrt[3]{\frac{2}{\tan k}} \cdot \sqrt[3]{\frac{2}{\tan k}}}{\frac{\sin k}{\frac{\ell}{t}}} \cdot \frac{\sqrt[3]{\frac{2}{\tan k}}}{\frac{t}{\frac{\ell}{t}}}}}{\frac{k}{t} \cdot \frac{k}{t}}\]
7. Applied times-frac16.2
  \[\leadsto \color{blue}{\frac{\frac{\sqrt[3]{\frac{2}{\tan k}} \cdot \sqrt[3]{\frac{2}{\tan k}}}{\frac{\sin k}{\frac{\ell}{t}}}}{\frac{k}{t}} \cdot \frac{\frac{\sqrt[3]{\frac{2}{\tan k}}}{\frac{t}{\frac{\ell}{t}}}}{\frac{k}{t}}}\]
8. Simplified10.4
  \[\leadsto \frac{\frac{\sqrt[3]{\frac{2}{\tan k}} \cdot \sqrt[3]{\frac{2}{\tan k}}}{\frac{\sin k}{\frac{\ell}{t}}}}{\frac{k}{t}} \cdot \color{blue}{\left(\left(\frac{1}{k} \cdot \frac{\ell}{t}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}\right)}\]
9. Using strategy rm
10. Applied div-inv10.4
  \[\leadsto \frac{\frac{\sqrt[3]{\frac{2}{\tan k}} \cdot \sqrt[3]{\frac{2}{\tan k}}}{\frac{\sin k}{\frac{\ell}{t}}}}{\color{blue}{k \cdot \frac{1}{t}}} \cdot \left(\left(\frac{1}{k} \cdot \frac{\ell}{t}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}\right)\]
11. Applied add-cube-cbrt10.5
  \[\leadsto \frac{\frac{\sqrt[3]{\frac{2}{\tan k}} \cdot \sqrt[3]{\frac{2}{\tan k}}}{\color{blue}{\left(\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}} \cdot \sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}\right) \cdot \sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}}}{k \cdot \frac{1}{t}} \cdot \left(\left(\frac{1}{k} \cdot \frac{\ell}{t}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}\right)\]
12. Applied times-frac10.5
  \[\leadsto \frac{\color{blue}{\frac{\sqrt[3]{\frac{2}{\tan k}}}{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}} \cdot \sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}} \cdot \frac{\sqrt[3]{\frac{2}{\tan k}}}{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}}}{k \cdot \frac{1}{t}} \cdot \left(\left(\frac{1}{k} \cdot \frac{\ell}{t}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}\right)\]
13. Applied times-frac8.2
  \[\leadsto \color{blue}{\left(\frac{\frac{\sqrt[3]{\frac{2}{\tan k}}}{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}} \cdot \sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}}{k} \cdot \frac{\frac{\sqrt[3]{\frac{2}{\tan k}}}{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}}{\frac{1}{t}}\right)} \cdot \left(\left(\frac{1}{k} \cdot \frac{\ell}{t}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}\right)\]
14. Simplified8.2
  \[\leadsto \left(\frac{\frac{\sqrt[3]{\frac{2}{\tan k}}}{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}} \cdot \sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}}{k} \cdot \color{blue}{\frac{t}{\frac{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}{\sqrt[3]{\frac{2}{\tan k}}}}}\right) \cdot \left(\left(\frac{1}{k} \cdot \frac{\ell}{t}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}\right)\]
15. Using strategy rm
16. Applied cbrt-div8.1
  \[\leadsto \left(\frac{\frac{\sqrt[3]{\frac{2}{\tan k}}}{\color{blue}{\frac{\sqrt[3]{\sin k}}{\sqrt[3]{\frac{\ell}{t}}}} \cdot \sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}}{k} \cdot \frac{t}{\frac{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}{\sqrt[3]{\frac{2}{\tan k}}}}\right) \cdot \left(\left(\frac{1}{k} \cdot \frac{\ell}{t}\right) \cdot \sqrt[3]{\frac{2}{\tan k}}\right)\]
if 3.5206845039667455e-117 < (* l l) < 1.774355983930986e+307
1. Initial program 44.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. Initial simplification34.4
  \[\leadsto \frac{\frac{\frac{2}{\tan k}}{\frac{\sin k \cdot t}{\frac{\ell}{t} \cdot \frac{\ell}{t}}}}{\frac{k}{t} \cdot \frac{k}{t}}\]
3. Using strategy rm
4. Applied associate-/r/34.1
  \[\leadsto \frac{\color{blue}{\frac{\frac{2}{\tan k}}{\sin k \cdot t} \cdot \left(\frac{\ell}{t} \cdot \frac{\ell}{t}\right)}}{\frac{k}{t} \cdot \frac{k}{t}}\]
5. Applied times-frac22.6
  \[\leadsto \color{blue}{\frac{\frac{\frac{2}{\tan k}}{\sin k \cdot t}}{\frac{k}{t}} \cdot \frac{\frac{\ell}{t} \cdot \frac{\ell}{t}}{\frac{k}{t}}}\]
6. Simplified22.6
  \[\leadsto \color{blue}{\frac{\frac{\frac{2}{k}}{\sin k}}{\tan k}} \cdot \frac{\frac{\ell}{t} \cdot \frac{\ell}{t}}{\frac{k}{t}}\]
7. Simplified4.6
  \[\leadsto \frac{\frac{\frac{2}{k}}{\sin k}}{\tan k} \cdot \color{blue}{\frac{\ell \cdot \ell}{t \cdot k}}\]
Recombined 2 regimes into one program.
Final simplification6.9
\[\leadsto \begin{array}{l} \mathbf{if}\;\ell \cdot \ell \le 3.5206845039667455 \cdot 10^{-117} \lor \neg \left(\ell \cdot \ell \le 1.774355983930986 \cdot 10^{+307}\right):\\ \;\;\;\;\left(\sqrt[3]{\frac{2}{\tan k}} \cdot \left(\frac{1}{k} \cdot \frac{\ell}{t}\right)\right) \cdot \left(\frac{t}{\frac{\sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}{\sqrt[3]{\frac{2}{\tan k}}}} \cdot \frac{\frac{\sqrt[3]{\frac{2}{\tan k}}}{\frac{\sqrt[3]{\sin k}}{\sqrt[3]{\frac{\ell}{t}}} \cdot \sqrt[3]{\frac{\sin k}{\frac{\ell}{t}}}}}{k}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\ell \cdot \ell}{k \cdot t} \cdot \frac{\frac{\frac{2}{k}}{\sin k}}{\tan k}\\ \end{array}\]

Error

Try it out

Derivation

`if (* l l) < 3.5206845039667455e-117 or 1.774355983930986e+307 < (* l l)`

`if 3.5206845039667455e-117 < (* l l) < 1.774355983930986e+307`

Runtime

In
Out