Simplified3.4
\[\leadsto \frac{\color{blue}{\mathsf{fma}\left(-0.5, \frac{{\left(-1.125 \cdot \left(\left(c \cdot c\right) \cdot \left(a \cdot a\right)\right)\right)}^{2} + 5.0625 \cdot \left({c}^{4} \cdot {a}^{4}\right)}{{b}^{7}}, \mathsf{fma}\left(-1.125, \frac{c \cdot c}{\frac{{b}^{3}}{a \cdot a}}, \mathsf{fma}\left(-1.5, \frac{c}{\frac{b}{a}}, -1.6875 \cdot \frac{{\left(c \cdot a\right)}^{3}}{{b}^{5}}\right)\right)\right)}}{3 \cdot a}
\]
Proof
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (*.f64 c c) (*.f64 a a))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 c c) (/.f64 (pow.f64 b 3) (*.f64 a a))) (fma.f64 -3/2 (/.f64 c (/.f64 b a)) (*.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 a a))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 c c) (/.f64 (pow.f64 b 3) (*.f64 a a))) (fma.f64 -3/2 (/.f64 c (/.f64 b a)) (*.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2)))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 c c) (/.f64 (pow.f64 b 3) (*.f64 a a))) (fma.f64 -3/2 (/.f64 c (/.f64 b a)) (*.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (/.f64 (pow.f64 b 3) (*.f64 a a))) (fma.f64 -3/2 (/.f64 c (/.f64 b a)) (*.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (pow.f64 c 2) (/.f64 (pow.f64 b 3) (Rewrite<= unpow2_binary64 (pow.f64 a 2)))) (fma.f64 -3/2 (/.f64 c (/.f64 b a)) (*.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3))) (fma.f64 -3/2 (/.f64 c (/.f64 b a)) (*.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (fma.f64 -3/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c a) b)) (*.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)))))): 41 points increase in error, 37 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (fma.f64 -3/2 (/.f64 (*.f64 c a) b) (*.f64 -27/16 (/.f64 (Rewrite=> cube-prod_binary64 (*.f64 (pow.f64 c 3) (pow.f64 a 3))) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -3/2 (/.f64 (*.f64 c a) b)) (*.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5))))))): 27 points increase in error, 26 points decrease in error
(fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3))) (+.f64 (*.f64 -3/2 (/.f64 (*.f64 c a) b)) (*.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5))))))): 0 points increase in error, 1 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7))) (+.f64 (*.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3))) (+.f64 (*.f64 -3/2 (/.f64 (*.f64 c a) b)) (*.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5))))))): 0 points increase in error, 0 points decrease in error
Simplified3.0
\[\leadsto \color{blue}{\mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.375, \frac{a}{{b}^{3}} \cdot \left(c \cdot c\right), \mathsf{fma}\left(\frac{-0.16666666666666666}{a}, \frac{{\left(c \cdot a\right)}^{4}}{\frac{{b}^{7}}{6.328125}}, \frac{-0.5625 \cdot {c}^{3}}{\frac{{b}^{5}}{a}} \cdot a\right)\right)\right)}
\]
Proof
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (*.f64 (/.f64 a (pow.f64 b 3)) (*.f64 c c)) (fma.f64 (/.f64 -1/6 a) (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (Rewrite<= associate-/r/_binary64 (/.f64 a (/.f64 (pow.f64 b 3) (*.f64 c c)))) (fma.f64 (/.f64 -1/6 a) (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a (*.f64 c c)) (pow.f64 b 3))) (fma.f64 (/.f64 -1/6 a) (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c c) a)) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (pow.f64 (*.f64 c a) (Rewrite<= metadata-eval (*.f64 2 2))) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (*.f64 c a) 2) (pow.f64 (*.f64 c a) 2))) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 (*.f64 c a) (*.f64 c a))) (pow.f64 (*.f64 c a) 2)) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (*.f64 c a) (*.f64 c a)) (Rewrite=> unpow2_binary64 (*.f64 (*.f64 c a) (*.f64 c a)))) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 (*.f64 (*.f64 c a) (*.f64 c a)) 2)) (/.f64 (pow.f64 b 7) 405/64)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (pow.f64 (*.f64 (*.f64 c a) (*.f64 c a)) 2) (/.f64 (pow.f64 b 7) (Rewrite<= metadata-eval (+.f64 81/64 81/16)))) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 (*.f64 (*.f64 c a) (*.f64 c a)) 2) (+.f64 81/64 81/16)) (pow.f64 b 7))) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 (*.f64 (*.f64 c a) (*.f64 c a)) (*.f64 (*.f64 c a) (*.f64 c a)))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 a a))) (*.f64 (*.f64 c a) (*.f64 c a))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 1 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 c c) (*.f64 a a)) (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 a a)))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 (*.f64 c c) (*.f64 c c)) (*.f64 (*.f64 a a) (*.f64 a a)))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 c c)) (*.f64 (*.f64 a a) (*.f64 a a))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 c 2))) (*.f64 (*.f64 a a) (*.f64 a a))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 c (*.f64 2 2))) (*.f64 (*.f64 a a) (*.f64 a a))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 1 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (pow.f64 c (Rewrite=> metadata-eval 4)) (*.f64 (*.f64 a a) (*.f64 a a))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 (*.f64 a a) a) a))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (*.f64 (Rewrite<= unpow3_binary64 (pow.f64 a 3)) a)) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (Rewrite=> pow-plus_binary64 (pow.f64 a (+.f64 3 1)))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a (Rewrite=> metadata-eval 4))) (+.f64 81/64 81/16)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (Rewrite=> metadata-eval 405/64)) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (Rewrite<= metadata-eval (+.f64 81/16 81/64))) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4))))) (pow.f64 b 7)) (*.f64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (pow.f64 b 5) a)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (/.f64 (/.f64 (pow.f64 b 5) a) a)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (/.f64 (*.f64 -9/16 (pow.f64 c 3)) (Rewrite<= associate-/r*_binary64 (/.f64 (pow.f64 b 5) (*.f64 a a))))))): 0 points increase in error, 1 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (Rewrite<= associate-*r/_binary64 (*.f64 -9/16 (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (*.f64 a a)))))))): 1 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (*.f64 -9/16 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 c 3) (*.f64 a a)) (pow.f64 b 5))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 (/.f64 -1/6 a) (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (Rewrite<= unpow2_binary64 (pow.f64 a 2))) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 -1/6 a) (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1/6 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4))))) (*.f64 a (pow.f64 b 7)))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))))))): 1 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 c b) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/2 (/.f64 c b)) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 11 points increase in error, 6 points decrease in error
(+.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))): 6 points increase in error, 6 points decrease in error
(Rewrite=> associate-+l+_binary64 (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))))): 7 points increase in error, 10 points decrease in error
(+.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -1/2 (/.f64 c b)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> fma-def_binary64 (fma.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))) (*.f64 -1/2 (/.f64 c b)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 -1/6 (/.f64 (Rewrite=> distribute-rgt-out_binary64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (+.f64 81/16 81/64))) (*.f64 a (pow.f64 b 7))) (*.f64 -1/2 (/.f64 c b))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 -1/6 (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (Rewrite=> metadata-eval 405/64)) (*.f64 a (pow.f64 b 7))) (*.f64 -1/2 (/.f64 c b))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 -1/6 (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (Rewrite<= metadata-eval (+.f64 81/64 81/16))) (*.f64 a (pow.f64 b 7))) (*.f64 -1/2 (/.f64 c b))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 -1/6 (/.f64 (Rewrite=> associate-*l*_binary64 (*.f64 (pow.f64 c 4) (*.f64 (pow.f64 a 4) (+.f64 81/64 81/16)))) (*.f64 a (pow.f64 b 7))) (*.f64 -1/2 (/.f64 c b))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4))))) (*.f64 a (pow.f64 b 7))) (*.f64 -1/2 (/.f64 c b))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -1/2 (/.f64 c b)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -1/2 (/.f64 c b))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 10 points increase in error, 7 points decrease in error
(+.f64 (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error