Falkner and Boettcher, Equation (20:1,3)

Average Error: 0.5 → 0.3

Time: 14.1s

Precision: 64

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

Math

\[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]

↓

\[\left(\frac{\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{{\left({1}^{3}\right)}^{3} - {\left({v}^{6}\right)}^{3}}}{t}}{\sqrt{2 \cdot \left({1}^{4} - {v}^{8} \cdot \left(3 \cdot {3}^{3}\right)\right)}} \cdot \left(\left({1}^{3} \cdot {1}^{3} + \left({v}^{6} \cdot {v}^{6} + {1}^{3} \cdot {v}^{6}\right)\right) \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right)\right) \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

C

double f(double v, double t) {
        double r188301 = 1.0;
        double r188302 = 5.0;
        double r188303 = v;
        double r188304 = r188303 * r188303;
        double r188305 = r188302 * r188304;
        double r188306 = r188301 - r188305;
        double r188307 = atan2(1.0, 0.0);
        double r188308 = t;
        double r188309 = r188307 * r188308;
        double r188310 = 2.0;
        double r188311 = 3.0;
        double r188312 = r188311 * r188304;
        double r188313 = r188301 - r188312;
        double r188314 = r188310 * r188313;
        double r188315 = sqrt(r188314);
        double r188316 = r188309 * r188315;
        double r188317 = r188301 - r188304;
        double r188318 = r188316 * r188317;
        double r188319 = r188306 / r188318;
        return r188319;
}

↓

double f(double v, double t) {
        double r188320 = 1.0;
        double r188321 = 5.0;
        double r188322 = v;
        double r188323 = r188322 * r188322;
        double r188324 = r188321 * r188323;
        double r188325 = r188320 - r188324;
        double r188326 = atan2(1.0, 0.0);
        double r188327 = r188325 / r188326;
        double r188328 = 3.0;
        double r188329 = pow(r188320, r188328);
        double r188330 = pow(r188329, r188328);
        double r188331 = 6.0;
        double r188332 = pow(r188322, r188331);
        double r188333 = pow(r188332, r188328);
        double r188334 = r188330 - r188333;
        double r188335 = r188327 / r188334;
        double r188336 = t;
        double r188337 = r188335 / r188336;
        double r188338 = 2.0;
        double r188339 = 4.0;
        double r188340 = pow(r188320, r188339);
        double r188341 = 8.0;
        double r188342 = pow(r188322, r188341);
        double r188343 = 3.0;
        double r188344 = pow(r188343, r188328);
        double r188345 = r188343 * r188344;
        double r188346 = r188342 * r188345;
        double r188347 = r188340 - r188346;
        double r188348 = r188338 * r188347;
        double r188349 = sqrt(r188348);
        double r188350 = r188337 / r188349;
        double r188351 = r188329 * r188329;
        double r188352 = r188332 * r188332;
        double r188353 = r188329 * r188332;
        double r188354 = r188352 + r188353;
        double r188355 = r188351 + r188354;
        double r188356 = r188320 * r188320;
        double r188357 = r188343 * r188343;
        double r188358 = pow(r188322, r188339);
        double r188359 = r188357 * r188358;
        double r188360 = r188356 + r188359;
        double r188361 = sqrt(r188360);
        double r188362 = r188355 * r188361;
        double r188363 = r188350 * r188362;
        double r188364 = r188343 * r188323;
        double r188365 = r188320 + r188364;
        double r188366 = sqrt(r188365);
        double r188367 = r188323 * r188323;
        double r188368 = r188320 * r188323;
        double r188369 = r188367 + r188368;
        double r188370 = r188356 + r188369;
        double r188371 = r188366 * r188370;
        double r188372 = r188363 * r188371;
        return r188372;
}

Error

Bits error versus v

Bits error versus t

Derivation

1. Initial program 0.5

   \[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
2. Using strategy rm

3. Applied associate-*l* 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\left(\pi \cdot \left(t \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right)\right)} \cdot \left(1 - v \cdot v\right)}\]
4. Using strategy rm

5. Applied flip3-- 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right)\right) \cdot \color{blue}{\frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}}\]

6. Applied flip-- 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \sqrt{2 \cdot \color{blue}{\frac{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right)\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

7. Applied associate-*r/ 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \sqrt{\color{blue}{\frac{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right)\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

8. Applied sqrt-div 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \color{blue}{\frac{\sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}}\right)\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

9. Applied associate-*r/ 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \color{blue}{\frac{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

10. Applied associate-*r/ 0.5

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\pi \cdot \left(t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right)}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}} \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

11. Applied frac-times 0.5

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(\pi \cdot \left(t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right)\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)}}}\]

