Simplified0.9
\[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{\left(-2 - \beta\right) - \beta}{\alpha}, \frac{2 + \beta}{\alpha}, \frac{\left(\beta + \beta\right) + 2}{\alpha}\right)}}{2}
\]
Proof
(fma.f64 (/.f64 (-.f64 (-.f64 -2 beta) beta) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (-.f64 (Rewrite<= metadata-eval (neg.f64 2)) beta) beta) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 2) (neg.f64 beta))) beta) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 2 beta))) beta) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 beta 2))) beta) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 beta 2))) beta) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (+.f64 beta 2)) (neg.f64 beta))) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (+.f64 (*.f64 -1 (+.f64 beta 2)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 beta))) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 beta) (*.f64 -1 (+.f64 beta 2)))) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (+.f64 (*.f64 -1 beta) (Rewrite=> mul-1-neg_binary64 (neg.f64 (+.f64 beta 2)))) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2))) alpha) (/.f64 (+.f64 2 beta) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 beta 2)) alpha) (/.f64 (+.f64 (+.f64 beta beta) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (+.f64 (+.f64 beta (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 beta)))) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (+.f64 (+.f64 beta (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 beta)))) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (+.f64 (Rewrite<= sub-neg_binary64 (-.f64 beta (*.f64 -1 beta))) 2) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (+.f64 (-.f64 beta (*.f64 -1 beta)) (Rewrite<= metadata-eval (neg.f64 -2))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (+.f64 (-.f64 beta (*.f64 -1 beta)) (neg.f64 (Rewrite<= metadata-eval (neg.f64 2)))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (-.f64 beta (*.f64 -1 beta)) (neg.f64 2))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (Rewrite<= associate--r+_binary64 (-.f64 beta (+.f64 (*.f64 -1 beta) (neg.f64 2)))) alpha)): 1 points increase in error, 2 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (-.f64 beta (+.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 beta)) (neg.f64 2))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (-.f64 beta (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 beta 2)))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (-.f64 beta (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 beta 2)))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (-.f64 beta (*.f64 -1 (+.f64 beta 2)))))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (neg.f64 (neg.f64 (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 beta (*.f64 (neg.f64 -1) (+.f64 beta 2)))))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (neg.f64 (neg.f64 (+.f64 beta (*.f64 (Rewrite=> metadata-eval 1) (+.f64 beta 2))))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (neg.f64 (neg.f64 (+.f64 beta (Rewrite=> *-lft-identity_binary64 (+.f64 beta 2))))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (neg.f64 (Rewrite<= distribute-neg-out_binary64 (+.f64 (neg.f64 beta) (neg.f64 (+.f64 beta 2))))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.f64 (neg.f64 (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 beta)) (neg.f64 (+.f64 beta 2)))) alpha)): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (/.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
(fma.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha) (/.f64 (+.f64 beta 2) alpha)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha))): 3 points increase in error, 1 points decrease in error
(-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) (+.f64 beta 2)) (*.f64 alpha alpha))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 37 points increase in error, 22 points decrease in error
(-.f64 (/.f64 (*.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) (+.f64 beta 2)) (Rewrite<= unpow2_binary64 (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 -1 beta) (neg.f64 (+.f64 beta 2)))) (+.f64 beta 2)) (pow.f64 alpha 2)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 (+.f64 (*.f64 -1 beta) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 beta 2)))) (+.f64 beta 2)) (pow.f64 alpha 2)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 (Rewrite=> distribute-lft-out_binary64 (*.f64 -1 (+.f64 beta (+.f64 beta 2)))) (+.f64 beta 2)) (pow.f64 alpha 2)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 (*.f64 -1 (+.f64 beta (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 beta 2))))) (+.f64 beta 2)) (pow.f64 alpha 2)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 (*.f64 -1 (+.f64 beta (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) (+.f64 beta 2)))) (+.f64 beta 2)) (pow.f64 alpha 2)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 (*.f64 -1 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 beta (*.f64 -1 (+.f64 beta 2))))) (+.f64 beta 2)) (pow.f64 alpha 2)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (-.f64 beta (*.f64 -1 (+.f64 beta 2))) (+.f64 beta 2)))) (pow.f64 alpha 2)) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 beta (*.f64 -1 (+.f64 beta 2))) (+.f64 beta 2)) (pow.f64 alpha 2)))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 beta 2) (-.f64 beta (*.f64 -1 (+.f64 beta 2))))) (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1 (/.f64 (*.f64 (+.f64 beta 2) (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 beta (*.f64 (neg.f64 -1) (+.f64 beta 2))))) (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1 (/.f64 (*.f64 (+.f64 beta 2) (+.f64 beta (*.f64 (Rewrite=> metadata-eval 1) (+.f64 beta 2)))) (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1 (/.f64 (*.f64 (+.f64 beta 2) (+.f64 beta (Rewrite=> *-lft-identity_binary64 (+.f64 beta 2)))) (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1 (/.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 beta (+.f64 beta 2)) (*.f64 (+.f64 beta 2) (+.f64 beta 2)))) (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 1 points decrease in error
(-.f64 (*.f64 -1 (/.f64 (+.f64 (*.f64 beta (+.f64 beta 2)) (Rewrite<= unpow2_binary64 (pow.f64 (+.f64 beta 2) 2))) (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (+.f64 beta 2) 2) (*.f64 beta (+.f64 beta 2)))) (pow.f64 alpha 2))) (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (/.f64 (+.f64 (pow.f64 (+.f64 beta 2) 2) (*.f64 beta (+.f64 beta 2))) (pow.f64 alpha 2))) (neg.f64 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (+.f64 (pow.f64 (+.f64 beta 2) 2) (*.f64 beta (+.f64 beta 2))) (pow.f64 alpha 2))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 beta) (+.f64 beta 2)) alpha)) (*.f64 -1 (/.f64 (+.f64 (pow.f64 (+.f64 beta 2) 2) (*.f64 beta (+.f64 beta 2))) (pow.f64 alpha 2))))): 0 points increase in error, 0 points decrease in error