2tan (problem 3.3.2)

Average Error: 37.0 → 12.2

Time: 1.9m

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.03727708017792 \cdot 10^{-42}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \left((\left(\frac{1}{1 + \tan x \cdot \tan \varepsilon}\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon}\right) + \left(-\tan x\right))_*\right))_*\\ \mathbf{elif}\;\varepsilon \le 5.006308968668795 \cdot 10^{-103}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \left((\varepsilon \cdot \frac{1}{3} + \left(x \cdot \left(x \cdot x\right)\right))_* \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \left((\left(\frac{1}{1 + \tan x \cdot \tan \varepsilon}\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon}\right) + \left(-\tan x\right))_*\right))_*\\ \end{array}\]

C

double f(double x, double eps) {
        double r18740960 = x;
        double r18740961 = eps;
        double r18740962 = r18740960 + r18740961;
        double r18740963 = tan(r18740962);
        double r18740964 = tan(r18740960);
        double r18740965 = r18740963 - r18740964;
        return r18740965;
}

↓

double f(double x, double eps) {
        double r18740966 = eps;
        double r18740967 = -2.03727708017792e-42;
        bool r18740968 = r18740966 <= r18740967;
        double r18740969 = x;
        double r18740970 = tan(r18740969);
        double r18740971 = tan(r18740966);
        double r18740972 = r18740970 * r18740971;
        double r18740973 = r18740971 + r18740970;
        double r18740974 = 1.0;
        double r18740975 = r18740972 * r18740972;
        double r18740976 = r18740974 - r18740975;
        double r18740977 = r18740973 / r18740976;
        double r18740978 = r18740974 + r18740972;
        double r18740979 = r18740974 / r18740978;
        double r18740980 = r18740974 - r18740972;
        double r18740981 = r18740973 / r18740980;
        double r18740982 = -r18740970;
        double r18740983 = fma(r18740979, r18740981, r18740982);
        double r18740984 = fma(r18740972, r18740977, r18740983);
        double r18740985 = 5.006308968668795e-103;
        bool r18740986 = r18740966 <= r18740985;
        double r18740987 = 0.3333333333333333;
        double r18740988 = r18740969 * r18740969;
        double r18740989 = r18740969 * r18740988;
        double r18740990 = fma(r18740966, r18740987, r18740989);
        double r18740991 = r18740966 * r18740966;
        double r18740992 = r18740990 * r18740991;
        double r18740993 = r18740992 + r18740966;
        double r18740994 = fma(r18740972, r18740977, r18740993);
        double r18740995 = r18740986 ? r18740994 : r18740984;
        double r18740996 = r18740968 ? r18740984 : r18740995;
        return r18740996;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.0
Target	15.2
Herbie	12.2

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

Derivation

1. Split input into 2 regimes

2. if eps < -2.03727708017792e-42 or 5.006308968668795e-103 < eps

   1. Initial program 30.5

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

   3. Applied tan-sum 5.9

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

   5. Applied add-cube-cbrt 6.1

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

   6. Applied flip-- 6.1

      \[\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}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   7. Applied associate-/r/ 6.1

      \[\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)} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   8. Applied prod-diff 6.1

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

   9. Simplified 5.8

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

   10. Simplified 5.9

       \[\leadsto \left((\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + \left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right))_* - \tan x\right) + \color{blue}{0}\]
   11. Using strategy rm

   12. Applied add-cube-cbrt 6.1

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

   13. Applied add-sqr-sqrt 34.0

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

   14. Applied prod-diff 34.0

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

   15. Simplified 5.8

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

   16. Simplified 5.1

       \[\leadsto \left((\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} - \tan x\right))_* + \color{blue}{0}\right) + 0\]
   17. Using strategy rm

   18. Applied *-un-lft-identity 5.1

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

   19. Applied difference-of-squares 5.2

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

   20. Applied *-un-lft-identity 5.2

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

   21. Applied *-un-lft-identity 5.2

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

   22. Applied distribute-lft-out 5.2

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

   23. Applied times-frac 5.2

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

   24. Applied fma-neg 5.2

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

   if -2.03727708017792e-42 < eps < 5.006308968668795e-103

   1. Initial program 47.5

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

   3. Applied tan-sum 47.5

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

   5. Applied add-cube-cbrt 48.5

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

   6. Applied flip-- 48.5

      \[\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}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   7. Applied associate-/r/ 48.5

      \[\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)} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   8. Applied prod-diff 48.7

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

   9. Simplified 48.6

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

   10. Simplified 47.5

       \[\leadsto \left((\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + \left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right))_* - \tan x\right) + \color{blue}{0}\]
   11. Using strategy rm

   12. Applied add-cube-cbrt 48.5

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

   13. Applied add-sqr-sqrt 57.1

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

   14. Applied prod-diff 57.2

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

   15. Simplified 48.6

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

   16. Simplified 42.8

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

   17. Taylor expanded around 0 23.5

       \[\leadsto \left((\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \color{blue}{\left({x}^{3} \cdot {\varepsilon}^{2} + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \varepsilon\right)\right)})_* + 0\right) + 0\]

   18. Simplified 23.5

       \[\leadsto \left((\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \color{blue}{\left(\varepsilon + (\varepsilon \cdot \frac{1}{3} + \left(\left(x \cdot x\right) \cdot x\right))_* \cdot \left(\varepsilon \cdot \varepsilon\right)\right)})_* + 0\right) + 0\]
3. Recombined 2 regimes into one program.

4. Final simplification 12.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.03727708017792 \cdot 10^{-42}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \left((\left(\frac{1}{1 + \tan x \cdot \tan \varepsilon}\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon}\right) + \left(-\tan x\right))_*\right))_*\\ \mathbf{elif}\;\varepsilon \le 5.006308968668795 \cdot 10^{-103}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \left((\varepsilon \cdot \frac{1}{3} + \left(x \cdot \left(x \cdot x\right)\right))_* \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) + \left((\left(\frac{1}{1 + \tan x \cdot \tan \varepsilon}\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon}\right) + \left(-\tan x\right))_*\right))_*\\ \end{array}\]

Reproduce

herbie shell --seed 2019107 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

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

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