Toniolo and Linder, Equation (10-)

Average Error: 48.2 → 18.1

Time: 47.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;t \le -9.5806908744214479 \cdot 10^{119}:\\ \;\;\;\;2 \cdot \left({\left(\frac{\sqrt{1}}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left(\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}}{\sqrt[3]{{\left(\sin k\right)}^{2}} \cdot \sqrt[3]{{\left(\sin k\right)}^{2}}} \cdot \frac{\cos k \cdot {\ell}^{2}}{\sqrt[3]{{\left(\sin k\right)}^{2}}}\right)\right)\\ \mathbf{elif}\;t \le -6.4170747030907667 \cdot 10^{-80}:\\ \;\;\;\;\frac{\frac{\sqrt{2}}{\frac{\sqrt[3]{{t}^{3}} \cdot \sqrt[3]{{t}^{3}}}{\ell}}}{\sin k \cdot \tan k} \cdot \frac{\frac{\sqrt{2}}{\frac{\sqrt[3]{{t}^{3}}}{\ell}}}{{\left(\frac{k}{t}\right)}^{2}}\\ \mathbf{elif}\;t \le 1.7472655777358584 \cdot 10^{-199}:\\ \;\;\;\;2 \cdot \left(\left(\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}}{\sin k} \cdot {\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1}\right) \cdot \frac{\cos k \cdot {\ell}^{2}}{\sin k}\right)\\ \mathbf{elif}\;t \le 4.331663927949164 \cdot 10^{-163}:\\ \;\;\;\;\frac{\frac{\sqrt{2}}{\frac{{\left(\sqrt{t}\right)}^{3}}{\ell}}}{\sin k \cdot \tan k} \cdot \frac{\frac{\sqrt{2}}{\frac{{\left(\sqrt{t}\right)}^{3}}{\ell}}}{{\left(\frac{k}{t}\right)}^{2}}\\ \mathbf{elif}\;t \le 2.21127017487973713 \cdot 10^{-96}:\\ \;\;\;\;2 \cdot \left(\left(\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}}{\sin k} \cdot {\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1}\right) \cdot \frac{\cos k \cdot {\ell}^{2}}{\sin k}\right)\\ \mathbf{elif}\;t \le 4.09195981999163155 \cdot 10^{194}:\\ \;\;\;\;\frac{\frac{\ell}{{t}^{\left(\frac{3}{2}\right)}}}{\sin k \cdot \tan k} \cdot \frac{\frac{2}{\frac{{t}^{\left(\frac{3}{2}\right)}}{\ell}}}{{\left(\frac{k}{t}\right)}^{2}}\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left({\left(\frac{1}{{k}^{2} \cdot {t}^{1}}\right)}^{1} \cdot \left(\frac{\cos k}{\left|\sin k\right|} \cdot \frac{\ell}{\frac{\left|\sin k\right|}{\ell}}\right)\right)\\ \end{array}\]

C

double f(double t, double l, double k) {
        double r119624 = 2.0;
        double r119625 = t;
        double r119626 = 3.0;
        double r119627 = pow(r119625, r119626);
        double r119628 = l;
        double r119629 = r119628 * r119628;
        double r119630 = r119627 / r119629;
        double r119631 = k;
        double r119632 = sin(r119631);
        double r119633 = r119630 * r119632;
        double r119634 = tan(r119631);
        double r119635 = r119633 * r119634;
        double r119636 = 1.0;
        double r119637 = r119631 / r119625;
        double r119638 = pow(r119637, r119624);
        double r119639 = r119636 + r119638;
        double r119640 = r119639 - r119636;
        double r119641 = r119635 * r119640;
        double r119642 = r119624 / r119641;
        return r119642;
}

↓

