Average Error: 4.3 → 3.4
Time: 56.7s
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{\left(\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 0.0005064034 + \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)\right) + \left(1 + \left(x \cdot x\right) \cdot 0.1049934947\right)\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0072644182 \cdot \left(x \cdot x\right) + 0.0424060604\right)}{\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + 0.0140005442 \cdot \left(x \cdot x\right)\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 \left(0.0008327945 + 2 \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right)\right)\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot 0.2909738639 + \left(1 + \left(x \cdot x\right) \cdot 0.7715471019\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{\left(\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 0.0005064034 + \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)\right) + \left(1 + \left(x \cdot x\right) \cdot 0.1049934947\right)\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0072644182 \cdot \left(x \cdot x\right) + 0.0424060604\right)}{\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0694555761 + 0.0140005442 \cdot \left(x \cdot x\right)\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 \left(0.0008327945 + 2 \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right)\right)\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot 0.2909738639 + \left(1 + \left(x \cdot x\right) \cdot 0.7715471019\right)\right)} \cdot x
double f(double x) {
        double r2143738 = 1.0;
        double r2143739 = /* ERROR: no posit support in C */;
        double r2143740 = 0.1049934947;
        double r2143741 = /* ERROR: no posit support in C */;
        double r2143742 = x;
        double r2143743 = r2143742 * r2143742;
        double r2143744 = r2143741 * r2143743;
        double r2143745 = r2143739 + r2143744;
        double r2143746 = 0.0424060604;
        double r2143747 = /* ERROR: no posit support in C */;
        double r2143748 = r2143743 * r2143743;
        double r2143749 = r2143747 * r2143748;
        double r2143750 = r2143745 + r2143749;
        double r2143751 = 0.0072644182;
        double r2143752 = /* ERROR: no posit support in C */;
        double r2143753 = r2143748 * r2143743;
        double r2143754 = r2143752 * r2143753;
        double r2143755 = r2143750 + r2143754;
        double r2143756 = 0.0005064034;
        double r2143757 = /* ERROR: no posit support in C */;
        double r2143758 = r2143753 * r2143743;
        double r2143759 = r2143757 * r2143758;
        double r2143760 = r2143755 + r2143759;
        double r2143761 = 0.0001789971;
        double r2143762 = /* ERROR: no posit support in C */;
        double r2143763 = r2143758 * r2143743;
        double r2143764 = r2143762 * r2143763;
        double r2143765 = r2143760 + r2143764;
        double r2143766 = 0.7715471019;
        double r2143767 = /* ERROR: no posit support in C */;
        double r2143768 = r2143767 * r2143743;
        double r2143769 = r2143739 + r2143768;
        double r2143770 = 0.2909738639;
        double r2143771 = /* ERROR: no posit support in C */;
        double r2143772 = r2143771 * r2143748;
        double r2143773 = r2143769 + r2143772;
        double r2143774 = 0.0694555761;
        double r2143775 = /* ERROR: no posit support in C */;
        double r2143776 = r2143775 * r2143753;
        double r2143777 = r2143773 + r2143776;
        double r2143778 = 0.0140005442;
        double r2143779 = /* ERROR: no posit support in C */;
        double r2143780 = r2143779 * r2143758;
        double r2143781 = r2143777 + r2143780;
        double r2143782 = 0.0008327945;
        double r2143783 = /* ERROR: no posit support in C */;
        double r2143784 = r2143783 * r2143763;
        double r2143785 = r2143781 + r2143784;
        double r2143786 = 2.0;
        double r2143787 = /* ERROR: no posit support in C */;
        double r2143788 = r2143787 * r2143762;
        double r2143789 = r2143763 * r2143743;
        double r2143790 = r2143788 * r2143789;
        double r2143791 = r2143785 + r2143790;
        double r2143792 = r2143765 / r2143791;
        double r2143793 = r2143792 * r2143742;
        return r2143793;
}
↓
double f(double x) {
        double r2143794 = x;
        double r2143795 = r2143794 * r2143794;
        double r2143796 = r2143795 * r2143795;
        double r2143797 = r2143796 * r2143796;
        double r2143798 = 0.0005064034;
        double r2143799 = r2143797 * r2143798;
        double r2143800 = 0.0001789971;
        double r2143801 = r2143795 * r2143800;
        double r2143802 = r2143797 * r2143801;
        double r2143803 = r2143799 + r2143802;
        double r2143804 = 1.0;
        double r2143805 = 0.1049934947;
        double r2143806 = r2143795 * r2143805;
        double r2143807 = r2143804 + r2143806;
        double r2143808 = r2143803 + r2143807;
        double r2143809 = 0.0072644182;
        double r2143810 = r2143809 * r2143795;
        double r2143811 = 0.0424060604;
        double r2143812 = r2143810 + r2143811;
        double r2143813 = r2143796 * r2143812;
        double r2143814 = r2143808 + r2143813;
        double r2143815 = 0.0694555761;
        double r2143816 = 0.0140005442;
        double r2143817 = r2143816 * r2143795;
        double r2143818 = r2143815 + r2143817;
        double r2143819 = r2143796 * r2143818;
        double r2143820 = 0.0008327945;
        double r2143821 = 2.0;
        double r2143822 = r2143821 * r2143801;
        double r2143823 = r2143820 + r2143822;
        double r2143824 = r2143797 * r2143823;
        double r2143825 = r2143819 + r2143824;
        double r2143826 = r2143795 * r2143825;
        double r2143827 = 0.2909738639;
        double r2143828 = r2143796 * r2143827;
        double r2143829 = 0.7715471019;
        double r2143830 = r2143795 * r2143829;
        double r2143831 = r2143804 + r2143830;
        double r2143832 = r2143828 + r2143831;
        double r2143833 = r2143826 + r2143832;
        double r2143834 = r2143814 / r2143833;
        double r2143835 = r2143834 * r2143794;
        return r2143835;
}

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

  4. Applied distribute-lft-in3.4

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

  5. Final simplification3.4

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

Reproduce

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