Average Error: 36.7 → 15.3
Time: 12.1s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -8.40451542959736362 \cdot 10^{-107} \lor \neg \left(\varepsilon \le 1.5951375447724633 \cdot 10^{-59}\right):\\ \;\;\;\;1 \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \sin \varepsilon\right)}{\cos \varepsilon}} + \tan x \cdot \left(\tan \varepsilon \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \sin \varepsilon\right)}{\cos \varepsilon}} - 1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -8.40451542959736362 \cdot 10^{-107} \lor \neg \left(\varepsilon \le 1.5951375447724633 \cdot 10^{-59}\right):\\
\;\;\;\;1 \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \sin \varepsilon\right)}{\cos \varepsilon}} + \tan x \cdot \left(\tan \varepsilon \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \sin \varepsilon\right)}{\cos \varepsilon}} - 1\right)\\

\mathbf{else}:\\
\;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\

\end{array}
double f(double x, double eps) {
        double r133093 = x;
        double r133094 = eps;
        double r133095 = r133093 + r133094;
        double r133096 = tan(r133095);
        double r133097 = tan(r133093);
        double r133098 = r133096 - r133097;
        return r133098;
}
↓
double f(double x, double eps) {
        double r133099 = eps;
        double r133100 = -8.404515429597364e-107;
        bool r133101 = r133099 <= r133100;
        double r133102 = 1.5951375447724633e-59;
        bool r133103 = r133099 <= r133102;
        double r133104 = !r133103;
        bool r133105 = r133101 || r133104;
        double r133106 = 1.0;
        double r133107 = x;
        double r133108 = tan(r133107);
        double r133109 = tan(r133099);
        double r133110 = r133108 + r133109;
        double r133111 = r133108 * r133109;
        double r133112 = sin(r133099);
        double r133113 = r133108 * r133112;
        double r133114 = r133111 * r133113;
        double r133115 = cos(r133099);
        double r133116 = r133114 / r133115;
        double r133117 = r133106 - r133116;
        double r133118 = r133110 / r133117;
        double r133119 = r133106 * r133118;
        double r133120 = r133109 * r133118;
        double r133121 = r133120 - r133106;
        double r133122 = r133108 * r133121;
        double r133123 = r133119 + r133122;
        double r133124 = r133099 * r133107;
        double r133125 = r133107 + r133099;
        double r133126 = r133124 * r133125;
        double r133127 = r133126 + r133099;
        double r133128 = r133105 ? r133123 : r133127;
        return r133128;
}

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

Derivation

  1. Split input into 2 regimes

  2. if eps < -8.404515429597364e-107 or 1.5951375447724633e-59 < eps

    1. Initial program 30.2

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

    3. Applied tan-sum6.3

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

    5. Applied flip--6.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/6.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. Simplified6.4

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{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\]
    8. Using strategy rm

    9. Applied tan-quot6.4

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

    10. Applied associate-*r/6.4

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

    11. Applied associate-*r/6.4

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

    13. Applied distribute-rgt-in6.4

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

    14. Applied associate--l+6.4

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

    15. Simplified6.4

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

    if -8.404515429597364e-107 < eps < 1.5951375447724633e-59

    1. Initial program 48.1

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

    2. Taylor expanded around 0 31.0

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

    3. Simplified30.8

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

  4. Final simplification15.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -8.40451542959736362 \cdot 10^{-107} \lor \neg \left(\varepsilon \le 1.5951375447724633 \cdot 10^{-59}\right):\\ \;\;\;\;1 \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \sin \varepsilon\right)}{\cos \varepsilon}} + \tan x \cdot \left(\tan \varepsilon \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \sin \varepsilon\right)}{\cos \varepsilon}} - 1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \end{array}\]

Reproduce

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

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

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