Average Error: 37.0 → 14.4
Time: 33.7s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.411031888842386686832542331338415511525 \cdot 10^{-53}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \sin x \cdot \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right)}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 8.988728992921953113303178437386507341613 \cdot 10^{-40}:\\ \;\;\;\;\frac{1}{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \varepsilon\right)\right) + \left(\varepsilon \cdot \left(x \cdot \varepsilon\right) + \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \sin x \cdot \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right)}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.411031888842386686832542331338415511525 \cdot 10^{-53}:\\
\;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \sin x \cdot \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right)}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}\\

\mathbf{elif}\;\varepsilon \le 8.988728992921953113303178437386507341613 \cdot 10^{-40}:\\
\;\;\;\;\frac{1}{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \varepsilon\right)\right) + \left(\varepsilon \cdot \left(x \cdot \varepsilon\right) + \varepsilon\right)\\

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

\end{array}
double f(double x, double eps) {
        double r6160149 = x;
        double r6160150 = eps;
        double r6160151 = r6160149 + r6160150;
        double r6160152 = tan(r6160151);
        double r6160153 = tan(r6160149);
        double r6160154 = r6160152 - r6160153;
        return r6160154;
}
↓
double f(double x, double eps) {
        double r6160155 = eps;
        double r6160156 = -1.4110318888423867e-53;
        bool r6160157 = r6160155 <= r6160156;
        double r6160158 = x;
        double r6160159 = cos(r6160158);
        double r6160160 = tan(r6160155);
        double r6160161 = tan(r6160158);
        double r6160162 = r6160160 + r6160161;
        double r6160163 = r6160159 * r6160162;
        double r6160164 = sin(r6160158);
        double r6160165 = 1.0;
        double r6160166 = sin(r6160155);
        double r6160167 = r6160161 * r6160166;
        double r6160168 = cos(r6160155);
        double r6160169 = r6160167 / r6160168;
        double r6160170 = r6160165 - r6160169;
        double r6160171 = r6160164 * r6160170;
        double r6160172 = r6160163 - r6160171;
        double r6160173 = r6160170 * r6160159;
        double r6160174 = r6160172 / r6160173;
        double r6160175 = 8.988728992921953e-40;
        bool r6160176 = r6160155 <= r6160175;
        double r6160177 = 0.3333333333333333;
        double r6160178 = r6160155 * r6160155;
        double r6160179 = r6160155 * r6160178;
        double r6160180 = r6160177 * r6160179;
        double r6160181 = r6160158 * r6160155;
        double r6160182 = r6160155 * r6160181;
        double r6160183 = r6160182 + r6160155;
        double r6160184 = r6160180 + r6160183;
        double r6160185 = r6160176 ? r6160184 : r6160174;
        double r6160186 = r6160157 ? r6160174 : r6160185;
        return r6160186;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original37.0
Target15.1
Herbie14.4
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 2 regimes

  2. if eps < -1.4110318888423867e-53 or 8.988728992921953e-40 < eps

    1. Initial program 30.1

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

    3. Applied tan-sum3.9

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

    5. Applied tan-quot3.9

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

    6. Applied associate-*r/3.9

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

    8. Applied tan-quot3.9

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

    9. Applied frac-sub3.9

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

    if -1.4110318888423867e-53 < eps < 8.988728992921953e-40

    1. Initial program 46.4

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

    3. Applied tan-sum46.4

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

    5. Applied tan-quot46.4

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

    6. Applied associate-*r/46.4

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

    8. Applied flip3--46.4

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

    9. Applied associate-/r/46.4

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

    10. Simplified46.4

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

    11. Taylor expanded around 0 28.1

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

    12. Simplified28.7

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

  4. Final simplification14.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.411031888842386686832542331338415511525 \cdot 10^{-53}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \sin x \cdot \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right)}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 8.988728992921953113303178437386507341613 \cdot 10^{-40}:\\ \;\;\;\;\frac{1}{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \varepsilon\right)\right) + \left(\varepsilon \cdot \left(x \cdot \varepsilon\right) + \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \sin x \cdot \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right)}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}\\ \end{array}\]

Reproduce

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

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

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