Simplified44.5
\[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)} - b}{3 \cdot a}}
\]
Proof
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -3)))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 3)))))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a c) (neg.f64 3))))) b) (*.f64 3 a)): 8 points increase in error, 9 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) 3))))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 3 (*.f64 a c)))))) b) (*.f64 3 a)): 0 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 3 a) c))))) b) (*.f64 3 a)): 1 points increase in error, 9 points decrease in error
(/.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) b) (*.f64 3 a)): 0 points increase in error, 1 points decrease in error
(/.f64 (-.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))) 1)) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))) (Rewrite<= metadata-eval (/.f64 -1 -1))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))) -1) -1)) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (Rewrite<= /-rgt-identity_binary64 (/.f64 b 1))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 b (Rewrite<= metadata-eval (/.f64 -1 -1)))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 b -1) -1))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 b)) -1)) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 b)) -1)) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 b)) -1)) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite=> sub-neg_binary64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 (neg.f64 b)))) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (Rewrite=> remove-double-neg_binary64 b)) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 -1 (*.f64 3 a)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) (*.f64 -1 (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (*.f64 -1 (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
(Rewrite=> times-frac_binary64 (*.f64 (/.f64 (neg.f64 -1) -1) (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite=> metadata-eval 1) -1) (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> metadata-eval -1) (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (*.f64 3 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 (*.f64 3 a) c)))))) (*.f64 3 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 (*.f64 3 a) c)))))) (*.f64 3 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 (*.f64 3 a) c))))) (*.f64 3 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 (*.f64 3 a) c)))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error