Initial program 36.6
\[\sin \left(x + \varepsilon\right) - \sin x
\]
Applied egg-rr21.4
\[\leadsto \color{blue}{\mathsf{fma}\left(\sin \varepsilon, \cos x, \sin x \cdot \cos \varepsilon\right)} - \sin x
\]
Applied egg-rr0.4
\[\leadsto \color{blue}{\mathsf{fma}\left(\sin \varepsilon, \cos x, \sin x \cdot \cos \varepsilon - \sin x\right)}
\]
Taylor expanded in x around inf 0.4
\[\leadsto \mathsf{fma}\left(\sin \varepsilon, \cos x, \color{blue}{\cos \varepsilon \cdot \sin x - \sin x}\right)
\]
Simplified0.4
\[\leadsto \mathsf{fma}\left(\sin \varepsilon, \cos x, \color{blue}{\left(\cos \varepsilon + -1\right) \cdot \sin x}\right)
\]
Proof
(*.f64 (+.f64 (cos.f64 eps) -1) (sin.f64 x)): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (cos.f64 eps) (Rewrite<= metadata-eval (neg.f64 1))) (sin.f64 x)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= sub-neg_binary64 (-.f64 (cos.f64 eps) 1)) (sin.f64 x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 x) (-.f64 (cos.f64 eps) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 x) (Rewrite=> sub-neg_binary64 (+.f64 (cos.f64 eps) (neg.f64 1)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (*.f64 (neg.f64 1) (sin.f64 x)))): 39 points increase in error, 35 points decrease in error
(+.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (*.f64 (Rewrite=> metadata-eval -1) (sin.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (Rewrite<= neg-mul-1_binary64 (neg.f64 (sin.f64 x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_binary64 (-.f64 (*.f64 (cos.f64 eps) (sin.f64 x)) (sin.f64 x))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.4
\[\leadsto \mathsf{fma}\left(\sin \varepsilon, \cos x, \color{blue}{\frac{\sin x \cdot \left(-{\sin \varepsilon}^{2}\right)}{\cos \varepsilon + 1}}\right)
\]
Final simplification0.4
\[\leadsto \mathsf{fma}\left(\sin \varepsilon, \cos x, \frac{\sin x \cdot \left(-{\sin \varepsilon}^{2}\right)}{\cos \varepsilon + 1}\right)
\]