Simplified13.9
\[\leadsto \color{blue}{\mathsf{fma}\left(-0.5, \frac{a}{\left|b_2\right|} \cdot {\left(\frac{-0.5}{\frac{\left|b_2\right|}{c}}\right)}^{2}, \frac{\left|b_2\right| - b_2}{a} + \frac{-0.5}{\frac{\left|b_2\right|}{c}}\right)}
\]
Proof
(fma.f64 -1/2 (*.f64 (/.f64 a (fabs.f64 b_2)) (pow.f64 (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)) 2)) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (Rewrite<= rem-sqrt-square_binary64 (sqrt.f64 (*.f64 b_2 b_2)))) (pow.f64 (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)) 2)) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 0 points increase in error, 21 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (sqrt.f64 (Rewrite<= unpow2_binary64 (pow.f64 b_2 2)))) (pow.f64 (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)) 2)) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 0 points increase in error, 4 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (sqrt.f64 (pow.f64 b_2 2))) (pow.f64 (/.f64 -1/2 (/.f64 (Rewrite<= rem-sqrt-square_binary64 (sqrt.f64 (*.f64 b_2 b_2))) c)) 2)) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 21 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (sqrt.f64 (pow.f64 b_2 2))) (pow.f64 (/.f64 -1/2 (/.f64 (sqrt.f64 (Rewrite<= unpow2_binary64 (pow.f64 b_2 2))) c)) 2)) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 12 points increase in error, 9 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (sqrt.f64 (pow.f64 b_2 2))) (pow.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1/2 c) (sqrt.f64 (pow.f64 b_2 2)))) 2)) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (sqrt.f64 (pow.f64 b_2 2))) (pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2))))) 2)) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 9 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (Rewrite<= associate-/r/_binary64 (/.f64 a (/.f64 (sqrt.f64 (pow.f64 b_2 2)) (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)))) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 0 points increase in error, 9 points decrease in error
(fma.f64 -1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2)))) (+.f64 (/.f64 (-.f64 (fabs.f64 b_2) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 0 points increase in error, 21 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (+.f64 (/.f64 (-.f64 (Rewrite<= rem-sqrt-square_binary64 (sqrt.f64 (*.f64 b_2 b_2))) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 21 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (+.f64 (/.f64 (-.f64 (sqrt.f64 (Rewrite<= unpow2_binary64 (pow.f64 b_2 2))) b_2) a) (/.f64 -1/2 (/.f64 (fabs.f64 b_2) c)))): 0 points increase in error, 21 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (+.f64 (/.f64 (-.f64 (sqrt.f64 (pow.f64 b_2 2)) b_2) a) (/.f64 -1/2 (/.f64 (Rewrite<= rem-sqrt-square_binary64 (sqrt.f64 (*.f64 b_2 b_2))) c)))): 21 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (+.f64 (/.f64 (-.f64 (sqrt.f64 (pow.f64 b_2 2)) b_2) a) (/.f64 -1/2 (/.f64 (sqrt.f64 (Rewrite<= unpow2_binary64 (pow.f64 b_2 2))) c)))): 0 points increase in error, 21 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (+.f64 (/.f64 (-.f64 (sqrt.f64 (pow.f64 b_2 2)) b_2) a) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1/2 c) (sqrt.f64 (pow.f64 b_2 2)))))): 1 points increase in error, 16 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (+.f64 (/.f64 (-.f64 (sqrt.f64 (pow.f64 b_2 2)) b_2) a) (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2))))))): 12 points increase in error, 1 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) (/.f64 (-.f64 (sqrt.f64 (pow.f64 b_2 2)) b_2) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (+.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (sqrt.f64 (pow.f64 b_2 2)) a) (/.f64 b_2 a))))): 9 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) (/.f64 (sqrt.f64 (pow.f64 b_2 2)) a)) (/.f64 b_2 a)))): 0 points increase in error, 1 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2))) (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (sqrt.f64 (pow.f64 b_2 2)) a) (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))))) (/.f64 b_2 a))): 0 points increase in error, 9 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2)))) (-.f64 (+.f64 (/.f64 (sqrt.f64 (pow.f64 b_2 2)) a) (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2))))) (/.f64 b_2 a)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 a (pow.f64 (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))) 2)) (sqrt.f64 (pow.f64 b_2 2)))) (+.f64 (/.f64 (sqrt.f64 (pow.f64 b_2 2)) a) (*.f64 -1/2 (/.f64 c (sqrt.f64 (pow.f64 b_2 2)))))) (/.f64 b_2 a))): 0 points increase in error, 12 points decrease in error