Jmat.Real.dawson

Average Error: 4.4 → 3.6

Time: 1.8m

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\]

↓

\[\left(\frac{\left(1.0\right)}{\left(\frac{\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)}{\left(\frac{\left(\left(x \cdot x\right) \cdot \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(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(0.0001789971\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}{\left(0.0072644182\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)\right)}{\left(1\right)}\right)}\right)}\right) \cdot x\]

C

double f(double x) {
        double r6826769 = 1.0;
        double r6826770 = /* ERROR: no posit support in C */;
        double r6826771 = 0.1049934947;
        double r6826772 = /* ERROR: no posit support in C */;
        double r6826773 = x;
        double r6826774 = r6826773 * r6826773;
        double r6826775 = r6826772 * r6826774;
        double r6826776 = r6826770 + r6826775;
        double r6826777 = 0.0424060604;
        double r6826778 = /* ERROR: no posit support in C */;
        double r6826779 = r6826774 * r6826774;
        double r6826780 = r6826778 * r6826779;
        double r6826781 = r6826776 + r6826780;
        double r6826782 = 0.0072644182;
        double r6826783 = /* ERROR: no posit support in C */;
        double r6826784 = r6826779 * r6826774;
        double r6826785 = r6826783 * r6826784;
        double r6826786 = r6826781 + r6826785;
        double r6826787 = 0.0005064034;
        double r6826788 = /* ERROR: no posit support in C */;
        double r6826789 = r6826784 * r6826774;
        double r6826790 = r6826788 * r6826789;
        double r6826791 = r6826786 + r6826790;
        double r6826792 = 0.0001789971;
        double r6826793 = /* ERROR: no posit support in C */;
        double r6826794 = r6826789 * r6826774;
        double r6826795 = r6826793 * r6826794;
        double r6826796 = r6826791 + r6826795;
        double r6826797 = 0.7715471019;
        double r6826798 = /* ERROR: no posit support in C */;
        double r6826799 = r6826798 * r6826774;
        double r6826800 = r6826770 + r6826799;
        double r6826801 = 0.2909738639;
        double r6826802 = /* ERROR: no posit support in C */;
        double r6826803 = r6826802 * r6826779;
        double r6826804 = r6826800 + r6826803;
        double r6826805 = 0.0694555761;
        double r6826806 = /* ERROR: no posit support in C */;
        double r6826807 = r6826806 * r6826784;
        double r6826808 = r6826804 + r6826807;
        double r6826809 = 0.0140005442;
        double r6826810 = /* ERROR: no posit support in C */;
        double r6826811 = r6826810 * r6826789;
        double r6826812 = r6826808 + r6826811;
        double r6826813 = 0.0008327945;
        double r6826814 = /* ERROR: no posit support in C */;
        double r6826815 = r6826814 * r6826794;
        double r6826816 = r6826812 + r6826815;
        double r6826817 = 2.0;
        double r6826818 = /* ERROR: no posit support in C */;
        double r6826819 = r6826818 * r6826793;
        double r6826820 = r6826794 * r6826774;
        double r6826821 = r6826819 * r6826820;
        double r6826822 = r6826816 + r6826821;
        double r6826823 = r6826796 / r6826822;
        double r6826824 = r6826823 * r6826773;
        return r6826824;
}

↓

double f(double x) {
        double r6826825 = 1.0;
        double r6826826 = /* ERROR: no posit support in C */;
        double r6826827 = 1.0;
        double r6826828 = /* ERROR: no posit support in C */;
        double r6826829 = x;
        double r6826830 = r6826829 * r6826829;
        double r6826831 = 0.7715471019;
        double r6826832 = /* ERROR: no posit support in C */;
        double r6826833 = 0.2909738639;
        double r6826834 = /* ERROR: no posit support in C */;
        double r6826835 = r6826834 * r6826830;
        double r6826836 = r6826832 + r6826835;
        double r6826837 = r6826830 * r6826830;
        double r6826838 = 0.0694555761;
        double r6826839 = /* ERROR: no posit support in C */;
        double r6826840 = 0.0001789971;
        double r6826841 = /* ERROR: no posit support in C */;
        double r6826842 = r6826841 * r6826830;
        double r6826843 = 2.0;
        double r6826844 = /* ERROR: no posit support in C */;
        double r6826845 = r6826842 * r6826844;
        double r6826846 = 0.0008327945;
        double r6826847 = /* ERROR: no posit support in C */;
        double r6826848 = r6826845 + r6826847;
        double r6826849 = r6826848 * r6826837;
        double r6826850 = r6826839 + r6826849;
        double r6826851 = r6826837 * r6826850;
        double r6826852 = r6826836 + r6826851;
        double r6826853 = r6826830 * r6826852;
        double r6826854 = r6826828 + r6826853;
        double r6826855 = 0.0140005442;
        double r6826856 = /* ERROR: no posit support in C */;
        double r6826857 = r6826856 * r6826837;
        double r6826858 = r6826857 * r6826837;
        double r6826859 = r6826854 + r6826858;
        double r6826860 = 0.1049934947;
        double r6826861 = /* ERROR: no posit support in C */;
        double r6826862 = 0.0005064034;
        double r6826863 = /* ERROR: no posit support in C */;
        double r6826864 = r6826863 + r6826842;
        double r6826865 = r6826830 * r6826864;
        double r6826866 = 0.0072644182;
        double r6826867 = /* ERROR: no posit support in C */;
        double r6826868 = r6826865 + r6826867;
        double r6826869 = r6826830 * r6826868;
        double r6826870 = 0.0424060604;
        double r6826871 = /* ERROR: no posit support in C */;
        double r6826872 = r6826869 + r6826871;
        double r6826873 = r6826830 * r6826872;
        double r6826874 = r6826861 + r6826873;
        double r6826875 = r6826830 * r6826874;
        double r6826876 = r6826875 + r6826828;
        double r6826877 = r6826859 / r6826876;
        double r6826878 = r6826826 / r6826877;
        double r6826879 = r6826878 * r6826829;
        return r6826879;
}

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-*-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(\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\]

9. Applied associate-/l* 3.6

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

11. Applied *p16-rgt-identity-expand 3.6

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

12. Applied associate-/l* 3.6

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

13. Simplified 3.6

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

14. Final simplification 3.6

    \[\leadsto \left(\frac{\left(1.0\right)}{\left(\frac{\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)}{\left(\frac{\left(\left(x \cdot x\right) \cdot \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(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(0.0001789971\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}{\left(0.0072644182\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)\right)}{\left(1\right)}\right)}\right)}\right) \cdot x\]

Reproduce

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