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