- Split input into 3 regimes
if (- (* 1/6 (* eps (pow x 3))) (+ (* eps x) (* 1/2 (pow eps 2)))) < -715.475509890268
Initial program 26.4
\[\cos \left(x + \varepsilon\right) - \cos x\]
- Using strategy
rm Applied cos-sum15.0
\[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
- Using strategy
rm Applied add-cbrt-cube15.0
\[\leadsto \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \color{blue}{\sqrt[3]{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}}\right) - \cos x\]
Applied add-cbrt-cube15.0
\[\leadsto \left(\cos x \cdot \cos \varepsilon - \color{blue}{\sqrt[3]{\left(\sin x \cdot \sin x\right) \cdot \sin x}} \cdot \sqrt[3]{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}\right) - \cos x\]
Applied cbrt-unprod15.0
\[\leadsto \left(\cos x \cdot \cos \varepsilon - \color{blue}{\sqrt[3]{\left(\left(\sin x \cdot \sin x\right) \cdot \sin x\right) \cdot \left(\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon\right)}}\right) - \cos x\]
Simplified15.0
\[\leadsto \left(\cos x \cdot \cos \varepsilon - \sqrt[3]{\color{blue}{{\left(\sin \varepsilon \cdot \sin x\right)}^{3}}}\right) - \cos x\]
if -715.475509890268 < (- (* 1/6 (* eps (pow x 3))) (+ (* eps x) (* 1/2 (pow eps 2)))) < 2.706880890868039e-44
Initial program 39.9
\[\cos \left(x + \varepsilon\right) - \cos x\]
Taylor expanded around 0 8.8
\[\leadsto \color{blue}{\frac{1}{6} \cdot \left(\varepsilon \cdot {x}^{3}\right) - \left(\varepsilon \cdot x + \frac{1}{2} \cdot {\varepsilon}^{2}\right)}\]
if 2.706880890868039e-44 < (- (* 1/6 (* eps (pow x 3))) (+ (* eps x) (* 1/2 (pow eps 2))))
Initial program 59.3
\[\cos \left(x + \varepsilon\right) - \cos x\]
- Using strategy
rm Applied cos-sum22.8
\[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
- Using strategy
rm Applied add-cube-cbrt23.1
\[\leadsto \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \color{blue}{\left(\left(\sqrt[3]{\sin \varepsilon} \cdot \sqrt[3]{\sin \varepsilon}\right) \cdot \sqrt[3]{\sin \varepsilon}\right)}\right) - \cos x\]
Applied associate-*r*23.1
\[\leadsto \left(\cos x \cdot \cos \varepsilon - \color{blue}{\left(\sin x \cdot \left(\sqrt[3]{\sin \varepsilon} \cdot \sqrt[3]{\sin \varepsilon}\right)\right) \cdot \sqrt[3]{\sin \varepsilon}}\right) - \cos x\]
- Recombined 3 regimes into one program.
Final simplification15.5
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\varepsilon \cdot {x}^{3}\right) \cdot \frac{1}{6} - \left({\varepsilon}^{2} \cdot \frac{1}{2} + x \cdot \varepsilon\right) \le -715.475509890268:\\
\;\;\;\;\left(\cos x \cdot \cos \varepsilon - \sqrt[3]{{\left(\sin \varepsilon \cdot \sin x\right)}^{3}}\right) - \cos x\\
\mathbf{elif}\;\left(\varepsilon \cdot {x}^{3}\right) \cdot \frac{1}{6} - \left({\varepsilon}^{2} \cdot \frac{1}{2} + x \cdot \varepsilon\right) \le 2.706880890868039 \cdot 10^{-44}:\\
\;\;\;\;\left(\varepsilon \cdot {x}^{3}\right) \cdot \frac{1}{6} - \left({\varepsilon}^{2} \cdot \frac{1}{2} + x \cdot \varepsilon\right)\\
\mathbf{else}:\\
\;\;\;\;\left(\cos x \cdot \cos \varepsilon - \sqrt[3]{\sin \varepsilon} \cdot \left(\sin x \cdot \left(\sqrt[3]{\sin \varepsilon} \cdot \sqrt[3]{\sin \varepsilon}\right)\right)\right) - \cos x\\
\end{array}\]