Average Error: 4.4 → 3.6
Time: 2.0m
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\]
↓
\[\left(\left(\frac{\left(\left(\left(0.0424060604 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0005064034 + x \cdot \left(x \cdot 0.0001789971\right)\right)\right) + \left(x \cdot x\right) \cdot 0.0072644182\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) + 0.1049934947 \cdot \left(x \cdot x\right)\right) + 1}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(2 \cdot \left(x \cdot 0.0001789971\right)\right) \cdot x + 0.0008327945\right)\right) + \left(\left(x \cdot x\right) \cdot 0.2909738639 + 0.7715471019\right)\right) \cdot \left(x \cdot x\right) + \left(1 + 0.0140005442 \cdot \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)\right)}\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
↓
\left(\left(\frac{\left(\left(\left(0.0424060604 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0005064034 + x \cdot \left(x \cdot 0.0001789971\right)\right)\right) + \left(x \cdot x\right) \cdot 0.0072644182\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) + 0.1049934947 \cdot \left(x \cdot x\right)\right) + 1}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(2 \cdot \left(x \cdot 0.0001789971\right)\right) \cdot x + 0.0008327945\right)\right) + \left(\left(x \cdot x\right) \cdot 0.2909738639 + 0.7715471019\right)\right) \cdot \left(x \cdot x\right) + \left(1 + 0.0140005442 \cdot \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)\right)}\right)\right) \cdot x
double f(double x) {
        double r6487904 = 1.0;
        double r6487905 = /* ERROR: no posit support in C */;
        double r6487906 = 0.1049934947;
        double r6487907 = /* ERROR: no posit support in C */;
        double r6487908 = x;
        double r6487909 = r6487908 * r6487908;
        double r6487910 = r6487907 * r6487909;
        double r6487911 = r6487905 + r6487910;
        double r6487912 = 0.0424060604;
        double r6487913 = /* ERROR: no posit support in C */;
        double r6487914 = r6487909 * r6487909;
        double r6487915 = r6487913 * r6487914;
        double r6487916 = r6487911 + r6487915;
        double r6487917 = 0.0072644182;
        double r6487918 = /* ERROR: no posit support in C */;
        double r6487919 = r6487914 * r6487909;
        double r6487920 = r6487918 * r6487919;
        double r6487921 = r6487916 + r6487920;
        double r6487922 = 0.0005064034;
        double r6487923 = /* ERROR: no posit support in C */;
        double r6487924 = r6487919 * r6487909;
        double r6487925 = r6487923 * r6487924;
        double r6487926 = r6487921 + r6487925;
        double r6487927 = 0.0001789971;
        double r6487928 = /* ERROR: no posit support in C */;
        double r6487929 = r6487924 * r6487909;
        double r6487930 = r6487928 * r6487929;
        double r6487931 = r6487926 + r6487930;
        double r6487932 = 0.7715471019;
        double r6487933 = /* ERROR: no posit support in C */;
        double r6487934 = r6487933 * r6487909;
        double r6487935 = r6487905 + r6487934;
        double r6487936 = 0.2909738639;
        double r6487937 = /* ERROR: no posit support in C */;
        double r6487938 = r6487937 * r6487914;
        double r6487939 = r6487935 + r6487938;
        double r6487940 = 0.0694555761;
        double r6487941 = /* ERROR: no posit support in C */;
        double r6487942 = r6487941 * r6487919;
        double r6487943 = r6487939 + r6487942;
        double r6487944 = 0.0140005442;
        double r6487945 = /* ERROR: no posit support in C */;
        double r6487946 = r6487945 * r6487924;
        double r6487947 = r6487943 + r6487946;
        double r6487948 = 0.0008327945;
        double r6487949 = /* ERROR: no posit support in C */;
        double r6487950 = r6487949 * r6487929;
        double r6487951 = r6487947 + r6487950;
        double r6487952 = 2.0;
        double r6487953 = /* ERROR: no posit support in C */;
        double r6487954 = r6487953 * r6487928;
        double r6487955 = r6487929 * r6487909;
        double r6487956 = r6487954 * r6487955;
        double r6487957 = r6487951 + r6487956;
        double r6487958 = r6487931 / r6487957;
        double r6487959 = r6487958 * r6487908;
        return r6487959;
}
↓
double f(double x) {
        double r6487960 = 0.0424060604;
        double r6487961 = x;
        double r6487962 = r6487961 * r6487961;
        double r6487963 = r6487962 * r6487962;
        double r6487964 = 0.0005064034;
        double r6487965 = 0.0001789971;
        double r6487966 = r6487961 * r6487965;
        double r6487967 = r6487961 * r6487966;
        double r6487968 = r6487964 + r6487967;
        double r6487969 = r6487963 * r6487968;
        double r6487970 = r6487960 + r6487969;
        double r6487971 = 0.0072644182;
        double r6487972 = r6487962 * r6487971;
        double r6487973 = r6487970 + r6487972;
        double r6487974 = r6487973 * r6487963;
        double r6487975 = 0.1049934947;
        double r6487976 = r6487975 * r6487962;
        double r6487977 = r6487974 + r6487976;
        double r6487978 = 1.0;
        double r6487979 = r6487977 + r6487978;
        double r6487980 = 0.0694555761;
        double r6487981 = 2.0;
        double r6487982 = r6487981 * r6487966;
        double r6487983 = r6487982 * r6487961;
        double r6487984 = 0.0008327945;
        double r6487985 = r6487983 + r6487984;
        double r6487986 = r6487963 * r6487985;
        double r6487987 = r6487980 + r6487986;
        double r6487988 = r6487963 * r6487987;
        double r6487989 = 0.2909738639;
        double r6487990 = r6487962 * r6487989;
        double r6487991 = 0.7715471019;
        double r6487992 = r6487990 + r6487991;
        double r6487993 = r6487988 + r6487992;
        double r6487994 = r6487993 * r6487962;
        double r6487995 = 0.0140005442;
        double r6487996 = r6487963 * r6487963;
        double r6487997 = r6487995 * r6487996;
        double r6487998 = r6487978 + r6487997;
        double r6487999 = r6487994 + r6487998;
        double r6488000 = r6487979 / r6487999;
        double r6488001 = /*Error: no posit support in C */;
        double r6488002 = /*Error: no posit support in C */;
        double r6488003 = r6488002 * r6487961;
        return r6488003;
}

