Average Error: 37.3 → 0.4
Time: 21.8s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\frac{\frac{\frac{\sin \varepsilon \cdot \cos x}{\cos \varepsilon} - \left(\left(-\tan x\right) \cdot \tan \varepsilon\right) \cdot \sin x}{\cos x}}{1 - \tan x \cdot \tan \varepsilon}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\frac{\frac{\frac{\sin \varepsilon \cdot \cos x}{\cos \varepsilon} - \left(\left(-\tan x\right) \cdot \tan \varepsilon\right) \cdot \sin x}{\cos x}}{1 - \tan x \cdot \tan \varepsilon}
double f(double x, double eps) {
        double r141313 = x;
        double r141314 = eps;
        double r141315 = r141313 + r141314;
        double r141316 = tan(r141315);
        double r141317 = tan(r141313);
        double r141318 = r141316 - r141317;
        return r141318;
}
↓
double f(double x, double eps) {
        double r141319 = eps;
        double r141320 = sin(r141319);
        double r141321 = x;
        double r141322 = cos(r141321);
        double r141323 = r141320 * r141322;
        double r141324 = cos(r141319);
        double r141325 = r141323 / r141324;
        double r141326 = tan(r141321);
        double r141327 = -r141326;
        double r141328 = tan(r141319);
        double r141329 = r141327 * r141328;
        double r141330 = sin(r141321);
        double r141331 = r141329 * r141330;
        double r141332 = r141325 - r141331;
        double r141333 = r141332 / r141322;
        double r141334 = 1.0;
        double r141335 = r141326 * r141328;
        double r141336 = r141334 - r141335;
        double r141337 = r141333 / r141336;
        return r141337;
}

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

Derivation

  1. Initial program 37.3

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

  3. Applied tan-sum22.0

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

  4. Simplified22.0

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

  6. Applied add-cube-cbrt22.1

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

  7. Applied associate-*l*22.1

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

  9. Applied tan-quot22.2

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

  10. Applied frac-sub22.2

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

  11. Simplified20.9

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

  12. Simplified20.7

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

  13. Taylor expanded around inf 0.4

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

  14. Final simplification0.4

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

Reproduce

herbie shell --seed 2019291 
(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)))