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