Simplified64.0
\[\leadsto \color{blue}{\begin{array}{l}
\color{blue}{\mathbf{if}\;b \geq 0:\\
\;\;\;\;\frac{-0.5}{a} \cdot \left(b + \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -4\right)\right)}\right)\\
\mathbf{else}:\\
\;\;\;\;c \cdot \frac{2}{\sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -4\right)\right)} - b}\\
}
\end{array}}
\]
Proof
(if (>=.f64 b 0) (*.f64 (/.f64 -1/2 a) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) a) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 2 a))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 4)))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a c) (neg.f64 4))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 1 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 4) (*.f64 a c))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 4 (*.f64 a c)))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 1 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 1 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (Rewrite<= sub-neg_binary64 (-.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (Rewrite=> sub-neg_binary64 (+.f64 b (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (Rewrite=> remove-double-neg_binary64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 -1 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (*.f64 2 a))) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 2 points increase in error, 18 points decrease in error
(if (>=.f64 b 0) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (Rewrite<= distribute-neg-out_binary64 (+.f64 (neg.f64 b) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 4)))))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a c) (neg.f64 4))))) b)))): 1 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 4) (*.f64 a c))))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 4 (*.f64 a c)))))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))) b)))): 1 points increase in error, 1 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (-.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b)))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) (neg.f64 b)))))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 c (/.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 2 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) c))): 0 points increase in error, 0 points decrease in error
(if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 1 points increase in error, 13 points decrease in error