Average Error: 4.2 → 3.3
Time: 1.1m
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 r6648070 = 1.0;
        double r6648071 = /* ERROR: no posit support in C */;
        double r6648072 = 0.1049934947;
        double r6648073 = /* ERROR: no posit support in C */;
        double r6648074 = x;
        double r6648075 = r6648074 * r6648074;
        double r6648076 = r6648073 * r6648075;
        double r6648077 = r6648071 + r6648076;
        double r6648078 = 0.0424060604;
        double r6648079 = /* ERROR: no posit support in C */;
        double r6648080 = r6648075 * r6648075;
        double r6648081 = r6648079 * r6648080;
        double r6648082 = r6648077 + r6648081;
        double r6648083 = 0.0072644182;
        double r6648084 = /* ERROR: no posit support in C */;
        double r6648085 = r6648080 * r6648075;
        double r6648086 = r6648084 * r6648085;
        double r6648087 = r6648082 + r6648086;
        double r6648088 = 0.0005064034;
        double r6648089 = /* ERROR: no posit support in C */;
        double r6648090 = r6648085 * r6648075;
        double r6648091 = r6648089 * r6648090;
        double r6648092 = r6648087 + r6648091;
        double r6648093 = 0.0001789971;
        double r6648094 = /* ERROR: no posit support in C */;
        double r6648095 = r6648090 * r6648075;
        double r6648096 = r6648094 * r6648095;
        double r6648097 = r6648092 + r6648096;
        double r6648098 = 0.7715471019;
        double r6648099 = /* ERROR: no posit support in C */;
        double r6648100 = r6648099 * r6648075;
        double r6648101 = r6648071 + r6648100;
        double r6648102 = 0.2909738639;
        double r6648103 = /* ERROR: no posit support in C */;
        double r6648104 = r6648103 * r6648080;
        double r6648105 = r6648101 + r6648104;
        double r6648106 = 0.0694555761;
        double r6648107 = /* ERROR: no posit support in C */;
        double r6648108 = r6648107 * r6648085;
        double r6648109 = r6648105 + r6648108;
        double r6648110 = 0.0140005442;
        double r6648111 = /* ERROR: no posit support in C */;
        double r6648112 = r6648111 * r6648090;
        double r6648113 = r6648109 + r6648112;
        double r6648114 = 0.0008327945;
        double r6648115 = /* ERROR: no posit support in C */;
        double r6648116 = r6648115 * r6648095;
        double r6648117 = r6648113 + r6648116;
        double r6648118 = 2.0;
        double r6648119 = /* ERROR: no posit support in C */;
        double r6648120 = r6648119 * r6648094;
        double r6648121 = r6648095 * r6648075;
        double r6648122 = r6648120 * r6648121;
        double r6648123 = r6648117 + r6648122;
        double r6648124 = r6648097 / r6648123;
        double r6648125 = r6648124 * r6648074;
        return r6648125;
}
↓
double f(double x) {
        double r6648126 = x;
        double r6648127 = r6648126 * r6648126;
        double r6648128 = 0.0005064034;
        double r6648129 = r6648128 * r6648127;
        double r6648130 = 0.0001789971;
        double r6648131 = r6648127 * r6648130;
        double r6648132 = r6648127 * r6648131;
        double r6648133 = r6648129 + r6648132;
        double r6648134 = 0.0072644182;
        double r6648135 = r6648133 + r6648134;
        double r6648136 = r6648127 * r6648135;
        double r6648137 = 0.0424060604;
        double r6648138 = r6648136 + r6648137;
        double r6648139 = r6648138 * r6648127;
        double r6648140 = 0.1049934947;
        double r6648141 = r6648139 + r6648140;
        double r6648142 = r6648127 * r6648141;
        double r6648143 = 1.0;
        double r6648144 = r6648142 + r6648143;
        double r6648145 = r6648126 * r6648144;
        double r6648146 = 0.7715471019;
        double r6648147 = r6648127 * r6648146;
        double r6648148 = r6648147 + r6648143;
        double r6648149 = r6648127 * r6648127;
        double r6648150 = 0.0694555761;
        double r6648151 = r6648127 * r6648150;
        double r6648152 = 0.2909738639;
        double r6648153 = r6648151 + r6648152;
        double r6648154 = 0.0008327945;
        double r6648155 = 2.0;
        double r6648156 = r6648130 * r6648155;
        double r6648157 = r6648126 * r6648156;
        double r6648158 = r6648126 * r6648157;
        double r6648159 = r6648154 + r6648158;
        double r6648160 = r6648127 * r6648159;
        double r6648161 = 0.0140005442;
        double r6648162 = r6648160 + r6648161;
        double r6648163 = r6648162 * r6648149;
        double r6648164 = r6648153 + r6648163;
        double r6648165 = r6648149 * r6648164;
        double r6648166 = r6648148 + r6648165;
        double r6648167 = r6648145 / r6648166;
        return r6648167;
}

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 +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))