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, \sin y \cdot \left(-z\right)\right)}
\]
Proof
(fma.f64 (cos.f64 y) x (*.f64 (sin.f64 y) (neg.f64 z))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 y) x (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (sin.f64 y) z)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 y) x (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 z (sin.f64 y))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> fma-udef_binary64 (+.f64 (*.f64 (cos.f64 y) x) (neg.f64 (*.f64 z (sin.f64 y))))): 1 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (*.f64 z (sin.f64 y))) (*.f64 (cos.f64 y) x))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 z (sin.f64 y)))) (*.f64 (cos.f64 y) x)): 0 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto \mathsf{fma}\left(\cos y, x, \sin y \cdot \left(-z\right)\right)
\]