double f(double t, double l, double k) {
        double r119643 = t;
        double r119644 = -9.580690874421448e+119;
        bool r119645 = r119643 <= r119644;
        double r119646 = 2.0;
        double r119647 = 1.0;
        double r119648 = sqrt(r119647);
        double r119649 = k;
        double r119650 = 2.0;
        double r119651 = r119646 / r119650;
        double r119652 = pow(r119649, r119651);
        double r119653 = r119648 / r119652;
        double r119654 = 1.0;
        double r119655 = pow(r119653, r119654);
        double r119656 = pow(r119643, r119654);
        double r119657 = r119652 * r119656;
        double r119658 = r119647 / r119657;
        double r119659 = pow(r119658, r119654);
        double r119660 = sin(r119649);
        double r119661 = pow(r119660, r119650);
        double r119662 = cbrt(r119661);
        double r119663 = r119662 * r119662;
        double r119664 = r119659 / r119663;
        double r119665 = cos(r119649);
        double r119666 = l;
        double r119667 = pow(r119666, r119650);
        double r119668 = r119665 * r119667;
        double r119669 = r119668 / r119662;
        double r119670 = r119664 * r119669;
        double r119671 = r119655 * r119670;
        double r119672 = r119646 * r119671;
        double r119673 = -6.417074703090767e-80;
        bool r119674 = r119643 <= r119673;
        double r119675 = sqrt(r119646);
        double r119676 = 3.0;
        double r119677 = pow(r119643, r119676);
        double r119678 = cbrt(r119677);
        double r119679 = r119678 * r119678;
        double r119680 = r119679 / r119666;
        double r119681 = r119675 / r119680;
        double r119682 = tan(r119649);
        double r119683 = r119660 * r119682;
        double r119684 = r119681 / r119683;
        double r119685 = r119678 / r119666;
        double r119686 = r119675 / r119685;
        double r119687 = r119649 / r119643;
        double r119688 = pow(r119687, r119646);
        double r119689 = r119686 / r119688;
        double r119690 = r119684 * r119689;
        double r119691 = 1.7472655777358584e-199;
        bool r119692 = r119643 <= r119691;
        double r119693 = r119659 / r119660;
        double r119694 = r119647 / r119652;
        double r119695 = pow(r119694, r119654);
        double r119696 = r119693 * r119695;
        double r119697 = r119668 / r119660;
        double r119698 = r119696 * r119697;
        double r119699 = r119646 * r119698;
        double r119700 = 4.331663927949164e-163;
        bool r119701 = r119643 <= r119700;
        double r119702 = sqrt(r119643);
        double r119703 = pow(r119702, r119676);
        double r119704 = r119703 / r119666;
        double r119705 = r119675 / r119704;
        double r119706 = r119705 / r119683;
        double r119707 = r119705 / r119688;
        double r119708 = r119706 * r119707;
        double r119709 = 2.211270174879737e-96;
        bool r119710 = r119643 <= r119709;
        double r119711 = 4.0919598199916316e+194;
        bool r119712 = r119643 <= r119711;
        double r119713 = r119676 / r119650;
        double r119714 = pow(r119643, r119713);
        double r119715 = r119666 / r119714;
        double r119716 = r119715 / r119683;
        double r119717 = r119714 / r119666;
        double r119718 = r119646 / r119717;
        double r119719 = r119718 / r119688;
        double r119720 = r119716 * r119719;
        double r119721 = pow(r119649, r119646);
        double r119722 = r119721 * r119656;
        double r119723 = r119647 / r119722;
        double r119724 = pow(r119723, r119654);
        double r119725 = fabs(r119660);
        double r119726 = r119665 / r119725;
        double r119727 = r119725 / r119666;
        double r119728 = r119666 / r119727;
        double r119729 = r119726 * r119728;
        double r119730 = r119724 * r119729;
        double r119731 = r119646 * r119730;
        double r119732 = r119712 ? r119720 : r119731;
        double r119733 = r119710 ? r119699 : r119732;
        double r119734 = r119701 ? r119708 : r119733;
        double r119735 = r119692 ? r119699 : r119734;
        double r119736 = r119674 ? r119690 : r119735;
        double r119737 = r119645 ? r119672 : r119736;
        return r119737;
}

