Simplified8.2
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{-8}{x}, \frac{y}{\frac{x}{y}}, 1\right)}
\]
Proof
(fma.f64 (/.f64 -8 x) (/.f64 y (/.f64 x y)) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 -8 x) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y y) x)) 1): 27 points increase in error, 7 points decrease in error
(fma.f64 (/.f64 -8 x) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 y 2)) x) 1): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 -8 x) (/.f64 (pow.f64 y 2) x)) 1)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 -8 (pow.f64 y 2)) (*.f64 x x))) 1): 27 points increase in error, 3 points decrease in error
(+.f64 (/.f64 (*.f64 -8 (pow.f64 y 2)) (Rewrite<= unpow2_binary64 (pow.f64 x 2))) 1): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -8 (/.f64 (pow.f64 y 2) (pow.f64 x 2)))) 1): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 1 (*.f64 -8 (/.f64 (pow.f64 y 2) (pow.f64 x 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (pow.f64 y 2) (pow.f64 x 2)) -8))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (*.f64 (/.f64 (pow.f64 y 2) (pow.f64 x 2)) (Rewrite<= metadata-eval (-.f64 -4 4)))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -4 (/.f64 (pow.f64 y 2) (pow.f64 x 2))) (*.f64 4 (/.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 (*.f64 -4 (/.f64 (pow.f64 y 2) (pow.f64 x 2)))) (*.f64 4 (/.f64 (pow.f64 y 2) (pow.f64 x 2))))): 3 points increase in error, 1 points decrease in error
Simplified8.0
\[\leadsto \color{blue}{y \cdot \left(-8 \cdot \frac{\frac{y}{x}}{x}\right)} + 1
\]
Proof
(*.f64 y (*.f64 -8 (/.f64 (/.f64 y x) x))): 0 points increase in error, 0 points decrease in error
(*.f64 y (*.f64 -8 (Rewrite<= associate-/r*_binary64 (/.f64 y (*.f64 x x))))): 31 points increase in error, 22 points decrease in error
(*.f64 y (*.f64 -8 (/.f64 y (Rewrite<= unpow2_binary64 (pow.f64 x 2))))): 0 points increase in error, 0 points decrease in error
(*.f64 y (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -8 y) (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (*.f64 -8 y) (pow.f64 x 2)) y)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (*.f64 -8 y) y) (pow.f64 x 2))): 30 points increase in error, 17 points decrease in error
(/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -8 (*.f64 y y))) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -8 (Rewrite<= unpow2_binary64 (pow.f64 y 2))) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -8 (/.f64 (pow.f64 y 2) (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error