if eps < -8.102966659834604e-08

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   29.7
2. Using strategy rm
   29.7
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.1
4. Using strategy rm
   1.1
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.1
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.1
7. Using strategy rm
   1.1
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.6
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.7
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.7
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.7
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.4

---

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.1

if -8.102966659834604e-08 < eps < 0.0009667373424041872

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   49.7
2. Using strategy rm
   49.7
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\]
   49.3
4. Using strategy rm
   49.3
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\]
   49.3
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

if 0.0009667373424041872 < eps

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   29.2
2. Using strategy rm
   29.2
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\]
   0.8
4. Using strategy rm
   0.8
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\]
   0.8
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)}\]
   0.8
7. Using strategy rm
   0.8
8. Applied fma-def to get
   \[\color{red}{\cos x \cdot \cos \varepsilon + \left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)} \leadsto \color{blue}{(\left(\cos x\right) * \left(\cos \varepsilon\right) + \left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right))_*}\]
   0.8