Initial program 55.0
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\]
Simplified55.0
\[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)} - b}{a \cdot 2}}
\]
Proof
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -4)))) b) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a (Rewrite<= metadata-eval (neg.f64 4)))))) b) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4)))))) b) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 a)))))) b) (*.f64 a 2)): 0 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 c (*.f64 4 a)))))) b) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 4 a) c))))) b) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b) (*.f64 a 2)): 1 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 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (*.f64 a 2)): 0 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)))) (Rewrite<= *-commutative_binary64 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
Taylor expanded in b around -inf 9.4
\[\leadsto \frac{\color{blue}{2 \cdot \frac{c \cdot a}{b} + -2 \cdot b}}{a \cdot 2}
\]
Simplified2.7
\[\leadsto \frac{\color{blue}{\mathsf{fma}\left(b, -2, \frac{c \cdot 2}{\frac{b}{a}}\right)}}{a \cdot 2}
\]
Proof
(fma.f64 b -2 (/.f64 (*.f64 c 2) (/.f64 b a))): 0 points increase in error, 0 points decrease in error
(fma.f64 b -2 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 c (/.f64 b a)) 2))): 0 points increase in error, 0 points decrease in error
(fma.f64 b -2 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c a) b)) 2)): 16 points increase in error, 25 points decrease in error
(fma.f64 b -2 (Rewrite<= *-commutative_binary64 (*.f64 2 (/.f64 (*.f64 c a) b)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 b -2) (*.f64 2 (/.f64 (*.f64 c a) b)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 -2 b)) (*.f64 2 (/.f64 (*.f64 c a) b))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 (/.f64 (*.f64 c a) b)) (*.f64 -2 b))): 0 points increase in error, 0 points decrease in error
Applied egg-rr2.6
\[\leadsto \frac{\color{blue}{b \cdot -2 + 2 \cdot \frac{c}{\frac{b}{a}}}}{a \cdot 2}
\]
Initial program 25.2
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\]
Simplified25.2
\[\leadsto \color{blue}{\left(\sqrt{\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 (fma.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 4))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.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 (fma.f64 a (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 4 c))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 4) c)) (*.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 (neg.f64 4) c)) (*.f64 b b)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a (neg.f64 4)) c)) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 a))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 4 a)) c)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b) (/.f64 1/2 a)): 0 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, 0 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)): 0 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, 0 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)): 0 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)))) (Rewrite<= associate-/r*_binary64 (/.f64 (neg.f64 -1) (*.f64 2 a)))): 0 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)))) (neg.f64 -1)) (*.f64 2 a))): 9 points increase in error, 13 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 (*.f64 2 a) (neg.f64 -1)))): 0 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 (*.f64 2 a) (Rewrite=> metadata-eval 1))): 0 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)))) (Rewrite=> /-rgt-identity_binary64 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
Applied egg-rr25.1
\[\leadsto \color{blue}{\frac{1}{\frac{a}{\left(\mathsf{hypot}\left(b, \sqrt{\left(a \cdot c\right) \cdot -4}\right) - b\right) \cdot 0.5}}}
\]
Applied egg-rr25.2
\[\leadsto \frac{1}{\color{blue}{\frac{2}{\mathsf{hypot}\left(\sqrt{a \cdot \left(c \cdot -4\right)}, b\right) - b} \cdot a}}
\]
Applied egg-rr26.1
\[\leadsto \frac{1}{\color{blue}{\left(\frac{2}{\mathsf{fma}\left(c, -4 \cdot a, b \cdot b\right) - b \cdot b} \cdot \left(b + \mathsf{hypot}\left(\sqrt{c \cdot \left(-4 \cdot a\right)}, b\right)\right)\right)} \cdot a}
\]
Simplified22.6
\[\leadsto \frac{1}{\color{blue}{\left(\left(b + \mathsf{hypot}\left(\sqrt{a \cdot \left(c \cdot -4\right)}, b\right)\right) \cdot \frac{2}{a \cdot \left(c \cdot -4\right) + 0}\right)} \cdot a}
\]
Proof
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (*.f64 a (*.f64 c -4))) b)) (/.f64 2 (+.f64 (*.f64 a (*.f64 c -4)) 0))): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c -4) a))) b)) (/.f64 2 (+.f64 (*.f64 a (*.f64 c -4)) 0))): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 -4 a)))) b)) (/.f64 2 (+.f64 (*.f64 a (*.f64 c -4)) 0))): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b)) (/.f64 2 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c -4) a)) 0))): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b)) (/.f64 2 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 -4 a))) 0))): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b)) (/.f64 2 (+.f64 (*.f64 c (*.f64 -4 a)) (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 b b) (*.f64 b b)))))): 32 points increase in error, 0 points decrease in error
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b)) (/.f64 2 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 c (*.f64 -4 a)) (*.f64 b b)) (*.f64 b b))))): 27 points increase in error, 1 points decrease in error
(*.f64 (+.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b)) (/.f64 2 (-.f64 (Rewrite<= fma-udef_binary64 (fma.f64 c (*.f64 -4 a) (*.f64 b b))) (*.f64 b b)))): 1 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 2 (-.f64 (fma.f64 c (*.f64 -4 a) (*.f64 b b)) (*.f64 b b))) (+.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr22.1
\[\leadsto \frac{1}{\color{blue}{0 + a \cdot \left(\frac{b + \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)}{a \cdot c} \cdot -0.5\right)}}
\]
Simplified14.7
\[\leadsto \frac{1}{\color{blue}{\frac{b + \mathsf{hypot}\left(b, \sqrt{c \cdot \left(a \cdot -4\right)}\right)}{\frac{c}{-0.5}}}}
\]
Proof
(/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 c (*.f64 a -4))))) (/.f64 c -1/2)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c a) -4))))) (/.f64 c -1/2)): 1 points increase in error, 0 points decrease in error
(/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 a c)) -4)))) (/.f64 c -1/2)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 a (*.f64 c -4)))))) (/.f64 c -1/2)): 0 points increase in error, 1 points decrease in error
(/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))) (/.f64 c -1/2)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 1 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))) (/.f64 c (Rewrite<= metadata-eval (/.f64 2 -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 1 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c -4) 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 1 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (/.f64 (*.f64 c -4) 2)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= *-inverses_binary64 (/.f64 a a)) (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (/.f64 (*.f64 c -4) 2))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 a a) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 2) (*.f64 c -4)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 a (*.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) 2)) (*.f64 a (*.f64 c -4)))): 52 points increase in error, 10 points decrease in error
(/.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 a (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))) 2)) (*.f64 a (*.f64 c -4))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 a (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))) 2) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 a c) -4))): 0 points increase in error, 1 points decrease in error
(Rewrite=> times-frac_binary64 (*.f64 (/.f64 (*.f64 a (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))) (*.f64 a c)) (/.f64 2 -4))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-*r/_binary64 (*.f64 a (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (*.f64 a c)))) (/.f64 2 -4)): 18 points increase in error, 25 points decrease in error
(*.f64 (*.f64 a (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (*.f64 a c))) (Rewrite=> metadata-eval -1/2)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 a (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (*.f64 a c)) -1/2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 a (*.f64 (/.f64 (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (*.f64 a c)) -1/2)))): 0 points increase in error, 0 points decrease in error
Initial program 55.6
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\]
Simplified55.6
\[\leadsto \color{blue}{\left(\sqrt{\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 (fma.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 4))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.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 (fma.f64 a (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 4 c))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 4) c)) (*.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 (neg.f64 4) c)) (*.f64 b b)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a (neg.f64 4)) c)) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 a))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 4 a)) c)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b) (/.f64 1/2 a)): 0 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, 0 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)): 0 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, 0 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)): 0 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)))) (Rewrite<= associate-/r*_binary64 (/.f64 (neg.f64 -1) (*.f64 2 a)))): 0 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)))) (neg.f64 -1)) (*.f64 2 a))): 9 points increase in error, 13 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 (*.f64 2 a) (neg.f64 -1)))): 0 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 (*.f64 2 a) (Rewrite=> metadata-eval 1))): 0 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)))) (Rewrite=> /-rgt-identity_binary64 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
Taylor expanded in a around 0 5.8
\[\leadsto \color{blue}{-1 \cdot \frac{c}{b}}
\]
Simplified5.8
\[\leadsto \color{blue}{\frac{-c}{b}}
\]
Proof
(/.f64 (neg.f64 c) b): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 c)) b): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 c b))): 0 points increase in error, 0 points decrease in error