Initial program 0.1
\[\left(x + \cos y\right) - z \cdot \sin y
\]
Simplified0.1
\[\leadsto \color{blue}{x - \mathsf{fma}\left(z, \sin y, -\cos y\right)}
\]
Proof
(-.f64 x (fma.f64 z (sin.f64 y) (neg.f64 (cos.f64 y)))): 0 points increase in error, 0 points decrease in error
(-.f64 x (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 z (sin.f64 y)) (cos.f64 y)))): 1 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 x (*.f64 z (sin.f64 y))) (cos.f64 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 x (*.f64 (neg.f64 z) (sin.f64 y)))) (cos.f64 y)): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (cos.f64 y) (+.f64 x (*.f64 (neg.f64 z) (sin.f64 y))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (cos.f64 y) x) (*.f64 (neg.f64 z) (sin.f64 y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (cos.f64 y))) (*.f64 (neg.f64 z) (sin.f64 y))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (+.f64 x (cos.f64 y)) (*.f64 z (sin.f64 y)))): 0 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto x - \mathsf{fma}\left(z, \sin y, -\cos y\right)
\]