Error

Bits error versus t

Bits error versus l

Bits error versus k

Derivation

1. Split input into 6 regimes

2. if t < -9.580690874421448e+119

   1. Initial program 53.7

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

   2. Simplified 39.3

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

   3. Taylor expanded around inf 21.4

      \[\leadsto \color{blue}{2 \cdot \left({\left(\frac{1}{{k}^{2} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot {\ell}^{2}}{{\left(\sin k\right)}^{2}}\right)}\]
   4. Using strategy rm

   5. Applied sqr-pow 21.4

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

   6. Applied associate-*l* 21.4

      \[\leadsto 2 \cdot \left({\left(\frac{1}{\color{blue}{{k}^{\left(\frac{2}{2}\right)} \cdot \left({k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}\right)}}\right)}^{1} \cdot \frac{\cos k \cdot {\ell}^{2}}{{\left(\sin k\right)}^{2}}\right)\]
   7. Using strategy rm

   8. Applied add-sqr-sqrt 21.4

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

   9. Applied times-frac 21.1

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

   10. Applied unpow-prod-down 21.1

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

   11. Applied associate-*l* 19.9

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

   12. Simplified 20.2

       \[\leadsto 2 \cdot \left({\left(\frac{\sqrt{1}}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \color{blue}{\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot {\ell}^{2}\right)}{{\left(\sin k\right)}^{2}}}\right)\]
   13. Using strategy rm

   14. Applied add-cube-cbrt 20.3

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

   15. Applied times-frac 19.2

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

   if -9.580690874421448e+119 < t < -6.417074703090767e-80

   1. Initial program 32.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. Simplified 24.6

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

   4. Applied add-cube-cbrt 24.7

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

   5. Applied times-frac 21.3

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

   6. Applied add-sqr-sqrt 21.3

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

   7. Applied times-frac 21.3

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

   8. Applied times-frac 14.8

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

   if -6.417074703090767e-80 < t < 1.7472655777358584e-199 or 4.331663927949164e-163 < t < 2.211270174879737e-96

   1. Initial program 60.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. Simplified 60.6

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

   3. Taylor expanded around inf 25.8

      \[\leadsto \color{blue}{2 \cdot \left({\left(\frac{1}{{k}^{2} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot {\ell}^{2}}{{\left(\sin k\right)}^{2}}\right)}\]
   4. Using strategy rm

   5. Applied sqr-pow 25.8

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

   6. Applied associate-*l* 19.2

      \[\leadsto 2 \cdot \left({\left(\frac{1}{\color{blue}{{k}^{\left(\frac{2}{2}\right)} \cdot \left({k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}\right)}}\right)}^{1} \cdot \frac{\cos k \cdot {\ell}^{2}}{{\left(\sin k\right)}^{2}}\right)\]
   7. Using strategy rm

   8. Applied add-sqr-sqrt 19.2

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

   9. Applied times-frac 19.1

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

   10. Applied unpow-prod-down 19.1

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

   11. Applied associate-*l* 18.7

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

   12. Simplified 18.7

       \[\leadsto 2 \cdot \left({\left(\frac{\sqrt{1}}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \color{blue}{\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot {\ell}^{2}\right)}{{\left(\sin k\right)}^{2}}}\right)\]
   13. Using strategy rm

   14. Applied unpow2 18.7

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

   15. Applied times-frac 19.2

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

   16. Applied associate-*r* 19.8

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

   17. Simplified 19.8

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

   if 1.7472655777358584e-199 < t < 4.331663927949164e-163

   1. Initial program 64.0

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

   2. Simplified 64.0

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

   4. Applied add-sqr-sqrt 64.0

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

   5. Applied unpow-prod-down 64.0

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

   6. Applied times-frac 39.1

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

   7. Applied add-sqr-sqrt 39.1

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

   8. Applied times-frac 39.1

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

   9. Applied times-frac 33.1

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

   if 2.211270174879737e-96 < t < 4.0919598199916316e+194

   1. Initial program 36.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. Simplified 28.9

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

   4. Applied sqr-pow 28.9

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

   5. Applied times-frac 21.5

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

   6. Applied *-un-lft-identity 21.5

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

   7. Applied times-frac 21.4

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

   8. Applied times-frac 15.2

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

   9. Simplified 15.2

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

   if 4.0919598199916316e+194 < t

   1. Initial program 55.8

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

   2. Simplified 40.7

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

   3. Taylor expanded around inf 20.4

      \[\leadsto \color{blue}{2 \cdot \left({\left(\frac{1}{{k}^{2} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot {\ell}^{2}}{{\left(\sin k\right)}^{2}}\right)}\]
   4. Using strategy rm

   5. Applied add-sqr-sqrt 20.4

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

   6. Applied times-frac 20.4

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

   7. Simplified 20.4

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

   8. Simplified 19.4

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

4. Final simplification 18.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \le -9.5806908744214479 \cdot 10^{119}:\\ \;\;\;\;2 \cdot \left({\left(\frac{\sqrt{1}}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left(\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}}{\sqrt[3]{{\left(\sin k\right)}^{2}} \cdot \sqrt[3]{{\left(\sin k\right)}^{2}}} \cdot \frac{\cos k \cdot {\ell}^{2}}{\sqrt[3]{{\left(\sin k\right)}^{2}}}\right)\right)\\ \mathbf{elif}\;t \le -6.4170747030907667 \cdot 10^{-80}:\\ \;\;\;\;\frac{\frac{\sqrt{2}}{\frac{\sqrt[3]{{t}^{3}} \cdot \sqrt[3]{{t}^{3}}}{\ell}}}{\sin k \cdot \tan k} \cdot \frac{\frac{\sqrt{2}}{\frac{\sqrt[3]{{t}^{3}}}{\ell}}}{{\left(\frac{k}{t}\right)}^{2}}\\ \mathbf{elif}\;t \le 1.7472655777358584 \cdot 10^{-199}:\\ \;\;\;\;2 \cdot \left(\left(\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}}{\sin k} \cdot {\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1}\right) \cdot \frac{\cos k \cdot {\ell}^{2}}{\sin k}\right)\\ \mathbf{elif}\;t \le 4.331663927949164 \cdot 10^{-163}:\\ \;\;\;\;\frac{\frac{\sqrt{2}}{\frac{{\left(\sqrt{t}\right)}^{3}}{\ell}}}{\sin k \cdot \tan k} \cdot \frac{\frac{\sqrt{2}}{\frac{{\left(\sqrt{t}\right)}^{3}}{\ell}}}{{\left(\frac{k}{t}\right)}^{2}}\\ \mathbf{elif}\;t \le 2.21127017487973713 \cdot 10^{-96}:\\ \;\;\;\;2 \cdot \left(\left(\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}}{\sin k} \cdot {\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1}\right) \cdot \frac{\cos k \cdot {\ell}^{2}}{\sin k}\right)\\ \mathbf{elif}\;t \le 4.09195981999163155 \cdot 10^{194}:\\ \;\;\;\;\frac{\frac{\ell}{{t}^{\left(\frac{3}{2}\right)}}}{\sin k \cdot \tan k} \cdot \frac{\frac{2}{\frac{{t}^{\left(\frac{3}{2}\right)}}{\ell}}}{{\left(\frac{k}{t}\right)}^{2}}\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left({\left(\frac{1}{{k}^{2} \cdot {t}^{1}}\right)}^{1} \cdot \left(\frac{\cos k}{\left|\sin k\right|} \cdot \frac{\ell}{\frac{\left|\sin k\right|}{\ell}}\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020047 +o rules:numerics
(FPCore (t l k)
  :name "Toniolo and Linder, Equation (10-)"
  :precision binary64
  (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (- (+ 1 (pow (/ k t) 2)) 1))))