Simplified0.5
\[\leadsto \color{blue}{\left|\frac{\left|x\right| \cdot \left(\mathsf{fma}\left(0.6666666666666666, x \cdot x, 2\right) + \mathsf{fma}\left(0.2, {\left(\left|x\right|\right)}^{4}, 0.047619047619047616 \cdot {\left(\left|x\right|\right)}^{6}\right)\right)}{\sqrt{\pi}}\right|}
\]
Proof
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (fma.f64 2/3 (*.f64 x x) 2) (fma.f64 1/5 (pow.f64 (fabs.f64 x) 4) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (fma.f64 (Rewrite<= metadata-eval (/.f64 2 3)) (*.f64 x x) 2) (fma.f64 1/5 (pow.f64 (fabs.f64 x) 4) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 25 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (fma.f64 (/.f64 2 3) (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 1/5 (pow.f64 (fabs.f64 x) 4) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2)) (fma.f64 1/5 (pow.f64 (fabs.f64 x) 4) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 25 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (Rewrite<= metadata-eval (/.f64 1 5)) (pow.f64 (fabs.f64 x) 4) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (pow.f64 (fabs.f64 x) (Rewrite<= metadata-eval (+.f64 3 1))) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 25 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (Rewrite<= pow-plus_binary64 (*.f64 (pow.f64 (fabs.f64 x) 3) (fabs.f64 x))) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (Rewrite=> unpow3_binary64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x))) (fabs.f64 x)) (*.f64 1/21 (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (*.f64 (Rewrite<= metadata-eval (/.f64 1 21)) (pow.f64 (fabs.f64 x) 6))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (*.f64 (/.f64 1 21) (pow.f64 (fabs.f64 x) (Rewrite<= metadata-eval (*.f64 2 3))))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (*.f64 (/.f64 1 21) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (fabs.f64 x) 3) (pow.f64 (fabs.f64 x) 3))))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 25 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (*.f64 (/.f64 1 21) (Rewrite<= cube-prod_binary64 (pow.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) 3)))))) (sqrt.f64 (PI.f64)))): 1 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (*.f64 (/.f64 1 21) (Rewrite=> unpow3_binary64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (*.f64 (fabs.f64 x) (fabs.f64 x))) (*.f64 (fabs.f64 x) (fabs.f64 x)))))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 1 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (*.f64 (/.f64 1 21) (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (*.f64 (fabs.f64 x) (fabs.f64 x))))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (fma.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (*.f64 (/.f64 1 21) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))))))) (sqrt.f64 (PI.f64)))): 25 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 25 points decrease in error
(fabs.f64 (/.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (fabs.f64 x) (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2)) (*.f64 (fabs.f64 x) (+.f64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))))))) (sqrt.f64 (PI.f64)))): 25 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (+.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) (fabs.f64 x)) (*.f64 2 (fabs.f64 x)))) (*.f64 (fabs.f64 x) (+.f64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (+.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 2 (fabs.f64 x))) (*.f64 (fabs.f64 x) (+.f64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 (fabs.f64 x)) (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x))))) (*.f64 (fabs.f64 x) (+.f64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (+.f64 (+.f64 (*.f64 2 (fabs.f64 x)) (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (fabs.f64 x)) (*.f64 (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (fabs.f64 x))))) (sqrt.f64 (PI.f64)))): 1 points increase in error, 22 points decrease in error
(fabs.f64 (/.f64 (+.f64 (+.f64 (*.f64 2 (fabs.f64 x)) (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (fabs.f64 x)))) (sqrt.f64 (PI.f64)))): 22 points increase in error, 1 points decrease in error
(fabs.f64 (/.f64 (+.f64 (+.f64 (*.f64 2 (fabs.f64 x)) (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (+.f64 (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 (*.f64 2 (fabs.f64 x)) (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 25 points decrease in error
(fabs.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 (+.f64 (+.f64 (*.f64 2 (fabs.f64 x)) (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))))) (sqrt.f64 (PI.f64)))): 1 points increase in error, 0 points decrease in error
(fabs.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (sqrt.f64 (PI.f64))) (+.f64 (+.f64 (+.f64 (*.f64 2 (fabs.f64 x)) (*.f64 (/.f64 2 3) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 1 5) (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 1 21) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))))))): 25 points increase in error, 1 points decrease in error