if (/ (- beta alpha) (+ (+ alpha beta) 2.0)) < -0.9999955f0

1. Started with
   \[\frac{\frac{\beta - \alpha}{\left(\alpha + \beta\right) + 2.0} + 1.0}{2.0}\]
   27.7
2. Using strategy rm
   27.7
3. 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}\]
   27.7
4. 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}\]
   24.0
5. Applied taylor to get
   \[\frac{\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \left(\frac{\alpha}{\left(\alpha + \beta\right) + 2.0} - 1.0\right)}{2.0} \leadsto \frac{\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \left(4.0 \cdot \frac{1}{{\alpha}^2} - \left(8.0 \cdot \frac{1}{{\alpha}^{3}} + 2.0 \cdot \frac{1}{\alpha}\right)\right)}{2.0}\]
   0.1
6. Taylor expanded around inf to get
   \[\frac{\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \color{red}{\left(4.0 \cdot \frac{1}{{\alpha}^2} - \left(8.0 \cdot \frac{1}{{\alpha}^{3}} + 2.0 \cdot \frac{1}{\alpha}\right)\right)}}{2.0} \leadsto \frac{\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \color{blue}{\left(4.0 \cdot \frac{1}{{\alpha}^2} - \left(8.0 \cdot \frac{1}{{\alpha}^{3}} + 2.0 \cdot \frac{1}{\alpha}\right)\right)}}{2.0}\]
   0.1
7. Applied simplify to get
   \[\frac{\frac{\beta}{\left(\alpha + \beta\right) + 2.0} - \left(4.0 \cdot \frac{1}{{\alpha}^2} - \left(8.0 \cdot \frac{1}{{\alpha}^{3}} + 2.0 \cdot \frac{1}{\alpha}\right)\right)}{2.0} \leadsto \left(\frac{\frac{\beta}{2.0}}{\left(\alpha + 2.0\right) + \beta} - \frac{\frac{4.0}{\alpha \cdot \alpha}}{2.0}\right) + \frac{\frac{2.0}{\alpha} + \frac{8.0}{{\alpha}^3}}{2.0}\]
   0.1

---

8. Applied final simplification

if -0.9999955f0 < (/ (- beta alpha) (+ (+ alpha beta) 2.0))

1. Started with
   \[\frac{\frac{\beta - \alpha}{\left(\alpha + \beta\right) + 2.0} + 1.0}{2.0}\]
   0.5
2. Using strategy rm
   0.5
3. 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}\]
   0.5
4. 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}\]
   0.2
5. Applied taylor to get
   \[\frac{\frac{\beta - \alpha}{(1 * \left(\alpha + \beta\right) + 2.0)_*} + 1.0}{2.0} \leadsto \frac{\left(\frac{\beta}{(1 * \left(\beta + \alpha\right) + 2.0)_*} + 1.0\right) - \frac{\alpha}{(1 * \left(\beta + \alpha\right) + 2.0)_*}}{2.0}\]
   0.2
6. Taylor expanded around 0 to get
   \[\frac{\color{red}{\left(\frac{\beta}{(1 * \left(\beta + \alpha\right) + 2.0)_*} + 1.0\right) - \frac{\alpha}{(1 * \left(\beta + \alpha\right) + 2.0)_*}}}{2.0} \leadsto \frac{\color{blue}{\left(\frac{\beta}{(1 * \left(\beta + \alpha\right) + 2.0)_*} + 1.0\right) - \frac{\alpha}{(1 * \left(\beta + \alpha\right) + 2.0)_*}}}{2.0}\]
   0.2
7. Using strategy rm
   0.2
8. Applied log1p-expm1-u to get
   \[\frac{\color{red}{\left(\frac{\beta}{(1 * \left(\beta + \alpha\right) + 2.0)_*} + 1.0\right)} - \frac{\alpha}{(1 * \left(\beta + \alpha\right) + 2.0)_*}}{2.0} \leadsto \frac{\color{blue}{\log_* (1 + (e^{\frac{\beta}{(1 * \left(\beta + \alpha\right) + 2.0)_*} + 1.0} - 1)^*)} - \frac{\alpha}{(1 * \left(\beta + \alpha\right) + 2.0)_*}}{2.0}\]
   0.3