Simplified27.1
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{{\left(e^{x}\right)}^{\left(-x\right)}}{\mathsf{fma}\left(0.3275911, \left|x\right|, 1\right)}, -0.254829592 + \frac{0.284496736 - \frac{1.421413741 + \frac{-1.453152027 + \frac{1.061405429}{\mathsf{fma}\left(0.3275911, \left|x\right|, 1\right)}}{\mathsf{fma}\left(0.3275911, \left|x\right|, 1\right)}}{\mathsf{fma}\left(0.3275911, \left|x\right|, 1\right)}}{\mathsf{fma}\left(0.3275911, \left|x\right|, 1\right)}, 1\right)}
\]
Proof
(fma.f64 (/.f64 (pow.f64 (exp.f64 x) (neg.f64 x)) (fma.f64 3275911/10000000 (fabs.f64 x) 1)) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (pow.f64 (exp.f64 x) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))) (fma.f64 3275911/10000000 (fabs.f64 x) 1)) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 x (*.f64 -1 x)))) (fma.f64 3275911/10000000 (fabs.f64 x) 1)) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 x (Rewrite=> mul-1-neg_binary64 (neg.f64 x)))) (fma.f64 3275911/10000000 (fabs.f64 x) 1)) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 x x)))) (fma.f64 3275911/10000000 (fabs.f64 x) 1)) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (neg.f64 (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1)) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 3275911/10000000 (fabs.f64 x)) 1))) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (/.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (Rewrite<= /-rgt-identity_binary64 (/.f64 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))) 1))) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) 1) (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))))) (+.f64 -31853699/125000000 (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (Rewrite<= metadata-eval (neg.f64 31853699/125000000)) (/.f64 (-.f64 8890523/31250000 (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (Rewrite<= metadata-eval (-.f64 0 -8890523/31250000)) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 1061405429/1000000000 (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 (Rewrite<= metadata-eval (*.f64 1 1061405429/1000000000)) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 (*.f64 1 1061405429/1000000000) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 3275911/10000000 (fabs.f64 x)) 1)))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (/.f64 (*.f64 1 1061405429/1000000000) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (+.f64 -1453152027/1000000000 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (*.f64 1 (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 3275911/10000000 (fabs.f64 x)) 1)))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (/.f64 (*.f64 1 (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (+.f64 1421413741/1000000000 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (*.f64 1 (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 3275911/10000000 (fabs.f64 x)) 1)))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (/.f64 (*.f64 1 (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))))) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (-.f64 (-.f64 0 -8890523/31250000) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (Rewrite<= associate--r+_binary64 (-.f64 0 (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))) (fma.f64 3275911/10000000 (fabs.f64 x) 1))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (neg.f64 (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))))))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 3275911/10000000 (fabs.f64 x)) 1)))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (/.f64 (neg.f64 (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))))))) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))))) 1): 39 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))) (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (neg.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))) (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))))) 1): 0 points increase in error, 39 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (+.f64 (neg.f64 31853699/125000000) (neg.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 31853699/125000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))))) 1): 39 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x))))) (neg.f64 (+.f64 31853699/125000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))))) 1)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (neg.f64 (+.f64 31853699/125000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))))))) 1): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 31853699/125000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))))))) 1): 0 points increase in error, 39 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 31853699/125000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))))) (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))))) 1): 39 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 (neg.f64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 31853699/125000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000)))))))))) (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 1 (*.f64 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 31853699/125000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -8890523/31250000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 1421413741/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) (+.f64 -1453152027/1000000000 (*.f64 (/.f64 1 (+.f64 1 (*.f64 3275911/10000000 (fabs.f64 x)))) 1061405429/1000000000))))))))) (exp.f64 (neg.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))))))): 0 points increase in error, 39 points decrease in error