Average Error: 4.3 → 3.4
Time: 1.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{\left(\left(0.0005064034 \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) + \left(\left(x \cdot x\right) \cdot 0.0001789971\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) + \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)\right) + \left(1 + \left(x \cdot x\right) \cdot 0.1049934947\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 + \left(0.0140005442 \cdot x\right) \cdot x\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(1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot 0.2909738639\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(0.0005064034 \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) + \left(\left(x \cdot x\right) \cdot 0.0001789971\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) + \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)\right) + \left(1 + \left(x \cdot x\right) \cdot 0.1049934947\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 + \left(0.0140005442 \cdot x\right) \cdot x\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(1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot 0.2909738639\right)\right)} \cdot x
double f(double x) {
        double r2360068 = 1.0;
        double r2360069 = /* ERROR: no posit support in C */;
        double r2360070 = 0.1049934947;
        double r2360071 = /* ERROR: no posit support in C */;
        double r2360072 = x;
        double r2360073 = r2360072 * r2360072;
        double r2360074 = r2360071 * r2360073;
        double r2360075 = r2360069 + r2360074;
        double r2360076 = 0.0424060604;
        double r2360077 = /* ERROR: no posit support in C */;
        double r2360078 = r2360073 * r2360073;
        double r2360079 = r2360077 * r2360078;
        double r2360080 = r2360075 + r2360079;
        double r2360081 = 0.0072644182;
        double r2360082 = /* ERROR: no posit support in C */;
        double r2360083 = r2360078 * r2360073;
        double r2360084 = r2360082 * r2360083;
        double r2360085 = r2360080 + r2360084;
        double r2360086 = 0.0005064034;
        double r2360087 = /* ERROR: no posit support in C */;
        double r2360088 = r2360083 * r2360073;
        double r2360089 = r2360087 * r2360088;
        double r2360090 = r2360085 + r2360089;
        double r2360091 = 0.0001789971;
        double r2360092 = /* ERROR: no posit support in C */;
        double r2360093 = r2360088 * r2360073;
        double r2360094 = r2360092 * r2360093;
        double r2360095 = r2360090 + r2360094;
        double r2360096 = 0.7715471019;
        double r2360097 = /* ERROR: no posit support in C */;
        double r2360098 = r2360097 * r2360073;
        double r2360099 = r2360069 + r2360098;
        double r2360100 = 0.2909738639;
        double r2360101 = /* ERROR: no posit support in C */;
        double r2360102 = r2360101 * r2360078;
        double r2360103 = r2360099 + r2360102;
        double r2360104 = 0.0694555761;
        double r2360105 = /* ERROR: no posit support in C */;
        double r2360106 = r2360105 * r2360083;
        double r2360107 = r2360103 + r2360106;
        double r2360108 = 0.0140005442;
        double r2360109 = /* ERROR: no posit support in C */;
        double r2360110 = r2360109 * r2360088;
        double r2360111 = r2360107 + r2360110;
        double r2360112 = 0.0008327945;
        double r2360113 = /* ERROR: no posit support in C */;
        double r2360114 = r2360113 * r2360093;
        double r2360115 = r2360111 + r2360114;
        double r2360116 = 2.0;
        double r2360117 = /* ERROR: no posit support in C */;
        double r2360118 = r2360117 * r2360092;
        double r2360119 = r2360093 * r2360073;
        double r2360120 = r2360118 * r2360119;
        double r2360121 = r2360115 + r2360120;
        double r2360122 = r2360095 / r2360121;
        double r2360123 = r2360122 * r2360072;
        return r2360123;
}
↓
double f(double x) {
        double r2360124 = 0.0005064034;
        double r2360125 = x;
        double r2360126 = r2360125 * r2360125;
        double r2360127 = r2360126 * r2360126;
        double r2360128 = r2360127 * r2360127;
        double r2360129 = r2360124 * r2360128;
        double r2360130 = 0.0001789971;
        double r2360131 = r2360126 * r2360130;
        double r2360132 = r2360131 * r2360128;
        double r2360133 = r2360129 + r2360132;
        double r2360134 = 0.0072644182;
        double r2360135 = r2360134 * r2360126;
        double r2360136 = 0.0424060604;
        double r2360137 = r2360135 + r2360136;
        double r2360138 = r2360127 * r2360137;
        double r2360139 = r2360133 + r2360138;
        double r2360140 = 1.0;
        double r2360141 = 0.1049934947;
        double r2360142 = r2360126 * r2360141;
        double r2360143 = r2360140 + r2360142;
        double r2360144 = r2360139 + r2360143;
        double r2360145 = 0.0694555761;
        double r2360146 = 0.0140005442;
        double r2360147 = r2360146 * r2360125;
        double r2360148 = r2360147 * r2360125;
        double r2360149 = r2360145 + r2360148;
        double r2360150 = r2360127 * r2360149;
        double r2360151 = 0.0008327945;
        double r2360152 = 2.0;
        double r2360153 = r2360152 * r2360131;
        double r2360154 = r2360151 + r2360153;
        double r2360155 = r2360128 * r2360154;
        double r2360156 = r2360150 + r2360155;
        double r2360157 = r2360126 * r2360156;
        double r2360158 = 0.7715471019;
        double r2360159 = 0.2909738639;
        double r2360160 = r2360126 * r2360159;
        double r2360161 = r2360158 + r2360160;
        double r2360162 = r2360126 * r2360161;
        double r2360163 = r2360140 + r2360162;
        double r2360164 = r2360157 + r2360163;
        double r2360165 = r2360144 / r2360164;
        double r2360166 = r2360165 * r2360125;
        return r2360166;
}

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(\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(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.1049934947\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(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.7715471019\right)}{\left(\left(x \cdot x\right) \cdot \left(0.2909738639\right)\right)}\right)\right)}\right)}\right)}\right) \cdot x}\]
  3. Using strategy rm

  4. Applied distribute-rgt-in3.4

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

  6. Applied associate-*r*3.4

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

  7. Final simplification3.4

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

Reproduce

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