\(\frac{\frac{\beta}{(1 * \left(\alpha + \beta\right) + 2.0)_*} - \left(\alpha \cdot \frac{1}{(1 * \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}\]
6.9
- Using strategy
rm 6.9
- Applied *-un-lft-identity to get
\[\frac{\frac{\beta - \alpha}{\color{red}{\left(\alpha + \beta\right)} + 2.0} + 1.0}{2.0} \leadsto \frac{\frac{\beta - \alpha}{\color{blue}{1 \cdot \left(\alpha + \beta\right)} + 2.0} + 1.0}{2.0}\]
6.9
- Applied fma-def to get
\[\frac{\frac{\beta - \alpha}{\color{red}{1 \cdot \left(\alpha + \beta\right) + 2.0}} + 1.0}{2.0} \leadsto \frac{\frac{\beta - \alpha}{\color{blue}{(1 * \left(\alpha + \beta\right) + 2.0)_*}} + 1.0}{2.0}\]
6.6
- Using strategy
rm 6.6
- Applied div-sub to get
\[\frac{\color{red}{\frac{\beta - \alpha}{(1 * \left(\alpha + \beta\right) + 2.0)_*}} + 1.0}{2.0} \leadsto \frac{\color{blue}{\left(\frac{\beta}{(1 * \left(\alpha + \beta\right) + 2.0)_*} - \frac{\alpha}{(1 * \left(\alpha + \beta\right) + 2.0)_*}\right)} + 1.0}{2.0}\]
6.4
- Applied associate-+l- to get
\[\frac{\color{red}{\left(\frac{\beta}{(1 * \left(\alpha + \beta\right) + 2.0)_*} - \frac{\alpha}{(1 * \left(\alpha + \beta\right) + 2.0)_*}\right) + 1.0}}{2.0} \leadsto \frac{\color{blue}{\frac{\beta}{(1 * \left(\alpha + \beta\right) + 2.0)_*} - \left(\frac{\alpha}{(1 * \left(\alpha + \beta\right) + 2.0)_*} - 1.0\right)}}{2.0}\]
6.3
- Using strategy
rm 6.3
- Applied div-inv to get
\[\frac{\frac{\beta}{(1 * \left(\alpha + \beta\right) + 2.0)_*} - \left(\color{red}{\frac{\alpha}{(1 * \left(\alpha + \beta\right) + 2.0)_*}} - 1.0\right)}{2.0} \leadsto \frac{\frac{\beta}{(1 * \left(\alpha + \beta\right) + 2.0)_*} - \left(\color{blue}{\alpha \cdot \frac{1}{(1 * \left(\alpha + \beta\right) + 2.0)_*}} - 1.0\right)}{2.0}\]
6.3