Simplified0.0
\[\leadsto \frac{\color{blue}{\frac{\left(\beta + \beta\right) + 2}{\alpha}}}{2}
\]
Proof
(/.f64 (+.f64 (+.f64 beta beta) 2) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (+.f64 beta (Rewrite<= *-lft-identity_binary64 (*.f64 1 beta))) 2) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (+.f64 beta (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) beta)) 2) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 beta (*.f64 -1 beta))) 2) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (-.f64 beta (*.f64 -1 beta)) (Rewrite<= metadata-eval (neg.f64 -2))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (-.f64 beta (*.f64 -1 beta)) (neg.f64 (Rewrite<= metadata-eval (*.f64 2 -1)))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (-.f64 beta (*.f64 -1 beta)) (*.f64 2 -1))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate--r+_binary64 (-.f64 beta (+.f64 (*.f64 -1 beta) (*.f64 2 -1)))) alpha): 1 points increase in error, 4 points decrease in error
(/.f64 (-.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 beta))) (+.f64 (*.f64 -1 beta) (*.f64 2 -1))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 beta))) (+.f64 (*.f64 -1 beta) (*.f64 2 -1))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (neg.f64 (*.f64 -1 beta)) (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 beta -1)) (*.f64 2 -1))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (neg.f64 (*.f64 -1 beta)) (Rewrite<= distribute-rgt-in_binary64 (*.f64 -1 (+.f64 beta 2)))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 (*.f64 -1 beta)) (neg.f64 (*.f64 -1 (+.f64 beta 2))))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 -1 beta) (*.f64 -1 (+.f64 beta 2))))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (+.f64 (*.f64 -1 beta) (Rewrite=> mul-1-neg_binary64 (neg.f64 (+.f64 beta 2))))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)))) alpha): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)))) alpha): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha))): 0 points increase in error, 0 points decrease in error