if eps < -5.084423344895139e-11 or 0.056213882732527594 < eps

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   30.0
2. Using strategy rm
   30.0
3. Applied cos-sum to get
   \[\color{red}{\cos \left(x + \varepsilon\right)} - \cos x \leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
   1.2
4. Using strategy rm
   1.2
5. Applied sub-neg to get
   \[\color{red}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x \leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon + \left(-\sin x \cdot \sin \varepsilon\right)\right)} - \cos x\]
   1.2
6. Applied associate--l+ to get
   \[\color{red}{\left(\cos x \cdot \cos \varepsilon + \left(-\sin x \cdot \sin \varepsilon\right)\right) - \cos x} \leadsto \color{blue}{\cos x \cdot \cos \varepsilon + \left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}\]
   1.2
7. Using strategy rm
   1.2
8. Applied flip-+ to get
   \[\color{red}{\cos x \cdot \cos \varepsilon + \left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)} \leadsto \color{blue}{\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{\cos x \cdot \cos \varepsilon - \left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}}\]
   1.7
9. Applied simplify to get
   \[\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{\color{red}{\cos x \cdot \cos \varepsilon - \left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}} \leadsto \frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{\color{blue}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_* - \sin x \cdot \left(-\sin \varepsilon\right)}}\]
   1.8
10. Applied taylor to get
    \[\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_* - \sin x \cdot \left(-\sin \varepsilon\right)} \leadsto \frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_* - \sin x \cdot \left(-\sin \varepsilon\right)}\]
    1.8
11. Taylor expanded around 0 to get
    \[\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{\color{red}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_*} - \sin x \cdot \left(-\sin \varepsilon\right)} \leadsto \frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{\color{blue}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_*} - \sin x \cdot \left(-\sin \varepsilon\right)}\]
    1.8
12. Applied simplify to get
    \[\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^2 - {\left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}^2}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_* - \sin x \cdot \left(-\sin \varepsilon\right)} \leadsto \frac{\sin \varepsilon \cdot \left(-\sin x\right) - \left(\cos x - \cos \varepsilon \cdot \cos x\right)}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_* - \sin \varepsilon \cdot \left(-\sin x\right)} \cdot \left(\cos \varepsilon \cdot \cos x - \left(\sin \varepsilon \cdot \left(-\sin x\right) - \cos x\right)\right)\]
    1.5

---

13. Applied final simplification
14. Applied simplify to get
    \[\color{red}{\frac{\sin \varepsilon \cdot \left(-\sin x\right) - \left(\cos x - \cos \varepsilon \cdot \cos x\right)}{(\left(\cos \varepsilon\right) * \left(\cos x\right) + \left(\cos x\right))_* - \sin \varepsilon \cdot \left(-\sin x\right)} \cdot \left(\cos \varepsilon \cdot \cos x - \left(\sin \varepsilon \cdot \left(-\sin x\right) - \cos x\right)\right)} \leadsto \color{blue}{\frac{(\left(-\sin \varepsilon\right) * \left(\sin x\right) + \left(\cos x \cdot \cos \varepsilon\right))_* - \cos x}{\frac{(\left(\cos x\right) * \left(\cos \varepsilon\right) + \left(\cos x\right))_* - \left(-\sin x \cdot \sin \varepsilon\right)}{(\left(\cos x\right) * \left(\cos \varepsilon\right) + \left(\cos x\right))_* - \left(-\sin x \cdot \sin \varepsilon\right)}}}\]
    1.2

if -5.084423344895139e-11 < eps < 0.056213882732527594

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   49.1
2. Using strategy rm
   49.1
3. Applied cos-sum to get
   \[\color{red}{\cos \left(x + \varepsilon\right)} - \cos x \leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
   48.7
4. Using strategy rm
   48.7
5. Applied add-cube-cbrt to get
   \[\left(\cos x \cdot \cos \varepsilon - \color{red}{\sin x \cdot \sin \varepsilon}\right) - \cos x \leadsto \left(\cos x \cdot \cos \varepsilon - \color{blue}{{\left(\sqrt[3]{\sin x \cdot \sin \varepsilon}\right)}^3}\right) - \cos x\]
   48.7
6. Applied taylor to get
   \[\left(\cos x \cdot \cos \varepsilon - {\left(\sqrt[3]{\sin x \cdot \sin \varepsilon}\right)}^3\right) - \cos x \leadsto \frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot \sin x\right) - \left(\frac{1}{2} \cdot {\varepsilon}^2 + \varepsilon \cdot \sin x\right)\]
   0.1
7. Taylor expanded around 0 to get
   \[\color{red}{\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot \sin x\right) - \left(\frac{1}{2} \cdot {\varepsilon}^2 + \varepsilon \cdot \sin x\right)} \leadsto \color{blue}{\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot \sin x\right) - \left(\frac{1}{2} \cdot {\varepsilon}^2 + \varepsilon \cdot \sin x\right)}\]
   0.1
8. Applied simplify to get
   \[\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot \sin x\right) - \left(\frac{1}{2} \cdot {\varepsilon}^2 + \varepsilon \cdot \sin x\right) \leadsto \frac{1}{6} \cdot \left({\varepsilon}^3 \cdot \sin x\right) - \varepsilon \cdot \left(\sin x + \frac{1}{2} \cdot \varepsilon\right)\]
   0.1

---

9. Applied final simplification
10. Applied simplify to get
    \[\color{red}{\frac{1}{6} \cdot \left({\varepsilon}^3 \cdot \sin x\right) - \varepsilon \cdot \left(\sin x + \frac{1}{2} \cdot \varepsilon\right)} \leadsto \color{blue}{{\varepsilon}^3 \cdot \left(\frac{1}{6} \cdot \sin x\right) - \varepsilon \cdot (\frac{1}{2} * \varepsilon + \left(\sin x\right))_*}\]
    0.1