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(1.0\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
- Using strategy
rm Applied *p16-lft-identity-expand0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(1.0\right)\right)}}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied *p16-lft-identity-expand0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)\right)}}{\left(\left(1.0\right) \cdot \left(1.0\right)\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied distribute-lft-out0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)\right)}}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied associate-/l*0.4
\[\leadsto \frac{\left(\frac{\color{blue}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)}\right)}\right)}}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
- Using strategy
rm Applied *p16-rgt-identity-expand0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(1.0\right)\right)}}\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied *p16-lft-identity-expand0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)\right)}}{\left(\left(1.0\right) \cdot \left(1.0\right)\right)}\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied p16-distribute-lft-out0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)\right)}}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied *p16-rgt-identity-expand0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right) \cdot \left(1.0\right)\right)}}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied p16-times-frac0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\left(1.0\right)}{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)}\right)\right)}}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied *p16-rgt-identity-expand0.4
\[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(1.0\right)\right)}}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)}\right)\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied p16-times-frac0.4
\[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)}\right)}\right)\right)}}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Applied associate-/l*0.4
\[\leadsto \frac{\color{blue}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)}\right)}\right)}\right)}\right)}}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Simplified0.3
\[\leadsto \frac{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\right)}{\color{blue}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\beta}\right)}{\left(\frac{\left(\beta \cdot \alpha\right)}{\left(\frac{\left(1.0\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}\right)}\right)}}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
Final simplification0.3
\[\leadsto \frac{\frac{\frac{1.0}{\frac{\left(\alpha + \beta\right) + 2 \cdot 1}{1.0}}}{\frac{\left(\alpha + 2 \cdot 1\right) + \beta}{\beta \cdot \alpha + \left(1.0 + \left(\beta + \alpha\right)\right)}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]