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 r5625345 = 1.0;
        double r5625346 = /* ERROR: no posit support in C */;
        double r5625347 = 0.1049934947;
        double r5625348 = /* ERROR: no posit support in C */;
        double r5625349 = x;
        double r5625350 = r5625349 * r5625349;
        double r5625351 = r5625348 * r5625350;
        double r5625352 = r5625346 + r5625351;
        double r5625353 = 0.0424060604;
        double r5625354 = /* ERROR: no posit support in C */;
        double r5625355 = r5625350 * r5625350;
        double r5625356 = r5625354 * r5625355;
        double r5625357 = r5625352 + r5625356;
        double r5625358 = 0.0072644182;
        double r5625359 = /* ERROR: no posit support in C */;
        double r5625360 = r5625355 * r5625350;
        double r5625361 = r5625359 * r5625360;
        double r5625362 = r5625357 + r5625361;
        double r5625363 = 0.0005064034;
        double r5625364 = /* ERROR: no posit support in C */;
        double r5625365 = r5625360 * r5625350;
        double r5625366 = r5625364 * r5625365;
        double r5625367 = r5625362 + r5625366;
        double r5625368 = 0.0001789971;
        double r5625369 = /* ERROR: no posit support in C */;
        double r5625370 = r5625365 * r5625350;
        double r5625371 = r5625369 * r5625370;
        double r5625372 = r5625367 + r5625371;
        double r5625373 = 0.7715471019;
        double r5625374 = /* ERROR: no posit support in C */;
        double r5625375 = r5625374 * r5625350;
        double r5625376 = r5625346 + r5625375;
        double r5625377 = 0.2909738639;
        double r5625378 = /* ERROR: no posit support in C */;
        double r5625379 = r5625378 * r5625355;
        double r5625380 = r5625376 + r5625379;
        double r5625381 = 0.0694555761;
        double r5625382 = /* ERROR: no posit support in C */;
        double r5625383 = r5625382 * r5625360;
        double r5625384 = r5625380 + r5625383;
        double r5625385 = 0.0140005442;
        double r5625386 = /* ERROR: no posit support in C */;
        double r5625387 = r5625386 * r5625365;
        double r5625388 = r5625384 + r5625387;
        double r5625389 = 0.0008327945;
        double r5625390 = /* ERROR: no posit support in C */;
        double r5625391 = r5625390 * r5625370;
        double r5625392 = r5625388 + r5625391;
        double r5625393 = 2.0;
        double r5625394 = /* ERROR: no posit support in C */;
        double r5625395 = r5625394 * r5625369;
        double r5625396 = r5625370 * r5625350;
        double r5625397 = r5625395 * r5625396;
        double r5625398 = r5625392 + r5625397;
        double r5625399 = r5625372 / r5625398;
        double r5625400 = r5625399 * r5625349;
        return r5625400;
}
↓
double f(double x) {
        double r5625401 = 1.0;
        double r5625402 = x;
        double r5625403 = r5625402 * r5625402;
        double r5625404 = r5625403 * r5625403;
        double r5625405 = 0.0072644182;
        double r5625406 = r5625404 * r5625405;
        double r5625407 = 0.1049934947;
        double r5625408 = 0.0424060604;
        double r5625409 = r5625403 * r5625408;
        double r5625410 = r5625407 + r5625409;
        double r5625411 = r5625406 + r5625410;
        double r5625412 = r5625403 * r5625411;
        double r5625413 = r5625404 * r5625404;
        double r5625414 = 0.0001789971;
        double r5625415 = r5625403 * r5625414;
        double r5625416 = r5625413 * r5625415;
        double r5625417 = 0.0005064034;
        double r5625418 = r5625413 * r5625417;
        double r5625419 = r5625416 + r5625418;
        double r5625420 = r5625412 + r5625419;
        double r5625421 = r5625401 + r5625420;
        double r5625422 = 0.0694555761;
        double r5625423 = r5625422 * r5625403;
        double r5625424 = 0.2909738639;
        double r5625425 = r5625423 + r5625424;
        double r5625426 = r5625403 * r5625425;
        double r5625427 = 0.7715471019;
        double r5625428 = r5625426 + r5625427;
        double r5625429 = r5625403 * r5625428;
        double r5625430 = 0.0140005442;
        double r5625431 = 2.0;
        double r5625432 = r5625431 * r5625403;
        double r5625433 = r5625432 * r5625414;
        double r5625434 = 0.0008327945;
        double r5625435 = r5625433 + r5625434;
        double r5625436 = r5625403 * r5625435;
        double r5625437 = r5625430 + r5625436;
        double r5625438 = r5625413 * r5625437;
        double r5625439 = r5625401 + r5625438;
        double r5625440 = r5625429 + r5625439;
        double r5625441 = r5625421 / r5625440;
        double r5625442 = r5625441 * r5625402;
        return r5625442;
}

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