- Split input into 2 regimes
if (- (* (cos x) (cos eps)) (fma (sin eps) (sin x) (cos x))) < -0.025003930529898438 or 1.725264261496313e-07 < (- (* (cos x) (cos eps)) (fma (sin eps) (sin x) (cos x)))
Initial program 30.2
\[\cos \left(x + \varepsilon\right) - \cos x\]
- Using strategy
rm Applied cos-sum0.6
\[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
if -0.025003930529898438 < (- (* (cos x) (cos eps)) (fma (sin eps) (sin x) (cos x))) < 1.725264261496313e-07
Initial program 47.3
\[\cos \left(x + \varepsilon\right) - \cos x\]
- Using strategy
rm Applied diff-cos36.4
\[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right)}\]
Applied simplify1.1
\[\leadsto -2 \cdot \color{blue}{\left(\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{x + \left(\varepsilon + x\right)}{2}\right)\right)}\]
- Recombined 2 regimes into one program.
Applied simplify0.9
\[\leadsto \color{blue}{\begin{array}{l}
\mathbf{if}\;\cos \varepsilon \cdot \cos x - (\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_* \le -0.025003930529898438 \lor \neg \left(\cos \varepsilon \cdot \cos x - (\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_* \le 1.725264261496313 \cdot 10^{-07}\right):\\
\;\;\;\;\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) - \cos x\\
\mathbf{else}:\\
\;\;\;\;\left(\sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right) \cdot -2\\
\end{array}}\]