Average Error: 36.4 → 15.5
Time: 2.2m
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -9.72020893704794 \cdot 10^{-87}:\\ \;\;\;\;\left(\left(\frac{\sin \varepsilon \cdot \sin \varepsilon}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} + \left(\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}} + \left(\frac{\sin x \cdot \sin x}{\frac{\left(\cos x \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right) \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)\right)}{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\right)\right) + \frac{\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos x\right)}\right)\right) - \frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \cos x}}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\\ \mathbf{elif}\;\varepsilon \le 5.774589762410481 \cdot 10^{-177}:\\ \;\;\;\;\varepsilon + \left(\left(\varepsilon + x\right) \cdot \varepsilon\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\frac{\sin \varepsilon \cdot \sin \varepsilon}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} + \left(\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}} + \left(\frac{\sin x \cdot \sin x}{\frac{\left(\cos x \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right) \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)\right)}{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\right)\right) + \frac{\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos x\right)}\right)\right) - \frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \cos x}}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -9.72020893704794 \cdot 10^{-87}:\\
\;\;\;\;\left(\left(\frac{\sin \varepsilon \cdot \sin \varepsilon}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} + \left(\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}} + \left(\frac{\sin x \cdot \sin x}{\frac{\left(\cos x \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right) \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)\right)}{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\right)\right) + \frac{\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos x\right)}\right)\right) - \frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \cos x}}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\\

\mathbf{elif}\;\varepsilon \le 5.774589762410481 \cdot 10^{-177}:\\
\;\;\;\;\varepsilon + \left(\left(\varepsilon + x\right) \cdot \varepsilon\right) \cdot x\\

\mathbf{else}:\\
\;\;\;\;\left(\left(\frac{\sin \varepsilon \cdot \sin \varepsilon}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} + \left(\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}} + \left(\frac{\sin x \cdot \sin x}{\frac{\left(\cos x \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right) \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)\right)}{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\right)\right) + \frac{\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos x\right)}\right)\right) - \frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \cos x}}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\\

\end{array}
double f(double x, double eps) {
        double r6384886 = x;
        double r6384887 = eps;
        double r6384888 = r6384886 + r6384887;
        double r6384889 = tan(r6384888);
        double r6384890 = tan(r6384886);
        double r6384891 = r6384889 - r6384890;
        return r6384891;
}

double f(double x, double eps) {
        double r6384892 = eps;
        double r6384893 = -9.72020893704794e-87;
        bool r6384894 = r6384892 <= r6384893;
        double r6384895 = sin(r6384892);
        double r6384896 = r6384895 * r6384895;
        double r6384897 = 1.0;
        double r6384898 = x;
        double r6384899 = sin(r6384898);
        double r6384900 = r6384899 * r6384899;
        double r6384901 = r6384899 * r6384900;
        double r6384902 = r6384895 * r6384896;
        double r6384903 = r6384901 * r6384902;
        double r6384904 = cos(r6384898);
        double r6384905 = r6384904 * r6384904;
        double r6384906 = r6384905 * r6384904;
        double r6384907 = cos(r6384892);
        double r6384908 = r6384907 * r6384907;
        double r6384909 = r6384907 * r6384908;
        double r6384910 = r6384906 * r6384909;
        double r6384911 = r6384903 / r6384910;
        double r6384912 = r6384897 - r6384911;
        double r6384913 = r6384912 * r6384908;
        double r6384914 = r6384896 / r6384913;
        double r6384915 = r6384901 / r6384906;
        double r6384916 = r6384914 * r6384915;
        double r6384917 = r6384899 / r6384904;
        double r6384918 = r6384917 / r6384912;
        double r6384919 = r6384909 * r6384912;
        double r6384920 = r6384905 * r6384919;
        double r6384921 = r6384920 / r6384902;
        double r6384922 = r6384900 / r6384921;
        double r6384923 = r6384907 * r6384912;
        double r6384924 = r6384895 / r6384923;
        double r6384925 = r6384922 + r6384924;
        double r6384926 = r6384918 + r6384925;
        double r6384927 = r6384899 * r6384896;
        double r6384928 = r6384908 * r6384904;
        double r6384929 = r6384912 * r6384928;
        double r6384930 = r6384927 / r6384929;
        double r6384931 = r6384926 + r6384930;
        double r6384932 = r6384916 + r6384931;
        double r6384933 = r6384932 - r6384917;
        double r6384934 = r6384895 * r6384900;
        double r6384935 = r6384934 / r6384905;
        double r6384936 = r6384935 / r6384923;
        double r6384937 = r6384933 + r6384936;
        double r6384938 = 5.774589762410481e-177;
        bool r6384939 = r6384892 <= r6384938;
        double r6384940 = r6384892 + r6384898;
        double r6384941 = r6384940 * r6384892;
        double r6384942 = r6384941 * r6384898;
        double r6384943 = r6384892 + r6384942;
        double r6384944 = r6384939 ? r6384943 : r6384937;
        double r6384945 = r6384894 ? r6384937 : r6384944;
        return r6384945;
}

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

Derivation

  1. Split input into 2 regimes
  2. if eps < -9.72020893704794e-87 or 5.774589762410481e-177 < eps

    1. Initial program 31.1

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

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

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]
    6. Applied associate-/r/10.2

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]
    7. Simplified10.2

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

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\sqrt[3]{\left(\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right)\right) \cdot \left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right)}} \cdot \left(\tan \varepsilon \cdot \tan x\right)} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) - \tan x\]
    10. Taylor expanded around -inf 10.4

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

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

    if -9.72020893704794e-87 < eps < 5.774589762410481e-177

    1. Initial program 49.7

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Taylor expanded around 0 31.4

      \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
    3. Simplified31.3

      \[\leadsto \color{blue}{\varepsilon + \left(\varepsilon \cdot \left(x + \varepsilon\right)\right) \cdot x}\]
  3. Recombined 2 regimes into one program.
  4. Final simplification15.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -9.72020893704794 \cdot 10^{-87}:\\ \;\;\;\;\left(\left(\frac{\sin \varepsilon \cdot \sin \varepsilon}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} + \left(\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}} + \left(\frac{\sin x \cdot \sin x}{\frac{\left(\cos x \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right) \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)\right)}{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\right)\right) + \frac{\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos x\right)}\right)\right) - \frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \cos x}}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\\ \mathbf{elif}\;\varepsilon \le 5.774589762410481 \cdot 10^{-177}:\\ \;\;\;\;\varepsilon + \left(\left(\varepsilon + x\right) \cdot \varepsilon\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\frac{\sin \varepsilon \cdot \sin \varepsilon}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} + \left(\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}} + \left(\frac{\sin x \cdot \sin x}{\frac{\left(\cos x \cdot \cos x\right) \cdot \left(\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right) \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)\right)}{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\right)\right) + \frac{\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right) \cdot \left(\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos x\right)}\right)\right) - \frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \cos x}}{\cos \varepsilon \cdot \left(1 - \frac{\left(\sin x \cdot \left(\sin x \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)\right)}{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\right)}\right)}\\ \end{array}\]

Reproduce

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

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

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