Simplified12.6
\[\leadsto \color{blue}{\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}}
\]
Proof
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) (neg.f64 b_2))) a): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))))) a): 0 points increase in error, 0 points decrease in error
Simplified12.6
\[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(b_2, b_2, c \cdot \left(-a\right)\right)}}{a} - \frac{b_2}{a}}
\]
Proof
(-.f64 (/.f64 (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 c (neg.f64 a)))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (sqrt.f64 (fma.f64 b_2 b_2 (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 c a))))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (sqrt.f64 (fma.f64 b_2 b_2 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 a c))))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= unpow1/2_binary64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/2)) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) (Rewrite<= metadata-eval (*.f64 2 1/4))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4))) a) (/.f64 b_2 a)): 42 points increase in error, 11 points decrease in error
(-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) a))) (/.f64 b_2 a)): 18 points increase in error, 24 points decrease in error
(Rewrite=> fma-neg_binary64 (fma.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) a) (neg.f64 (/.f64 b_2 a)))): 32 points increase in error, 26 points decrease in error
(fma.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) 1)) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) a) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error