Initial program 13.1
\[\left(\left(x \cdot y - y \cdot y\right) + y \cdot y\right) - y \cdot z
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(x, y, y \cdot \left(-z\right)\right)}
\]
Proof
(fma.f64 x y (*.f64 y (neg.f64 z))): 0 points increase in error, 0 points decrease in error
(fma.f64 x y (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x y) (*.f64 y z))): 3 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= --rgt-identity_binary64 (-.f64 (*.f64 x y) 0)) (*.f64 y z)): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (*.f64 x y) (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 y y) (*.f64 y y)))) (*.f64 y z)): 30 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> associate--r-_binary64 (+.f64 (-.f64 (*.f64 x y) (*.f64 y y)) (*.f64 y y))) (*.f64 y z)): 27 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{fma}\left(x, y, z \cdot \left(-y\right)\right)
\]