Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(x, \mathsf{fma}\left(y, z, -z\right), x\right)}
\]
Proof
(fma.f64 x (fma.f64 y z (neg.f64 z)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y z) (neg.f64 z))) x): 1 points increase in error, 0 points decrease in error
(fma.f64 x (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 y z)))) (neg.f64 z)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 x (+.f64 (neg.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 y) z))) (neg.f64 z)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 x (+.f64 (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 (neg.f64 y) (neg.f64 z))) (neg.f64 z)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite=> distribute-lft1-in_binary64 (*.f64 (+.f64 (neg.f64 y) 1) (neg.f64 z))) x): 0 points increase in error, 1 points decrease in error
(fma.f64 x (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (neg.f64 y))) (neg.f64 z)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 y)) (neg.f64 z)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (-.f64 1 y) z))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (-.f64 1 y)) z)) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (*.f64 (neg.f64 (-.f64 1 y)) z)) x)): 1 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x (*.f64 (neg.f64 (-.f64 1 y)) z)) (Rewrite<= *-rgt-identity_binary64 (*.f64 x 1))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-in_binary64 (*.f64 x (+.f64 (*.f64 (neg.f64 (-.f64 1 y)) z) 1))): 3 points increase in error, 1 points decrease in error
(*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 (neg.f64 (-.f64 1 y)) z)))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 1 (*.f64 (-.f64 1 y) z)))): 0 points increase in error, 0 points decrease in error