Average Error: 36.7 → 0.4
Time: 28.0s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\frac{\left(\sin x \cdot \frac{\sin x}{\frac{\cos \varepsilon \cdot \cos x}{\sin \varepsilon}}\right) \cdot \left(\left(1 + \left(1 - \frac{\sin x}{\frac{\cos \varepsilon \cdot \cos x}{\sin \varepsilon}}\right)\right) \cdot \sin x\right)}{\left(1 + \left(1 - \frac{\sin x}{\frac{\cos \varepsilon \cdot \cos x}{\sin \varepsilon}}\right)\right) \cdot \sin x}}{\cos x \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\frac{\left(\sin x \cdot \frac{\sin x}{\frac{\cos \varepsilon \cdot \cos x}{\sin \varepsilon}}\right) \cdot \left(\left(1 + \left(1 - \frac{\sin x}{\frac{\cos \varepsilon \cdot \cos x}{\sin \varepsilon}}\right)\right) \cdot \sin x\right)}{\left(1 + \left(1 - \frac{\sin x}{\frac{\cos \varepsilon \cdot \cos x}{\sin \varepsilon}}\right)\right) \cdot \sin x}}{\cos x \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)}
double f(double x, double eps) {
        double r87486 = x;
        double r87487 = eps;
        double r87488 = r87486 + r87487;
        double r87489 = tan(r87488);
        double r87490 = tan(r87486);
        double r87491 = r87489 - r87490;
        return r87491;
}
↓
double f(double x, double eps) {
        double r87492 = eps;
        double r87493 = sin(r87492);
        double r87494 = cos(r87492);
        double r87495 = r87493 / r87494;
        double r87496 = 1.0;
        double r87497 = x;
        double r87498 = sin(r87497);
        double r87499 = cos(r87497);
        double r87500 = r87498 / r87499;
        double r87501 = r87495 * r87500;
        double r87502 = r87496 - r87501;
        double r87503 = r87495 / r87502;
        double r87504 = r87494 * r87499;
        double r87505 = r87504 / r87493;
        double r87506 = r87498 / r87505;
        double r87507 = r87498 * r87506;
        double r87508 = r87496 - r87506;
        double r87509 = r87496 + r87508;
        double r87510 = r87509 * r87498;
        double r87511 = r87507 * r87510;
        double r87512 = r87511 / r87510;
        double r87513 = r87499 * r87502;
        double r87514 = r87512 / r87513;
        double r87515 = r87503 + r87514;
        return r87515;
}

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

Derivation

  1. Initial program 36.7

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

  2. Simplified36.7

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

  4. Applied tan-sum21.7

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

  5. Simplified21.7

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

  6. Taylor expanded around inf 21.8

    \[\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. Simplified12.7

    \[\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.0

    \[\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. Simplified12.8

    \[\leadsto \frac{\color{blue}{\sin 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}}\]

  11. Simplified12.8

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

  13. Applied flip--12.8

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

  14. Simplified0.4

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

  15. Simplified0.4

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

  16. Final simplification0.4

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

Reproduce

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

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

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