Average Error: 4.3 → 3.4
Time: 57.2s
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(1 + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(0.0005064034 + \left(0.0001789971 \cdot x\right) \cdot x\right) \cdot \left(x \cdot x\right) + 0.0072644182\right) + 0.0424060604\right) + 0.1049934947\right)\right)}{\left(0.7715471019 + \left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 2\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right)\right) + \left(0.0140005442 + \left(x \cdot x\right) \cdot 0.0008327945\right)\right) + 0.0694555761\right) \cdot \left(x \cdot x\right) + 0.2909738639\right)\right) \cdot \left(x \cdot x\right) + 1}\]
\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(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(0.0005064034 + \left(0.0001789971 \cdot x\right) \cdot x\right) \cdot \left(x \cdot x\right) + 0.0072644182\right) + 0.0424060604\right) + 0.1049934947\right)\right)}{\left(0.7715471019 + \left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 2\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right)\right) + \left(0.0140005442 + \left(x \cdot x\right) \cdot 0.0008327945\right)\right) + 0.0694555761\right) \cdot \left(x \cdot x\right) + 0.2909738639\right)\right) \cdot \left(x \cdot x\right) + 1}
double f(double x) {
        double r5841693 = 1.0;
        double r5841694 = /* ERROR: no posit support in C */;
        double r5841695 = 0.1049934947;
        double r5841696 = /* ERROR: no posit support in C */;
        double r5841697 = x;
        double r5841698 = r5841697 * r5841697;
        double r5841699 = r5841696 * r5841698;
        double r5841700 = r5841694 + r5841699;
        double r5841701 = 0.0424060604;
        double r5841702 = /* ERROR: no posit support in C */;
        double r5841703 = r5841698 * r5841698;
        double r5841704 = r5841702 * r5841703;
        double r5841705 = r5841700 + r5841704;
        double r5841706 = 0.0072644182;
        double r5841707 = /* ERROR: no posit support in C */;
        double r5841708 = r5841703 * r5841698;
        double r5841709 = r5841707 * r5841708;
        double r5841710 = r5841705 + r5841709;
        double r5841711 = 0.0005064034;
        double r5841712 = /* ERROR: no posit support in C */;
        double r5841713 = r5841708 * r5841698;
        double r5841714 = r5841712 * r5841713;
        double r5841715 = r5841710 + r5841714;
        double r5841716 = 0.0001789971;
        double r5841717 = /* ERROR: no posit support in C */;
        double r5841718 = r5841713 * r5841698;
        double r5841719 = r5841717 * r5841718;
        double r5841720 = r5841715 + r5841719;
        double r5841721 = 0.7715471019;
        double r5841722 = /* ERROR: no posit support in C */;
        double r5841723 = r5841722 * r5841698;
        double r5841724 = r5841694 + r5841723;
        double r5841725 = 0.2909738639;
        double r5841726 = /* ERROR: no posit support in C */;
        double r5841727 = r5841726 * r5841703;
        double r5841728 = r5841724 + r5841727;
        double r5841729 = 0.0694555761;
        double r5841730 = /* ERROR: no posit support in C */;
        double r5841731 = r5841730 * r5841708;
        double r5841732 = r5841728 + r5841731;
        double r5841733 = 0.0140005442;
        double r5841734 = /* ERROR: no posit support in C */;
        double r5841735 = r5841734 * r5841713;
        double r5841736 = r5841732 + r5841735;
        double r5841737 = 0.0008327945;
        double r5841738 = /* ERROR: no posit support in C */;
        double r5841739 = r5841738 * r5841718;
        double r5841740 = r5841736 + r5841739;
        double r5841741 = 2.0;
        double r5841742 = /* ERROR: no posit support in C */;
        double r5841743 = r5841742 * r5841717;
        double r5841744 = r5841718 * r5841698;
        double r5841745 = r5841743 * r5841744;
        double r5841746 = r5841740 + r5841745;
        double r5841747 = r5841720 / r5841746;
        double r5841748 = r5841747 * r5841697;
        return r5841748;
}
↓
double f(double x) {
        double r5841749 = x;
        double r5841750 = 1.0;
        double r5841751 = r5841749 * r5841749;
        double r5841752 = 0.0005064034;
        double r5841753 = 0.0001789971;
        double r5841754 = r5841753 * r5841749;
        double r5841755 = r5841754 * r5841749;
        double r5841756 = r5841752 + r5841755;
        double r5841757 = r5841756 * r5841751;
        double r5841758 = 0.0072644182;
        double r5841759 = r5841757 + r5841758;
        double r5841760 = r5841751 * r5841759;
        double r5841761 = 0.0424060604;
        double r5841762 = r5841760 + r5841761;
        double r5841763 = r5841751 * r5841762;
        double r5841764 = 0.1049934947;
        double r5841765 = r5841763 + r5841764;
        double r5841766 = r5841751 * r5841765;
        double r5841767 = r5841750 + r5841766;
        double r5841768 = r5841749 * r5841767;
        double r5841769 = 0.7715471019;
        double r5841770 = 2.0;
        double r5841771 = r5841751 * r5841770;
        double r5841772 = r5841753 * r5841751;
        double r5841773 = r5841771 * r5841772;
        double r5841774 = 0.0140005442;
        double r5841775 = 0.0008327945;
        double r5841776 = r5841751 * r5841775;
        double r5841777 = r5841774 + r5841776;
        double r5841778 = r5841773 + r5841777;
        double r5841779 = r5841751 * r5841778;
        double r5841780 = 0.0694555761;
        double r5841781 = r5841779 + r5841780;
        double r5841782 = r5841781 * r5841751;
        double r5841783 = 0.2909738639;
        double r5841784 = r5841782 + r5841783;
        double r5841785 = r5841751 * r5841784;
        double r5841786 = r5841769 + r5841785;
        double r5841787 = r5841786 * r5841751;
        double r5841788 = r5841787 + r5841750;
        double r5841789 = r5841768 / r5841788;
        return r5841789;
}

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

    \[\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.5

    \[\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. Simplified3.4

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

  6. Applied associate-*r*3.4

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

  7. Final simplification3.4

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

Reproduce

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