Initial program 56.1
\[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}
\]
Simplified56.1
\[\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, 0 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 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (/.f64 (Rewrite<= metadata-eval (/.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))): 8 points increase in error, 23 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<= 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-rr57.8
\[\leadsto \color{blue}{\frac{\frac{-0.5}{a} \cdot \left(b \cdot b - \mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}{b - \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)}}
\]
Taylor expanded in a around 0 29.0
\[\leadsto \frac{\color{blue}{-2 \cdot c}}{b - \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)}
\]
Simplified29.0
\[\leadsto \frac{\color{blue}{c \cdot -2}}{b - \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)}
\]
Proof
(*.f64 c -2): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 -2 c)): 0 points increase in error, 0 points decrease in error
Taylor expanded in b around -inf 64.0
\[\leadsto \frac{c \cdot -2}{\color{blue}{0.5 \cdot \frac{c \cdot \left(a \cdot {\left(\sqrt{-4}\right)}^{2}\right)}{b} + 2 \cdot b}}
\]
Simplified4.6
\[\leadsto \frac{c \cdot -2}{\color{blue}{\mathsf{fma}\left(b, 2, \frac{c}{b} \cdot \left(-2 \cdot a\right)\right)}}
\]
Proof
(fma.f64 b 2 (*.f64 (/.f64 c b) (*.f64 -2 a))): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (*.f64 (/.f64 c b) (*.f64 (Rewrite<= metadata-eval (*.f64 1/2 -4)) a))): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (*.f64 (/.f64 c b) (*.f64 (*.f64 1/2 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 -4) (sqrt.f64 -4)))) a))): 214 points increase in error, 0 points decrease in error
(fma.f64 b 2 (*.f64 (/.f64 c b) (*.f64 (*.f64 1/2 (Rewrite<= unpow2_binary64 (pow.f64 (sqrt.f64 -4) 2))) a))): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (*.f64 (/.f64 c b) (Rewrite<= associate-*r*_binary64 (*.f64 1/2 (*.f64 (pow.f64 (sqrt.f64 -4) 2) a))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (*.f64 (/.f64 c b) (*.f64 1/2 (Rewrite<= *-commutative_binary64 (*.f64 a (pow.f64 (sqrt.f64 -4) 2)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (*.f64 (/.f64 c b) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 a (pow.f64 (sqrt.f64 -4) 2)) 1/2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 c b) (*.f64 a (pow.f64 (sqrt.f64 -4) 2))) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (*.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 -4) 2))) b)) 1/2)): 0 points increase in error, 0 points decrease in error
(fma.f64 b 2 (Rewrite<= *-commutative_binary64 (*.f64 1/2 (/.f64 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 -4) 2))) b)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 b 2) (*.f64 1/2 (/.f64 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 -4) 2))) b)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 b)) (*.f64 1/2 (/.f64 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 -4) 2))) b))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 -4) 2))) b)) (*.f64 2 b))): 0 points increase in error, 0 points decrease in error
Initial program 27.8
\[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}
\]
Simplified27.8
\[\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, 0 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 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (/.f64 (Rewrite<= metadata-eval (/.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))): 8 points increase in error, 23 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<= 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-rr28.3
\[\leadsto \color{blue}{\frac{\frac{-0.5}{a} \cdot \left(b \cdot b - \mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)\right)}{b - \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)}}
\]
Taylor expanded in a around 0 13.5
\[\leadsto \frac{\color{blue}{-2 \cdot c}}{b - \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)}
\]
Simplified13.5
\[\leadsto \frac{\color{blue}{c \cdot -2}}{b - \mathsf{hypot}\left(b, \sqrt{a \cdot \left(c \cdot -4\right)}\right)}
\]
Proof
(*.f64 c -2): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 -2 c)): 0 points increase in error, 0 points decrease in error
Initial program 11.9
\[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}
\]
Simplified11.9
\[\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, 0 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 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (/.f64 (Rewrite<= metadata-eval (/.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))): 8 points increase in error, 23 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<= 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-rr11.9
\[\leadsto \left(b + \sqrt{\color{blue}{b \cdot b + a \cdot \left(c \cdot -4\right)}}\right) \cdot \frac{-0.5}{a}
\]
Taylor expanded in b around 0 11.9
\[\leadsto \left(b + \sqrt{\color{blue}{-4 \cdot \left(c \cdot a\right)}}\right) \cdot \frac{-0.5}{a}
\]
Simplified11.9
\[\leadsto \left(b + \sqrt{\color{blue}{c \cdot \left(a \cdot -4\right)}}\right) \cdot \frac{-0.5}{a}
\]
Proof
(*.f64 c (*.f64 a -4)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c a) -4)): 1 points increase in error, 1 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 -4 (*.f64 c a))): 0 points increase in error, 0 points decrease in error
Applied egg-rr33.5
\[\leadsto \left(b + \color{blue}{\sqrt{a \cdot -4} \cdot \sqrt{c}}\right) \cdot \frac{-0.5}{a}
\]
Initial program 44.6
\[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}
\]
Simplified44.7
\[\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, 0 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 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (/.f64 (Rewrite<= metadata-eval (/.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))): 8 points increase in error, 23 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<= 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 b around inf 4.1
\[\leadsto \color{blue}{\frac{c}{b} + -1 \cdot \frac{b}{a}}
\]
Simplified4.1
\[\leadsto \color{blue}{\frac{c}{b} - \frac{b}{a}}
\]
Proof
(-.f64 (/.f64 c b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 c b) (neg.f64 (/.f64 b a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 c b) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 b a)))): 0 points increase in error, 0 points decrease in error