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

Average Error: 0.5 → 0.1

Time: 11.2s

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{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{4} - \left(3 \cdot {3}^{3}\right) \cdot {v}^{8}\right)} \cdot \left({1}^{3} - {v}^{6}\right)}}{t} \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\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 r229412 = 1.0;
        double r229413 = 5.0;
        double r229414 = v;
        double r229415 = r229414 * r229414;
        double r229416 = r229413 * r229415;
        double r229417 = r229412 - r229416;
        double r229418 = atan2(1.0, 0.0);
        double r229419 = t;
        double r229420 = r229418 * r229419;
        double r229421 = 2.0;
        double r229422 = 3.0;
        double r229423 = r229422 * r229415;
        double r229424 = r229412 - r229423;
        double r229425 = r229421 * r229424;
        double r229426 = sqrt(r229425);
        double r229427 = r229420 * r229426;
        double r229428 = r229412 - r229415;
        double r229429 = r229427 * r229428;
        double r229430 = r229417 / r229429;
        return r229430;
}

↓

double f(double v, double t) {
        double r229431 = 1.0;
        double r229432 = 5.0;
        double r229433 = v;
        double r229434 = r229433 * r229433;
        double r229435 = r229432 * r229434;
        double r229436 = r229431 - r229435;
        double r229437 = atan2(1.0, 0.0);
        double r229438 = r229436 / r229437;
        double r229439 = 2.0;
        double r229440 = 4.0;
        double r229441 = pow(r229431, r229440);
        double r229442 = 3.0;
        double r229443 = 3.0;
        double r229444 = pow(r229442, r229443);
        double r229445 = r229442 * r229444;
        double r229446 = 8.0;
        double r229447 = pow(r229433, r229446);
        double r229448 = r229445 * r229447;
        double r229449 = r229441 - r229448;
        double r229450 = r229439 * r229449;
        double r229451 = sqrt(r229450);
        double r229452 = pow(r229431, r229443);
        double r229453 = 6.0;
        double r229454 = pow(r229433, r229453);
        double r229455 = r229452 - r229454;
        double r229456 = r229451 * r229455;
        double r229457 = r229438 / r229456;
        double r229458 = t;
        double r229459 = r229457 / r229458;
        double r229460 = r229431 * r229431;
        double r229461 = r229442 * r229442;
        double r229462 = pow(r229433, r229440);
        double r229463 = r229461 * r229462;
        double r229464 = r229460 + r229463;
        double r229465 = sqrt(r229464);
        double r229466 = r229459 * r229465;
        double r229467 = r229442 * r229434;
        double r229468 = r229431 + r229467;
        double r229469 = sqrt(r229468);
        double r229470 = r229434 * r229434;
        double r229471 = r229431 * r229434;
        double r229472 = r229470 + r229471;
        double r229473 = r229460 + r229472;
        double r229474 = r229469 * r229473;
        double r229475 = r229466 * r229474;
        return r229475;
}

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.4

   \[\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.4

   \[\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.4

   \[\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.4

   \[\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 associate-*r/ 0.3

    \[\leadsto \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\color{blue}{\frac{\left({1}^{3} - {v}^{6}\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)}{\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 associate-/r/ 0.3

    \[\leadsto \color{blue}{\left(\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({1}^{3} - {v}^{6}\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 \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\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)\]

21. Simplified 0.1

    \[\leadsto \left(\color{blue}{\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{4} - \left(3 \cdot {3}^{3}\right) \cdot {v}^{8}\right)} \cdot \left({1}^{3} - {v}^{6}\right)}}{t}} \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\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. Final simplification 0.1

    \[\leadsto \left(\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{4} - \left(3 \cdot {3}^{3}\right) \cdot {v}^{8}\right)} \cdot \left({1}^{3} - {v}^{6}\right)}}{t} \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\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 2020045 
(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)))))