Error

Bits error versus x

Derivation

  1. Initial program 4.4

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

    \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\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(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}{\left(0.7715471019\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761\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(\left(x \cdot x\right) \cdot \left(2\right)\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \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)\right)}\right)}\right) \cdot x}\]
  3. Using strategy rm

  4. Applied *p16-rgt-identity-expand3.7

    \[\leadsto \left(\frac{\color{blue}{\left(\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}\right)}\right)\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.1049934947\right)\right)}\right)}\right) \cdot \left(1.0\right)\right)}}{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}{\left(0.7715471019\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761\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(\left(x \cdot x\right) \cdot \left(2\right)\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \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)\right)}\right)}\right) \cdot x\]

  5. Applied associate-/l*3.7

    \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\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(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}{\left(0.7715471019\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761\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(\left(x \cdot x\right) \cdot \left(2\right)\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \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)\right)}\right)}{\left(1.0\right)}\right)}\right)} \cdot x\]

  6. Simplified3.6

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

  8. Applied p16-*-un-lft-identity3.6

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

  9. Applied *p16-rgt-identity-expand3.6

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

  10. Applied p16-times-frac3.6

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

  11. Simplified3.6

    \[\leadsto \left(\color{blue}{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(\left(0.0001789971\right) \cdot x\right) \cdot x\right)}\right)\right)}{\left(0.0072644182\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}{\left(0.1049934947\right)}\right)\right)}{\left(1\right)}\right)} \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(0.7715471019\right)}{\left(\left(0.2909738639\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0694555761\right)}{\left(\left(\frac{\left(\left(\left(0.0001789971\right) \cdot \left(x \cdot x\right)\right) \cdot \left(2\right)\right)}{\left(0.0008327945\right)}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)\right)}\right)\right)}\right)}{\left(\left(\left(0.0140005442\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right)\right) \cdot x\]
  12. Using strategy rm

  13. Applied introduce-quire3.6

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

  14. Simplified3.6

    \[\leadsto \left(\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(0.0424060604\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0072644182\right)\right)}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(1\right)}\right)}{\left(\frac{\left(\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(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(\left(2\right) \cdot \left(x \cdot \left(0.0001789971\right)\right)\right) \cdot x\right)}{\left(0.0008327945\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}{\left(0.7715471019\right)}\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(\frac{\left(1\right)}{\left(\left(0.0140005442\right) \cdot \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)\right)}\right)}\right)}\right)\right)}\right) \cdot x\]
  15. Using strategy rm

  16. Applied associate-*l*3.6

    \[\leadsto \left(\left(\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(0.0424060604\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\color{blue}{\left(x \cdot \left(x \cdot \left(0.0001789971\right)\right)\right)}}\right)\right)}\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0072644182\right)\right)}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(1\right)}\right)}{\left(\frac{\left(\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(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(\left(2\right) \cdot \left(x \cdot \left(0.0001789971\right)\right)\right) \cdot x\right)}{\left(0.0008327945\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}{\left(0.7715471019\right)}\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(\frac{\left(1\right)}{\left(\left(0.0140005442\right) \cdot \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)\right)}\right)}\right)}\right)\right)\right) \cdot x\]

  17. Final simplification3.6

    \[\leadsto \left(\left(\frac{\left(\left(\left(0.0424060604 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0005064034 + x \cdot \left(x \cdot 0.0001789971\right)\right)\right) + \left(x \cdot x\right) \cdot 0.0072644182\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) + 0.1049934947 \cdot \left(x \cdot x\right)\right) + 1}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(2 \cdot \left(x \cdot 0.0001789971\right)\right) \cdot x + 0.0008327945\right)\right) + \left(\left(x \cdot x\right) \cdot 0.2909738639 + 0.7715471019\right)\right) \cdot \left(x \cdot x\right) + \left(1 + 0.0140005442 \cdot \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)\right)}\right)\right) \cdot x\]

Reproduce

herbie shell --seed 2019162 
(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))