Initial program 1.2
\[\frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}\]
- Using strategy
rm Applied *-un-lft-identity1.2
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\color{blue}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1\right)}}\]
Applied add-sqr-sqrt1.8
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\color{blue}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1\right)}\]
Applied add-sqr-sqrt2.1
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\color{blue}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1\right)}\]
Applied *-un-lft-identity2.1
\[\leadsto \frac{\frac{\frac{\color{blue}{1 \cdot \left(\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1\right)}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1\right)}\]
Applied times-frac2.1
\[\leadsto \frac{\frac{\color{blue}{\frac{1}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}} \cdot \frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1\right)}\]
Applied times-frac1.9
\[\leadsto \frac{\color{blue}{\frac{\frac{1}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}} \cdot \frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1\right)}\]
Applied times-frac1.9
\[\leadsto \color{blue}{\frac{\frac{\frac{1}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{1} \cdot \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\]
Simplified1.3
\[\leadsto \color{blue}{\frac{1}{\left(\alpha + \beta\right) + 2 \cdot 1}} \cdot \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}\]
Simplified1.2
\[\leadsto \frac{1}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \color{blue}{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\]
- Using strategy
rm Applied add-sqr-sqrt1.3
\[\leadsto \frac{1}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \color{blue}{\left(\sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\right)}\]
Applied associate-*r*1.3
\[\leadsto \color{blue}{\left(\frac{1}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\right) \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}}\]
Simplified1.3
\[\leadsto \color{blue}{\frac{\sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}}{\left(\alpha + \beta\right) + 2 \cdot 1}} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\]
- Using strategy
rm Applied *-un-lft-identity1.3
\[\leadsto \frac{\sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\color{blue}{1 \cdot \left(\left(\alpha + \beta\right) + 2 \cdot 1\right)}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\]
Applied add-sqr-sqrt1.3
\[\leadsto \frac{\sqrt{\frac{\frac{\color{blue}{\sqrt{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1} \cdot \sqrt{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}}}{1 \cdot \left(\left(\alpha + \beta\right) + 2 \cdot 1\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\]
Applied times-frac1.3
\[\leadsto \frac{\sqrt{\frac{\color{blue}{\frac{\sqrt{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}}{1} \cdot \frac{\sqrt{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\]
Simplified1.3
\[\leadsto \frac{\sqrt{\frac{\color{blue}{\sqrt{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}} \cdot \frac{\sqrt{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}}\]