Initial program 37.1
\[\sin \left(x + \varepsilon\right) - \sin x
\]
Applied egg-rr21.8
\[\leadsto \color{blue}{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - \sin x
\]
Taylor expanded in x around inf 21.8
\[\leadsto \color{blue}{\left(\cos x \cdot \sin \varepsilon + \cos \varepsilon \cdot \sin x\right) - \sin x}
\]
Simplified0.4
\[\leadsto \color{blue}{\mathsf{fma}\left(\cos \varepsilon + -1, \sin x, \sin \varepsilon \cdot \cos x\right)}
\]
Proof
(fma.f64 (+.f64 (cos.f64 eps) -1) (sin.f64 x) (*.f64 (sin.f64 eps) (cos.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (cos.f64 eps) (Rewrite<= metadata-eval (neg.f64 1))) (sin.f64 x) (*.f64 (sin.f64 eps) (cos.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= sub-neg_binary64 (-.f64 (cos.f64 eps) 1)) (sin.f64 x) (*.f64 (sin.f64 eps) (cos.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (cos.f64 eps) 1) (sin.f64 x) (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 x) (sin.f64 eps)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> fma-udef_binary64 (+.f64 (*.f64 (-.f64 (cos.f64 eps) 1) (sin.f64 x)) (*.f64 (cos.f64 x) (sin.f64 eps)))): 11 points increase in error, 3 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 x) (-.f64 (cos.f64 eps) 1))) (*.f64 (cos.f64 x) (sin.f64 eps))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (*.f64 1 (sin.f64 x)))) (*.f64 (cos.f64 x) (sin.f64 eps))): 11 points increase in error, 14 points decrease in error
(+.f64 (-.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (Rewrite=> *-lft-identity_binary64 (sin.f64 x))) (*.f64 (cos.f64 x) (sin.f64 eps))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (-.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (sin.f64 x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (sin.f64 x))) (sin.f64 x))): 99 points increase in error, 12 points decrease in error
Final simplification0.4
\[\leadsto \mathsf{fma}\left(\cos \varepsilon + -1, \sin x, \sin \varepsilon \cdot \cos x\right)
\]