Simplified0.1
\[\leadsto \color{blue}{\mathsf{fma}\left(x, -0.70711, \frac{\mathsf{fma}\left(x, 0.1913510371, 1.6316775383\right)}{\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.04481, 0.99229\right), 1\right)}\right)}
\]
Proof
(fma.f64 x -70711/100000 (/.f64 (fma.f64 x 1913510371/10000000000 16316775383/10000000000) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= metadata-eval (*.f64 70711/100000 -1)) (/.f64 (fma.f64 x 1913510371/10000000000 16316775383/10000000000) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (fma.f64 x (Rewrite<= metadata-eval (*.f64 27061/100000 70711/100000)) 16316775383/10000000000) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (fma.f64 x (*.f64 27061/100000 70711/100000) (Rewrite<= metadata-eval (*.f64 230753/100000 70711/100000))) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (*.f64 27061/100000 70711/100000)) (*.f64 230753/100000 70711/100000))) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 27061/100000) 70711/100000)) (*.f64 230753/100000 70711/100000)) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 230753/100000 70711/100000) (*.f64 (*.f64 x 27061/100000) 70711/100000))) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 70711/100000 (+.f64 230753/100000 (*.f64 x 27061/100000)))) (fma.f64 x (fma.f64 x 4481/100000 99229/100000) 1))): 0 points increase in error, 1 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (*.f64 70711/100000 (+.f64 230753/100000 (*.f64 x 27061/100000))) (fma.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x 4481/100000) 99229/100000)) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (*.f64 70711/100000 (+.f64 230753/100000 (*.f64 x 27061/100000))) (fma.f64 x (Rewrite<= +-commutative_binary64 (+.f64 99229/100000 (*.f64 x 4481/100000))) 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (*.f64 70711/100000 (+.f64 230753/100000 (*.f64 x 27061/100000))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))) 1)))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (/.f64 (*.f64 70711/100000 (+.f64 230753/100000 (*.f64 x 27061/100000))) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (Rewrite<= associate-*r/_binary64 (*.f64 70711/100000 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000)))))))): 3 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (*.f64 70711/100000 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000)))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (*.f64 70711/100000 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (neg.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000)))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 70711/100000 -1) (neg.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 70711/100000 -1) (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000)))))) (*.f64 70711/100000 -1)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (*.f64 70711/100000 -1)) (*.f64 (neg.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000)))))) (*.f64 70711/100000 -1)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-in_binary64 (*.f64 (*.f64 70711/100000 -1) (+.f64 x (neg.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))))))): 1 points increase in error, 1 points decrease in error
(*.f64 (*.f64 70711/100000 -1) (Rewrite<= sub-neg_binary64 (-.f64 x (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000)))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 70711/100000 (*.f64 -1 (-.f64 x (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 70711/100000 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 x (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 70711/100000 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 x (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 70711/100000 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 x) (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 70711/100000 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 x)) (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))))): 0 points increase in error, 0 points decrease in error
(*.f64 70711/100000 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))) (neg.f64 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 70711/100000 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 (+.f64 230753/100000 (*.f64 x 27061/100000)) (+.f64 1 (*.f64 x (+.f64 99229/100000 (*.f64 x 4481/100000))))) x))): 0 points increase in error, 0 points decrease in error