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