Average Error: 39.8 → 15.8
Time: 9.0s
Precision: 64
\[\cos \left(x + \varepsilon\right) - \cos x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -9.206885999863947166050042077156678743677 \cdot 10^{-7}:\\ \;\;\;\;1 \cdot \frac{{\left(\cos \varepsilon \cdot \cos x\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 \varepsilon \cdot \cos x\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right)}\\ \mathbf{elif}\;\varepsilon \le 2.130358258945720065918871810595192073379 \cdot 10^{-4}:\\ \;\;\;\;1 \cdot \left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(x \cdot \varepsilon + \frac{1}{2} \cdot {\varepsilon}^{2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(e^{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x}\right)\\ \end{array}\]
\cos \left(x + \varepsilon\right) - \cos x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -9.206885999863947166050042077156678743677 \cdot 10^{-7}:\\
\;\;\;\;1 \cdot \frac{{\left(\cos \varepsilon \cdot \cos x\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 \varepsilon \cdot \cos x\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right)}\\

\mathbf{elif}\;\varepsilon \le 2.130358258945720065918871810595192073379 \cdot 10^{-4}:\\
\;\;\;\;1 \cdot \left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(x \cdot \varepsilon + \frac{1}{2} \cdot {\varepsilon}^{2}\right)\right)\\

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

\end{array}
double f(double x, double eps) {
        double r46360 = x;
        double r46361 = eps;
        double r46362 = r46360 + r46361;
        double r46363 = cos(r46362);
        double r46364 = cos(r46360);
        double r46365 = r46363 - r46364;
        return r46365;
}
↓
double f(double x, double eps) {
        double r46366 = eps;
        double r46367 = -9.206885999863947e-07;
        bool r46368 = r46366 <= r46367;
        double r46369 = 1.0;
        double r46370 = cos(r46366);
        double r46371 = x;
        double r46372 = cos(r46371);
        double r46373 = r46370 * r46372;
        double r46374 = 3.0;
        double r46375 = pow(r46373, r46374);
        double r46376 = sin(r46371);
        double r46377 = sin(r46366);
        double r46378 = r46376 * r46377;
        double r46379 = r46378 + r46372;
        double r46380 = pow(r46379, r46374);
        double r46381 = r46375 - r46380;
        double r46382 = r46379 + r46373;
        double r46383 = r46379 * r46382;
        double r46384 = r46373 * r46373;
        double r46385 = r46383 + r46384;
        double r46386 = r46381 / r46385;
        double r46387 = r46369 * r46386;
        double r46388 = 0.000213035825894572;
        bool r46389 = r46366 <= r46388;
        double r46390 = 0.041666666666666664;
        double r46391 = 4.0;
        double r46392 = pow(r46366, r46391);
        double r46393 = r46390 * r46392;
        double r46394 = r46371 * r46366;
        double r46395 = 0.5;
        double r46396 = 2.0;
        double r46397 = pow(r46366, r46396);
        double r46398 = r46395 * r46397;
        double r46399 = r46394 + r46398;
        double r46400 = r46393 - r46399;
        double r46401 = r46369 * r46400;
        double r46402 = r46372 * r46370;
        double r46403 = r46402 - r46378;
        double r46404 = r46403 - r46372;
        double r46405 = exp(r46404);
        double r46406 = log(r46405);
        double r46407 = r46389 ? r46401 : r46406;
        double r46408 = r46368 ? r46387 : r46407;
        return r46408;
}

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 < -9.206885999863947e-07

    1. Initial program 31.2

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

    3. Applied cos-sum1.0

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

    5. Applied *-un-lft-identity1.0

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

    6. Applied *-un-lft-identity1.0

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

    7. Applied distribute-lft-out--1.0

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

    8. Simplified1.1

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

    10. Applied flip3--1.2

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

    11. Simplified1.2

      \[\leadsto 1 \cdot \frac{{\left(\cos \varepsilon \cdot \cos x\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 \varepsilon \cdot \cos x\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right)}}\]

    if -9.206885999863947e-07 < eps < 0.000213035825894572

    1. Initial program 49.4

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

    3. Applied cos-sum49.0

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

    5. Applied *-un-lft-identity49.0

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

    6. Applied *-un-lft-identity49.0

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

    7. Applied distribute-lft-out--49.0

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

    8. Simplified49.0

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

    9. Taylor expanded around 0 31.6

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

    if 0.000213035825894572 < eps

    1. Initial program 30.4

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

    3. Applied cos-sum0.9

      \[\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-exp0.9

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

    6. Applied add-log-exp1.0

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

    7. Applied add-log-exp1.1

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

    8. Applied diff-log1.2

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

    9. Applied diff-log1.3

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

    10. Simplified1.0

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

  4. Final simplification15.8

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -9.206885999863947166050042077156678743677 \cdot 10^{-7}:\\ \;\;\;\;1 \cdot \frac{{\left(\cos \varepsilon \cdot \cos x\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 \varepsilon \cdot \cos x\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right)}\\ \mathbf{elif}\;\varepsilon \le 2.130358258945720065918871810595192073379 \cdot 10^{-4}:\\ \;\;\;\;1 \cdot \left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(x \cdot \varepsilon + \frac{1}{2} \cdot {\varepsilon}^{2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(e^{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x}\right)\\ \end{array}\]

Reproduce

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