Simplified13.0
\[\leadsto \color{blue}{\left(\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -3\right)\right)} - b\right) \cdot \frac{0.3333333333333333}{a}}
\]
Proof
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))) b) (/.f64 1/3 a)): 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 3)))))) b) (/.f64 1/3 a)): 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 3)))))) b) (/.f64 1/3 a)): 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 3 a)))))) b) (/.f64 1/3 a)): 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 3 a)))))) b) (/.f64 1/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 (*.f64 3 a) c))))) b) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) b) (/.f64 1/3 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 3 a) c))) (neg.f64 b))) (/.f64 1/3 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 3 a) c))))) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) 1)) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (Rewrite<= metadata-eval (*.f64 -1 -1))) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) -1)) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (Rewrite=> sub0-neg_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1)) -1) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite=> associate-/l*_binary64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (/.f64 -1 -1))) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (Rewrite=> metadata-eval 1)) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite=> /-rgt-identity_binary64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) (/.f64 1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 (Rewrite<= metadata-eval (/.f64 1 3)) a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) 3) a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (Rewrite<= associate-/r*_binary64 (/.f64 (neg.f64 -1) (*.f64 3 a)))): 15 points increase in error, 17 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 -1)) (*.f64 -1 (*.f64 3 a)))): 12 points increase in error, 19 points decrease in error
(/.f64 (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 -1)) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 3 a) -1))): 0 points increase in error, 0 points decrease in error
(Rewrite=> times-frac_binary64 (*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)) (/.f64 (neg.f64 -1) -1))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)) (/.f64 (Rewrite=> metadata-eval 1) -1)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)) (Rewrite=> metadata-eval -1)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.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
(/.f64 (Rewrite<= *-commutative_binary64 (*.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