Henrywood and Agarwal, Equation (12)

Average Error: 25.3 → 9.7

Time: 1.1m

Precision: 64

Math

\[\left({\left(\frac{d}{h}\right)}^{\left(\frac{1}{2}\right)} \cdot {\left(\frac{d}{\ell}\right)}^{\left(\frac{1}{2}\right)}\right) \cdot \left(1 - \left(\frac{1}{2} \cdot {\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2}\right) \cdot \frac{h}{\ell}\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;\left(1 - \frac{h}{\ell} \cdot \left({\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2} \cdot \frac{1}{2}\right)\right) \cdot \left({\left(\frac{d}{\ell}\right)}^{\frac{1}{2}} \cdot {\left(\frac{d}{h}\right)}^{\frac{1}{2}}\right) \le -3.091515759590372 \cdot 10^{+302}:\\ \;\;\;\;\left(\sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}} \cdot \left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right|\right) \cdot \left(\sqrt{\frac{\sqrt[3]{d}}{\ell}} \cdot \left|\sqrt[3]{d}\right| - h \cdot \left(\left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell} \cdot \left(\sqrt{\frac{d}{\sqrt[3]{\ell}}} \cdot \sqrt{\frac{1}{\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}}}\right)\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right)\right)\\ \mathbf{elif}\;\left(1 - \frac{h}{\ell} \cdot \left({\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2} \cdot \frac{1}{2}\right)\right) \cdot \left({\left(\frac{d}{\ell}\right)}^{\frac{1}{2}} \cdot {\left(\frac{d}{h}\right)}^{\frac{1}{2}}\right) \le -5.77055822624534 \cdot 10^{-99}:\\ \;\;\;\;\left(1 - \frac{h}{\ell} \cdot \left({\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2} \cdot \frac{1}{2}\right)\right) \cdot \left({\left(\frac{d}{\ell}\right)}^{\frac{1}{2}} \cdot {\left(\frac{d}{h}\right)}^{\frac{1}{2}}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}} \cdot \left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right|\right) \cdot \left(\sqrt{\frac{\sqrt[3]{d}}{\ell}} \cdot \left|\sqrt[3]{d}\right| - h \cdot \left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{2} \cdot \left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell} \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}}\right)\right)\right)\right)\\ \end{array}\]

C

double f(double d, double h, double l, double M, double D) {
        double r6091333 = d;
        double r6091334 = h;
        double r6091335 = r6091333 / r6091334;
        double r6091336 = 1.0;
        double r6091337 = 2.0;
        double r6091338 = r6091336 / r6091337;
        double r6091339 = pow(r6091335, r6091338);
        double r6091340 = l;
        double r6091341 = r6091333 / r6091340;
        double r6091342 = pow(r6091341, r6091338);
        double r6091343 = r6091339 * r6091342;
        double r6091344 = M;
        double r6091345 = D;
        double r6091346 = r6091344 * r6091345;
        double r6091347 = r6091337 * r6091333;
        double r6091348 = r6091346 / r6091347;
        double r6091349 = pow(r6091348, r6091337);
        double r6091350 = r6091338 * r6091349;
        double r6091351 = r6091334 / r6091340;
        double r6091352 = r6091350 * r6091351;
        double r6091353 = r6091336 - r6091352;
        double r6091354 = r6091343 * r6091353;
        return r6091354;
}

↓

