Average Error: 36.7 → 0.6
Time: 48.2s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\left(\frac{\sin x}{\left(1 - \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right)\right) \cdot \cos x} - \frac{\sin x}{\cos x}\right) + \left(\left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}\right) \cdot \frac{\sin x}{1 - \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right)} + \frac{\sin \varepsilon}{\left(1 - \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right)\right) \cdot \cos \varepsilon} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x} + 1\right)\right)\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\left(\frac{\sin x}{\left(1 - \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right)\right) \cdot \cos x} - \frac{\sin x}{\cos x}\right) + \left(\left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}\right) \cdot \frac{\sin x}{1 - \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right)} + \frac{\sin \varepsilon}{\left(1 - \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right)\right) \cdot \cos \varepsilon} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x} + 1\right)\right)
double f(double x, double eps) {
        double r6502077 = x;
        double r6502078 = eps;
        double r6502079 = r6502077 + r6502078;
        double r6502080 = tan(r6502079);
        double r6502081 = tan(r6502077);
        double r6502082 = r6502080 - r6502081;
        return r6502082;
}
↓
double f(double x, double eps) {
        double r6502083 = x;
        double r6502084 = sin(r6502083);
        double r6502085 = 1.0;
        double r6502086 = eps;
        double r6502087 = sin(r6502086);
        double r6502088 = cos(r6502083);
        double r6502089 = r6502087 / r6502088;
        double r6502090 = r6502089 * r6502089;
        double r6502091 = cos(r6502086);
        double r6502092 = r6502084 / r6502091;
        double r6502093 = r6502092 * r6502092;
        double r6502094 = r6502090 * r6502093;
        double r6502095 = r6502085 - r6502094;
        double r6502096 = r6502095 * r6502088;
        double r6502097 = r6502084 / r6502096;
        double r6502098 = r6502084 / r6502088;
        double r6502099 = r6502097 - r6502098;
        double r6502100 = r6502091 * r6502091;
        double r6502101 = r6502087 / r6502100;
        double r6502102 = r6502089 * r6502101;
        double r6502103 = r6502084 / r6502095;
        double r6502104 = r6502102 * r6502103;
        double r6502105 = r6502095 * r6502091;
        double r6502106 = r6502087 / r6502105;
        double r6502107 = r6502098 * r6502098;
        double r6502108 = r6502107 + r6502085;
        double r6502109 = r6502106 * r6502108;
        double r6502110 = r6502104 + r6502109;
        double r6502111 = r6502099 + r6502110;
        return r6502111;
}

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

  3. Applied tan-sum21.7

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

  5. Applied flip--21.7

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

  6. Applied associate-/r/21.7

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

  8. Applied tan-quot21.7

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

  9. Applied tan-quot21.7

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

  10. Applied frac-times21.7

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

  11. Applied tan-quot21.8

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

  12. Applied tan-quot21.8

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

  13. Applied frac-times21.8

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

  14. Applied frac-times21.8

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

  15. Taylor expanded around inf 21.9

    \[\leadsto \color{blue}{\left(\frac{\sin x}{\cos x \cdot \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)} + \left(\frac{\sin x \cdot {\left(\sin \varepsilon\right)}^{2}}{\cos x \cdot \left({\left(\cos \varepsilon\right)}^{2} \cdot \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)\right)} + \left(\frac{{\left(\sin x\right)}^{2} \cdot \sin \varepsilon}{{\left(\cos x\right)}^{2} \cdot \left(\cos \varepsilon \cdot \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)\right)} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \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)}\right)\right)\right) - \frac{\sin x}{\cos x}}\]

  16. Simplified0.6

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

  17. Final simplification0.6

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

Reproduce

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

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

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