Initial program 0.0
\[x \cdot y + \left(x - 1\right) \cdot z
\]
Simplified0.0
\[\leadsto \color{blue}{x \cdot \left(y + z\right) - z}
\]
Proof
(-.f64 (*.f64 x (+.f64 y z)) z): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 x y) (*.f64 x z))) z): 2 points increase in error, 3 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (+.f64 (*.f64 x y) (*.f64 x z)) (neg.f64 z))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 x y) (*.f64 x z)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 z))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 x y) (*.f64 x z)) (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 x y) (+.f64 (*.f64 x z) (*.f64 (neg.f64 1) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x y) (Rewrite<= distribute-rgt-in_binary64 (*.f64 z (+.f64 x (neg.f64 1))))): 6 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x y) (*.f64 z (Rewrite<= sub-neg_binary64 (-.f64 x 1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x y) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 x 1) z))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(y + z, x, -z\right)}
\]
Final simplification0.0
\[\leadsto \mathsf{fma}\left(y + z, x, -z\right)
\]