double f(double d, double h, double l, double M, double D) {
        double r6091355 = 1.0;
        double r6091356 = h;
        double r6091357 = l;
        double r6091358 = r6091356 / r6091357;
        double r6091359 = M;
        double r6091360 = D;
        double r6091361 = r6091359 * r6091360;
        double r6091362 = 2.0;
        double r6091363 = d;
        double r6091364 = r6091362 * r6091363;
        double r6091365 = r6091361 / r6091364;
        double r6091366 = pow(r6091365, r6091362);
        double r6091367 = 0.5;
        double r6091368 = r6091366 * r6091367;
        double r6091369 = r6091358 * r6091368;
        double r6091370 = r6091355 - r6091369;
        double r6091371 = r6091363 / r6091357;
        double r6091372 = pow(r6091371, r6091367);
        double r6091373 = r6091363 / r6091356;
        double r6091374 = pow(r6091373, r6091367);
        double r6091375 = r6091372 * r6091374;
        double r6091376 = r6091370 * r6091375;
        double r6091377 = -3.091515759590372e+302;
        bool r6091378 = r6091376 <= r6091377;
        double r6091379 = cbrt(r6091363);
        double r6091380 = cbrt(r6091356);
        double r6091381 = r6091379 / r6091380;
        double r6091382 = sqrt(r6091381);
        double r6091383 = fabs(r6091381);
        double r6091384 = r6091382 * r6091383;
        double r6091385 = r6091379 / r6091357;
        double r6091386 = sqrt(r6091385);
        double r6091387 = fabs(r6091379);
        double r6091388 = r6091386 * r6091387;
        double r6091389 = r6091359 / r6091363;
        double r6091390 = r6091360 / r6091362;
        double r6091391 = r6091389 * r6091390;
        double r6091392 = r6091391 / r6091357;
        double r6091393 = cbrt(r6091357);
        double r6091394 = r6091363 / r6091393;
        double r6091395 = sqrt(r6091394);
        double r6091396 = r6091393 * r6091393;
        double r6091397 = r6091355 / r6091396;
        double r6091398 = sqrt(r6091397);
        double r6091399 = r6091395 * r6091398;
        double r6091400 = r6091392 * r6091399;
        double r6091401 = r6091391 / r6091362;
        double r6091402 = r6091400 * r6091401;
        double r6091403 = r6091356 * r6091402;
        double r6091404 = r6091388 - r6091403;
        double r6091405 = r6091384 * r6091404;
        double r6091406 = -5.77055822624534e-99;
        bool r6091407 = r6091376 <= r6091406;
        double r6091408 = r6091379 / r6091393;
        double r6091409 = fabs(r6091408);
        double r6091410 = sqrt(r6091408);
        double r6091411 = r6091409 * r6091410;
        double r6091412 = r6091392 * r6091411;
        double r6091413 = r6091401 * r6091412;
        double r6091414 = r6091356 * r6091413;
        double r6091415 = r6091388 - r6091414;
        double r6091416 = r6091384 * r6091415;
        double r6091417 = r6091407 ? r6091376 : r6091416;
        double r6091418 = r6091378 ? r6091405 : r6091417;
        return r6091418;
}

Error

Bits error versus d

Bits error versus h

Bits error versus l

Bits error versus M

Bits error versus D

Derivation

1. Split input into 3 regimes

