Average Error: 37.2 → 0.4
Time: 28.8s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{{\left(\sin x\right)}^{2}}{\cos x}}{\cos x \cdot \left(1 - \frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos x}\right)} + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{{\left(\sin x\right)}^{2}}{\cos x}}{\cos x \cdot \left(1 - \frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos x}\right)} + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}}
double f(double x, double eps) {
        double r115265 = x;
        double r115266 = eps;
        double r115267 = r115265 + r115266;
        double r115268 = tan(r115267);
        double r115269 = tan(r115265);
        double r115270 = r115268 - r115269;
        return r115270;
}
↓
double f(double x, double eps) {
        double r115271 = eps;
        double r115272 = sin(r115271);
        double r115273 = cos(r115271);
        double r115274 = r115272 / r115273;
        double r115275 = x;
        double r115276 = sin(r115275);
        double r115277 = 2.0;
        double r115278 = pow(r115276, r115277);
        double r115279 = cos(r115275);
        double r115280 = r115278 / r115279;
        double r115281 = r115274 * r115280;
        double r115282 = 1.0;
        double r115283 = r115276 / r115273;
        double r115284 = r115272 / r115279;
        double r115285 = r115283 * r115284;
        double r115286 = r115282 - r115285;
        double r115287 = r115279 * r115286;
        double r115288 = r115281 / r115287;
        double r115289 = r115276 / r115279;
        double r115290 = r115274 * r115289;
        double r115291 = r115282 - r115290;
        double r115292 = r115274 / r115291;
        double r115293 = r115288 + r115292;
        return r115293;
}

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.2
Target15.0
Herbie0.4
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Initial program 37.2

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

  2. Simplified37.2

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

  4. Applied tan-sum22.2

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

  5. Simplified22.2

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

  6. Taylor expanded around inf 22.3

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

  7. Simplified13.1

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

  9. Applied frac-sub13.3

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

  10. Simplified13.1

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

  11. Simplified13.1

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

  12. Taylor expanded around inf 0.4

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

  13. Simplified0.4

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

  14. Final simplification0.4

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

Reproduce

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

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

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