Simplified1.3
\[\leadsto \color{blue}{\mathsf{fma}\left(-2, \frac{a}{\frac{\frac{{b}^{5}}{{c}^{3}}}{a}}, \frac{{a}^{3} \cdot -0.25}{b} \cdot \left(\frac{{c}^{4}}{{b}^{6}} \cdot 20\right)\right) - \mathsf{fma}\left(\frac{c \cdot c}{{b}^{3}}, a, \frac{c}{b}\right)}
\]
Proof
(-.f64 (fma.f64 -2 (/.f64 a (/.f64 (/.f64 (pow.f64 b 5) (pow.f64 c 3)) a)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) 20))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a a) (/.f64 (pow.f64 b 5) (pow.f64 c 3)))) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) 20))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) (/.f64 (pow.f64 b 5) (pow.f64 c 3))) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) 20))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 a 2) (pow.f64 c 3)) (pow.f64 b 5))) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) 20))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 c 3) (pow.f64 a 2))) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) 20))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) (Rewrite<= metadata-eval (+.f64 16 4))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 4 (/.f64 (pow.f64 c 4) (pow.f64 b 6))))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (Rewrite<= metadata-eval (*.f64 -2 -2)) (/.f64 (pow.f64 c 4) (pow.f64 b 6)))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -2 -2) (/.f64 (pow.f64 c (Rewrite<= metadata-eval (*.f64 2 2))) (pow.f64 b 6)))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -2 -2) (/.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 c 2) (pow.f64 c 2))) (pow.f64 b 6)))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -2 -2) (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (pow.f64 b (Rewrite<= metadata-eval (*.f64 2 3)))))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -2 -2) (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 b 3) (pow.f64 b 3)))))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -2 -2) (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (pow.f64 c 2) (pow.f64 b 3)) (/.f64 (pow.f64 c 2) (pow.f64 b 3)))))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3)))))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) b) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (Rewrite<= unpow2_binary64 (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 (pow.f64 a 3) -1/4) (/.f64 b (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2)))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (pow.f64 a 3) (/.f64 b (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2)))) -1/4))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) -1/4)) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (fma.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= *-commutative_binary64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))) (fma.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (fma.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (pow.f64 b 3)) a (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (pow.f64 c 2) (pow.f64 b 3)) a) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (/.f64 c b))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (neg.f64 (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -1 (/.f64 c b))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -1 (/.f64 c b))) (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.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-+r+_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (+.f64 (*.f64 -1 (/.f64 c b)) (+.f64 (*.f64 -1/4 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -2 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (*.f64 -2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))))): 0 points increase in error, 0 points decrease in error