Error

Derivation

1. Initial program 4.3

   \[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(real->posit(1)\right)}{\left(\left(real->posit(0.1049934947)\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(real->posit(0.0424060604)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(real->posit(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(real->posit(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(real->posit(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(real->posit(1)\right)}{\left(\left(real->posit(0.7715471019)\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(real->posit(0.2909738639)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(real->posit(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(real->posit(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(real->posit(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(real->posit(2)\right) \cdot \left(real->posit(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. Using strategy rm

3. Applied associate-*r*3.4

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

5. Applied *-commutative3.4

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

6. Applied associate-*r*3.5

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

7. Applied associate-*r*3.5

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

9. Applied associate-*l*3.5

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

10. Applied associate-*l*3.5

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

11. Applied associate-*l*3.6

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

12. Applied associate-*l*3.6

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

13. Applied associate-*r*3.3

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

14. Simplified3.3

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

16. Applied *-commutative3.3

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

17. Applied associate-*r*3.3

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

18. Applied associate-*l*3.3

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

19. Applied associate-*l*3.3

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

20. Applied associate-*l*3.3

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

21. Applied associate-*r*3.3

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

22. Simplified3.3

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

23. Final simplification3.3

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

Reproduce

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