Initial program 0.4
\[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(real->posit(1.0)\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
- Using strategy
rm Applied +-commutative0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\color{blue}{\left(\frac{\left(\beta \cdot \alpha\right)}{\left(\frac{\alpha}{\beta}\right)}\right)}}{\left(real->posit(1.0)\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
Applied associate-+l+0.3
\[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\frac{\left(\beta \cdot \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(real->posit(1.0)\right)}\right)}\right)}}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
- Using strategy
rm Applied +-commutative0.3
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\beta \cdot \alpha\right)}{\left(\frac{\color{blue}{\left(\frac{\beta}{\alpha}\right)}}{\left(real->posit(1.0)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
Applied associate-+l+0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\beta \cdot \alpha\right)}{\color{blue}{\left(\frac{\beta}{\left(\frac{\alpha}{\left(real->posit(1.0)\right)}\right)}\right)}}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
Applied associate-+r+0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\frac{\left(\frac{\left(\beta \cdot \alpha\right)}{\beta}\right)}{\left(\frac{\alpha}{\left(real->posit(1.0)\right)}\right)}\right)}}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
- Using strategy
rm Applied *-commutative0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\color{blue}{\left(\alpha \cdot \beta\right)}}{\beta}\right)}{\left(\frac{\alpha}{\left(real->posit(1.0)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
Applied distribute-lft1-in0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\frac{\alpha}{\left(real->posit(1.0)\right)}\right) \cdot \beta\right)}}{\left(\frac{\alpha}{\left(real->posit(1.0)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(real->posit(2)\right) \cdot \left(real->posit(1)\right)\right)}\right)}{\left(real->posit(1.0)\right)}\right)}\]
Final simplification0.4
\[\leadsto \frac{\frac{\frac{\left(\alpha + 1.0\right) \cdot \beta + \left(\alpha + 1.0\right)}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]