Average Error: 4.3 → 3.5
Time: 1.2m
Precision: 64
\[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]
\[\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0005064034 + \left(x \cdot x\right) \cdot 0.0001789971\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0072644182 \cdot \left(x \cdot x\right) + 0.0424060604\right)\right) + \left(1 + \left(x \cdot x\right) \cdot 0.1049934947\right)}{\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + 0.0140005442 \cdot \left(x \cdot x\right)\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0008327945 + 2 \cdot \left(x \cdot \left(x \cdot 0.0001789971\right)\right)\right)\right) + \left(1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot 0.2909738639\right)\right)} \cdot x\]
\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x
\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0005064034 + \left(x \cdot x\right) \cdot 0.0001789971\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0072644182 \cdot \left(x \cdot x\right) + 0.0424060604\right)\right) + \left(1 + \left(x \cdot x\right) \cdot 0.1049934947\right)}{\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + 0.0140005442 \cdot \left(x \cdot x\right)\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0008327945 + 2 \cdot \left(x \cdot \left(x \cdot 0.0001789971\right)\right)\right)\right) + \left(1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot 0.2909738639\right)\right)} \cdot x
double f(double x) {
        double r2140842 = 1.0;
        double r2140843 = /* ERROR: no posit support in C */;
        double r2140844 = 0.1049934947;
        double r2140845 = /* ERROR: no posit support in C */;
        double r2140846 = x;
        double r2140847 = r2140846 * r2140846;
        double r2140848 = r2140845 * r2140847;
        double r2140849 = r2140843 + r2140848;
        double r2140850 = 0.0424060604;
        double r2140851 = /* ERROR: no posit support in C */;
        double r2140852 = r2140847 * r2140847;
        double r2140853 = r2140851 * r2140852;
        double r2140854 = r2140849 + r2140853;
        double r2140855 = 0.0072644182;
        double r2140856 = /* ERROR: no posit support in C */;
        double r2140857 = r2140852 * r2140847;
        double r2140858 = r2140856 * r2140857;
        double r2140859 = r2140854 + r2140858;
        double r2140860 = 0.0005064034;
        double r2140861 = /* ERROR: no posit support in C */;
        double r2140862 = r2140857 * r2140847;
        double r2140863 = r2140861 * r2140862;
        double r2140864 = r2140859 + r2140863;
        double r2140865 = 0.0001789971;
        double r2140866 = /* ERROR: no posit support in C */;
        double r2140867 = r2140862 * r2140847;
        double r2140868 = r2140866 * r2140867;
        double r2140869 = r2140864 + r2140868;
        double r2140870 = 0.7715471019;
        double r2140871 = /* ERROR: no posit support in C */;
        double r2140872 = r2140871 * r2140847;
        double r2140873 = r2140843 + r2140872;
        double r2140874 = 0.2909738639;
        double r2140875 = /* ERROR: no posit support in C */;
        double r2140876 = r2140875 * r2140852;
        double r2140877 = r2140873 + r2140876;
        double r2140878 = 0.0694555761;
        double r2140879 = /* ERROR: no posit support in C */;
        double r2140880 = r2140879 * r2140857;
        double r2140881 = r2140877 + r2140880;
        double r2140882 = 0.0140005442;
        double r2140883 = /* ERROR: no posit support in C */;
        double r2140884 = r2140883 * r2140862;
        double r2140885 = r2140881 + r2140884;
        double r2140886 = 0.0008327945;
        double r2140887 = /* ERROR: no posit support in C */;
        double r2140888 = r2140887 * r2140867;
        double r2140889 = r2140885 + r2140888;
        double r2140890 = 2.0;
        double r2140891 = /* ERROR: no posit support in C */;
        double r2140892 = r2140891 * r2140866;
        double r2140893 = r2140867 * r2140847;
        double r2140894 = r2140892 * r2140893;
        double r2140895 = r2140889 + r2140894;
        double r2140896 = r2140869 / r2140895;
        double r2140897 = r2140896 * r2140846;
        return r2140897;
}

double f(double x) {
        double r2140898 = x;
        double r2140899 = r2140898 * r2140898;
        double r2140900 = r2140899 * r2140899;
        double r2140901 = r2140900 * r2140900;
        double r2140902 = 0.0005064034;
        double r2140903 = 0.0001789971;
        double r2140904 = r2140899 * r2140903;
        double r2140905 = r2140902 + r2140904;
        double r2140906 = r2140901 * r2140905;
        double r2140907 = 0.0072644182;
        double r2140908 = r2140907 * r2140899;
        double r2140909 = 0.0424060604;
        double r2140910 = r2140908 + r2140909;
        double r2140911 = r2140900 * r2140910;
        double r2140912 = r2140906 + r2140911;
        double r2140913 = 1.0;
        double r2140914 = 0.1049934947;
        double r2140915 = r2140899 * r2140914;
        double r2140916 = r2140913 + r2140915;
        double r2140917 = r2140912 + r2140916;
        double r2140918 = 0.0694555761;
        double r2140919 = 0.0140005442;
        double r2140920 = r2140919 * r2140899;
        double r2140921 = r2140918 + r2140920;
        double r2140922 = r2140900 * r2140921;
        double r2140923 = 0.0008327945;
        double r2140924 = 2.0;
        double r2140925 = r2140898 * r2140903;
        double r2140926 = r2140898 * r2140925;
        double r2140927 = r2140924 * r2140926;
        double r2140928 = r2140923 + r2140927;
        double r2140929 = r2140901 * r2140928;
        double r2140930 = r2140922 + r2140929;
        double r2140931 = r2140899 * r2140930;
        double r2140932 = 0.7715471019;
        double r2140933 = 0.2909738639;
        double r2140934 = r2140899 * r2140933;
        double r2140935 = r2140932 + r2140934;
        double r2140936 = r2140899 * r2140935;
        double r2140937 = r2140913 + r2140936;
        double r2140938 = r2140931 + r2140937;
        double r2140939 = r2140917 / r2140938;
        double r2140940 = r2140939 * r2140898;
        return r2140940;
}

Error

Bits error versus x

Derivation

  1. Initial program 4.3

    \[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]
  2. Simplified3.5

    \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.1049934947\right)\right)}\right)}\right)}{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0694555761\right)}{\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0008327945\right)}{\left(\left(2\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)\right)}\right)\right)}\right)\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.7715471019\right)}{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}\right)\right)}\right)}\right)}\right) \cdot x}\]
  3. Using strategy rm
  4. Applied associate-*l*3.5

    \[\leadsto \left(\frac{\left(\frac{\left(\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.1049934947\right)\right)}\right)}\right)}{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0694555761\right)}{\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0008327945\right)}{\left(\left(2\right) \cdot \color{blue}{\left(x \cdot \left(x \cdot \left(0.0001789971\right)\right)\right)}\right)}\right)\right)}\right)\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.7715471019\right)}{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}\right)\right)}\right)}\right)}\right) \cdot x\]
  5. Final simplification3.5

    \[\leadsto \frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0005064034 + \left(x \cdot x\right) \cdot 0.0001789971\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0072644182 \cdot \left(x \cdot x\right) + 0.0424060604\right)\right) + \left(1 + \left(x \cdot x\right) \cdot 0.1049934947\right)}{\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + 0.0140005442 \cdot \left(x \cdot x\right)\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0008327945 + 2 \cdot \left(x \cdot \left(x \cdot 0.0001789971\right)\right)\right)\right) + \left(1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot 0.2909738639\right)\right)} \cdot x\]

Reproduce

herbie shell --seed 2019154 
(FPCore (x)
  :name "Jmat.Real.dawson"
  (*.p16 (/.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x))