\(\frac{\frac{\frac{1}{\left(\alpha + \beta\right) + 2.0}}{\frac{1}{\beta}} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0}\)
- Started with
\[\frac{\frac{\beta - \alpha}{\left(\alpha + \beta\right) + 2.0} + 1.0}{2.0}\]
15.8
- Using strategy
rm 15.8
- Applied div-sub to get
\[\frac{\color{red}{\frac{\beta - \alpha}{\left(\alpha + \beta\right) + 2.0}} + 1.0}{2.0} \leadsto \frac{\color{blue}{\left(\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \frac{\alpha}{\left(\alpha + \beta\right) + 2.0}\right)} + 1.0}{2.0}\]
15.7
- Applied associate-+l- to get
\[\frac{\color{red}{\left(\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \frac{\alpha}{\left(\alpha + \beta\right) + 2.0}\right) + 1.0}}{2.0} \leadsto \frac{\color{blue}{\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}}{2.0}\]
15.3
- Using strategy
rm 15.3
- Applied clear-num to get
\[\frac{\color{red}{\frac{\beta}{\left(\alpha + \beta\right) + 2.0}} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0} \leadsto \frac{\color{blue}{\frac{1}{\frac{\left(\alpha + \beta\right) + 2.0}{\beta}}} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0}\]
15.3
- Using strategy
rm 15.3
- Applied div-inv to get
\[\frac{\frac{1}{\color{red}{\frac{\left(\alpha + \beta\right) + 2.0}{\beta}}} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0} \leadsto \frac{\frac{1}{\color{blue}{\left(\left(\alpha + \beta\right) + 2.0\right) \cdot \frac{1}{\beta}}} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0}\]
15.3
- Applied associate-/r* to get
\[\frac{\color{red}{\frac{1}{\left(\left(\alpha + \beta\right) + 2.0\right) \cdot \frac{1}{\beta}}} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0} \leadsto \frac{\color{blue}{\frac{\frac{1}{\left(\alpha + \beta\right) + 2.0}}{\frac{1}{\beta}}} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0}\]
15.3