Simplified0.4
\[\leadsto \color{blue}{\sqrt{x} \cdot \left(-3 - \mathsf{fma}\left(y, -3, \frac{-0.3333333333333333}{x}\right)\right)}
\]
Proof
(*.f64 (sqrt.f64 x) (-.f64 -3 (fma.f64 y -3 (/.f64 -1/3 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (Rewrite<= metadata-eval (*.f64 -1 3)) (fma.f64 y -3 (/.f64 -1/3 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) 3) (fma.f64 y -3 (/.f64 -1/3 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (Rewrite<= metadata-eval (*.f64 -1 3)) (/.f64 -1/3 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) 3) (/.f64 -1/3 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (/.f64 (Rewrite<= metadata-eval (*.f64 3 -1/9)) x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (/.f64 (*.f64 3 (Rewrite<= metadata-eval (neg.f64 1/9))) x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (/.f64 (*.f64 3 (neg.f64 (Rewrite<= metadata-eval (/.f64 1 9)))) x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (Rewrite<= associate-*r/_binary64 (*.f64 3 (/.f64 (neg.f64 (/.f64 1 9)) x)))))): 21 points increase in error, 8 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (*.f64 3 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (/.f64 1 9) x))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (*.f64 3 (neg.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 9 x)))))))): 14 points increase in error, 17 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (*.f64 3 (neg.f64 (/.f64 1 (Rewrite<= *-commutative_binary64 (*.f64 x 9)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (fma.f64 y (*.f64 (neg.f64 1) 3) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 3 (/.f64 1 (*.f64 x 9)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (*.f64 (neg.f64 1) 3)) (neg.f64 (*.f64 3 (/.f64 1 (*.f64 x 9)))))))): 5 points increase in error, 2 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (+.f64 (*.f64 y (*.f64 (Rewrite=> metadata-eval -1) 3)) (neg.f64 (*.f64 3 (/.f64 1 (*.f64 x 9))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (+.f64 (*.f64 y (Rewrite=> metadata-eval -3)) (neg.f64 (*.f64 3 (/.f64 1 (*.f64 x 9))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (+.f64 (*.f64 y (Rewrite<= metadata-eval (neg.f64 3))) (neg.f64 (*.f64 3 (/.f64 1 (*.f64 x 9))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y 3))) (neg.f64 (*.f64 3 (/.f64 1 (*.f64 x 9))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 y 3) (*.f64 3 (/.f64 1 (*.f64 x 9)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (neg.f64 (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 3 y)) (*.f64 3 (/.f64 1 (*.f64 x 9))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (neg.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 3 (+.f64 y (/.f64 1 (*.f64 x 9)))))))): 1 points increase in error, 2 points decrease in error
(*.f64 (sqrt.f64 x) (-.f64 (*.f64 (neg.f64 1) 3) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) 3))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 (neg.f64 1) 3) (sqrt.f64 x)) (*.f64 (neg.f64 (*.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) 3)) (sqrt.f64 x)))): 3 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (neg.f64 1) (*.f64 3 (sqrt.f64 x)))) (*.f64 (neg.f64 (*.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) 3)) (sqrt.f64 x))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 3 (sqrt.f64 x)) (neg.f64 1))) (*.f64 (neg.f64 (*.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) 3)) (sqrt.f64 x))): 0 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub_binary64 (+.f64 (*.f64 (*.f64 3 (sqrt.f64 x)) (neg.f64 1)) (*.f64 (*.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) 3) (sqrt.f64 x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (*.f64 3 (sqrt.f64 x)) (neg.f64 1)) (Rewrite<= associate-*r*_binary64 (*.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) (*.f64 3 (sqrt.f64 x))))): 39 points increase in error, 35 points decrease in error
(+.f64 (*.f64 (*.f64 3 (sqrt.f64 x)) (neg.f64 1)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 3 (sqrt.f64 x)) (+.f64 y (/.f64 1 (*.f64 x 9)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-in_binary64 (*.f64 (*.f64 3 (sqrt.f64 x)) (+.f64 (neg.f64 1) (+.f64 y (/.f64 1 (*.f64 x 9)))))): 1 points increase in error, 0 points decrease in error
(*.f64 (*.f64 3 (sqrt.f64 x)) (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) (neg.f64 1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 3 (sqrt.f64 x)) (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 y (/.f64 1 (*.f64 x 9))) 1))): 0 points increase in error, 0 points decrease in error