Jmat.Real.dawson

Average Error: 4.4 → 3.5

Time: 1.9m

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

C

double f(double x) {
        double r6123269 = 1.0;
        double r6123270 = /* ERROR: no posit support in C */;
        double r6123271 = 0.1049934947;
        double r6123272 = /* ERROR: no posit support in C */;
        double r6123273 = x;
        double r6123274 = r6123273 * r6123273;
        double r6123275 = r6123272 * r6123274;
        double r6123276 = r6123270 + r6123275;
        double r6123277 = 0.0424060604;
        double r6123278 = /* ERROR: no posit support in C */;
        double r6123279 = r6123274 * r6123274;
        double r6123280 = r6123278 * r6123279;
        double r6123281 = r6123276 + r6123280;
        double r6123282 = 0.0072644182;
        double r6123283 = /* ERROR: no posit support in C */;
        double r6123284 = r6123279 * r6123274;
        double r6123285 = r6123283 * r6123284;
        double r6123286 = r6123281 + r6123285;
        double r6123287 = 0.0005064034;
        double r6123288 = /* ERROR: no posit support in C */;
        double r6123289 = r6123284 * r6123274;
        double r6123290 = r6123288 * r6123289;
        double r6123291 = r6123286 + r6123290;
        double r6123292 = 0.0001789971;
        double r6123293 = /* ERROR: no posit support in C */;
        double r6123294 = r6123289 * r6123274;
        double r6123295 = r6123293 * r6123294;
        double r6123296 = r6123291 + r6123295;
        double r6123297 = 0.7715471019;
        double r6123298 = /* ERROR: no posit support in C */;
        double r6123299 = r6123298 * r6123274;
        double r6123300 = r6123270 + r6123299;
        double r6123301 = 0.2909738639;
        double r6123302 = /* ERROR: no posit support in C */;
        double r6123303 = r6123302 * r6123279;
        double r6123304 = r6123300 + r6123303;
        double r6123305 = 0.0694555761;
        double r6123306 = /* ERROR: no posit support in C */;
        double r6123307 = r6123306 * r6123284;
        double r6123308 = r6123304 + r6123307;
        double r6123309 = 0.0140005442;
        double r6123310 = /* ERROR: no posit support in C */;
        double r6123311 = r6123310 * r6123289;
        double r6123312 = r6123308 + r6123311;
        double r6123313 = 0.0008327945;
        double r6123314 = /* ERROR: no posit support in C */;
        double r6123315 = r6123314 * r6123294;
        double r6123316 = r6123312 + r6123315;
        double r6123317 = 2.0;
        double r6123318 = /* ERROR: no posit support in C */;
        double r6123319 = r6123318 * r6123293;
        double r6123320 = r6123294 * r6123274;
        double r6123321 = r6123319 * r6123320;
        double r6123322 = r6123316 + r6123321;
        double r6123323 = r6123296 / r6123322;
        double r6123324 = r6123323 * r6123273;
        return r6123324;
}

↓

double f(double x) {
        double r6123325 = x;
        double r6123326 = 1.0;
        double r6123327 = 0.1049934947;
        double r6123328 = r6123325 * r6123325;
        double r6123329 = 0.0072644182;
        double r6123330 = 0.0001789971;
        double r6123331 = r6123328 * r6123330;
        double r6123332 = 0.0005064034;
        double r6123333 = r6123331 + r6123332;
        double r6123334 = r6123328 * r6123333;
        double r6123335 = r6123329 + r6123334;
        double r6123336 = r6123328 * r6123335;
        double r6123337 = 0.0424060604;
        double r6123338 = r6123336 + r6123337;
        double r6123339 = r6123328 * r6123338;
        double r6123340 = r6123327 + r6123339;
        double r6123341 = r6123340 * r6123328;
        double r6123342 = r6123326 + r6123341;
        double r6123343 = r6123325 * r6123342;
        double r6123344 = 0.7715471019;
        double r6123345 = 0.2909738639;
        double r6123346 = r6123328 * r6123345;
        double r6123347 = r6123344 + r6123346;
        double r6123348 = r6123328 * r6123328;
        double r6123349 = 2.0;
        double r6123350 = r6123328 * r6123349;
        double r6123351 = r6123330 * r6123350;
        double r6123352 = 0.0008327945;
        double r6123353 = r6123351 + r6123352;
        double r6123354 = r6123348 * r6123353;
        double r6123355 = 0.0694555761;
        double r6123356 = r6123354 + r6123355;
        double r6123357 = r6123348 * r6123356;
        double r6123358 = r6123347 + r6123357;
        double r6123359 = r6123328 * r6123358;
        double r6123360 = 0.0140005442;
        double r6123361 = r6123360 * r6123348;
        double r6123362 = r6123361 * r6123348;
        double r6123363 = r6123326 + r6123362;
        double r6123364 = r6123359 + r6123363;
        double r6123365 = r6123343 / r6123364;
        return r6123365;
}

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-rgt-identity-expand 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(\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) \cdot \left(1.0\right)\right)}}\right) \cdot x\]

9. Applied p16-*-un-lft-identity 3.6

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

10. Applied p16-times-frac 3.6

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

11. Simplified 3.6

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

12. Simplified 3.5

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

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

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

15. Applied associate-/r* 3.5

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

16. Simplified 3.5

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

17. Final simplification 3.5

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

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