Initial program 17.1
\[\left(\left(x \cdot y + y \cdot y\right) - y \cdot z\right) - y \cdot y
\]
Simplified0.0
\[\leadsto \color{blue}{y \cdot \left(x - z\right)}
\]
Proof
(*.f64 y (-.f64 x z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 y x) (*.f64 y z))): 2 points increase in error, 1 points decrease in error
(-.f64 (Rewrite<= *-commutative_binary64 (*.f64 x y)) (*.f64 y z)): 0 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)): 35 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (*.f64 y y))) (*.f64 y z)): 24 points increase in error, 0 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (+.f64 (*.f64 y y) (*.f64 y z)))): 25 points increase in error, 10 points decrease in error
(-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y z) (*.f64 y y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l-_binary64 (-.f64 (-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (*.f64 y z)) (*.f64 y y))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.0
\[\leadsto \color{blue}{y \cdot x + y \cdot \left(-z\right)}
\]
Applied egg-rr0.0
\[\leadsto \color{blue}{y \cdot x - y \cdot z}
\]
Applied egg-rr0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(y, x, z \cdot \left(-y\right)\right)}
\]
Final simplification0.0
\[\leadsto \mathsf{fma}\left(y, x, y \cdot \left(-z\right)\right)
\]