Average Error: 39.6 → 16.0
Time: 13.0s
Precision: 64
\[\cos \left(x + \varepsilon\right) - \cos x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le \frac{-5117057790700741}{1208925819614629174706176} \lor \neg \left(\varepsilon \le \frac{8032266710981389}{37778931862957161709568}\right):\\ \;\;\;\;\cos \varepsilon \cdot \cos x - \left(\sin x \cdot \sin \varepsilon + \cos x\right)\\ \mathbf{else}:\\ \;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)\\ \end{array}\]
\cos \left(x + \varepsilon\right) - \cos x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le \frac{-5117057790700741}{1208925819614629174706176} \lor \neg \left(\varepsilon \le \frac{8032266710981389}{37778931862957161709568}\right):\\
\;\;\;\;\cos \varepsilon \cdot \cos x - \left(\sin x \cdot \sin \varepsilon + \cos x\right)\\

\mathbf{else}:\\
\;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)\\

\end{array}
double f(double x, double eps) {
        double r38722 = x;
        double r38723 = eps;
        double r38724 = r38722 + r38723;
        double r38725 = cos(r38724);
        double r38726 = cos(r38722);
        double r38727 = r38725 - r38726;
        return r38727;
}
↓
double f(double x, double eps) {
        double r38728 = eps;
        double r38729 = -5117057790700741.0;
        double r38730 = 1.2089258196146292e+24;
        double r38731 = r38729 / r38730;
        bool r38732 = r38728 <= r38731;
        double r38733 = 8032266710981389.0;
        double r38734 = 3.777893186295716e+22;
        double r38735 = r38733 / r38734;
        bool r38736 = r38728 <= r38735;
        double r38737 = !r38736;
        bool r38738 = r38732 || r38737;
        double r38739 = cos(r38728);
        double r38740 = x;
        double r38741 = cos(r38740);
        double r38742 = r38739 * r38741;
        double r38743 = sin(r38740);
        double r38744 = sin(r38728);
        double r38745 = r38743 * r38744;
        double r38746 = r38745 + r38741;
        double r38747 = r38742 - r38746;
        double r38748 = 0.16666666666666666;
        double r38749 = 3.0;
        double r38750 = pow(r38740, r38749);
        double r38751 = r38748 * r38750;
        double r38752 = r38751 - r38740;
        double r38753 = 0.5;
        double r38754 = r38728 * r38753;
        double r38755 = r38752 - r38754;
        double r38756 = r38728 * r38755;
        double r38757 = r38738 ? r38747 : r38756;
        return r38757;
}

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 < -4.2327309977810814e-09

    1. Initial program 30.7

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

    3. Applied cos-sum1.3

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

    5. Applied sub-neg1.3

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

    6. Applied associate--l+1.3

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

    8. Applied add-log-exp1.4

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

    9. Applied add-log-exp1.4

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

    10. Applied neg-log1.5

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

    11. Applied diff-log1.5

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

    12. Applied add-log-exp1.6

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

    13. Applied sum-log1.7

      \[\leadsto \color{blue}{\log \left(e^{\cos x \cdot \cos \varepsilon} \cdot \frac{\frac{1}{e^{\sin x \cdot \sin \varepsilon}}}{e^{\cos x}}\right)}\]

    14. Simplified1.4

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

    if -4.2327309977810814e-09 < eps < 2.126123295417241e-07

    1. Initial program 49.1

      \[\cos \left(x + \varepsilon\right) - \cos x\]

    2. Taylor expanded around 0 31.5

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

    3. Simplified31.5

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

    if 2.126123295417241e-07 < eps

    1. Initial program 30.3

      \[\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. Using strategy rm

    5. Applied add-log-exp1.2

      \[\leadsto \left(\cos x \cdot \cos \varepsilon - \color{blue}{\log \left(e^{\sin x \cdot \sin \varepsilon}\right)}\right) - \cos x\]
    6. Using strategy rm

    7. Applied flip--1.7

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

    8. Simplified1.3

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

    9. Simplified1.2

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

  4. Final simplification16.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le \frac{-5117057790700741}{1208925819614629174706176} \lor \neg \left(\varepsilon \le \frac{8032266710981389}{37778931862957161709568}\right):\\ \;\;\;\;\cos \varepsilon \cdot \cos x - \left(\sin x \cdot \sin \varepsilon + \cos x\right)\\ \mathbf{else}:\\ \;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)\\ \end{array}\]

Reproduce

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