12. Applied associate-/r/ 0.5

    \[\leadsto \color{blue}{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right)\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)}\]

13. Simplified 0.3

    \[\leadsto \color{blue}{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({1}^{3} - {v}^{6}\right) \cdot \left(\sqrt{\left(1 \cdot 1 - \left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot 2} \cdot t\right)}} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
14. Using strategy rm

15. Applied flip-- 0.3

    \[\leadsto \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({1}^{3} - {v}^{6}\right) \cdot \left(\sqrt{\color{blue}{\frac{\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right)}{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}} \cdot 2} \cdot t\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

16. Applied associate-*l/ 0.3

    \[\leadsto \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({1}^{3} - {v}^{6}\right) \cdot \left(\sqrt{\color{blue}{\frac{\left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right)\right) \cdot 2}{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}}} \cdot t\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

17. Applied sqrt-div 0.3

    \[\leadsto \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({1}^{3} - {v}^{6}\right) \cdot \left(\color{blue}{\frac{\sqrt{\left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right)\right) \cdot 2}}{\sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}}} \cdot t\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

18. Applied associate-*l/ 0.3

    \[\leadsto \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({1}^{3} - {v}^{6}\right) \cdot \color{blue}{\frac{\sqrt{\left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right)\right) \cdot 2} \cdot t}{\sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}}}} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

19. Applied flip3-- 0.3

    \[\leadsto \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\color{blue}{\frac{{\left({1}^{3}\right)}^{3} - {\left({v}^{6}\right)}^{3}}{{1}^{3} \cdot {1}^{3} + \left({v}^{6} \cdot {v}^{6} + {1}^{3} \cdot {v}^{6}\right)}} \cdot \frac{\sqrt{\left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right)\right) \cdot 2} \cdot t}{\sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}}} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

20. Applied frac-times 0.3

    \[\leadsto \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\color{blue}{\frac{\left({\left({1}^{3}\right)}^{3} - {\left({v}^{6}\right)}^{3}\right) \cdot \left(\sqrt{\left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right)\right) \cdot 2} \cdot t\right)}{\left({1}^{3} \cdot {1}^{3} + \left({v}^{6} \cdot {v}^{6} + {1}^{3} \cdot {v}^{6}\right)\right) \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}}}} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

21. Applied associate-/r/ 0.3

    \[\leadsto \color{blue}{\left(\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({\left({1}^{3}\right)}^{3} - {\left({v}^{6}\right)}^{3}\right) \cdot \left(\sqrt{\left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot \left(\left(3 \cdot 3\right) \cdot {v}^{4}\right)\right) \cdot 2} \cdot t\right)} \cdot \left(\left({1}^{3} \cdot {1}^{3} + \left({v}^{6} \cdot {v}^{6} + {1}^{3} \cdot {v}^{6}\right)\right) \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

22. Simplified 0.3

    \[\leadsto \left(\color{blue}{\frac{\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{{\left({1}^{3}\right)}^{3} - {\left({v}^{6}\right)}^{3}}}{t}}{\sqrt{2 \cdot \left({1}^{4} - {v}^{8} \cdot \left(3 \cdot {3}^{3}\right)\right)}}} \cdot \left(\left({1}^{3} \cdot {1}^{3} + \left({v}^{6} \cdot {v}^{6} + {1}^{3} \cdot {v}^{6}\right)\right) \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right)\right) \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

23. Final simplification 0.3

    \[\leadsto \left(\frac{\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{{\left({1}^{3}\right)}^{3} - {\left({v}^{6}\right)}^{3}}}{t}}{\sqrt{2 \cdot \left({1}^{4} - {v}^{8} \cdot \left(3 \cdot {3}^{3}\right)\right)}} \cdot \left(\left({1}^{3} \cdot {1}^{3} + \left({v}^{6} \cdot {v}^{6} + {1}^{3} \cdot {v}^{6}\right)\right) \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right)\right) \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

Reproduce

herbie shell --seed 2020042 
(FPCore (v t)
  :name "Falkner and Boettcher, Equation (20:1,3)"
  :precision binary64
  (/ (- 1 (* 5 (* v v))) (* (* (* PI t) (sqrt (* 2 (- 1 (* 3 (* v v)))))) (- 1 (* v v)))))