Simplified3.8
\[\leadsto \color{blue}{0.5 \cdot \mathsf{fma}\left(x, \frac{x}{y}, y\right)}
\]
Proof
(*.f64 1/2 (fma.f64 x (/.f64 x y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (/.f64 x y)) y))): 2 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 x y) x)) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 x x) y)) y)): 33 points increase in error, 16 points decrease in error
(*.f64 1/2 (+.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) y) y)): 0 points increase in error, 0 points decrease in error
(Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 x 2) y)) (*.f64 1/2 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 1/2 (pow.f64 x 2)) y)) (*.f64 1/2 y)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1/2 y) (pow.f64 x 2))) (*.f64 1/2 y)): 11 points increase in error, 3 points decrease in error
(+.f64 (*.f64 (/.f64 1/2 y) (pow.f64 x 2)) (*.f64 1/2 (Rewrite<= /-rgt-identity_binary64 (/.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 1/2 y) (pow.f64 x 2)) (*.f64 1/2 (/.f64 y (Rewrite<= *-inverses_binary64 (/.f64 y y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 1/2 y) (pow.f64 x 2)) (*.f64 1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y y) y)))): 82 points increase in error, 15 points decrease in error
(+.f64 (*.f64 (/.f64 1/2 y) (pow.f64 x 2)) (*.f64 1/2 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 y 2)) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 1/2 y) (pow.f64 x 2)) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 1/2 (pow.f64 y 2)) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 1/2 y) (pow.f64 x 2)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1/2 y) (pow.f64 y 2)))): 20 points increase in error, 4 points decrease in error
(Rewrite<= distribute-lft-in_binary64 (*.f64 (/.f64 1/2 y) (+.f64 (pow.f64 x 2) (pow.f64 y 2)))): 1 points increase in error, 3 points decrease in error
(*.f64 (/.f64 1/2 y) (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 y 2) (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1/2 (+.f64 (pow.f64 y 2) (pow.f64 x 2))) y)): 8 points increase in error, 30 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 1/2 (/.f64 (+.f64 (pow.f64 y 2) (pow.f64 x 2)) y))): 0 points increase in error, 0 points decrease in error