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