Simplified31.7
\[\leadsto \color{blue}{\frac{i}{\mathsf{fma}\left(\beta + \mathsf{fma}\left(i, 2, \alpha\right), \beta + \mathsf{fma}\left(i, 2, \alpha\right), -1\right)} \cdot \frac{\mathsf{fma}\left(i, i + \left(\alpha + \beta\right), \alpha \cdot \beta\right)}{\frac{\left(\beta + \mathsf{fma}\left(i, 2, \alpha\right)\right) \cdot \left(\beta + \mathsf{fma}\left(i, 2, \alpha\right)\right)}{i + \left(\alpha + \beta\right)}}}
\]
Proof
(*.f64 (/.f64 i (fma.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha))) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i)))) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha))) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i)))) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= metadata-eval (neg.f64 1)))) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1))) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (fma.f64 i (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (fma.f64 i (+.f64 (+.f64 alpha beta) i) (Rewrite<= *-commutative_binary64 (*.f64 beta alpha))) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (*.f64 beta alpha))) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha))) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i)))) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha)))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i))))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (+.f64 (+.f64 alpha beta) i)) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))))): 48 points increase in error, 2 points decrease in error
(*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (+.f64 alpha beta) i) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 i (*.f64 (+.f64 (+.f64 alpha beta) i) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))))): 30 points increase in error, 8 points decrease in error
(/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))))): 0 points increase in error, 8 points decrease in error
(Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1))): 4 points increase in error, 12 points decrease in error