Average Error: 4.3 → 3.4
Time: 2.4m
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{1 + \left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot 0.0072644182 + \left(0.1049934947 + \left(x \cdot x\right) \cdot 0.0424060604\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(\left(x \cdot x\right) \cdot 0.0001789971\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 0.0005064034\right)\right)}{\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0694555761 \cdot \left(x \cdot x\right) + 0.2909738639\right) + 0.7715471019\right) + \left(1 + \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.0140005442 + \left(x \cdot x\right) \cdot \left(\left(2 \cdot \left(x \cdot x\right)\right) \cdot 0.0001789971 + 0.0008327945\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
\frac{1 + \left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot 0.0072644182 + \left(0.1049934947 + \left(x \cdot x\right) \cdot 0.0424060604\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(\left(x \cdot x\right) \cdot 0.0001789971\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 0.0005064034\right)\right)}{\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0694555761 \cdot \left(x \cdot x\right) + 0.2909738639\right) + 0.7715471019\right) + \left(1 + \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.0140005442 + \left(x \cdot x\right) \cdot \left(\left(2 \cdot \left(x \cdot x\right)\right) \cdot 0.0001789971 + 0.0008327945\right)\right)\right)} \cdot x
double f(double x) {
        double r4745932 = 1.0;
        double r4745933 = /* ERROR: no posit support in C */;
        double r4745934 = 0.1049934947;
        double r4745935 = /* ERROR: no posit support in C */;
        double r4745936 = x;
        double r4745937 = r4745936 * r4745936;
        double r4745938 = r4745935 * r4745937;
        double r4745939 = r4745933 + r4745938;
        double r4745940 = 0.0424060604;
        double r4745941 = /* ERROR: no posit support in C */;
        double r4745942 = r4745937 * r4745937;
        double r4745943 = r4745941 * r4745942;
        double r4745944 = r4745939 + r4745943;
        double r4745945 = 0.0072644182;
        double r4745946 = /* ERROR: no posit support in C */;
        double r4745947 = r4745942 * r4745937;
        double r4745948 = r4745946 * r4745947;
        double r4745949 = r4745944 + r4745948;
        double r4745950 = 0.0005064034;
        double r4745951 = /* ERROR: no posit support in C */;
        double r4745952 = r4745947 * r4745937;
        double r4745953 = r4745951 * r4745952;
        double r4745954 = r4745949 + r4745953;
        double r4745955 = 0.0001789971;
        double r4745956 = /* ERROR: no posit support in C */;
        double r4745957 = r4745952 * r4745937;
        double r4745958 = r4745956 * r4745957;
        double r4745959 = r4745954 + r4745958;
        double r4745960 = 0.7715471019;
        double r4745961 = /* ERROR: no posit support in C */;
        double r4745962 = r4745961 * r4745937;
        double r4745963 = r4745933 + r4745962;
        double r4745964 = 0.2909738639;
        double r4745965 = /* ERROR: no posit support in C */;
        double r4745966 = r4745965 * r4745942;
        double r4745967 = r4745963 + r4745966;
        double r4745968 = 0.0694555761;
        double r4745969 = /* ERROR: no posit support in C */;
        double r4745970 = r4745969 * r4745947;
        double r4745971 = r4745967 + r4745970;
        double r4745972 = 0.0140005442;
        double r4745973 = /* ERROR: no posit support in C */;
        double r4745974 = r4745973 * r4745952;
        double r4745975 = r4745971 + r4745974;
        double r4745976 = 0.0008327945;
        double r4745977 = /* ERROR: no posit support in C */;
        double r4745978 = r4745977 * r4745957;
        double r4745979 = r4745975 + r4745978;
        double r4745980 = 2.0;
        double r4745981 = /* ERROR: no posit support in C */;
        double r4745982 = r4745981 * r4745956;
        double r4745983 = r4745957 * r4745937;
        double r4745984 = r4745982 * r4745983;
        double r4745985 = r4745979 + r4745984;
        double r4745986 = r4745959 / r4745985;
        double r4745987 = r4745986 * r4745936;
        return r4745987;
}

