Initial program 26.7
\[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}
\]
Simplified26.8
\[\leadsto \color{blue}{\frac{-0.5}{a} \cdot \left(b + \sqrt{\mathsf{fma}\left(a \cdot c, -4, b \cdot b\right)}\right)}
\]
Proof
(*.f64 (/.f64 -1/2 a) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) -4 (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) a) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) -4 (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 2 a))) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) -4 (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) (Rewrite<= metadata-eval (neg.f64 4)) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 a c) (neg.f64 4)) (*.f64 b b)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) 4))) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 a c)))) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (neg.f64 (*.f64 4 (*.f64 a c)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (Rewrite<= sub-neg_binary64 (-.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (Rewrite=> sub-neg_binary64 (+.f64 b (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (Rewrite=> remove-double-neg_binary64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 -1 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))) (*.f64 2 a))): 8 points increase in error, 24 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<= distribute-neg-out_binary64 (+.f64 (neg.f64 b) (neg.f64 (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<= sub-neg_binary64 (-.f64 (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-rr29.7
\[\leadsto \frac{-0.5}{a} \cdot \color{blue}{e^{\log \left(b + \mathsf{hypot}\left(b, \sqrt{\left(a \cdot c\right) \cdot -4}\right)\right)}}
\]
Applied egg-rr33.8
\[\leadsto \color{blue}{\frac{b \cdot b - \mathsf{fma}\left(-4 \cdot a, c, b \cdot b\right)}{\left(a \cdot -2\right) \cdot \left(b - \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)\right)}}
\]
Simplified29.2
\[\leadsto \color{blue}{\frac{a \cdot \left(c \cdot -4\right) + 0}{a \cdot \left(\mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right) - b\right)} \cdot -0.5}
\]
Proof
(*.f64 (/.f64 (+.f64 (*.f64 a (*.f64 c -4)) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (*.f64 a (Rewrite=> *-commutative_binary64 (*.f64 -4 c))) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (*.f64 a (*.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 -4) (sqrt.f64 -4))) c)) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 129 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (*.f64 a (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (sqrt.f64 -4) 2)) c)) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a (pow.f64 (sqrt.f64 -4) 2)) c)) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (*.f64 (*.f64 a (Rewrite=> unpow2_binary64 (*.f64 (sqrt.f64 -4) (sqrt.f64 -4)))) c) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (*.f64 (*.f64 a (Rewrite=> rem-square-sqrt_binary64 -4)) c) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 129 points decrease in error
(*.f64 (/.f64 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -4 a)) c) 0) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (*.f64 (*.f64 -4 a) c) (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 b b) (*.f64 b b)))) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 24 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 (*.f64 -4 a) c) (*.f64 b b)) (*.f64 b b))) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 19 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 (Rewrite<= fma-udef_binary64 (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (*.f64 b b)) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite=> sub-neg_binary64 (+.f64 (fma.f64 (*.f64 -4 a) c (*.f64 b b)) (neg.f64 (*.f64 b b)))) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (*.f64 b b)) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 b b))) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))))) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))))) (*.f64 a (-.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) b))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (*.f64 a (Rewrite=> sub-neg_binary64 (+.f64 (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))) (neg.f64 b))))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (*.f64 a (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 b) (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (*.f64 a (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 b)) (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (*.f64 a (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (*.f64 a (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (neg.f64 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))) a)) -1/2): 11 points increase in error, 36 points decrease in error
(*.f64 (/.f64 (/.f64 (neg.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))))) a) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))))) (*.f64 -1 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))) a) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1 -1) (/.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))))) a) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (Rewrite=> metadata-eval 1) (/.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))) a) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite=> *-lft-identity_binary64 (/.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))) a) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> associate-/l/_binary64 (/.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (*.f64 a (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4)))))))) -1/2): 36 points increase in error, 11 points decrease in error
(*.f64 (/.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) a))) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (*.f64 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) a)) (Rewrite<= metadata-eval (/.f64 1 -2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) 1) (*.f64 (*.f64 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) a) -2))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) 1) (Rewrite<= associate-*r*_binary64 (*.f64 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (*.f64 a -2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> *-rgt-identity_binary64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b)))) (*.f64 (-.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))) (*.f64 a -2))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (*.f64 b b) (fma.f64 (*.f64 -4 a) c (*.f64 b b))) (Rewrite=> *-commutative_binary64 (*.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
Applied egg-rr29.7
\[\leadsto \color{blue}{\left(\left(\left(a \cdot c\right) \cdot 4\right) \cdot \frac{1}{a \cdot \left(-\left(\mathsf{hypot}\left(\sqrt{-4 \cdot \left(a \cdot c\right)}, b\right) - b\right)\right)}\right)} \cdot -0.5
\]
Simplified14.7
\[\leadsto \color{blue}{\frac{-\frac{c}{-0.25}}{b - \mathsf{hypot}\left(\sqrt{c \cdot \left(-4 \cdot a\right)}, b\right)}} \cdot -0.5
\]
Proof
(/.f64 (neg.f64 (/.f64 c -1/4)) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 c (Rewrite<= metadata-eval (/.f64 1 -4)))) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c -4) 1))) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 c -4) (Rewrite<= *-inverses_binary64 (/.f64 a a)))) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (*.f64 c -4) a) a))) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 17 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 a (/.f64 (*.f64 c -4) a)))) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 a (*.f64 c -4)) a))) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 43 points increase in error, 28 points decrease in error
(/.f64 (neg.f64 (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a c) -4)) a)) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 1 points increase in error, 1 points decrease in error
(/.f64 (neg.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -4 (*.f64 a c))) a)) (-.f64 b (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (-.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 b))) (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (-.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (neg.f64 b))) (hypot.f64 (sqrt.f64 (*.f64 c (*.f64 -4 a))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (-.f64 (-.f64 0 (neg.f64 b)) (hypot.f64 (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 -4 a) c))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (-.f64 (-.f64 0 (neg.f64 b)) (hypot.f64 (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -4 (*.f64 a c)))) b))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (Rewrite<= associate--r+_binary64 (-.f64 0 (+.f64 (neg.f64 b) (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (-.f64 0 (Rewrite=> +-commutative_binary64 (+.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) (neg.f64 b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (-.f64 0 (Rewrite=> unsub-neg_binary64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a)) (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (/.f64 (*.f64 -4 (*.f64 a c)) a) (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 -4 (*.f64 a c)) (*.f64 a (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))))): 22 points increase in error, 36 points decrease in error
(Rewrite=> distribute-neg-frac_binary64 (/.f64 (neg.f64 (*.f64 -4 (*.f64 a c))) (*.f64 a (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 a c) -4))) (*.f64 a (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 (*.f64 a c) (neg.f64 -4))) (*.f64 a (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 a c) (Rewrite=> metadata-eval 4)) (*.f64 a (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 (*.f64 a c) 4) 1)) (*.f64 a (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (*.f64 (*.f64 a c) 4) (/.f64 1 (*.f64 a (neg.f64 (-.f64 (hypot.f64 (sqrt.f64 (*.f64 -4 (*.f64 a c))) b) b)))))): 16 points increase in error, 10 points decrease in error
Initial program 56.7
\[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}
\]
Simplified56.8
\[\leadsto \color{blue}{\frac{-0.5}{a} \cdot \left(b + \sqrt{\mathsf{fma}\left(a \cdot c, -4, b \cdot b\right)}\right)}
\]
Proof
(*.f64 (/.f64 -1/2 a) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) -4 (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) a) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) -4 (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 2 a))) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) -4 (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (fma.f64 (*.f64 a c) (Rewrite<= metadata-eval (neg.f64 4)) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 a c) (neg.f64 4)) (*.f64 b b)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) 4))) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 a c)))) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (neg.f64 (*.f64 4 (*.f64 a c)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (sqrt.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (Rewrite<= sub-neg_binary64 (-.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (Rewrite=> sub-neg_binary64 (+.f64 b (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 (*.f64 2 a)) (+.f64 b (Rewrite=> remove-double-neg_binary64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 -1 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))) (*.f64 2 a))): 8 points increase in error, 24 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<= distribute-neg-out_binary64 (+.f64 (neg.f64 b) (neg.f64 (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<= sub-neg_binary64 (-.f64 (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
Taylor expanded in a around 0 3.0
\[\leadsto \color{blue}{-1 \cdot \frac{b}{a}}
\]
Simplified3.0
\[\leadsto \color{blue}{\frac{-b}{a}}
\]
Proof
(/.f64 (neg.f64 b) a): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 b)) a): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 b a))): 0 points increase in error, 0 points decrease in error