Jmat.Real.dawson

Average Error: 4.3 → 3.4

Time: 1.7m

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

C

double f(double x) {
        double r5091156 = 1.0;
        double r5091157 = /* ERROR: no posit support in C */;
        double r5091158 = 0.1049934947;
        double r5091159 = /* ERROR: no posit support in C */;
        double r5091160 = x;
        double r5091161 = r5091160 * r5091160;
        double r5091162 = r5091159 * r5091161;
        double r5091163 = r5091157 + r5091162;
        double r5091164 = 0.0424060604;
        double r5091165 = /* ERROR: no posit support in C */;
        double r5091166 = r5091161 * r5091161;
        double r5091167 = r5091165 * r5091166;
        double r5091168 = r5091163 + r5091167;
        double r5091169 = 0.0072644182;
        double r5091170 = /* ERROR: no posit support in C */;
        double r5091171 = r5091166 * r5091161;
        double r5091172 = r5091170 * r5091171;
        double r5091173 = r5091168 + r5091172;
        double r5091174 = 0.0005064034;
        double r5091175 = /* ERROR: no posit support in C */;
        double r5091176 = r5091171 * r5091161;
        double r5091177 = r5091175 * r5091176;
        double r5091178 = r5091173 + r5091177;
        double r5091179 = 0.0001789971;
        double r5091180 = /* ERROR: no posit support in C */;
        double r5091181 = r5091176 * r5091161;
        double r5091182 = r5091180 * r5091181;
        double r5091183 = r5091178 + r5091182;
        double r5091184 = 0.7715471019;
        double r5091185 = /* ERROR: no posit support in C */;
        double r5091186 = r5091185 * r5091161;
        double r5091187 = r5091157 + r5091186;
        double r5091188 = 0.2909738639;
        double r5091189 = /* ERROR: no posit support in C */;
        double r5091190 = r5091189 * r5091166;
        double r5091191 = r5091187 + r5091190;
        double r5091192 = 0.0694555761;
        double r5091193 = /* ERROR: no posit support in C */;
        double r5091194 = r5091193 * r5091171;
        double r5091195 = r5091191 + r5091194;
        double r5091196 = 0.0140005442;
        double r5091197 = /* ERROR: no posit support in C */;
        double r5091198 = r5091197 * r5091176;
        double r5091199 = r5091195 + r5091198;
        double r5091200 = 0.0008327945;
        double r5091201 = /* ERROR: no posit support in C */;
        double r5091202 = r5091201 * r5091181;
        double r5091203 = r5091199 + r5091202;
        double r5091204 = 2.0;
        double r5091205 = /* ERROR: no posit support in C */;
        double r5091206 = r5091205 * r5091180;
        double r5091207 = r5091181 * r5091161;
        double r5091208 = r5091206 * r5091207;
        double r5091209 = r5091203 + r5091208;
        double r5091210 = r5091183 / r5091209;
        double r5091211 = r5091210 * r5091160;
        return r5091211;
}

↓

double f(double x) {
        double r5091212 = x;
        double r5091213 = r5091212 * r5091212;
        double r5091214 = 0.0424060604;
        double r5091215 = /* ERROR: no posit support in C */;
        double r5091216 = 0.0072644182;
        double r5091217 = /* ERROR: no posit support in C */;
        double r5091218 = 0.0001789971;
        double r5091219 = /* ERROR: no posit support in C */;
        double r5091220 = r5091213 * r5091219;
        double r5091221 = 0.0005064034;
        double r5091222 = /* ERROR: no posit support in C */;
        double r5091223 = r5091220 + r5091222;
        double r5091224 = r5091223 * r5091213;
        double r5091225 = r5091217 + r5091224;
        double r5091226 = r5091225 * r5091213;
        double r5091227 = r5091215 + r5091226;
        double r5091228 = r5091227 * r5091213;
        double r5091229 = 0.1049934947;
        double r5091230 = /* ERROR: no posit support in C */;
        double r5091231 = r5091228 + r5091230;
        double r5091232 = r5091213 * r5091231;
        double r5091233 = 1.0;
        double r5091234 = /* ERROR: no posit support in C */;
        double r5091235 = r5091232 + r5091234;
        double r5091236 = r5091235 * r5091212;
        double r5091237 = r5091213 * r5091213;
        double r5091238 = 0.0140005442;
        double r5091239 = /* ERROR: no posit support in C */;
        double r5091240 = r5091237 * r5091239;
        double r5091241 = r5091240 * r5091237;
        double r5091242 = r5091241 + r5091234;
        double r5091243 = 0.0008327945;
        double r5091244 = /* ERROR: no posit support in C */;
        double r5091245 = 2.0;
        double r5091246 = /* ERROR: no posit support in C */;
        double r5091247 = r5091219 * r5091246;
        double r5091248 = r5091247 * r5091213;
        double r5091249 = r5091244 + r5091248;
        double r5091250 = r5091237 * r5091249;
        double r5091251 = 0.0694555761;
        double r5091252 = /* ERROR: no posit support in C */;
        double r5091253 = r5091250 + r5091252;
        double r5091254 = r5091237 * r5091253;
        double r5091255 = 0.7715471019;
        double r5091256 = /* ERROR: no posit support in C */;
        double r5091257 = 0.2909738639;
        double r5091258 = /* ERROR: no posit support in C */;
        double r5091259 = r5091258 * r5091213;
        double r5091260 = r5091256 + r5091259;
        double r5091261 = r5091254 + r5091260;
        double r5091262 = r5091213 * r5091261;
        double r5091263 = r5091242 + r5091262;
        double r5091264 = r5091236 / r5091263;
        return r5091264;
}

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. Simplified 3.6

   \[\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 associate-*l* 3.5

   \[\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)}{\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)}{\color{blue}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\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)}\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. Using strategy rm

6. Applied p16-*-un-lft-identity 3.5

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

7. Applied associate-/r* 3.5

   \[\leadsto \color{blue}{\left(\frac{\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)}{\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(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\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)}\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\]

8. Simplified 3.5

   \[\leadsto \left(\frac{\color{blue}{\left(\frac{\left(1\right)}{\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.0072644182\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}{\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(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\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)}\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\]

9. Simplified 3.3

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

11. Applied p16-*-un-lft-identity 3.3

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

12. Applied associate-/r* 3.3

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

13. Simplified 3.4

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

14. Final simplification 3.4

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

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))