Average Error: 36.7 → 15.5
Time: 31.5s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.1089423986131282 \cdot 10^{-63}:\\ \;\;\;\;\frac{\cos x \cdot \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(\tan \varepsilon + \tan x\right)\right) - \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\cos x \cdot \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right)}\\ \mathbf{elif}\;\varepsilon \le 5.810306508670788 \cdot 10^{-52}:\\ \;\;\;\;\varepsilon + \left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(\tan x - \tan \varepsilon\right) \cdot \left(\tan \varepsilon + \tan x\right)}{\tan x - \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.1089423986131282 \cdot 10^{-63}:\\
\;\;\;\;\frac{\cos x \cdot \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(\tan \varepsilon + \tan x\right)\right) - \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\cos x \cdot \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right)}\\

\mathbf{elif}\;\varepsilon \le 5.810306508670788 \cdot 10^{-52}:\\
\;\;\;\;\varepsilon + \left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\left(\tan x - \tan \varepsilon\right) \cdot \left(\tan \varepsilon + \tan x\right)}{\tan x - \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\

\end{array}
double f(double x, double eps) {
        double r3316628 = x;
        double r3316629 = eps;
        double r3316630 = r3316628 + r3316629;
        double r3316631 = tan(r3316630);
        double r3316632 = tan(r3316628);
        double r3316633 = r3316631 - r3316632;
        return r3316633;
}
↓
double f(double x, double eps) {
        double r3316634 = eps;
        double r3316635 = -2.1089423986131282e-63;
        bool r3316636 = r3316634 <= r3316635;
        double r3316637 = x;
        double r3316638 = cos(r3316637);
        double r3316639 = 1.0;
        double r3316640 = tan(r3316637);
        double r3316641 = tan(r3316634);
        double r3316642 = r3316640 * r3316641;
        double r3316643 = r3316642 * r3316642;
        double r3316644 = r3316639 - r3316643;
        double r3316645 = r3316641 + r3316640;
        double r3316646 = r3316644 * r3316645;
        double r3316647 = r3316638 * r3316646;
        double r3316648 = r3316639 - r3316642;
        double r3316649 = r3316644 * r3316648;
        double r3316650 = sin(r3316637);
        double r3316651 = r3316649 * r3316650;
        double r3316652 = r3316647 - r3316651;
        double r3316653 = r3316638 * r3316649;
        double r3316654 = r3316652 / r3316653;
        double r3316655 = 5.810306508670788e-52;
        bool r3316656 = r3316634 <= r3316655;
        double r3316657 = r3316637 * r3316634;
        double r3316658 = r3316637 + r3316634;
        double r3316659 = r3316657 * r3316658;
        double r3316660 = r3316634 + r3316659;
        double r3316661 = r3316640 - r3316641;
        double r3316662 = r3316661 * r3316645;
        double r3316663 = r3316662 / r3316661;
        double r3316664 = r3316663 / r3316648;
        double r3316665 = r3316664 - r3316640;
        double r3316666 = r3316656 ? r3316660 : r3316665;
        double r3316667 = r3316636 ? r3316654 : r3316666;
        return r3316667;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original36.7
Target14.9
Herbie15.5
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 3 regimes

  2. if eps < -2.1089423986131282e-63

    1. Initial program 30.4

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

    3. Applied tan-sum5.3

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm

    5. Applied flip--5.4

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

    6. Applied associate-/r/5.4

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

    8. Applied tan-quot5.4

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

    9. Applied flip-+5.4

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

    10. Applied frac-times5.4

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

    11. Applied frac-sub5.4

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

    if -2.1089423986131282e-63 < eps < 5.810306508670788e-52

    1. Initial program 47.0

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

    2. Taylor expanded around 0 31.6

      \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]

    3. Simplified31.5

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

    if 5.810306508670788e-52 < eps

    1. Initial program 29.1

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

    3. Applied tan-sum3.8

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm

    5. Applied flip-+3.9

      \[\leadsto \frac{\color{blue}{\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\tan x - \tan \varepsilon}}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]

    6. Simplified3.9

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

  4. Final simplification15.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.1089423986131282 \cdot 10^{-63}:\\ \;\;\;\;\frac{\cos x \cdot \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(\tan \varepsilon + \tan x\right)\right) - \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\cos x \cdot \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right)}\\ \mathbf{elif}\;\varepsilon \le 5.810306508670788 \cdot 10^{-52}:\\ \;\;\;\;\varepsilon + \left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(\tan x - \tan \varepsilon\right) \cdot \left(\tan \varepsilon + \tan x\right)}{\tan x - \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

Reproduce

herbie shell --seed 2019168 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))