Simplified0.2
\[\leadsto \color{blue}{1 - \left(\frac{1}{x \cdot 9} + \frac{\frac{y}{3}}{\sqrt{x}}\right)}
\]
Proof
(-.f64 1 (+.f64 (/.f64 1 (*.f64 x 9)) (/.f64 (/.f64 y 3) (sqrt.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (+.f64 (/.f64 1 (*.f64 x 9)) (Rewrite<= associate-/r*_binary64 (/.f64 y (*.f64 3 (sqrt.f64 x)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (+.f64 (/.f64 1 (*.f64 x 9)) (/.f64 y (*.f64 3 (sqrt.f64 x)))))))): 0 points increase in error, 13 points decrease in error
(-.f64 1 (neg.f64 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (/.f64 1 (*.f64 x 9))) (neg.f64 (/.f64 y (*.f64 3 (sqrt.f64 x)))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (neg.f64 (/.f64 1 (*.f64 x 9)))) (neg.f64 (neg.f64 (/.f64 y (*.f64 3 (sqrt.f64 x)))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (+.f64 (neg.f64 (neg.f64 (/.f64 1 (*.f64 x 9)))) (Rewrite=> remove-double-neg_binary64 (/.f64 y (*.f64 3 (sqrt.f64 x)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 y (*.f64 3 (sqrt.f64 x))) (neg.f64 (neg.f64 (/.f64 1 (*.f64 x 9))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 y (*.f64 3 (sqrt.f64 x))) (neg.f64 (/.f64 1 (*.f64 x 9)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 1 (/.f64 y (*.f64 3 (sqrt.f64 x)))) (neg.f64 (/.f64 1 (*.f64 x 9))))): 1 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 1 (*.f64 x 9))) (-.f64 1 (/.f64 y (*.f64 3 (sqrt.f64 x)))))): 0 points increase in error, 1 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (neg.f64 (/.f64 1 (*.f64 x 9))) 1) (/.f64 y (*.f64 3 (sqrt.f64 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (neg.f64 (/.f64 1 (*.f64 x 9))))) (/.f64 y (*.f64 3 (sqrt.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 (/.f64 1 (*.f64 x 9)))) (/.f64 y (*.f64 3 (sqrt.f64 x)))): 0 points increase in error, 0 points decrease in error