Simplified5.0
\[\leadsto \color{blue}{\frac{-\left(0.0625 \cdot \left(\beta \cdot \left(-\alpha\right) - {\left(\beta + \alpha\right)}^{2}\right) - \mathsf{fma}\left(-2, \left(\beta + \alpha\right) \cdot \mathsf{fma}\left(0.0625, 2 \cdot \left(\beta + \alpha\right), \left(\beta + \alpha\right) \cdot -0.125\right), \mathsf{fma}\left(4, {\left(\beta + \alpha\right)}^{2} + -1, {\left(\beta + \alpha\right)}^{2} \cdot 20\right) \cdot -0.00390625\right)\right)}{i \cdot i} + \left(0.0625 + \mathsf{fma}\left(0.0625, \frac{2 \cdot \left(\beta + \alpha\right)}{i}, \frac{\beta + \alpha}{i} \cdot -0.125\right)\right)}
\]
Proof
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (-.f64 (*.f64 beta (neg.f64 alpha)) (pow.f64 (+.f64 beta alpha) 2))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (*.f64 2 (+.f64 beta alpha)) (*.f64 (+.f64 beta alpha) -1/8))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (-.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 beta alpha))) (pow.f64 (+.f64 beta alpha) 2))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (*.f64 2 (+.f64 beta alpha)) (*.f64 (+.f64 beta alpha) -1/8))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (-.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 beta alpha))) (pow.f64 (+.f64 beta alpha) 2))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (*.f64 2 (+.f64 beta alpha)) (*.f64 (+.f64 beta alpha) -1/8))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (neg.f64 (pow.f64 (+.f64 beta alpha) 2))))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (*.f64 2 (+.f64 beta alpha)) (*.f64 (+.f64 beta alpha) -1/8))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2))))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (*.f64 2 (+.f64 beta alpha)) (*.f64 (+.f64 beta alpha) -1/8))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 (+.f64 beta alpha) -1/8))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) (*.f64 (+.f64 beta alpha) (Rewrite<= metadata-eval (neg.f64 1/8))))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (+.f64 beta alpha) 1/8))))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/8 (+.f64 beta alpha)))))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (fma.f64 1/16 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (neg.f64 (*.f64 1/8 (+.f64 beta alpha))))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (+.f64 beta alpha) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (Rewrite<= metadata-eval (neg.f64 1))) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 (fma.f64 4 (Rewrite<= sub-neg_binary64 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 (fma.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) (Rewrite<= metadata-eval (+.f64 16 4)))) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 (fma.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2))))) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2))))) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2))) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)))) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2))))) -1/256)))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (Rewrite<= *-commutative_binary64 (*.f64 -1/256 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2))))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (neg.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2))))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2))))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (Rewrite=> fma-def_binary64 (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 -1/256 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2))))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 (*.f64 2 alpha) (*.f64 2 beta)) 1/16)) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 -1/256 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) 1/16) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 -1/256 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 -1/256 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 -1/256 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))) (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 3 points increase in error, 5 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (fma.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (*.f64 -1/256 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))))) (*.f64 i i)) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)))))))) (Rewrite<= unpow2_binary64 (pow.f64 i 2))) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2)))) (+.f64 1/16 (fma.f64 1/16 (/.f64 (*.f64 2 (+.f64 beta alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (+.f64 1/16 (fma.f64 1/16 (/.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) i) (*.f64 (/.f64 (+.f64 beta alpha) i) -1/8)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (+.f64 1/16 (fma.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i) (*.f64 (/.f64 (+.f64 beta alpha) i) (Rewrite<= metadata-eval (neg.f64 1/8)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (+.f64 1/16 (fma.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 (+.f64 beta alpha) i) 1/8)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (+.f64 1/16 (fma.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/8 (/.f64 (+.f64 beta alpha) i))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (+.f64 1/16 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)) (*.f64 1/8 (/.f64 (+.f64 beta alpha) i)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (+.f64 1/16 (-.f64 (*.f64 1/16 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) i)) (*.f64 1/8 (/.f64 (+.f64 beta alpha) i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 1/16 (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 alpha) (*.f64 2 beta)) i))) (*.f64 1/8 (/.f64 (+.f64 beta alpha) i))))): 1 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 -1 (*.f64 beta alpha)) (*.f64 -1 (pow.f64 (+.f64 beta alpha) 2)))) (+.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha))) (*.f64 -1/256 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (+.f64 (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1))))))) (pow.f64 i 2))) (+.f64 1/16 (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 alpha) (*.f64 2 beta)) i)))) (*.f64 1/8 (/.f64 (+.f64 beta alpha) i)))): 3 points increase in error, 0 points decrease in error