2tan (problem 3.3.2)

Average Error: 36.4 → 6.2

Time: 18.4s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -7.995413078877312383943781788270193659077 \cdot 10^{-83}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot \log \left(e^{{\left(\cos \varepsilon\right)}^{3}}\right)}, \frac{{\left(\sin \varepsilon\right)}^{3}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \mathsf{fma}\left(\frac{\frac{{\left(\sin \varepsilon\right)}^{2}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}}{{\left(\cos \varepsilon\right)}^{2}}, {\left(\frac{\sin x}{\cos x}\right)}^{3} + \frac{\sin x}{\cos x}, \frac{\sin x}{\left(1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}\right) \cdot \cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}\right) - \frac{\sin x}{\cos x}\right)\\ \mathbf{elif}\;\varepsilon \le 2.893167462843807630943749385947839556285 \cdot 10^{-18}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{{\left(\sin x \cdot \tan \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3}}}, 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + \tan x \cdot \tan \varepsilon\right), -\tan x\right)\\ \end{array}\]

C

double f(double x, double eps) {
        double r160057 = x;
        double r160058 = eps;
        double r160059 = r160057 + r160058;
        double r160060 = tan(r160059);
        double r160061 = tan(r160057);
        double r160062 = r160060 - r160061;
        return r160062;
}

↓

