Initial program 28.6
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\]
Simplified28.5
\[\leadsto \color{blue}{\left(\sqrt{\mathsf{fma}\left(b, b, \left(a \cdot c\right) \cdot -4\right)} - b\right) \cdot \frac{0.5}{a}}
\]
Proof
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 (*.f64 a c) -4))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 (*.f64 a c) (Rewrite<= metadata-eval (neg.f64 4))))) b) (/.f64 1/2 a)): 16 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) 4))))) b) (/.f64 1/2 a)): 0 points increase in error, 16 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 a c)))))) b) (/.f64 1/2 a)): 16 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))) b) (/.f64 1/2 a)): 0 points increase in error, 16 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b) (/.f64 1/2 a)): 16 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) (neg.f64 b))) (/.f64 1/2 a)): 0 points increase in error, 16 points decrease in error
(*.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (/.f64 1/2 a)): 16 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) a)): 0 points increase in error, 16 points decrease in error
(*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) 2) a)): 16 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (neg.f64 -1) 2)) a)): 0 points increase in error, 16 points decrease in error
(Rewrite=> associate-/l*_binary64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 a (/.f64 (neg.f64 -1) 2)))): 0 points increase in error, 16 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a 2) (neg.f64 -1)))): 16 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 a)) (neg.f64 -1))): 0 points increase in error, 16 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (*.f64 2 a) (Rewrite=> metadata-eval 1))): 0 points increase in error, 16 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite=> /-rgt-identity_binary64 (*.f64 2 a))): 16 points increase in error, 0 points decrease in error
Taylor expanded in b around 0 28.6
\[\leadsto \left(\sqrt{\color{blue}{{b}^{2} + -4 \cdot \left(c \cdot a\right)}} - b\right) \cdot \frac{0.5}{a}
\]
Simplified28.6
\[\leadsto \left(\sqrt{\color{blue}{\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)}} - b\right) \cdot \frac{0.5}{a}
\]
Proof
(*.f64 (-.f64 (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (*.f64 c -4)) (*.f64 b b)))) b) (/.f64 1/2 a)): 7 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 a c) -4)) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 7 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 c a)) -4) (*.f64 b b))) b) (/.f64 1/2 a)): 7 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 -4 (*.f64 c a))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 7 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 -4 (*.f64 c a)) (Rewrite<= unpow2_binary64 (pow.f64 b 2)))) b) (/.f64 1/2 a)): 7 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 b 2) (*.f64 -4 (*.f64 c a))))) b) (/.f64 1/2 a)): 0 points increase in error, 7 points decrease in error
Applied egg-rr27.8
\[\leadsto \color{blue}{\frac{{\left(\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}^{2} - {b}^{4}}{\left(\left(a \cdot 2\right) \cdot \left(b + \sqrt{\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)}\right)\right) \cdot \left(b \cdot b + \mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}}
\]
Taylor expanded in a around 0 0.6
\[\leadsto \frac{\color{blue}{-8 \cdot \left(c \cdot \left(a \cdot {b}^{2}\right)\right) + 16 \cdot \left({c}^{2} \cdot {a}^{2}\right)}}{\left(\left(a \cdot 2\right) \cdot \left(b + \sqrt{\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)}\right)\right) \cdot \left(b \cdot b + \mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}
\]
Simplified0.6
\[\leadsto \frac{\color{blue}{\mathsf{fma}\left(-8, c \cdot \left(a \cdot \left(b \cdot b\right)\right), 16 \cdot \left(\left(c \cdot c\right) \cdot \left(a \cdot a\right)\right)\right)}}{\left(\left(a \cdot 2\right) \cdot \left(b + \sqrt{\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)}\right)\right) \cdot \left(b \cdot b + \mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}
\]
Proof
(/.f64 (fma.f64 -8 (*.f64 c (*.f64 a (*.f64 b b))) (*.f64 16 (*.f64 (*.f64 c c) (*.f64 a a)))) (*.f64 (*.f64 (*.f64 a 2) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -4) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 -8 (*.f64 c (*.f64 a (Rewrite<= unpow2_binary64 (pow.f64 b 2)))) (*.f64 16 (*.f64 (*.f64 c c) (*.f64 a a)))) (*.f64 (*.f64 (*.f64 a 2) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -4) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 -8 (*.f64 c (*.f64 a (pow.f64 b 2))) (*.f64 16 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 a a)))) (*.f64 (*.f64 (*.f64 a 2) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -4) (*.f64 b b))))): 0 points increase in error, 5 points decrease in error
(/.f64 (fma.f64 -8 (*.f64 c (*.f64 a (pow.f64 b 2))) (*.f64 16 (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2))))) (*.f64 (*.f64 (*.f64 a 2) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -4) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -8 (*.f64 c (*.f64 a (pow.f64 b 2)))) (*.f64 16 (*.f64 (pow.f64 c 2) (pow.f64 a 2))))) (*.f64 (*.f64 (*.f64 a 2) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -4) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
Final simplification0.6
\[\leadsto \frac{\mathsf{fma}\left(-8, c \cdot \left(a \cdot \left(b \cdot b\right)\right), 16 \cdot \left(\left(c \cdot c\right) \cdot \left(a \cdot a\right)\right)\right)}{\left(\left(a \cdot 2\right) \cdot \left(b + \sqrt{\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)}\right)\right) \cdot \left(b \cdot b + \mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}
\]