Simplified2.8
\[\leadsto \color{blue}{e^{x \cdot x} \cdot \frac{\frac{1 + \frac{0.5}{x \cdot x}}{\left|x\right|} + {\left(\frac{1}{\left|x\right|}\right)}^{5} \cdot \left(0.75 + \frac{1.875}{x \cdot x}\right)}{\sqrt{\pi}}}
\]
Proof
(*.f64 (exp.f64 (*.f64 x x)) (/.f64 (+.f64 (/.f64 (+.f64 1 (/.f64 1/2 (*.f64 x x))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (/.f64 (+.f64 (/.f64 (+.f64 1 (/.f64 1/2 (*.f64 x x))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (/.f64 (Rewrite<= metadata-eval (*.f64 1/2 1)) (*.f64 x x))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (/.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 1 2)) 1) (*.f64 x x))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (/.f64 (*.f64 (/.f64 1 2) 1) (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x))))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 1 2) (/.f64 1 (*.f64 (fabs.f64 x) (fabs.f64 x)))))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (*.f64 (/.f64 1 2) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 1 (fabs.f64 x)) (fabs.f64 x))))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 40 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (*.f64 (/.f64 1 2) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 (fabs.f64 x)))) (fabs.f64 x)))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 38 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (*.f64 (/.f64 1 2) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 33 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 1 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 (/.f64 1 2) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) 1))) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (Rewrite=> distribute-rgt1-in_binary64 (*.f64 (+.f64 (*.f64 (/.f64 1 2) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) 1) 1)) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 2 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (Rewrite=> *-rgt-identity_binary64 (+.f64 (*.f64 (/.f64 1 2) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) 1)) (fabs.f64 x)) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (/.f64 (+.f64 (*.f64 (/.f64 1 2) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) 1) (Rewrite<= /-rgt-identity_binary64 (/.f64 (fabs.f64 x) 1))) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (*.f64 (/.f64 1 2) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) 1) 1) (fabs.f64 x))) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (+.f64 (*.f64 (/.f64 1 2) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) 1) (/.f64 1 (fabs.f64 x)))) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (*.f64 (/.f64 1 2) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) (/.f64 1 (fabs.f64 x))))) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))))) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 5) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) (Rewrite<= metadata-eval (+.f64 4 1))) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (Rewrite<= pow-plus_binary64 (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 4) (/.f64 1 (fabs.f64 x)))) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) (Rewrite<= metadata-eval (+.f64 3 1))) (/.f64 1 (fabs.f64 x))) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (Rewrite<= pow-plus_binary64 (*.f64 (pow.f64 (/.f64 1 (fabs.f64 x)) 3) (/.f64 1 (fabs.f64 x)))) (/.f64 1 (fabs.f64 x))) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (Rewrite=> unpow3_binary64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 3/4 (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (Rewrite<= metadata-eval (/.f64 3 4)) (/.f64 15/8 (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 29 points increase in error, 4 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (/.f64 3 4) (/.f64 (Rewrite<= metadata-eval (*.f64 1 15/8)) (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 1 points increase in error, 26 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (/.f64 3 4) (/.f64 (*.f64 1 (Rewrite<= metadata-eval (/.f64 15 8))) (*.f64 x x))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (/.f64 3 4) (/.f64 (*.f64 1 (/.f64 15 8)) (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x))))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (/.f64 3 4) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 15 8)))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (/.f64 3 4) (*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 1 (fabs.f64 x)) (fabs.f64 x))) (/.f64 15 8))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (/.f64 3 4) (*.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 (fabs.f64 x)))) (fabs.f64 x)) (/.f64 15 8))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (+.f64 (/.f64 3 4) (*.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) (/.f64 15 8))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 22 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 3 4)) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 15 8)))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 15 8))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (+.f64 (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x)))) (/.f64 15 8))))) (sqrt.f64 (PI.f64)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (+.f64 (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))) (/.f64 15 8)))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (+.f64 (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))) (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))))) (sqrt.f64 (PI.f64)))): 34 points increase in error, 7 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (/.f64 (+.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (Rewrite<= /-rgt-identity_binary64 (/.f64 (sqrt.f64 (PI.f64)) 1)))): 42 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) 1) (sqrt.f64 (PI.f64))))): 0 points increase in error, 42 points decrease in error
(*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (Rewrite<= associate-*r/_binary64 (*.f64 (+.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (/.f64 1 (sqrt.f64 (PI.f64)))))): 32 points increase in error, 1 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (+.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))))) (/.f64 1 (sqrt.f64 (PI.f64))))): 42 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 (sqrt.f64 (PI.f64))) (*.f64 (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (+.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x)))))))): 42 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 1 (sqrt.f64 (PI.f64))) (exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (+.f64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 (/.f64 1 2) (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 3 4) (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))) (*.f64 (/.f64 15 8) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (/.f64 1 (fabs.f64 x)) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))) (/.f64 1 (fabs.f64 x))))))): 0 points increase in error, 42 points decrease in error