Initial program 36.5
\[\sin \left(x + \varepsilon\right) - \sin x
\]
Applied egg-rr21.3
\[\leadsto \color{blue}{\mathsf{fma}\left(\cos \varepsilon, \sin x, \cos x \cdot \sin \varepsilon\right)} - \sin x
\]
Taylor expanded in eps around inf 21.3
\[\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 x, \sin \varepsilon, \sin x \cdot \left(\cos \varepsilon + -1\right)\right)}
\]
Proof
(fma.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
(fma.f64 (cos.f64 x) (sin.f64 eps) (*.f64 (sin.f64 x) (+.f64 (cos.f64 eps) (Rewrite<= metadata-eval (neg.f64 1))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 x) (sin.f64 eps) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (*.f64 (neg.f64 1) (sin.f64 x))))): 14 points increase in error, 6 points decrease in error
(fma.f64 (cos.f64 x) (sin.f64 eps) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (*.f64 1 (sin.f64 x))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 x) (sin.f64 eps) (-.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (Rewrite=> *-lft-identity_binary64 (sin.f64 x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (cos.f64 x) (sin.f64 eps)) (-.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (sin.f64 x)))): 8 points increase in error, 5 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))): 103 points increase in error, 8 points decrease in error
Applied egg-rr0.3
\[\leadsto \mathsf{fma}\left(\cos x, \sin \varepsilon, \color{blue}{\frac{\left(-{\sin \varepsilon}^{2}\right) \cdot \sin x}{\cos \varepsilon + 1}}\right)
\]
Final simplification0.3
\[\leadsto \mathsf{fma}\left(\cos x, \sin \varepsilon, \frac{{\sin \varepsilon}^{2} \cdot \left(-\sin x\right)}{\cos \varepsilon + 1}\right)
\]