Initial program 1.0
\[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
- Using strategy
rm Applied *p16-rgt-identity-expand1.0
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) \cdot \left(1.0\right)\right)}}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied p16-times-frac0.6
\[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(1.0\right)}\right)\right)}}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied associate-/l*0.6
\[\leadsto \frac{\left(\frac{\color{blue}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}{\left(\frac{\left(\beta - \alpha\right)}{\left(1.0\right)}\right)}\right)}\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Simplified0.6
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\color{blue}{\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right)}{\left(\beta - \alpha\right)}\right)}}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
- Using strategy
rm Applied p16-*-un-lft-identity0.6
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\beta - \alpha\right)\right)}}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied *p16-rgt-identity-expand0.6
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\color{blue}{\left(\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right) \cdot \left(1.0\right)\right)}}{\left(\left(1.0\right) \cdot \left(\beta - \alpha\right)\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied p16-times-frac0.7
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\color{blue}{\left(\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)\right)}}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied p16-*-un-lft-identity0.7
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}}\right)}{\left(\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied *p16-rgt-identity-expand0.7
\[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(1.0\right)\right)}}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}\right)}{\left(\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied p16-times-frac0.7
\[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)\right)}}{\left(\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Applied p16-times-frac0.7
\[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)}\right)\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Simplified0.6
\[\leadsto \frac{\left(\frac{\left(\color{blue}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\beta}{\left(\frac{\left(\frac{\alpha}{\left(2.0\right)}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right)}\right)} \cdot \left(\frac{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Simplified0.6
\[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\beta}{\left(\frac{\left(\frac{\alpha}{\left(2.0\right)}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right)}\right) \cdot \color{blue}{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
Final simplification0.6
\[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\beta}{\left(\frac{\left(\frac{\alpha}{\left(2.0\right)}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]