Initial program 1.3
\[\frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\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}\]
- Using strategy
rm Applied associate-+l+1.3
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\color{blue}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}}\]
- Using strategy
rm Applied add-sqr-sqrt1.9
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\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}}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied add-sqr-sqrt2.3
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\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}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied *-un-lft-identity2.3
\[\leadsto \frac{\frac{\frac{\color{blue}{1 \cdot \left(\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0\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}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied times-frac2.3
\[\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.0}{\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}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied times-frac2.0
\[\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.0}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Simplified1.4
\[\leadsto \frac{\color{blue}{\frac{1}{\left(\beta + 2\right) + \alpha}} \cdot \frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Simplified1.3
\[\leadsto \frac{\frac{1}{\left(\beta + 2\right) + \alpha} \cdot \color{blue}{\frac{\left(\beta + 1.0\right) + (\beta \cdot \alpha + \alpha)_*}{\left(\alpha + 2\right) + \beta}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
- Using strategy
rm Applied div-inv1.4
\[\leadsto \frac{\frac{1}{\left(\beta + 2\right) + \alpha} \cdot \color{blue}{\left(\left(\left(\beta + 1.0\right) + (\beta \cdot \alpha + \alpha)_*\right) \cdot \frac{1}{\left(\alpha + 2\right) + \beta}\right)}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied associate-*r*1.4
\[\leadsto \frac{\color{blue}{\left(\frac{1}{\left(\beta + 2\right) + \alpha} \cdot \left(\left(\beta + 1.0\right) + (\beta \cdot \alpha + \alpha)_*\right)\right) \cdot \frac{1}{\left(\alpha + 2\right) + \beta}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Initial program 16.7
\[\frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\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}\]
- Using strategy
rm Applied associate-+l+16.7
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\color{blue}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}}\]
- Using strategy
rm Applied add-sqr-sqrt16.7
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\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}}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied add-sqr-sqrt16.7
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\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}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied *-un-lft-identity16.7
\[\leadsto \frac{\frac{\frac{\color{blue}{1 \cdot \left(\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0\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}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied times-frac16.7
\[\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.0}{\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}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied times-frac16.7
\[\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.0}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Simplified16.7
\[\leadsto \frac{\color{blue}{\frac{1}{\left(\beta + 2\right) + \alpha}} \cdot \frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\sqrt{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Simplified16.7
\[\leadsto \frac{\frac{1}{\left(\beta + 2\right) + \alpha} \cdot \color{blue}{\frac{\left(\beta + 1.0\right) + (\beta \cdot \alpha + \alpha)_*}{\left(\alpha + 2\right) + \beta}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
- Using strategy
rm Applied div-inv16.7
\[\leadsto \frac{\frac{1}{\left(\beta + 2\right) + \alpha} \cdot \color{blue}{\left(\left(\left(\beta + 1.0\right) + (\beta \cdot \alpha + \alpha)_*\right) \cdot \frac{1}{\left(\alpha + 2\right) + \beta}\right)}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Applied associate-*r*16.7
\[\leadsto \frac{\color{blue}{\left(\frac{1}{\left(\beta + 2\right) + \alpha} \cdot \left(\left(\beta + 1.0\right) + (\beta \cdot \alpha + \alpha)_*\right)\right) \cdot \frac{1}{\left(\alpha + 2\right) + \beta}}}{\left(\alpha + \beta\right) + \left(2 \cdot 1 + 1.0\right)}\]
Taylor expanded around -inf 7.1
\[\leadsto \color{blue}{0}\]