Initial program 48.5
\[\frac{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}
\]
Simplified48.5
\[\leadsto \color{blue}{\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -4\right)\right)}\right) \cdot \frac{-0.5}{a}}
\]
Proof
(*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4))))) (/.f64 -1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 4))))))) (/.f64 -1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a c) (neg.f64 4)))))) (/.f64 -1/2 a)): 0 points increase in error, 1 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) 4)))))) (/.f64 -1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 a c))))))) (/.f64 -1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))) (/.f64 -1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) 1)) (/.f64 -1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (Rewrite<= metadata-eval (neg.f64 -1))) (/.f64 -1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (neg.f64 -1)) (/.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (Rewrite=> metadata-eval 1)) (/.f64 (/.f64 -1 2) a)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> /-rgt-identity_binary64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))) (/.f64 (/.f64 -1 2) a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) -1) (*.f64 2 a))): 6 points increase in error, 32 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
Applied egg-rr48.5
\[\leadsto \left(b - \sqrt{\color{blue}{b \cdot b + a \cdot \left(c \cdot -4\right)}}\right) \cdot \frac{-0.5}{a}
\]
Applied egg-rr56.0
\[\leadsto \left(b - \color{blue}{e^{\log \left(\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -4\right)\right)\right) \cdot 0.5}}\right) \cdot \frac{-0.5}{a}
\]
Applied egg-rr56.1
\[\leadsto \left(b - \color{blue}{{\left(e^{0.5}\right)}^{\log \left(\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}}\right) \cdot \frac{-0.5}{a}
\]
Applied egg-rr53.9
\[\leadsto \color{blue}{\frac{b \cdot b - \mathsf{fma}\left(b, b, a \cdot \left(c \cdot -4\right)\right)}{\left(a \cdot -2\right) \cdot \left(b + \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)\right)}}
\]
Simplified33.2
\[\leadsto \color{blue}{\frac{-0.5}{\left(b + \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)\right) \cdot \frac{a}{\left(a \cdot c\right) \cdot 4}}}
\]
Proof
(/.f64 -1/2 (*.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (/.f64 a (*.f64 (*.f64 a c) 4)))): 0 points increase in error, 0 points decrease in error
(/.f64 -1/2 (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1)) (/.f64 a (*.f64 (*.f64 a c) 4)))): 0 points increase in error, 0 points decrease in error
(/.f64 -1/2 (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1) (/.f64 a (*.f64 (*.f64 a c) (Rewrite<= metadata-eval (neg.f64 -4)))))): 0 points increase in error, 0 points decrease in error
(/.f64 -1/2 (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1) (/.f64 a (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) -4)))))): 0 points increase in error, 0 points decrease in error
(/.f64 -1/2 (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1) (/.f64 a (neg.f64 (Rewrite<= associate-*r*_binary64 (*.f64 a (*.f64 c -4))))))): 1 points increase in error, 0 points decrease in error
(/.f64 -1/2 (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1) (/.f64 a (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 a (*.f64 c -4))))))): 0 points increase in error, 0 points decrease in error
(/.f64 -1/2 (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1) (/.f64 a (-.f64 (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 b b) (*.f64 b b))) (*.f64 a (*.f64 c -4)))))): 17 points increase in error, 0 points decrease in error
(/.f64 -1/2 (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1) (/.f64 a (Rewrite<= associate--r+_binary64 (-.f64 (*.f64 b b) (+.f64 (*.f64 b b) (*.f64 a (*.f64 c -4)))))))): 17 points increase in error, 1 points decrease in error
(/.f64 -1/2 (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 1) (/.f64 a (-.f64 (*.f64 b b) (Rewrite<= fma-udef_binary64 (fma.f64 b b (*.f64 a (*.f64 c -4)))))))): 0 points increase in error, 0 points decrease in error
(/.f64 -1/2 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) a) (*.f64 1 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4)))))))): 24 points increase in error, 9 points decrease in error
(/.f64 -1/2 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 a (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))) (*.f64 1 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4))))))): 0 points increase in error, 0 points decrease in error
(/.f64 -1/2 (/.f64 (*.f64 a (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))) (Rewrite=> *-lft-identity_binary64 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1/2 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4))))) (*.f64 a (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))))): 5 points increase in error, 9 points decrease in error
(Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1/2 a) (/.f64 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4)))) (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))))): 22 points increase in error, 26 points decrease in error
(*.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 1 -2)) a) (/.f64 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4)))) (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 -2 a))) (/.f64 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4)))) (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 1 (Rewrite<= *-commutative_binary64 (*.f64 a -2))) (/.f64 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4)))) (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 1 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4))))) (*.f64 (*.f64 a -2) (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))))): 26 points increase in error, 22 points decrease in error
(/.f64 (Rewrite=> *-lft-identity_binary64 (-.f64 (*.f64 b b) (fma.f64 b b (*.f64 a (*.f64 c -4))))) (*.f64 (*.f64 a -2) (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))): 0 points increase in error, 0 points decrease in error