Average Error: 40.1 → 16.4
Time: 22.4s
Precision: 64
\[\cos \left(x + \varepsilon\right) - \cos x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -3.968394187965513502976952269971078202104 \cdot 10^{-8}:\\ \;\;\;\;\frac{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon\right) - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\\ \mathbf{elif}\;\varepsilon \le 1.604210383402189457246122487182882210277 \cdot 10^{-7}:\\ \;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \frac{1}{2} \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\cos x \cdot \cos \varepsilon - \frac{\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) - \cos x \cdot \cos x}{\sin x \cdot \sin \varepsilon - \cos x}\\ \end{array}\]
\cos \left(x + \varepsilon\right) - \cos x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -3.968394187965513502976952269971078202104 \cdot 10^{-8}:\\
\;\;\;\;\frac{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon\right) - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\\

\mathbf{elif}\;\varepsilon \le 1.604210383402189457246122487182882210277 \cdot 10^{-7}:\\
\;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \frac{1}{2} \cdot \varepsilon\right)\\

\mathbf{else}:\\
\;\;\;\;\cos x \cdot \cos \varepsilon - \frac{\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) - \cos x \cdot \cos x}{\sin x \cdot \sin \varepsilon - \cos x}\\

\end{array}
double f(double x, double eps) {
        double r58902 = x;
        double r58903 = eps;
        double r58904 = r58902 + r58903;
        double r58905 = cos(r58904);
        double r58906 = cos(r58902);
        double r58907 = r58905 - r58906;
        return r58907;
}
↓
double f(double x, double eps) {
        double r58908 = eps;
        double r58909 = -3.9683941879655135e-08;
        bool r58910 = r58908 <= r58909;
        double r58911 = x;
        double r58912 = cos(r58911);
        double r58913 = r58912 * r58912;
        double r58914 = r58913 * r58912;
        double r58915 = cos(r58908);
        double r58916 = r58915 * r58915;
        double r58917 = r58916 * r58915;
        double r58918 = r58914 * r58917;
        double r58919 = sin(r58911);
        double r58920 = sin(r58908);
        double r58921 = r58919 * r58920;
        double r58922 = r58921 + r58912;
        double r58923 = 3.0;
        double r58924 = pow(r58922, r58923);
        double r58925 = r58918 - r58924;
        double r58926 = r58912 * r58915;
        double r58927 = r58922 + r58926;
        double r58928 = r58922 * r58927;
        double r58929 = r58926 * r58926;
        double r58930 = r58928 + r58929;
        double r58931 = r58925 / r58930;
        double r58932 = 1.6042103834021895e-07;
        bool r58933 = r58908 <= r58932;
        double r58934 = 0.16666666666666666;
        double r58935 = pow(r58911, r58923);
        double r58936 = r58934 * r58935;
        double r58937 = r58936 - r58911;
        double r58938 = 0.5;
        double r58939 = r58938 * r58908;
        double r58940 = r58937 - r58939;
        double r58941 = r58908 * r58940;
        double r58942 = r58921 * r58921;
        double r58943 = r58942 - r58913;
        double r58944 = r58921 - r58912;
        double r58945 = r58943 / r58944;
        double r58946 = r58926 - r58945;
        double r58947 = r58933 ? r58941 : r58946;
        double r58948 = r58910 ? r58931 : r58947;
        return r58948;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Split input into 3 regimes

  2. if eps < -3.9683941879655135e-08

    1. Initial program 30.9

      \[\cos \left(x + \varepsilon\right) - \cos x\]
    2. Using strategy rm

    3. Applied cos-sum1.2

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]

    4. Applied associate--l-1.2

      \[\leadsto \color{blue}{\cos x \cdot \cos \varepsilon - \left(\sin x \cdot \sin \varepsilon + \cos x\right)}\]
    5. Using strategy rm

    6. Applied flip3--1.4

      \[\leadsto \color{blue}{\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right) + \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos x\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos x\right)\right)}}\]

    7. Simplified1.4

      \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\color{blue}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}\]
    8. Using strategy rm

    9. Applied add-cbrt-cube1.7

      \[\leadsto \frac{{\left(\cos x \cdot \color{blue}{\sqrt[3]{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}}\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\]

    10. Applied add-cbrt-cube1.8

      \[\leadsto \frac{{\left(\color{blue}{\sqrt[3]{\left(\cos x \cdot \cos x\right) \cdot \cos x}} \cdot \sqrt[3]{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\]

    11. Applied cbrt-unprod1.7

      \[\leadsto \frac{{\color{blue}{\left(\sqrt[3]{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon\right)}\right)}}^{3} - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\]

    12. Applied rem-cube-cbrt1.4

      \[\leadsto \frac{\color{blue}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon\right)} - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\]

    if -3.9683941879655135e-08 < eps < 1.6042103834021895e-07

    1. Initial program 49.6

      \[\cos \left(x + \varepsilon\right) - \cos x\]
    2. Using strategy rm

    3. Applied cos-sum49.2

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]

    4. Applied associate--l-49.2

      \[\leadsto \color{blue}{\cos x \cdot \cos \varepsilon - \left(\sin x \cdot \sin \varepsilon + \cos x\right)}\]

    5. Taylor expanded around 0 32.0

      \[\leadsto \color{blue}{\frac{1}{6} \cdot \left({x}^{3} \cdot \varepsilon\right) - \left(x \cdot \varepsilon + \frac{1}{2} \cdot {\varepsilon}^{2}\right)}\]

    6. Simplified32.0

      \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \frac{1}{2} \cdot \varepsilon\right)}\]

    if 1.6042103834021895e-07 < eps

    1. Initial program 30.9

      \[\cos \left(x + \varepsilon\right) - \cos x\]
    2. Using strategy rm

    3. Applied cos-sum1.1

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]

    4. Applied associate--l-1.1

      \[\leadsto \color{blue}{\cos x \cdot \cos \varepsilon - \left(\sin x \cdot \sin \varepsilon + \cos x\right)}\]
    5. Using strategy rm

    6. Applied flip-+1.2

      \[\leadsto \cos x \cdot \cos \varepsilon - \color{blue}{\frac{\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) - \cos x \cdot \cos x}{\sin x \cdot \sin \varepsilon - \cos x}}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification16.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -3.968394187965513502976952269971078202104 \cdot 10^{-8}:\\ \;\;\;\;\frac{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon\right) - {\left(\sin x \cdot \sin \varepsilon + \cos x\right)}^{3}}{\left(\sin x \cdot \sin \varepsilon + \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon + \cos x\right) + \cos x \cdot \cos \varepsilon\right) + \left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\\ \mathbf{elif}\;\varepsilon \le 1.604210383402189457246122487182882210277 \cdot 10^{-7}:\\ \;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \frac{1}{2} \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\cos x \cdot \cos \varepsilon - \frac{\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) - \cos x \cdot \cos x}{\sin x \cdot \sin \varepsilon - \cos x}\\ \end{array}\]

Reproduce

herbie shell --seed 2019291 
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  :precision binary64
  (- (cos (+ x eps)) (cos x)))