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

Average Error: 0.4 → 0.3

Time: 8.8s

Precision: 64

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{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)} \cdot \left(t \cdot \left({1}^{6} + \left(-{\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}\right)\right)\right)} \cdot \left(\sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\right) \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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 r241873 = 1.0;
        double r241874 = 5.0;
        double r241875 = v;
        double r241876 = r241875 * r241875;
        double r241877 = r241874 * r241876;
        double r241878 = r241873 - r241877;
        double r241879 = atan2(1.0, 0.0);
        double r241880 = t;
        double r241881 = r241879 * r241880;
        double r241882 = 2.0;
        double r241883 = 3.0;
        double r241884 = r241883 * r241876;
        double r241885 = r241873 - r241884;
        double r241886 = r241882 * r241885;
        double r241887 = sqrt(r241886);
        double r241888 = r241881 * r241887;
        double r241889 = r241873 - r241876;
        double r241890 = r241888 * r241889;
        double r241891 = r241878 / r241890;
        return r241891;
}

↓

double f(double v, double t) {
        double r241892 = 1.0;
        double r241893 = 5.0;
        double r241894 = v;
        double r241895 = r241894 * r241894;
        double r241896 = r241893 * r241895;
        double r241897 = r241892 - r241896;
        double r241898 = atan2(1.0, 0.0);
        double r241899 = r241897 / r241898;
        double r241900 = 2.0;
        double r241901 = 3.0;
        double r241902 = pow(r241892, r241901);
        double r241903 = r241902 * r241902;
        double r241904 = 3.0;
        double r241905 = r241904 * r241895;
        double r241906 = pow(r241905, r241901);
        double r241907 = r241906 * r241906;
        double r241908 = r241903 - r241907;
        double r241909 = r241900 * r241908;
        double r241910 = sqrt(r241909);
        double r241911 = t;
        double r241912 = 6.0;
        double r241913 = pow(r241892, r241912);
        double r241914 = pow(r241895, r241901);
        double r241915 = r241914 * r241914;
        double r241916 = -r241915;
        double r241917 = r241913 + r241916;
        double r241918 = r241911 * r241917;
        double r241919 = r241910 * r241918;
        double r241920 = r241899 / r241919;
        double r241921 = r241902 + r241906;
        double r241922 = sqrt(r241921);
        double r241923 = r241902 + r241914;
        double r241924 = r241922 * r241923;
        double r241925 = r241920 * r241924;
        double r241926 = r241892 * r241892;
        double r241927 = r241905 * r241905;
        double r241928 = r241892 * r241905;
        double r241929 = r241927 + r241928;
        double r241930 = r241926 + r241929;
        double r241931 = sqrt(r241930);
        double r241932 = r241895 * r241895;
        double r241933 = r241892 * r241895;
        double r241934 = r241932 + r241933;
        double r241935 = r241926 + r241934;
        double r241936 = r241931 * r241935;
        double r241937 = r241925 * r241936;
        return r241937;
}

Error

Bits error versus v

Bits error versus t

Derivation

1. Initial program 0.4

   \[\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 flip3-- 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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\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)}}\]

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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}\right)}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(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)}}\]

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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}\right)\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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.4

    \[\leadsto \color{blue}{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \sqrt{2 \cdot \left({1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}\right)\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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. Using strategy rm

14. Applied flip-- 0.4

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

15. 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}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}}\right)\right) \cdot \frac{{1}^{3} \cdot {1}^{3} - {\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}}{{1}^{3} + {\left(v \cdot v\right)}^{3}}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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-*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}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}}\right)\right) \cdot \frac{{1}^{3} \cdot {1}^{3} - {\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}}{{1}^{3} + {\left(v \cdot v\right)}^{3}}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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.4

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \color{blue}{\frac{\sqrt{2 \cdot \left({1}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}}{\sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}}\right)\right) \cdot \frac{{1}^{3} \cdot {1}^{3} - {\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}}{{1}^{3} + {\left(v \cdot v\right)}^{3}}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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-*r/ 0.4

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

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

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

    \[\leadsto \color{blue}{\left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\pi \cdot \left(t \cdot \sqrt{2 \cdot \left({1}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}\right)\right) \cdot \left({1}^{3} \cdot {1}^{3} - {\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}\right)} \cdot \left(\sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\right)} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)} \cdot \left(t \cdot \left({1}^{6} + \left(-{\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}\right)\right)\right)}} \cdot \left(\sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\right) \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)} \cdot \left(t \cdot \left({1}^{6} + \left(-{\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}\right)\right)\right)} \cdot \left(\sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\right) \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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 2020060 +o rules:numerics
(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)))))