Simplified0.5
\[\leadsto \color{blue}{\frac{\left|x\right|}{\left|\frac{\sqrt{\pi}}{\mathsf{fma}\left(0.2, {x}^{4}, 0.047619047619047616 \cdot {x}^{6}\right) + \mathsf{fma}\left(0.6666666666666666, x \cdot x, 2\right)}\right|}}
\]
Proof
(/.f64 (fabs.f64 x) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 1/5 (pow.f64 x 4) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fabs-fabs_binary64 (fabs.f64 (fabs.f64 x))) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 1/5 (pow.f64 x 4) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (Rewrite<= metadata-eval (/.f64 1 5)) (pow.f64 x 4) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (/.f64 1 5) (pow.f64 x (Rewrite<= metadata-eval (*.f64 2 2))) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (/.f64 1 5) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 x 2) (pow.f64 x 2))) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (/.f64 1 5) (*.f64 (Rewrite=> unpow2_binary64 (*.f64 x x)) (pow.f64 x 2)) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (/.f64 1 5) (*.f64 (*.f64 x x) (Rewrite=> unpow2_binary64 (*.f64 x x))) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (/.f64 1 5) (*.f64 (*.f64 x x) (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x)))) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (/.f64 1 5) (*.f64 (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x))) (*.f64 (fabs.f64 x) (fabs.f64 x))) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (fma.f64 (/.f64 1 5) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x))) (*.f64 1/21 (pow.f64 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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 x 6))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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 x (Rewrite<= metadata-eval (*.f64 2 3))))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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 x 3) (pow.f64 x 3))))) (fma.f64 2/3 (*.f64 x x) 2))))): 6 points increase in error, 3 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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 x x) 3)))) (fma.f64 2/3 (*.f64 x x) 2))))): 13 points increase in error, 6 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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 (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x))) 3))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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)))))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 2 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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))))) (fma.f64 2/3 (*.f64 x x) 2))))): 4 points increase in error, 7 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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))))) (fma.f64 2/3 (*.f64 x x) 2))))): 6 points increase in error, 5 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (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))))) (fma.f64 2/3 (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (+.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)))) (fma.f64 (Rewrite<= metadata-eval (/.f64 2 3)) (*.f64 x x) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (+.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)))) (fma.f64 (/.f64 2 3) (Rewrite<= sqr-abs_binary64 (*.f64 (fabs.f64 x) (fabs.f64 x))) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (+.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)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (+.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))))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (Rewrite<= *-rgt-identity_binary64 (*.f64 (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (+.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))))) 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (fabs.f64 x)) (fabs.f64 (/.f64 (sqrt.f64 (PI.f64)) (Rewrite=> *-rgt-identity_binary64 (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (+.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))))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fabs-div_binary64 (fabs.f64 (/.f64 (fabs.f64 x) (/.f64 (sqrt.f64 (PI.f64)) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (+.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))))))))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (fabs.f64 x) (+.f64 (+.f64 (*.f64 (/.f64 2 3) (*.f64 (fabs.f64 x) (fabs.f64 x))) 2) (+.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))))): 7 points increase in error, 3 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)))): 1 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)))): 1 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, 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 (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)))): 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)))) (+.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)))): 1 points increase in error, 2 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, 0 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)))): 0 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))))))): 24 points increase in error, 132 points decrease in error