Average Error: 4.3 → 3.6
Time: 8.9m
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{1.0}{\left(\left(1 + \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(2 \cdot \left(0.0001789971 \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) + \left(0.0008327945 \cdot \left(x \cdot x\right) + 0.0140005442\right)\right)\right) + \left(x \cdot x\right) \cdot 0.7715471019\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.2909738639 + \left(x \cdot x\right) \cdot 0.0694555761\right)} \cdot \left(x \cdot \left(\left(0.1049934947 + \left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right) + 0.0005064034\right) + 0.0072644182\right) \cdot \left(x \cdot x\right) + 0.0424060604\right)\right) \cdot \left(x \cdot x\right) + 1\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{1.0}{\left(\left(1 + \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(2 \cdot \left(0.0001789971 \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) + \left(0.0008327945 \cdot \left(x \cdot x\right) + 0.0140005442\right)\right)\right) + \left(x \cdot x\right) \cdot 0.7715471019\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.2909738639 + \left(x \cdot x\right) \cdot 0.0694555761\right)} \cdot \left(x \cdot \left(\left(0.1049934947 + \left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right) + 0.0005064034\right) + 0.0072644182\right) \cdot \left(x \cdot x\right) + 0.0424060604\right)\right) \cdot \left(x \cdot x\right) + 1\right)\right)
double f(double x) {
        double r38792121 = 1.0;
        double r38792122 = /* ERROR: no posit support in C */;
        double r38792123 = 0.1049934947;
        double r38792124 = /* ERROR: no posit support in C */;
        double r38792125 = x;
        double r38792126 = r38792125 * r38792125;
        double r38792127 = r38792124 * r38792126;
        double r38792128 = r38792122 + r38792127;
        double r38792129 = 0.0424060604;
        double r38792130 = /* ERROR: no posit support in C */;
        double r38792131 = r38792126 * r38792126;
        double r38792132 = r38792130 * r38792131;
        double r38792133 = r38792128 + r38792132;
        double r38792134 = 0.0072644182;
        double r38792135 = /* ERROR: no posit support in C */;
        double r38792136 = r38792131 * r38792126;
        double r38792137 = r38792135 * r38792136;
        double r38792138 = r38792133 + r38792137;
        double r38792139 = 0.0005064034;
        double r38792140 = /* ERROR: no posit support in C */;
        double r38792141 = r38792136 * r38792126;
        double r38792142 = r38792140 * r38792141;
        double r38792143 = r38792138 + r38792142;
        double r38792144 = 0.0001789971;
        double r38792145 = /* ERROR: no posit support in C */;
        double r38792146 = r38792141 * r38792126;
        double r38792147 = r38792145 * r38792146;
        double r38792148 = r38792143 + r38792147;
        double r38792149 = 0.7715471019;
        double r38792150 = /* ERROR: no posit support in C */;
        double r38792151 = r38792150 * r38792126;
        double r38792152 = r38792122 + r38792151;
        double r38792153 = 0.2909738639;
        double r38792154 = /* ERROR: no posit support in C */;
        double r38792155 = r38792154 * r38792131;
        double r38792156 = r38792152 + r38792155;
        double r38792157 = 0.0694555761;
        double r38792158 = /* ERROR: no posit support in C */;
        double r38792159 = r38792158 * r38792136;
        double r38792160 = r38792156 + r38792159;
        double r38792161 = 0.0140005442;
        double r38792162 = /* ERROR: no posit support in C */;
        double r38792163 = r38792162 * r38792141;
        double r38792164 = r38792160 + r38792163;
        double r38792165 = 0.0008327945;
        double r38792166 = /* ERROR: no posit support in C */;
        double r38792167 = r38792166 * r38792146;
        double r38792168 = r38792164 + r38792167;
        double r38792169 = 2.0;
        double r38792170 = /* ERROR: no posit support in C */;
        double r38792171 = r38792170 * r38792145;
        double r38792172 = r38792146 * r38792126;
        double r38792173 = r38792171 * r38792172;
        double r38792174 = r38792168 + r38792173;
        double r38792175 = r38792148 / r38792174;
        double r38792176 = r38792175 * r38792125;
        return r38792176;
}
↓
double f(double x) {
        double r38792177 = 1.0;
        double r38792178 = 1.0;
        double r38792179 = x;
        double r38792180 = r38792179 * r38792179;
        double r38792181 = r38792180 * r38792180;
        double r38792182 = r38792181 * r38792181;
        double r38792183 = 2.0;
        double r38792184 = 0.0001789971;
        double r38792185 = r38792184 * r38792181;
        double r38792186 = r38792183 * r38792185;
        double r38792187 = 0.0008327945;
        double r38792188 = r38792187 * r38792180;
        double r38792189 = 0.0140005442;
        double r38792190 = r38792188 + r38792189;
        double r38792191 = r38792186 + r38792190;
        double r38792192 = r38792182 * r38792191;
        double r38792193 = r38792178 + r38792192;
        double r38792194 = 0.7715471019;
        double r38792195 = r38792180 * r38792194;
        double r38792196 = r38792193 + r38792195;
        double r38792197 = 0.2909738639;
        double r38792198 = 0.0694555761;
        double r38792199 = r38792180 * r38792198;
        double r38792200 = r38792197 + r38792199;
        double r38792201 = r38792181 * r38792200;
        double r38792202 = r38792196 + r38792201;
        double r38792203 = r38792177 / r38792202;
        double r38792204 = 0.1049934947;
        double r38792205 = r38792184 * r38792180;
        double r38792206 = 0.0005064034;
        double r38792207 = r38792205 + r38792206;
        double r38792208 = r38792180 * r38792207;
        double r38792209 = 0.0072644182;
        double r38792210 = r38792208 + r38792209;
        double r38792211 = r38792210 * r38792180;
        double r38792212 = 0.0424060604;
        double r38792213 = r38792211 + r38792212;
        double r38792214 = r38792180 * r38792213;
        double r38792215 = r38792204 + r38792214;
        double r38792216 = r38792215 * r38792180;
        double r38792217 = r38792216 + r38792178;
        double r38792218 = r38792179 * r38792217;
        double r38792219 = r38792203 * r38792218;
        return r38792219;
}

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

    \[\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 associate-*l*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)}{\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 \color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)}\right)}\right)}\right) \cdot x\]

  5. Applied associate-*r*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)}{\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)}{\color{blue}{\left(\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)}}\right)}\right) \cdot x\]
  6. Using strategy rm

  7. Applied p16-*-un-lft-identity3.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)}{\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(\color{blue}{\left(\left(1.0\right) \cdot \left(0.0140005442\right)\right)} \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)}\right)}\right) \cdot x\]

  8. Applied associate-*l*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)}{\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(\color{blue}{\left(\left(1.0\right) \cdot \left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right)\right)} \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)}\right)}\right) \cdot x\]

  9. Applied associate-*l*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)}{\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)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)\right)}}\right)}\right) \cdot x\]

  10. Applied p16-*-un-lft-identity3.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)}{\left(\frac{\left(\frac{\left(1\right)}{\left(\color{blue}{\left(\left(1.0\right) \cdot \left(x \cdot x\right)\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(1.0\right) \cdot \left(\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)\right)}\right)}\right) \cdot x\]

  11. Applied associate-*l*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)}{\left(\frac{\left(\frac{\left(1\right)}{\color{blue}{\left(\left(1.0\right) \cdot \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)}}\right)}{\left(\left(1.0\right) \cdot \left(\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)\right)}\right)}\right) \cdot x\]

  12. Applied p16-*-un-lft-identity3.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)}{\left(\frac{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(1\right)\right)}}{\left(\left(1.0\right) \cdot \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)}\right)}{\left(\left(1.0\right) \cdot \left(\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)\right)}\right)}\right) \cdot x\]

  13. Applied distribute-lft-out3.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)}{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \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)\right)}}{\left(\left(1.0\right) \cdot \left(\left(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)\right)}\right)}\right) \cdot x\]

  14. Applied distribute-lft-out3.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(\left(1.0\right) \cdot \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(\left(0.0140005442\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)}\right)\right)}}\right) \cdot x\]

  15. Applied associate-/r*3.6

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

  16. Simplified3.6

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

  17. Simplified3.5

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

  19. Applied *p16-rgt-identity-expand3.5

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

  20. Applied p16-*-un-lft-identity3.5

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

  21. Applied associate-*l*3.5

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

  22. Applied p16-*-un-lft-identity3.5

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

  23. Applied distribute-lft-out3.5

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

  24. Applied associate-*l*3.5

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

  25. Applied p16-times-frac3.5

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

  26. Simplified3.6

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

  27. Simplified3.6

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

  28. Final simplification3.6

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

Reproduce

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