Simplified35.1
\[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, \frac{c}{\frac{{b_2}^{3}}{c \cdot a}}, \frac{-0.5}{\frac{b_2}{c}}\right)}
\]
Proof
(fma.f64 -1/8 (/.f64 c (/.f64 (pow.f64 b_2 3) (*.f64 c a))) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (pow.f64 b_2 3) a) c))) (/.f64 -1/2 (/.f64 b_2 c))): 17 points increase in error, 8 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (Rewrite<= *-lft-identity_binary64 (*.f64 1 a))) c)) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (*.f64 (Rewrite<= metadata-eval (*.f64 -1 -1)) a)) c)) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (*.f64 (*.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 -1) (sqrt.f64 -1))) -1) a)) c)) (/.f64 -1/2 (/.f64 b_2 c))): 169 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (sqrt.f64 -1) 2)) -1) a)) c)) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (*.f64 (*.f64 (pow.f64 (sqrt.f64 -1) 2) (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 -1) (sqrt.f64 -1)))) a)) c)) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (*.f64 (*.f64 (pow.f64 (sqrt.f64 -1) 2) (Rewrite<= unpow2_binary64 (pow.f64 (sqrt.f64 -1) 2))) a)) c)) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 (sqrt.f64 -1) (*.f64 2 2))) a)) c)) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 c (/.f64 (/.f64 (pow.f64 b_2 3) (*.f64 (pow.f64 (sqrt.f64 -1) (Rewrite=> metadata-eval 4)) a)) c)) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c c) (/.f64 (pow.f64 b_2 3) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)))) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (/.f64 (pow.f64 b_2 3) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a))) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3))) (/.f64 -1/2 (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3)) (/.f64 (Rewrite<= metadata-eval (*.f64 1/2 -1)) (/.f64 b_2 c))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3)) (Rewrite<= associate-*r/_binary64 (*.f64 1/2 (/.f64 -1 (/.f64 b_2 c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3)) (*.f64 1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 c) b_2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3)) (*.f64 1/2 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 c -1)) b_2))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3)) (*.f64 1/2 (/.f64 (*.f64 c (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 -1) (sqrt.f64 -1)))) b_2))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3)) (*.f64 1/2 (/.f64 (*.f64 c (Rewrite<= unpow2_binary64 (pow.f64 (sqrt.f64 -1) 2))) b_2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3))) (*.f64 1/2 (/.f64 (*.f64 c (pow.f64 (sqrt.f64 -1) 2)) b_2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 c (pow.f64 (sqrt.f64 -1) 2)) b_2)) (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 (sqrt.f64 -1) 4) a)) (pow.f64 b_2 3))))): 0 points increase in error, 0 points decrease in error