Simplified43.8
\[\leadsto \color{blue}{\left(b - \sqrt{\mathsf{fma}\left(a, c \cdot -3, b \cdot b\right)}\right) \cdot \frac{-0.3333333333333333}{a}}
\]
Proof
(*.f64 (-.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b)))) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (fma.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 3))) (*.f64 b b)))) (/.f64 -1/3 a)): 31 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (*.f64 c (neg.f64 3))) (*.f64 b b))))) (/.f64 -1/3 a)): 0 points increase in error, 31 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c (neg.f64 3)) a)) (*.f64 b b)))) (/.f64 -1/3 a)): 0 points increase in error, 31 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 (neg.f64 3) a))) (*.f64 b b)))) (/.f64 -1/3 a)): 31 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (+.f64 (*.f64 c (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 3 a)))) (*.f64 b b)))) (/.f64 -1/3 a)): 0 points increase in error, 31 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 3 a)) c)) (*.f64 b b)))) (/.f64 -1/3 a)): 31 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 3 a)) c))))) (/.f64 -1/3 a)): 31 points increase in error, 0 points decrease in error
(*.f64 (-.f64 b (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 -1/3 a)): 31 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> sub-neg_binary64 (+.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) (/.f64 -1/3 a)): 0 points increase in error, 31 points decrease in error
(*.f64 (+.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 b 1)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 -1/3 a)): 0 points increase in error, 31 points decrease in error
(*.f64 (+.f64 (/.f64 b (Rewrite<= metadata-eval (/.f64 -1 -1))) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 -1/3 a)): 31 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 b -1) -1)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 -1/3 a)): 0 points increase in error, 31 points decrease in error
(*.f64 (+.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 b)) -1) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 -1/3 a)): 31 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 b)) -1) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 -1/3 a)): 0 points increase in error, 31 points decrease in error
(*.f64 (+.f64 (/.f64 (neg.f64 b) -1) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 (Rewrite<= metadata-eval (/.f64 -1 3)) a)): 31 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (/.f64 (neg.f64 b) -1) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 3 a)))): 0 points increase in error, 31 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 -1 (*.f64 3 a)) (+.f64 (/.f64 (neg.f64 b) -1) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))))): 31 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 -1 (*.f64 3 a)) (/.f64 (neg.f64 b) -1)) (*.f64 (/.f64 -1 (*.f64 3 a)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))))): 31 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 -1 (*.f64 3 a)) (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 b)) -1)) (*.f64 (/.f64 -1 (*.f64 3 a)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))): 0 points increase in error, 31 points decrease in error
(+.f64 (*.f64 (/.f64 -1 (*.f64 3 a)) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 b -1)) -1)) (*.f64 (/.f64 -1 (*.f64 3 a)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))): 0 points increase in error, 31 points decrease in error
(+.f64 (*.f64 (/.f64 -1 (*.f64 3 a)) (Rewrite=> associate-/l*_binary64 (/.f64 b (/.f64 -1 -1)))) (*.f64 (/.f64 -1 (*.f64 3 a)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))): 31 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 -1 (*.f64 3 a)) (/.f64 b (Rewrite=> metadata-eval 1))) (*.f64 (/.f64 -1 (*.f64 3 a)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))): 0 points increase in error, 31 points decrease in error
(+.f64 (*.f64 (/.f64 -1 (*.f64 3 a)) (Rewrite=> /-rgt-identity_binary64 b)) (*.f64 (/.f64 -1 (*.f64 3 a)) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))): 0 points increase in error, 31 points decrease in error
(Rewrite<= distribute-lft-in_binary64 (*.f64 (/.f64 -1 (*.f64 3 a)) (+.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))))): 0 points increase in error, 31 points decrease in error
(*.f64 (/.f64 -1 (*.f64 3 a)) (Rewrite<= sub-neg_binary64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))): 31 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 (*.f64 3 a) c))))) (*.f64 3 a))): 31 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, 31 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, 31 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, 31 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, 31 points decrease in error
Simplified0.6
\[\leadsto \frac{\color{blue}{\mathsf{fma}\left(6, c \cdot \left(a \cdot \left(b \cdot b\right)\right), -9 \cdot \left(\left(c \cdot c\right) \cdot \left(a \cdot a\right)\right)\right)}}{\left(\left(a \cdot -3\right) \cdot \left(b + \sqrt{\mathsf{fma}\left(a, c \cdot -3, b \cdot b\right)}\right)\right) \cdot \left(b \cdot b + \mathsf{fma}\left(a, c \cdot -3, b \cdot b\right)\right)}
\]
Proof
(/.f64 (fma.f64 6 (*.f64 c (*.f64 a (*.f64 b b))) (*.f64 -9 (*.f64 (*.f64 c c) (*.f64 a a)))) (*.f64 (*.f64 (*.f64 a -3) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -3) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 6 (*.f64 c (*.f64 a (Rewrite<= unpow2_binary64 (pow.f64 b 2)))) (*.f64 -9 (*.f64 (*.f64 c c) (*.f64 a a)))) (*.f64 (*.f64 (*.f64 a -3) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -3) (*.f64 b b))))): 5 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 6 (*.f64 c (*.f64 a (pow.f64 b 2))) (*.f64 -9 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 a a)))) (*.f64 (*.f64 (*.f64 a -3) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -3) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 6 (*.f64 c (*.f64 a (pow.f64 b 2))) (*.f64 -9 (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2))))) (*.f64 (*.f64 (*.f64 a -3) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -3) (*.f64 b b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 6 (*.f64 c (*.f64 a (pow.f64 b 2)))) (*.f64 -9 (*.f64 (pow.f64 c 2) (pow.f64 a 2))))) (*.f64 (*.f64 (*.f64 a -3) (+.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))))) (+.f64 (*.f64 b b) (fma.f64 a (*.f64 c -3) (*.f64 b b))))): 5 points increase in error, 0 points decrease in error