Initial program 36.9
\[\sin \left(x + \varepsilon\right) - \sin x
\]
Applied egg-rr21.5
\[\leadsto \color{blue}{\sin x \cdot \cos \varepsilon + \left(\cos x \cdot \sin \varepsilon - \sin x\right)}
\]
Simplified0.4
\[\leadsto \color{blue}{\sin \varepsilon \cdot \cos x + \sin x \cdot \left(\cos \varepsilon + -1\right)}
\]
Proof
(+.f64 (*.f64 (sin.f64 eps) (cos.f64 x)) (*.f64 (sin.f64 x) (+.f64 (cos.f64 eps) -1))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 x) (sin.f64 eps))) (*.f64 (sin.f64 x) (+.f64 (cos.f64 eps) -1))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (*.f64 (sin.f64 x) (Rewrite=> +-commutative_binary64 (+.f64 -1 (cos.f64 eps))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1 (sin.f64 x)) (*.f64 (cos.f64 eps) (sin.f64 x))))): 5 points increase in error, 10 points decrease in error
(+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (+.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (sin.f64 x))) (*.f64 (cos.f64 eps) (sin.f64 x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (+.f64 (neg.f64 (sin.f64 x)) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 x) (cos.f64 eps))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (neg.f64 (sin.f64 x))) (*.f64 (sin.f64 x) (cos.f64 eps)))): 116 points increase in error, 3 points decrease in error
(+.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (sin.f64 x))) (*.f64 (sin.f64 x) (cos.f64 eps))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (sin.f64 x) (cos.f64 eps)) (-.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (sin.f64 x)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.4
\[\leadsto \color{blue}{\mathsf{fma}\left(\cos \varepsilon + -1, \sin x, \sin \varepsilon \cdot \cos x\right)}
\]
Final simplification0.4
\[\leadsto \mathsf{fma}\left(\cos \varepsilon + -1, \sin x, \sin \varepsilon \cdot \cos x\right)
\]