2. if (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)))) < -3.091515759590372e+302

   1. Initial program 59.4

      \[\left({\left(\frac{d}{h}\right)}^{\left(\frac{1}{2}\right)} \cdot {\left(\frac{d}{\ell}\right)}^{\left(\frac{1}{2}\right)}\right) \cdot \left(1 - \left(\frac{1}{2} \cdot {\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2}\right) \cdot \frac{h}{\ell}\right)\]

   2. Simplified 51.7

      \[\leadsto \color{blue}{\left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\frac{d}{h}}}\]
   3. Using strategy rm

   4. Applied add-cube-cbrt 51.7

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\frac{d}{\color{blue}{\left(\sqrt[3]{h} \cdot \sqrt[3]{h}\right) \cdot \sqrt[3]{h}}}}\]

   5. Applied add-cube-cbrt 51.7

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\frac{\color{blue}{\left(\sqrt[3]{d} \cdot \sqrt[3]{d}\right) \cdot \sqrt[3]{d}}}{\left(\sqrt[3]{h} \cdot \sqrt[3]{h}\right) \cdot \sqrt[3]{h}}}\]

   6. Applied times-frac 51.7

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\color{blue}{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{\sqrt[3]{h} \cdot \sqrt[3]{h}} \cdot \frac{\sqrt[3]{d}}{\sqrt[3]{h}}}}\]

   7. Applied sqrt-prod 50.6

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \color{blue}{\left(\sqrt{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{\sqrt[3]{h} \cdot \sqrt[3]{h}}} \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)}\]

   8. Simplified 50.6

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\color{blue}{\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right|} \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]
   9. Using strategy rm

   10. Applied *-un-lft-identity 50.6

       \[\leadsto \left(\sqrt{\frac{d}{\color{blue}{1 \cdot \ell}}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   11. Applied add-cube-cbrt 50.6

       \[\leadsto \left(\sqrt{\frac{\color{blue}{\left(\sqrt[3]{d} \cdot \sqrt[3]{d}\right) \cdot \sqrt[3]{d}}}{1 \cdot \ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   12. Applied times-frac 50.6

       \[\leadsto \left(\sqrt{\color{blue}{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{1} \cdot \frac{\sqrt[3]{d}}{\ell}}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   13. Applied sqrt-prod 50.5

       \[\leadsto \left(\color{blue}{\sqrt{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{1}} \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   14. Simplified 50.5

       \[\leadsto \left(\color{blue}{\left|\sqrt[3]{d}\right|} \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]
   15. Using strategy rm

   16. Applied times-frac 37.4

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \color{blue}{\left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right)}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   17. Applied associate-*r* 32.2

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \color{blue}{\left(\left(\sqrt{\frac{d}{\ell}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right)} \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]
   18. Using strategy rm

   19. Applied add-cube-cbrt 32.3

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\sqrt{\frac{d}{\color{blue}{\left(\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}\right) \cdot \sqrt[3]{\ell}}}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   20. Applied *-un-lft-identity 32.3

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\sqrt{\frac{\color{blue}{1 \cdot d}}{\left(\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}\right) \cdot \sqrt[3]{\ell}}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   21. Applied times-frac 32.3

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\sqrt{\color{blue}{\frac{1}{\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}} \cdot \frac{d}{\sqrt[3]{\ell}}}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   22. Applied sqrt-prod 30.8

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\color{blue}{\left(\sqrt{\frac{1}{\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}}} \cdot \sqrt{\frac{d}{\sqrt[3]{\ell}}}\right)} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   if -3.091515759590372e+302 < (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)))) < -5.77055822624534e-99

   1. Initial program 1.3

      \[\left({\left(\frac{d}{h}\right)}^{\left(\frac{1}{2}\right)} \cdot {\left(\frac{d}{\ell}\right)}^{\left(\frac{1}{2}\right)}\right) \cdot \left(1 - \left(\frac{1}{2} \cdot {\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2}\right) \cdot \frac{h}{\ell}\right)\]

   if -5.77055822624534e-99 < (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l))))

   1. Initial program 25.0

      \[\left({\left(\frac{d}{h}\right)}^{\left(\frac{1}{2}\right)} \cdot {\left(\frac{d}{\ell}\right)}^{\left(\frac{1}{2}\right)}\right) \cdot \left(1 - \left(\frac{1}{2} \cdot {\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2}\right) \cdot \frac{h}{\ell}\right)\]

   2. Simplified 24.1

      \[\leadsto \color{blue}{\left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\frac{d}{h}}}\]
   3. Using strategy rm

   4. Applied add-cube-cbrt 24.4

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\frac{d}{\color{blue}{\left(\sqrt[3]{h} \cdot \sqrt[3]{h}\right) \cdot \sqrt[3]{h}}}}\]

   5. Applied add-cube-cbrt 24.5

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\frac{\color{blue}{\left(\sqrt[3]{d} \cdot \sqrt[3]{d}\right) \cdot \sqrt[3]{d}}}{\left(\sqrt[3]{h} \cdot \sqrt[3]{h}\right) \cdot \sqrt[3]{h}}}\]

   6. Applied times-frac 24.5

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \sqrt{\color{blue}{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{\sqrt[3]{h} \cdot \sqrt[3]{h}} \cdot \frac{\sqrt[3]{d}}{\sqrt[3]{h}}}}\]

   7. Applied sqrt-prod 17.7

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \color{blue}{\left(\sqrt{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{\sqrt[3]{h} \cdot \sqrt[3]{h}}} \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)}\]

   8. Simplified 16.6

      \[\leadsto \left(\sqrt{\frac{d}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\color{blue}{\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right|} \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]
   9. Using strategy rm

   10. Applied *-un-lft-identity 16.6

       \[\leadsto \left(\sqrt{\frac{d}{\color{blue}{1 \cdot \ell}}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   11. Applied add-cube-cbrt 16.8

       \[\leadsto \left(\sqrt{\frac{\color{blue}{\left(\sqrt[3]{d} \cdot \sqrt[3]{d}\right) \cdot \sqrt[3]{d}}}{1 \cdot \ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   12. Applied times-frac 16.8

       \[\leadsto \left(\sqrt{\color{blue}{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{1} \cdot \frac{\sqrt[3]{d}}{\ell}}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   13. Applied sqrt-prod 14.8

       \[\leadsto \left(\color{blue}{\sqrt{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{1}} \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   14. Simplified 14.8

       \[\leadsto \left(\color{blue}{\left|\sqrt[3]{d}\right|} \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \frac{\left(\frac{M}{d} \cdot \frac{D}{2}\right) \cdot \left(\frac{M}{d} \cdot \frac{D}{2}\right)}{\ell \cdot 2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]
   15. Using strategy rm

   16. Applied times-frac 13.7

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\sqrt{\frac{d}{\ell}} \cdot \color{blue}{\left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right)}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   17. Applied associate-*r* 13.7

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \color{blue}{\left(\left(\sqrt{\frac{d}{\ell}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right)} \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]
   18. Using strategy rm

   19. Applied add-cube-cbrt 13.7

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\sqrt{\frac{d}{\color{blue}{\left(\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}\right) \cdot \sqrt[3]{\ell}}}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   20. Applied add-cube-cbrt 13.7

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\sqrt{\frac{\color{blue}{\left(\sqrt[3]{d} \cdot \sqrt[3]{d}\right) \cdot \sqrt[3]{d}}}{\left(\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}\right) \cdot \sqrt[3]{\ell}}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   21. Applied times-frac 13.7

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\sqrt{\color{blue}{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}} \cdot \frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}}} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   22. Applied sqrt-prod 9.0

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\color{blue}{\left(\sqrt{\frac{\sqrt[3]{d} \cdot \sqrt[3]{d}}{\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}}} \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}}\right)} \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]

   23. Simplified 8.7

       \[\leadsto \left(\left|\sqrt[3]{d}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\ell}} - \left(\left(\left(\color{blue}{\left|\frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}\right|} \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell}\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right) \cdot h\right) \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}}\right)\]
3. Recombined 3 regimes into one program.

4. Final simplification 9.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(1 - \frac{h}{\ell} \cdot \left({\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2} \cdot \frac{1}{2}\right)\right) \cdot \left({\left(\frac{d}{\ell}\right)}^{\frac{1}{2}} \cdot {\left(\frac{d}{h}\right)}^{\frac{1}{2}}\right) \le -3.091515759590372 \cdot 10^{+302}:\\ \;\;\;\;\left(\sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}} \cdot \left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right|\right) \cdot \left(\sqrt{\frac{\sqrt[3]{d}}{\ell}} \cdot \left|\sqrt[3]{d}\right| - h \cdot \left(\left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell} \cdot \left(\sqrt{\frac{d}{\sqrt[3]{\ell}}} \cdot \sqrt{\frac{1}{\sqrt[3]{\ell} \cdot \sqrt[3]{\ell}}}\right)\right) \cdot \frac{\frac{M}{d} \cdot \frac{D}{2}}{2}\right)\right)\\ \mathbf{elif}\;\left(1 - \frac{h}{\ell} \cdot \left({\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2} \cdot \frac{1}{2}\right)\right) \cdot \left({\left(\frac{d}{\ell}\right)}^{\frac{1}{2}} \cdot {\left(\frac{d}{h}\right)}^{\frac{1}{2}}\right) \le -5.77055822624534 \cdot 10^{-99}:\\ \;\;\;\;\left(1 - \frac{h}{\ell} \cdot \left({\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2} \cdot \frac{1}{2}\right)\right) \cdot \left({\left(\frac{d}{\ell}\right)}^{\frac{1}{2}} \cdot {\left(\frac{d}{h}\right)}^{\frac{1}{2}}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{h}}} \cdot \left|\frac{\sqrt[3]{d}}{\sqrt[3]{h}}\right|\right) \cdot \left(\sqrt{\frac{\sqrt[3]{d}}{\ell}} \cdot \left|\sqrt[3]{d}\right| - h \cdot \left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{2} \cdot \left(\frac{\frac{M}{d} \cdot \frac{D}{2}}{\ell} \cdot \left(\left|\frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}\right| \cdot \sqrt{\frac{\sqrt[3]{d}}{\sqrt[3]{\ell}}}\right)\right)\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019141 
(FPCore (d h l M D)
  :name "Henrywood and Agarwal, Equation (12)"
  (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)))))