double f(double x, double eps) {
        double r160063 = eps;
        double r160064 = -7.995413078877312e-83;
        bool r160065 = r160063 <= r160064;
        double r160066 = sin(r160063);
        double r160067 = cos(r160063);
        double r160068 = r160066 / r160067;
        double r160069 = 1.0;
        double r160070 = x;
        double r160071 = sin(r160070);
        double r160072 = r160071 * r160066;
        double r160073 = cos(r160070);
        double r160074 = r160067 * r160073;
        double r160075 = r160072 / r160074;
        double r160076 = 3.0;
        double r160077 = pow(r160075, r160076);
        double r160078 = r160069 - r160077;
        double r160079 = r160068 / r160078;
        double r160080 = 2.0;
        double r160081 = pow(r160071, r160080);
        double r160082 = pow(r160073, r160080);
        double r160083 = r160081 / r160082;
        double r160084 = pow(r160067, r160076);
        double r160085 = exp(r160084);
        double r160086 = log(r160085);
        double r160087 = r160082 * r160086;
        double r160088 = r160081 / r160087;
        double r160089 = pow(r160066, r160076);
        double r160090 = r160089 / r160078;
        double r160091 = pow(r160066, r160080);
        double r160092 = r160091 / r160078;
        double r160093 = pow(r160067, r160080);
        double r160094 = r160092 / r160093;
        double r160095 = r160071 / r160073;
        double r160096 = pow(r160095, r160076);
        double r160097 = r160096 + r160095;
        double r160098 = r160078 * r160073;
        double r160099 = r160071 / r160098;
        double r160100 = fma(r160094, r160097, r160099);
        double r160101 = r160100 + r160079;
        double r160102 = fma(r160088, r160090, r160101);
        double r160103 = r160102 - r160095;
        double r160104 = fma(r160079, r160083, r160103);
        double r160105 = 2.8931674628438076e-18;
        bool r160106 = r160063 <= r160105;
        double r160107 = pow(r160063, r160080);
        double r160108 = 0.3333333333333333;
        double r160109 = pow(r160063, r160076);
        double r160110 = fma(r160108, r160109, r160063);
        double r160111 = fma(r160070, r160107, r160110);
        double r160112 = fma(r160079, r160083, r160111);
        double r160113 = tan(r160070);
        double r160114 = tan(r160063);
        double r160115 = r160113 + r160114;
        double r160116 = pow(r160069, r160076);
        double r160117 = r160071 * r160114;
        double r160118 = pow(r160117, r160076);
        double r160119 = pow(r160073, r160076);
        double r160120 = r160118 / r160119;
        double r160121 = r160116 - r160120;
        double r160122 = r160115 / r160121;
        double r160123 = r160113 * r160114;
        double r160124 = r160123 * r160123;
        double r160125 = r160124 + r160123;
        double r160126 = r160069 + r160125;
        double r160127 = -r160113;
        double r160128 = fma(r160122, r160126, r160127);
        double r160129 = r160106 ? r160112 : r160128;
        double r160130 = r160065 ? r160104 : r160129;
        return r160130;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.4
Target	14.6
Herbie	6.2

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

Derivation

1. Split input into 3 regimes

2. if eps < -7.995413078877312e-83

   1. Initial program 29.8

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

   3. Applied tan-sum 6.2

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

   5. Applied flip3-- 6.3

      \[\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/ 6.3

      \[\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. Applied fma-neg 6.3

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{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\right)}\]

   8. Taylor expanded around -inf 6.5

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

   9. Simplified 5.7

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{3}}, \frac{{\left(\sin \varepsilon\right)}^{3}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \mathsf{fma}\left(\frac{\frac{{\left(\sin \varepsilon\right)}^{2}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}}{{\left(\cos \varepsilon\right)}^{2}}, {\left(\frac{\sin x}{\cos x}\right)}^{3} + \frac{\sin x}{\cos x}, \frac{\sin x}{\left(1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}\right) \cdot \cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}\right) - \frac{\sin x}{\cos x}\right)}\]
   10. Using strategy rm

   11. Applied add-log-exp 6.1

       \[\leadsto \mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot \color{blue}{\log \left(e^{{\left(\cos \varepsilon\right)}^{3}}\right)}}, \frac{{\left(\sin \varepsilon\right)}^{3}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \mathsf{fma}\left(\frac{\frac{{\left(\sin \varepsilon\right)}^{2}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}}{{\left(\cos \varepsilon\right)}^{2}}, {\left(\frac{\sin x}{\cos x}\right)}^{3} + \frac{\sin x}{\cos x}, \frac{\sin x}{\left(1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}\right) \cdot \cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}\right) - \frac{\sin x}{\cos x}\right)\]

   if -7.995413078877312e-83 < eps < 2.8931674628438076e-18

   1. Initial program 46.3

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

   3. Applied tan-sum 46.3

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

   5. Applied flip3-- 46.3

      \[\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/ 46.3

      \[\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. Applied fma-neg 46.3

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{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\right)}\]

   8. Taylor expanded around -inf 46.3

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

   9. Simplified 41.5

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

   10. Taylor expanded around 0 9.5

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

   11. Simplified 9.5

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

   if 2.8931674628438076e-18 < eps

   1. Initial program 28.4

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

   3. Applied tan-sum 1.0

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

   5. Applied flip3-- 1.0

      \[\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/ 1.0

      \[\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. Applied fma-neg 1.0

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{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\right)}\]
   8. Using strategy rm

   9. Applied tan-quot 1.1

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\color{blue}{\frac{\sin x}{\cos 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\right)\]

   10. Applied associate-*l/ 1.1

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

   11. Applied cube-div 1.1

       \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \color{blue}{\frac{{\left(\sin x \cdot \tan \varepsilon\right)}^{3}}{{\left(\cos x\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\right)\]
3. Recombined 3 regimes into one program.

4. Final simplification 6.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -7.995413078877312383943781788270193659077 \cdot 10^{-83}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot \log \left(e^{{\left(\cos \varepsilon\right)}^{3}}\right)}, \frac{{\left(\sin \varepsilon\right)}^{3}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \mathsf{fma}\left(\frac{\frac{{\left(\sin \varepsilon\right)}^{2}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}}{{\left(\cos \varepsilon\right)}^{2}}, {\left(\frac{\sin x}{\cos x}\right)}^{3} + \frac{\sin x}{\cos x}, \frac{\sin x}{\left(1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}\right) \cdot \cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}\right) - \frac{\sin x}{\cos x}\right)\\ \mathbf{elif}\;\varepsilon \le 2.893167462843807630943749385947839556285 \cdot 10^{-18}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{{\left(\sin x \cdot \tan \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3}}}, 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + \tan x \cdot \tan \varepsilon\right), -\tan x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019351 +o rules:numerics
(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)))