Initial program 0.0
\[x - y \cdot z
\]
Simplified0
\[\leadsto \color{blue}{\mathsf{fma}\left(y, -z, x\right)}
\]
Proof
(fma.f64 y (neg.f64 z) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (neg.f64 z)) x)): 1 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y z))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 y) z)) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 (neg.f64 y) z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 x (*.f64 y z))): 0 points increase in error, 0 points decrease in error
Final simplification0
\[\leadsto \mathsf{fma}\left(y, -z, x\right)
\]