Simplified54.9
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(\alpha + \beta, \frac{\frac{\beta - \alpha}{\alpha + \mathsf{fma}\left(2, i, \beta\right)}}{\alpha + \mathsf{fma}\left(2, i, \beta + 2\right)}, 1\right)}{2}}
\]
Proof
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 alpha (fma.f64 2 i beta))) (+.f64 alpha (fma.f64 2 i (+.f64 beta 2)))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 alpha (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 i) beta)))) (+.f64 alpha (fma.f64 2 i (+.f64 beta 2)))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 alpha (Rewrite<= +-commutative_binary64 (+.f64 beta (*.f64 2 i))))) (+.f64 alpha (fma.f64 2 i (+.f64 beta 2)))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (+.f64 alpha (fma.f64 2 i (+.f64 beta 2)))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 alpha (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 i) (+.f64 beta 2))))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 alpha (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 2 i) beta) 2)))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 alpha (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 beta (*.f64 2 i))) 2))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha (+.f64 beta (*.f64 2 i))) 2))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (/.f64 (-.f64 beta alpha) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 2)) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (Rewrite=> associate-/l/_binary64 (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i))))) 1) 2): 51 points increase in error, 22 points decrease in error
(/.f64 (fma.f64 (+.f64 alpha beta) (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (Rewrite<= metadata-eval (neg.f64 -1))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (+.f64 alpha beta) (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i))))) -1)) 2): 8 points increase in error, 14 points decrease in error
(/.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (+.f64 alpha beta))) -1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> fma-neg_binary64 (fma.f64 (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (+.f64 alpha beta) (neg.f64 -1))) 2): 14 points increase in error, 8 points decrease in error
(/.f64 (fma.f64 (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (+.f64 alpha beta) (Rewrite=> metadata-eval 1)) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (+.f64 alpha beta)) 1)) 2): 8 points increase in error, 14 points decrease in error
(/.f64 (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 alpha beta) (/.f64 (-.f64 beta alpha) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))))) 1) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (+.f64 alpha beta) (-.f64 beta alpha)) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2) (+.f64 (+.f64 alpha beta) (*.f64 2 i))))) 1) 2): 82 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (*.f64 (+.f64 alpha beta) (-.f64 beta alpha)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) 2))) 1) 2): 3 points increase in error, 2 points decrease in error