double f(double x) {
        double r4745988 = 1.0;
        double r4745989 = x;
        double r4745990 = r4745989 * r4745989;
        double r4745991 = r4745990 * r4745990;
        double r4745992 = 0.0072644182;
        double r4745993 = r4745991 * r4745992;
        double r4745994 = 0.1049934947;
        double r4745995 = 0.0424060604;
        double r4745996 = r4745990 * r4745995;
        double r4745997 = r4745994 + r4745996;
        double r4745998 = r4745993 + r4745997;
        double r4745999 = r4745990 * r4745998;
        double r4746000 = r4745991 * r4745991;
        double r4746001 = 0.0001789971;
        double r4746002 = r4745990 * r4746001;
        double r4746003 = r4746000 * r4746002;
        double r4746004 = 0.0005064034;
        double r4746005 = r4746000 * r4746004;
        double r4746006 = r4746003 + r4746005;
        double r4746007 = r4745999 + r4746006;
        double r4746008 = r4745988 + r4746007;
        double r4746009 = 0.0694555761;
        double r4746010 = r4746009 * r4745990;
        double r4746011 = 0.2909738639;
        double r4746012 = r4746010 + r4746011;
        double r4746013 = r4745990 * r4746012;
        double r4746014 = 0.7715471019;
        double r4746015 = r4746013 + r4746014;
        double r4746016 = r4745990 * r4746015;
        double r4746017 = 0.0140005442;
        double r4746018 = 2.0;
        double r4746019 = r4746018 * r4745990;
        double r4746020 = r4746019 * r4746001;
        double r4746021 = 0.0008327945;
        double r4746022 = r4746020 + r4746021;
        double r4746023 = r4745990 * r4746022;
        double r4746024 = r4746017 + r4746023;
        double r4746025 = r4746000 * r4746024;
        double r4746026 = r4745988 + r4746025;
        double r4746027 = r4746016 + r4746026;
        double r4746028 = r4746008 / r4746027;
        double r4746029 = r4746028 * r4745989;
        return r4746029;
}

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

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

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

    \[\leadsto \left(\frac{\left(\frac{\left(1\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(0.0072644182\right)\right)}{\left(\frac{\left(0.1049934947\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0424060604\right)\right)}\right)}\right)\right)}{\color{blue}{\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(\left(x \cdot x\right) \cdot \left(0.0001789971\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(0.0005064034\right)\right)}\right)}}\right)}\right)}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.2909738639\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}\right)\right)}{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\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(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(2\right)\right) \cdot \left(0.0001789971\right)\right)}{\left(\frac{\left(x \cdot \left(x \cdot \left(0.0008327945\right)\right)\right)}{\left(0.0140005442\right)}\right)}\right)\right)}\right)}\right)}\right) \cdot x\]
  7. Using strategy rm
  8. Applied *p16-rgt-identity-expand3.4

    \[\leadsto \left(\frac{\color{blue}{\left(\left(\frac{\left(1\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(0.0072644182\right)\right)}{\left(\frac{\left(0.1049934947\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0424060604\right)\right)}\right)}\right)\right)}{\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(\left(x \cdot x\right) \cdot \left(0.0001789971\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(0.0005064034\right)\right)}\right)}\right)}\right) \cdot \left(1.0\right)\right)}}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(0.2909738639\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}\right)\right)}{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\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(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(2\right)\right) \cdot \left(0.0001789971\right)\right)}{\left(\frac{\left(x \cdot \left(x \cdot \left(0.0008327945\right)\right)\right)}{\left(0.0140005442\right)}\right)}\right)\right)}\right)}\right)}\right) \cdot x\]
  9. Applied associate-/l*3.4

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

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

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

Reproduce

herbie shell --seed 2019163 +o rules:numerics
(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))