Initial program 3.5
\[\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}
\]
Simplified2.1
\[\leadsto \color{blue}{\frac{\left(\alpha + 1\right) \cdot \frac{\beta + 1}{\left(\left(\alpha + \beta\right) + 2\right) \cdot \left(\left(\alpha + \beta\right) + 2\right)}}{\alpha + \left(\beta + 3\right)}}
\]
Applied *-un-lft-identity_binary642.1
\[\leadsto \frac{\left(\alpha + 1\right) \cdot \frac{\color{blue}{1 \cdot \left(\beta + 1\right)}}{\left(\left(\alpha + \beta\right) + 2\right) \cdot \left(\left(\alpha + \beta\right) + 2\right)}}{\alpha + \left(\beta + 3\right)}
\]
Applied times-frac_binary640.1
\[\leadsto \frac{\left(\alpha + 1\right) \cdot \color{blue}{\left(\frac{1}{\left(\alpha + \beta\right) + 2} \cdot \frac{\beta + 1}{\left(\alpha + \beta\right) + 2}\right)}}{\alpha + \left(\beta + 3\right)}
\]
Applied associate-*r*_binary640.1
\[\leadsto \frac{\color{blue}{\left(\left(\alpha + 1\right) \cdot \frac{1}{\left(\alpha + \beta\right) + 2}\right) \cdot \frac{\beta + 1}{\left(\alpha + \beta\right) + 2}}}{\alpha + \left(\beta + 3\right)}
\]
Simplified0.1
\[\leadsto \frac{\color{blue}{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}} \cdot \frac{\beta + 1}{\left(\alpha + \beta\right) + 2}}{\alpha + \left(\beta + 3\right)}
\]
Applied *-un-lft-identity_binary640.1
\[\leadsto \frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)} \cdot \frac{\beta + 1}{\color{blue}{1 \cdot \left(\left(\alpha + \beta\right) + 2\right)}}}{\alpha + \left(\beta + 3\right)}
\]
Applied add-sqr-sqrt_binary640.2
\[\leadsto \frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)} \cdot \frac{\color{blue}{\sqrt{\beta + 1} \cdot \sqrt{\beta + 1}}}{1 \cdot \left(\left(\alpha + \beta\right) + 2\right)}}{\alpha + \left(\beta + 3\right)}
\]
Applied times-frac_binary640.2
\[\leadsto \frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)} \cdot \color{blue}{\left(\frac{\sqrt{\beta + 1}}{1} \cdot \frac{\sqrt{\beta + 1}}{\left(\alpha + \beta\right) + 2}\right)}}{\alpha + \left(\beta + 3\right)}
\]
Simplified0.2
\[\leadsto \frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)} \cdot \left(\color{blue}{\sqrt{\beta + 1}} \cdot \frac{\sqrt{\beta + 1}}{\left(\alpha + \beta\right) + 2}\right)}{\alpha + \left(\beta + 3\right)}
\]
Simplified0.2
\[\leadsto \frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)} \cdot \left(\sqrt{\beta + 1} \cdot \color{blue}{\frac{\sqrt{\beta + 1}}{2 + \left(\beta + \alpha\right)}}\right)}{\alpha + \left(\beta + 3\right)}
\]
Applied add-sqr-sqrt_binary640.6
\[\leadsto \frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)} \cdot \left(\sqrt{\beta + 1} \cdot \frac{\sqrt{\beta + 1}}{2 + \left(\beta + \alpha\right)}\right)}{\color{blue}{\sqrt{\alpha + \left(\beta + 3\right)} \cdot \sqrt{\alpha + \left(\beta + 3\right)}}}
\]
Applied associate-/r*_binary640.6
\[\leadsto \color{blue}{\frac{\frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)} \cdot \left(\sqrt{\beta + 1} \cdot \frac{\sqrt{\beta + 1}}{2 + \left(\beta + \alpha\right)}\right)}{\sqrt{\alpha + \left(\beta + 3\right)}}}{\sqrt{\alpha + \left(\beta + 3\right)}}}
\]
Simplified0.6
\[\leadsto \frac{\color{blue}{\frac{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)} \cdot \frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\sqrt{\alpha + \left(\beta + 3\right)}}}}{\sqrt{\alpha + \left(\beta + 3\right)}}
\]
Applied *-un-lft-identity_binary640.6
\[\leadsto \frac{\frac{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)} \cdot \frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\sqrt{\alpha + \left(\beta + 3\right)}}}{\sqrt{\color{blue}{1 \cdot \left(\alpha + \left(\beta + 3\right)\right)}}}
\]
Applied sqrt-prod_binary640.6
\[\leadsto \frac{\frac{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)} \cdot \frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\sqrt{\alpha + \left(\beta + 3\right)}}}{\color{blue}{\sqrt{1} \cdot \sqrt{\alpha + \left(\beta + 3\right)}}}
\]
Applied *-un-lft-identity_binary640.6
\[\leadsto \frac{\frac{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)} \cdot \frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\sqrt{\color{blue}{1 \cdot \left(\alpha + \left(\beta + 3\right)\right)}}}}{\sqrt{1} \cdot \sqrt{\alpha + \left(\beta + 3\right)}}
\]
Applied sqrt-prod_binary640.6
\[\leadsto \frac{\frac{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)} \cdot \frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\color{blue}{\sqrt{1} \cdot \sqrt{\alpha + \left(\beta + 3\right)}}}}{\sqrt{1} \cdot \sqrt{\alpha + \left(\beta + 3\right)}}
\]
Applied times-frac_binary640.6
\[\leadsto \frac{\color{blue}{\frac{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)}}{\sqrt{1}} \cdot \frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\sqrt{\alpha + \left(\beta + 3\right)}}}}{\sqrt{1} \cdot \sqrt{\alpha + \left(\beta + 3\right)}}
\]
Applied times-frac_binary640.6
\[\leadsto \color{blue}{\frac{\frac{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)}}{\sqrt{1}}}{\sqrt{1}} \cdot \frac{\frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\sqrt{\alpha + \left(\beta + 3\right)}}}{\sqrt{\alpha + \left(\beta + 3\right)}}}
\]
Simplified0.6
\[\leadsto \color{blue}{\frac{1 + \beta}{2 + \left(\alpha + \beta\right)}} \cdot \frac{\frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\sqrt{\alpha + \left(\beta + 3\right)}}}{\sqrt{\alpha + \left(\beta + 3\right)}}
\]
Simplified0.1
\[\leadsto \frac{1 + \beta}{2 + \left(\alpha + \beta\right)} \cdot \color{blue}{\frac{\frac{1 + \alpha}{2 + \left(\alpha + \beta\right)}}{\alpha + \left(3 + \beta\right)}}
\]
Final simplification0.1
\[\leadsto \frac{1 + \beta}{2 + \left(\beta + \alpha\right)} \cdot \frac{\frac{1 + \alpha}{2 + \left(\beta + \alpha\right)}}{\alpha + \left(\beta + 3\right)}
\]