Jmat.Real.dawson

Average Error: 4.4 → 3.6

Time: 2.0m

Precision: 64

Math

\[\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(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)} \cdot x\]

C

double f(double x) {
        double r5268088 = 1.0;
        double r5268089 = /* ERROR: no posit support in C */;
        double r5268090 = 0.1049934947;
        double r5268091 = /* ERROR: no posit support in C */;
        double r5268092 = x;
        double r5268093 = r5268092 * r5268092;
        double r5268094 = r5268091 * r5268093;
        double r5268095 = r5268089 + r5268094;
        double r5268096 = 0.0424060604;
        double r5268097 = /* ERROR: no posit support in C */;
        double r5268098 = r5268093 * r5268093;
        double r5268099 = r5268097 * r5268098;
        double r5268100 = r5268095 + r5268099;
        double r5268101 = 0.0072644182;
        double r5268102 = /* ERROR: no posit support in C */;
        double r5268103 = r5268098 * r5268093;
        double r5268104 = r5268102 * r5268103;
        double r5268105 = r5268100 + r5268104;
        double r5268106 = 0.0005064034;
        double r5268107 = /* ERROR: no posit support in C */;
        double r5268108 = r5268103 * r5268093;
        double r5268109 = r5268107 * r5268108;
        double r5268110 = r5268105 + r5268109;
        double r5268111 = 0.0001789971;
        double r5268112 = /* ERROR: no posit support in C */;
        double r5268113 = r5268108 * r5268093;
        double r5268114 = r5268112 * r5268113;
        double r5268115 = r5268110 + r5268114;
        double r5268116 = 0.7715471019;
        double r5268117 = /* ERROR: no posit support in C */;
        double r5268118 = r5268117 * r5268093;
        double r5268119 = r5268089 + r5268118;
        double r5268120 = 0.2909738639;
        double r5268121 = /* ERROR: no posit support in C */;
        double r5268122 = r5268121 * r5268098;
        double r5268123 = r5268119 + r5268122;
        double r5268124 = 0.0694555761;
        double r5268125 = /* ERROR: no posit support in C */;
        double r5268126 = r5268125 * r5268103;
        double r5268127 = r5268123 + r5268126;
        double r5268128 = 0.0140005442;
        double r5268129 = /* ERROR: no posit support in C */;
        double r5268130 = r5268129 * r5268108;
        double r5268131 = r5268127 + r5268130;
        double r5268132 = 0.0008327945;
        double r5268133 = /* ERROR: no posit support in C */;
        double r5268134 = r5268133 * r5268113;
        double r5268135 = r5268131 + r5268134;
        double r5268136 = 2.0;
        double r5268137 = /* ERROR: no posit support in C */;
        double r5268138 = r5268137 * r5268112;
        double r5268139 = r5268113 * r5268093;
        double r5268140 = r5268138 * r5268139;
        double r5268141 = r5268135 + r5268140;
        double r5268142 = r5268115 / r5268141;
        double r5268143 = r5268142 * r5268092;
        return r5268143;
}

↓

double f(double x) {
        double r5268144 = 0.0424060604;
        double r5268145 = x;
        double r5268146 = r5268145 * r5268145;
        double r5268147 = r5268146 * r5268146;
        double r5268148 = 0.0005064034;
        double r5268149 = 0.0001789971;
        double r5268150 = r5268145 * r5268149;
        double r5268151 = r5268145 * r5268150;
        double r5268152 = r5268148 + r5268151;
        double r5268153 = r5268147 * r5268152;
        double r5268154 = r5268144 + r5268153;
        double r5268155 = 0.0072644182;
        double r5268156 = r5268146 * r5268155;
        double r5268157 = r5268154 + r5268156;
        double r5268158 = r5268157 * r5268147;
        double r5268159 = 0.1049934947;
        double r5268160 = r5268159 * r5268146;
        double r5268161 = r5268158 + r5268160;
        double r5268162 = 1.0;
        double r5268163 = r5268161 + r5268162;
        double r5268164 = 0.0694555761;
        double r5268165 = 2.0;
        double r5268166 = r5268165 * r5268150;
        double r5268167 = r5268166 * r5268145;
        double r5268168 = 0.0008327945;
        double r5268169 = r5268167 + r5268168;
        double r5268170 = r5268147 * r5268169;
        double r5268171 = r5268164 + r5268170;
        double r5268172 = r5268147 * r5268171;
        double r5268173 = 0.2909738639;
        double r5268174 = r5268146 * r5268173;
        double r5268175 = 0.7715471019;
        double r5268176 = r5268174 + r5268175;
        double r5268177 = r5268172 + r5268176;
        double r5268178 = r5268177 * r5268146;
        double r5268179 = 0.0140005442;
        double r5268180 = r5268147 * r5268147;
        double r5268181 = r5268179 * r5268180;
        double r5268182 = r5268162 + r5268181;
        double r5268183 = r5268178 + r5268182;
        double r5268184 = r5268163 / r5268183;
        double r5268185 = r5268184 * r5268145;
        return r5268185;
}

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. Simplified 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(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-expand 3.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. Simplified 3.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-identity 3.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-expand 3.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-frac 3.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. Simplified 3.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. Simplified 3.6

    \[\leadsto \color{blue}{\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) \cdot x}\]
13. Using strategy rm

14. Applied associate-*l* 3.6

    \[\leadsto \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) \cdot x\]

15. Final simplification 3.6

    \[\leadsto \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)} \cdot x\]

Reproduce

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