Simplified0.4
\[\leadsto \frac{\frac{\beta}{\beta + \left(\alpha + 2\right)} - \color{blue}{\left(\frac{\beta + 2}{\alpha} \cdot \left(-1 + \frac{\beta + 2}{\alpha}\right) - {\left(\frac{\beta + 2}{\alpha}\right)}^{3}\right)}}{2}
\]
Proof
(-.f64 (*.f64 (/.f64 (+.f64 beta 2) alpha) (+.f64 -1 (/.f64 (+.f64 beta 2) alpha))) (pow.f64 (/.f64 (+.f64 beta 2) alpha) 3)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (*.f64 (/.f64 (+.f64 beta 2) alpha) (/.f64 (+.f64 beta 2) alpha)))) (pow.f64 (/.f64 (+.f64 beta 2) alpha) 3)): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 beta 2) (+.f64 beta 2)) (*.f64 alpha alpha)))) (pow.f64 (/.f64 (+.f64 beta 2) alpha) 3)): 7 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 (+.f64 beta 2) 2)) (*.f64 alpha alpha))) (pow.f64 (/.f64 (+.f64 beta 2) alpha) 3)): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (Rewrite<= unpow2_binary64 (pow.f64 alpha 2)))) (pow.f64 (/.f64 (+.f64 beta 2) alpha) 3)): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (Rewrite<= cube-unmult_binary64 (*.f64 (/.f64 (+.f64 beta 2) alpha) (*.f64 (/.f64 (+.f64 beta 2) alpha) (/.f64 (+.f64 beta 2) alpha))))): 3 points increase in error, 6 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (*.f64 (/.f64 (+.f64 beta 2) alpha) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 beta 2) (+.f64 beta 2)) (*.f64 alpha alpha))))): 9 points increase in error, 11 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (*.f64 (/.f64 (+.f64 beta 2) alpha) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 (+.f64 beta 2) 2)) (*.f64 alpha alpha)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (*.f64 (/.f64 (+.f64 beta 2) alpha) (/.f64 (pow.f64 (+.f64 beta 2) 2) (Rewrite<= unpow2_binary64 (pow.f64 alpha 2))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 beta 2) (pow.f64 (+.f64 beta 2) 2)) (*.f64 alpha (pow.f64 alpha 2))))): 12 points increase in error, 17 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (/.f64 (*.f64 (+.f64 beta 2) (Rewrite=> unpow2_binary64 (*.f64 (+.f64 beta 2) (+.f64 beta 2)))) (*.f64 alpha (pow.f64 alpha 2)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (/.f64 (Rewrite<= cube-mult_binary64 (pow.f64 (+.f64 beta 2) 3)) (*.f64 alpha (pow.f64 alpha 2)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (/.f64 (pow.f64 (+.f64 beta 2) 3) (*.f64 alpha (Rewrite=> unpow2_binary64 (*.f64 alpha alpha))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (/.f64 (pow.f64 (+.f64 beta 2) 3) (Rewrite<= cube-mult_binary64 (pow.f64 alpha 3)))): 6 points increase in error, 4 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (neg.f64 (/.f64 (pow.f64 (+.f64 beta 2) 3) (pow.f64 alpha 3))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (pow.f64 (+.f64 beta 2) 3) (pow.f64 alpha 3))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1 (/.f64 (+.f64 beta 2) alpha)) (+.f64 (/.f64 (pow.f64 (+.f64 beta 2) 2) (pow.f64 alpha 2)) (*.f64 -1 (/.f64 (pow.f64 (+.f64 beta 2) 3) (pow.f64 alpha 3)))))): 1 points increase in error, 0 points decrease in error