Average Error: 4.2 → 3.3
Time: 1.2m
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{x \cdot \left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(\left(0.0005064034 \cdot \left(x \cdot x\right) + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right)\right) + 0.0072644182\right) + 0.0424060604\right) \cdot \left(x \cdot x\right) + 0.1049934947\right) + 1\right)}{\left(\left(x \cdot x\right) \cdot 0.7715471019 + 1\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 0.0694555761 + 0.2909738639\right) + \left(\left(x \cdot x\right) \cdot \left(0.0008327945 + x \cdot \left(x \cdot \left(0.0001789971 \cdot 2\right)\right)\right) + 0.0140005442\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\]
\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(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(\left(0.0005064034 \cdot \left(x \cdot x\right) + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right)\right) + 0.0072644182\right) + 0.0424060604\right) \cdot \left(x \cdot x\right) + 0.1049934947\right) + 1\right)}{\left(\left(x \cdot x\right) \cdot 0.7715471019 + 1\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 0.0694555761 + 0.2909738639\right) + \left(\left(x \cdot x\right) \cdot \left(0.0008327945 + x \cdot \left(x \cdot \left(0.0001789971 \cdot 2\right)\right)\right) + 0.0140005442\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}
double f(double x) {
        double r5472391 = 1.0;
        double r5472392 = /* ERROR: no posit support in C */;
        double r5472393 = 0.1049934947;
        double r5472394 = /* ERROR: no posit support in C */;
        double r5472395 = x;
        double r5472396 = r5472395 * r5472395;
        double r5472397 = r5472394 * r5472396;
        double r5472398 = r5472392 + r5472397;
        double r5472399 = 0.0424060604;
        double r5472400 = /* ERROR: no posit support in C */;
        double r5472401 = r5472396 * r5472396;
        double r5472402 = r5472400 * r5472401;
        double r5472403 = r5472398 + r5472402;
        double r5472404 = 0.0072644182;
        double r5472405 = /* ERROR: no posit support in C */;
        double r5472406 = r5472401 * r5472396;
        double r5472407 = r5472405 * r5472406;
        double r5472408 = r5472403 + r5472407;
        double r5472409 = 0.0005064034;
        double r5472410 = /* ERROR: no posit support in C */;
        double r5472411 = r5472406 * r5472396;
        double r5472412 = r5472410 * r5472411;
        double r5472413 = r5472408 + r5472412;
        double r5472414 = 0.0001789971;
        double r5472415 = /* ERROR: no posit support in C */;
        double r5472416 = r5472411 * r5472396;
        double r5472417 = r5472415 * r5472416;
        double r5472418 = r5472413 + r5472417;
        double r5472419 = 0.7715471019;
        double r5472420 = /* ERROR: no posit support in C */;
        double r5472421 = r5472420 * r5472396;
        double r5472422 = r5472392 + r5472421;
        double r5472423 = 0.2909738639;
        double r5472424 = /* ERROR: no posit support in C */;
        double r5472425 = r5472424 * r5472401;
        double r5472426 = r5472422 + r5472425;
        double r5472427 = 0.0694555761;
        double r5472428 = /* ERROR: no posit support in C */;
        double r5472429 = r5472428 * r5472406;
        double r5472430 = r5472426 + r5472429;
        double r5472431 = 0.0140005442;
        double r5472432 = /* ERROR: no posit support in C */;
        double r5472433 = r5472432 * r5472411;
        double r5472434 = r5472430 + r5472433;
        double r5472435 = 0.0008327945;
        double r5472436 = /* ERROR: no posit support in C */;
        double r5472437 = r5472436 * r5472416;
        double r5472438 = r5472434 + r5472437;
        double r5472439 = 2.0;
        double r5472440 = /* ERROR: no posit support in C */;
        double r5472441 = r5472440 * r5472415;
        double r5472442 = r5472416 * r5472396;
        double r5472443 = r5472441 * r5472442;
        double r5472444 = r5472438 + r5472443;
        double r5472445 = r5472418 / r5472444;
        double r5472446 = r5472445 * r5472395;
        return r5472446;
}
↓
double f(double x) {
        double r5472447 = x;
        double r5472448 = r5472447 * r5472447;
        double r5472449 = 0.0005064034;
        double r5472450 = r5472449 * r5472448;
        double r5472451 = 0.0001789971;
        double r5472452 = r5472448 * r5472451;
        double r5472453 = r5472448 * r5472452;
        double r5472454 = r5472450 + r5472453;
        double r5472455 = 0.0072644182;
        double r5472456 = r5472454 + r5472455;
        double r5472457 = r5472448 * r5472456;
        double r5472458 = 0.0424060604;
        double r5472459 = r5472457 + r5472458;
        double r5472460 = r5472459 * r5472448;
        double r5472461 = 0.1049934947;
        double r5472462 = r5472460 + r5472461;
        double r5472463 = r5472448 * r5472462;
        double r5472464 = 1.0;
        double r5472465 = r5472463 + r5472464;
        double r5472466 = r5472447 * r5472465;
        double r5472467 = 0.7715471019;
        double r5472468 = r5472448 * r5472467;
        double r5472469 = r5472468 + r5472464;
        double r5472470 = r5472448 * r5472448;
        double r5472471 = 0.0694555761;
        double r5472472 = r5472448 * r5472471;
        double r5472473 = 0.2909738639;
        double r5472474 = r5472472 + r5472473;
        double r5472475 = 0.0008327945;
        double r5472476 = 2.0;
        double r5472477 = r5472451 * r5472476;
        double r5472478 = r5472447 * r5472477;
        double r5472479 = r5472447 * r5472478;
        double r5472480 = r5472475 + r5472479;
        double r5472481 = r5472448 * r5472480;
        double r5472482 = 0.0140005442;
        double r5472483 = r5472481 + r5472482;
        double r5472484 = r5472483 * r5472470;
        double r5472485 = r5472474 + r5472484;
        double r5472486 = r5472470 * r5472485;
        double r5472487 = r5472469 + r5472486;
        double r5472488 = r5472466 / r5472487;
        return r5472488;
}

Error

Bits error versus x

Derivation

  1. Initial program 4.2

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

  3. Simplified3.4

    \[\leadsto \color{blue}{\left(\frac{x}{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}{\left(1\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0008327945\right)}{\left(\left(x \cdot x\right) \cdot \left(\left(0.0001789971\right) \cdot \left(2\right)\right)\right)}\right)\right)}{\left(0.0140005442\right)}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)\right)}\right)}\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0005064034\right) \cdot \left(x \cdot x\right)\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0001789971\right)\right)}\right)}{\left(0.0072644182\right)}\right)\right)}{\left(0.0424060604\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(0.1049934947\right)}\right)\right)}{\left(1\right)}\right)}\]
  4. Using strategy rm

  5. Applied associate-*l/3.3

    \[\leadsto \color{blue}{\frac{\left(x \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0005064034\right) \cdot \left(x \cdot x\right)\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0001789971\right)\right)}\right)}{\left(0.0072644182\right)}\right)\right)}{\left(0.0424060604\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(0.1049934947\right)}\right)\right)}{\left(1\right)}\right)\right)}{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}{\left(1\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0008327945\right)}{\left(\left(x \cdot x\right) \cdot \left(\left(0.0001789971\right) \cdot \left(2\right)\right)\right)}\right)\right)}{\left(0.0140005442\right)}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)\right)}\right)}}\]
  6. Using strategy rm

  7. Applied associate-*l*3.3

    \[\leadsto \frac{\left(x \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0005064034\right) \cdot \left(x \cdot x\right)\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)\right)}}\right)}{\left(0.0072644182\right)}\right)\right)}{\left(0.0424060604\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(0.1049934947\right)}\right)\right)}{\left(1\right)}\right)\right)}{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}{\left(1\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0008327945\right)}{\left(\left(x \cdot x\right) \cdot \left(\left(0.0001789971\right) \cdot \left(2\right)\right)\right)}\right)\right)}{\left(0.0140005442\right)}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)\right)}\right)}\]
  8. Using strategy rm

  9. Applied associate-*l*3.3

    \[\leadsto \frac{\left(x \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0005064034\right) \cdot \left(x \cdot x\right)\right)}{\left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)\right)}\right)}{\left(0.0072644182\right)}\right)\right)}{\left(0.0424060604\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(0.1049934947\right)}\right)\right)}{\left(1\right)}\right)\right)}{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}{\left(1\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0008327945\right)}{\color{blue}{\left(x \cdot \left(x \cdot \left(\left(0.0001789971\right) \cdot \left(2\right)\right)\right)\right)}}\right)\right)}{\left(0.0140005442\right)}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)\right)}\right)}\]

  10. Final simplification3.3

    \[\leadsto \frac{x \cdot \left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(\left(0.0005064034 \cdot \left(x \cdot x\right) + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right)\right) + 0.0072644182\right) + 0.0424060604\right) \cdot \left(x \cdot x\right) + 0.1049934947\right) + 1\right)}{\left(\left(x \cdot x\right) \cdot 0.7715471019 + 1\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 0.0694555761 + 0.2909738639\right) + \left(\left(x \cdot x\right) \cdot \left(0.0008327945 + x \cdot \left(x \cdot \left(0.0001789971 \cdot 2\right)\right)\right) + 0.0140005442\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\]

Reproduce

herbie shell --seed 2019134 
(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))