Average Error: 37.4 → 0.6
Time: 15.9s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\left(\frac{\sin x \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos \varepsilon\right)}^{2} \cdot \left(\left(1 - \frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{2}}\right) \cdot \cos x\right)} + \left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}} + 1\right) \cdot \frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{2}}\right) \cdot \cos \varepsilon}\right) + \left(\frac{\sin x}{\left(1 - \frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{2}}\right) \cdot \cos x} - \frac{\sin x}{\cos x}\right)\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\left(\frac{\sin x \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos \varepsilon\right)}^{2} \cdot \left(\left(1 - \frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{2}}\right) \cdot \cos x\right)} + \left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}} + 1\right) \cdot \frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{2}}\right) \cdot \cos \varepsilon}\right) + \left(\frac{\sin x}{\left(1 - \frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{2}}\right) \cdot \cos x} - \frac{\sin x}{\cos x}\right)
double f(double x, double eps) {
        double r122050 = x;
        double r122051 = eps;
        double r122052 = r122050 + r122051;
        double r122053 = tan(r122052);
        double r122054 = tan(r122050);
        double r122055 = r122053 - r122054;
        return r122055;
}
↓
double f(double x, double eps) {
        double r122056 = x;
        double r122057 = sin(r122056);
        double r122058 = eps;
        double r122059 = sin(r122058);
        double r122060 = 2.0;
        double r122061 = pow(r122059, r122060);
        double r122062 = r122057 * r122061;
        double r122063 = cos(r122058);
        double r122064 = pow(r122063, r122060);
        double r122065 = 1.0;
        double r122066 = pow(r122057, r122060);
        double r122067 = r122066 * r122061;
        double r122068 = cos(r122056);
        double r122069 = pow(r122068, r122060);
        double r122070 = r122069 * r122064;
        double r122071 = r122067 / r122070;
        double r122072 = r122065 - r122071;
        double r122073 = r122072 * r122068;
        double r122074 = r122064 * r122073;
        double r122075 = r122062 / r122074;
        double r122076 = r122066 / r122069;
        double r122077 = r122076 + r122065;
        double r122078 = r122072 * r122063;
        double r122079 = r122059 / r122078;
        double r122080 = r122077 * r122079;
        double r122081 = r122075 + r122080;
        double r122082 = r122057 / r122073;
        double r122083 = r122057 / r122068;
        double r122084 = r122082 - r122083;
        double r122085 = r122081 + r122084;
        return r122085;
}

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

Derivation

  1. Initial program 37.4

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

  3. Applied tan-sum22.1

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

  4. Simplified22.1

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

  6. Applied flip--22.2

    \[\leadsto \frac{\tan \varepsilon + \tan x}{\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\]

  7. Applied associate-/r/22.2

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

  8. Simplified22.2

    \[\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\]
  9. Using strategy rm

  10. Applied swap-sqr22.2

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

  11. Taylor expanded around inf 22.3

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

  12. Simplified0.6

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

  13. Final simplification0.6

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

Reproduce

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