Initial program 0.0
\[x + y \cdot \left(z - x\right)
\]
Taylor expanded in x around 0 0.0
\[\leadsto \color{blue}{y \cdot z + \left(1 + -1 \cdot y\right) \cdot x}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(y, z, \left(1 + \left(-y\right)\right) \cdot x\right)}
\]
Proof
(fma.f64 y z (*.f64 (+.f64 1 (neg.f64 y)) x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y z (*.f64 (+.f64 1 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 y))) x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y z) (*.f64 (+.f64 1 (*.f64 -1 y)) x))): 8 points increase in error, 0 points decrease in error
Taylor expanded in y around 0 0.0
\[\leadsto \mathsf{fma}\left(y, z, \color{blue}{-1 \cdot \left(y \cdot x\right) + x}\right)
\]
Simplified0.0
\[\leadsto \mathsf{fma}\left(y, z, \color{blue}{x - x \cdot y}\right)
\]
Proof
(-.f64 x (*.f64 x y)): 0 points increase in error, 0 points decrease in error
(-.f64 x (Rewrite<= *-commutative_binary64 (*.f64 y x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 x (neg.f64 (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 y x)) x)): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{fma}\left(y, z, x - y \cdot x\right)
\]