Initial program 2.8
\[\left(\frac{1}{\sqrt{\pi}} \cdot e^{\left|x\right| \cdot \left|x\right|}\right) \cdot \left(\left(\left(\frac{1}{\left|x\right|} + \frac{1}{2} \cdot \left(\left(\frac{1}{\left|x\right|} \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right)\right) + \frac{3}{4} \cdot \left(\left(\left(\left(\frac{1}{\left|x\right|} \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right)\right) + \frac{15}{8} \cdot \left(\left(\left(\left(\left(\left(\frac{1}{\left|x\right|} \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right) \cdot \frac{1}{\left|x\right|}\right)\right)
\]
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)))): 0 points increase in error, 40 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)))): 27 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 (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)))): 23 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 (/.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)))): 0 points increase in error, 27 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)))): 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 (/.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)))): 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) (/.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, 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)) (/.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)))): 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<= *-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, 42 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)))): 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)) (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)))): 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 (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)))): 0 points increase in error, 19 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)))): 0 points increase in error, 28 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)))): 1 points increase in error, 40 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)))): 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 (Rewrite<= metadata-eval (*.f64 1 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 (Rewrite<= metadata-eval (/.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 (/.f64 3 4) (/.f64 (*.f64 1 (/.f64 15 8)) (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 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) (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)))): 1 points increase in error, 9 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)))): 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))))) (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)))): 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)))) (*.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)))): 39 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)))) (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)))): 42 points increase in error, 0 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)))): 42 points increase in error, 0 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)))): 0 points increase in error, 42 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)))))): 0 points increase in error, 42 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))))): 1 points increase in error, 38 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
Taylor expanded in x around inf 2.8
\[\leadsto \color{blue}{e^{{x}^{2}}} \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}}
\]
Simplified1.3
\[\leadsto \color{blue}{{\left(e^{x}\right)}^{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 (pow.f64 (exp.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 (Rewrite<= exp-prod_binary64 (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)))): 1 points increase in error, 2 points decrease in error
(*.f64 (exp.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2))) (/.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, 1 points decrease in error
Taylor expanded in x around 0 1.2
\[\leadsto {\left(e^{x}\right)}^{x} \cdot \color{blue}{\left(\left(\frac{1}{\left|x\right|} + 0.75 \cdot \frac{1}{{\left(\left|x\right|\right)}^{5}}\right) \cdot \sqrt{\frac{1}{\pi}} + \frac{0.5 \cdot \frac{1}{\left|x\right|} + 1.875 \cdot \frac{1}{{\left(\left|x\right|\right)}^{5}}}{{x}^{2}} \cdot \sqrt{\frac{1}{\pi}}\right)}
\]
Simplified1.2
\[\leadsto {\left(e^{x}\right)}^{x} \cdot \color{blue}{\left(\sqrt{\frac{1}{\pi}} \cdot \left(\frac{\frac{0.5}{x} + \frac{1.875}{{x}^{5}}}{x \cdot x} + \left(\frac{0.75}{{x}^{5}} + \frac{1}{x}\right)\right)\right)}
\]
Proof
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (/.f64 1/2 x) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1/2 1)) x) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (/.f64 (*.f64 1/2 1) (Rewrite<= unpow1_binary64 (pow.f64 x 1))) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (/.f64 (*.f64 1/2 1) (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2))))) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 30 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (/.f64 (*.f64 1/2 1) (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2)))))) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 30 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (/.f64 (*.f64 1/2 1) (fabs.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 x 1)))) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (/.f64 (*.f64 1/2 1) (fabs.f64 (Rewrite=> unpow1_binary64 x))) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 1/2 (/.f64 1 (fabs.f64 x)))) (/.f64 15/8 (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 1 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (/.f64 (Rewrite<= metadata-eval (*.f64 15/8 1)) (pow.f64 x 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (/.f64 (*.f64 15/8 1) (pow.f64 (Rewrite<= unpow1_binary64 (pow.f64 x 1)) 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (/.f64 (*.f64 15/8 1) (pow.f64 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2)))) 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 29 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (/.f64 (*.f64 15/8 1) (pow.f64 (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2))))) 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 25 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (/.f64 (*.f64 15/8 1) (pow.f64 (fabs.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 x 1))) 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (/.f64 (*.f64 15/8 1) (pow.f64 (fabs.f64 (Rewrite=> unpow1_binary64 x)) 5))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (Rewrite<= associate-*r/_binary64 (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5))))) (*.f64 x x)) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 3 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (Rewrite<= unpow2_binary64 (pow.f64 x 2))) (+.f64 (/.f64 3/4 (pow.f64 x 5)) (/.f64 1 x))))): 0 points increase in error, 30 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 3/4 1)) (pow.f64 x 5)) (/.f64 1 x))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (/.f64 (*.f64 3/4 1) (pow.f64 (Rewrite<= unpow1_binary64 (pow.f64 x 1)) 5)) (/.f64 1 x))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (/.f64 (*.f64 3/4 1) (pow.f64 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2)))) 5)) (/.f64 1 x))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (/.f64 (*.f64 3/4 1) (pow.f64 (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2))))) 5)) (/.f64 1 x))))): 5 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (/.f64 (*.f64 3/4 1) (pow.f64 (fabs.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 x 1))) 5)) (/.f64 1 x))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (/.f64 (*.f64 3/4 1) (pow.f64 (fabs.f64 (Rewrite=> unpow1_binary64 x)) 5)) (/.f64 1 x))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (/.f64 1 x))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5))) (/.f64 1 (Rewrite<= unpow1_binary64 (pow.f64 x 1))))))): 0 points increase in error, 30 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5))) (/.f64 1 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2))))))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5))) (/.f64 1 (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (pow.f64 x (/.f64 1 2)) (pow.f64 x (/.f64 1 2)))))))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5))) (/.f64 1 (fabs.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 x 1)))))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (+.f64 (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5))) (/.f64 1 (fabs.f64 (Rewrite=> unpow1_binary64 x))))))): 29 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (+.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))))))): 0 points increase in error, 31 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (*.f64 (sqrt.f64 (/.f64 1 (PI.f64))) (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)))))): 31 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) x) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (+.f64 (/.f64 1 (fabs.f64 x)) (*.f64 3/4 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (sqrt.f64 (/.f64 1 (PI.f64)))) (*.f64 (/.f64 (+.f64 (*.f64 1/2 (/.f64 1 (fabs.f64 x))) (*.f64 15/8 (/.f64 1 (pow.f64 (fabs.f64 x) 5)))) (pow.f64 x 2)) (sqrt.f64 (/.f64 1 (PI.f64))))))): 0 points increase in error, 31 points decrease in error
Final simplification1.2
\[\leadsto {\left(e^{x}\right)}^{x} \cdot \left(\sqrt{\frac{1}{\pi}} \cdot \left(\frac{\frac{0.5}{x} + \frac{1.875}{{x}^{5}}}{x \cdot x} + \left(\frac{0.75}{{x}^{5}} + \frac{1}{x}\right)\right)\right)
\]