if eps < -6.974478371048821e-14

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   30.9
2. Using strategy rm
   30.9
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\]
   2.0
4. Using strategy rm
   2.0
5. Applied log1p-expm1-u to get
   \[\color{red}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x \leadsto \color{blue}{\log_* (1 + (e^{\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon} - 1)^*)} - \cos x\]
   2.1

if -6.974478371048821e-14 < eps < 0.00018005451351709028

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   44.6
2. Using strategy rm
   44.6
3. Applied add-sqr-sqrt to get
   \[\cos \left(x + \varepsilon\right) - \color{red}{\cos x} \leadsto \cos \left(x + \varepsilon\right) - \color{blue}{{\left(\sqrt{\cos x}\right)}^2}\]
   44.6
4. Applied add-sqr-sqrt to get
   \[\color{red}{\cos \left(x + \varepsilon\right)} - {\left(\sqrt{\cos x}\right)}^2 \leadsto \color{blue}{{\left(\sqrt{\cos \left(x + \varepsilon\right)}\right)}^2} - {\left(\sqrt{\cos x}\right)}^2\]
   44.6
5. Applied difference-of-squares to get
   \[\color{red}{{\left(\sqrt{\cos \left(x + \varepsilon\right)}\right)}^2 - {\left(\sqrt{\cos x}\right)}^2} \leadsto \color{blue}{\left(\sqrt{\cos \left(x + \varepsilon\right)} + \sqrt{\cos x}\right) \cdot \left(\sqrt{\cos \left(x + \varepsilon\right)} - \sqrt{\cos x}\right)}\]
   44.6
6. Applied taylor to get
   \[\left(\sqrt{\cos \left(x + \varepsilon\right)} + \sqrt{\cos x}\right) \cdot \left(\sqrt{\cos \left(x + \varepsilon\right)} - \sqrt{\cos x}\right) \leadsto \left(\sqrt{\cos \left(x + \varepsilon\right)} + \sqrt{\cos x}\right) \cdot \left(-\left(\frac{1}{4} \cdot {\varepsilon}^2 + \left(\frac{1}{16} \cdot \left({\varepsilon}^{3} \cdot {x}^{3}\right) + \frac{1}{2} \cdot \left(\varepsilon \cdot x\right)\right)\right)\right)\]
   10.2
7. Taylor expanded around 0 to get
   \[\left(\sqrt{\cos \left(x + \varepsilon\right)} + \sqrt{\cos x}\right) \cdot \color{red}{\left(-\left(\frac{1}{4} \cdot {\varepsilon}^2 + \left(\frac{1}{16} \cdot \left({\varepsilon}^{3} \cdot {x}^{3}\right) + \frac{1}{2} \cdot \left(\varepsilon \cdot x\right)\right)\right)\right)} \leadsto \left(\sqrt{\cos \left(x + \varepsilon\right)} + \sqrt{\cos x}\right) \cdot \color{blue}{\left(-\left(\frac{1}{4} \cdot {\varepsilon}^2 + \left(\frac{1}{16} \cdot \left({\varepsilon}^{3} \cdot {x}^{3}\right) + \frac{1}{2} \cdot \left(\varepsilon \cdot x\right)\right)\right)\right)}\]
   10.2
8. Applied simplify to get
   \[\left(\sqrt{\cos \left(x + \varepsilon\right)} + \sqrt{\cos x}\right) \cdot \left(-\left(\frac{1}{4} \cdot {\varepsilon}^2 + \left(\frac{1}{16} \cdot \left({\varepsilon}^{3} \cdot {x}^{3}\right) + \frac{1}{2} \cdot \left(\varepsilon \cdot x\right)\right)\right)\right) \leadsto \left(\sqrt{\cos \left(x + \varepsilon\right)} + \sqrt{\cos x}\right) \cdot \left(\left(\left(-\frac{1}{4}\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \left(-\frac{1}{2}\right) \cdot \left(\varepsilon \cdot x\right)\right) + \left({\varepsilon}^3 \cdot \frac{1}{16}\right) \cdot \left(-{x}^3\right)\right)\]
   10.2

---

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

if 0.00018005451351709028 < eps

1. Started with
   \[\cos \left(x + \varepsilon\right) - \cos x\]
   30.6
2. Using strategy rm
   30.6
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.9
4. Using strategy rm
   0.9
5. Applied flip3-- to get
   \[\color{red}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x \leadsto \color{blue}{\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^2 + \left({\left(\sin x \cdot \sin \varepsilon\right)}^2 + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right)}} - \cos x\]
   1.1
6. Applied simplify to get
   \[\frac{\color{red}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}}}{{\left(\cos x \cdot \cos \varepsilon\right)}^2 + \left({\left(\sin x \cdot \sin \varepsilon\right)}^2 + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right)} - \cos x \leadsto \frac{\color{blue}{{\left(\cos \varepsilon \cdot \cos x\right)}^3 - {\left(\sin x \cdot \sin \varepsilon\right)}^3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^2 + \left({\left(\sin x \cdot \sin \varepsilon\right)}^2 + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right)} - \cos x\]
   1.1