2tan (problem 3.3.2)

Average Error: 36.7 → 6.0

Time: 31.0s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -8.784974285695471601363619261390315751079 \cdot 10^{-89} \lor \neg \left(\varepsilon \le 6.726281342629977526189866836658949394819 \cdot 10^{-43}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{\cos \varepsilon}, \frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right) \cdot {\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}}, \mathsf{fma}\left(\frac{{\left(\sin \varepsilon\right)}^{2}}{{\left(\cos \varepsilon\right)}^{2} \cdot \left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right)}, \frac{\sin x}{\cos x} + \frac{{\left(\sin x\right)}^{3}}{{\left(\cos x\right)}^{3}}, \frac{\frac{\sin x}{\cos x}}{1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}}\right) + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right)}\right) - \frac{\sin x}{\cos x}\right) + \tan x \cdot 0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{\cos \varepsilon}, \frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right) \cdot {\left(\cos x\right)}^{2}}, \mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\right) + \tan x \cdot 0\\ \end{array}\]

C

double f(double x, double eps) {
        double r125625 = x;
        double r125626 = eps;
        double r125627 = r125625 + r125626;
        double r125628 = tan(r125627);
        double r125629 = tan(r125625);
        double r125630 = r125628 - r125629;
        return r125630;
}

↓

double f(double x, double eps) {
        double r125631 = eps;
        double r125632 = -8.784974285695472e-89;
        bool r125633 = r125631 <= r125632;
        double r125634 = 6.7262813426299775e-43;
        bool r125635 = r125631 <= r125634;
        double r125636 = !r125635;
        bool r125637 = r125633 || r125636;
        double r125638 = x;
        double r125639 = sin(r125638);
        double r125640 = 2.0;
        double r125641 = pow(r125639, r125640);
        double r125642 = cos(r125631);
        double r125643 = r125641 / r125642;
        double r125644 = sin(r125631);
        double r125645 = 1.0;
        double r125646 = r125639 * r125644;
        double r125647 = 3.0;
        double r125648 = pow(r125646, r125647);
        double r125649 = cos(r125638);
        double r125650 = r125649 * r125642;
        double r125651 = pow(r125650, r125647);
        double r125652 = r125648 / r125651;
        double r125653 = r125645 - r125652;
        double r125654 = pow(r125649, r125640);
        double r125655 = r125653 * r125654;
        double r125656 = r125644 / r125655;
        double r125657 = pow(r125644, r125647);
        double r125658 = pow(r125642, r125647);
        double r125659 = r125654 * r125658;
        double r125660 = r125657 / r125659;
        double r125661 = r125641 / r125653;
        double r125662 = pow(r125644, r125640);
        double r125663 = pow(r125642, r125640);
        double r125664 = r125663 * r125653;
        double r125665 = r125662 / r125664;
        double r125666 = r125639 / r125649;
        double r125667 = pow(r125639, r125647);
        double r125668 = pow(r125649, r125647);
        double r125669 = r125667 / r125668;
        double r125670 = r125666 + r125669;
        double r125671 = r125666 / r125653;
        double r125672 = fma(r125665, r125670, r125671);
        double r125673 = r125642 * r125653;
        double r125674 = r125644 / r125673;
        double r125675 = r125672 + r125674;
        double r125676 = fma(r125660, r125661, r125675);
        double r125677 = r125676 - r125666;
        double r125678 = fma(r125643, r125656, r125677);
        double r125679 = tan(r125638);
        double r125680 = 0.0;
        double r125681 = r125679 * r125680;
        double r125682 = r125678 + r125681;
        double r125683 = pow(r125631, r125640);
        double r125684 = 0.3333333333333333;
        double r125685 = pow(r125631, r125647);
        double r125686 = fma(r125684, r125685, r125631);
        double r125687 = fma(r125638, r125683, r125686);
        double r125688 = fma(r125643, r125656, r125687);
        double r125689 = r125688 + r125681;
        double r125690 = r125637 ? r125682 : r125689;
        return r125690;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.7
Target	14.9
Herbie	6.0

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

Derivation

1. Split input into 2 regimes

2. if eps < -8.784974285695472e-89 or 6.7262813426299775e-43 < eps

   1. Initial program 29.7

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

   3. Applied tan-sum 5.2

      \[\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 5.4

      \[\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 flip3-- 5.5

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

   7. Applied associate-/r/ 5.5

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

   8. Applied prod-diff 5.5

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

   9. Simplified 5.1

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

   10. Simplified 5.2

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

   11. Taylor expanded around -inf 5.5

       \[\leadsto \color{blue}{\left(\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}\right)} + \tan x \cdot 0\]

   12. Simplified 4.8

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

   if -8.784974285695472e-89 < eps < 6.7262813426299775e-43

   1. Initial program 47.3

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

   3. Applied tan-sum 47.3

      \[\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.2

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

   7. Applied associate-/r/ 48.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)} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   8. Applied prod-diff 48.4

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

   9. Simplified 48.3

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

   10. Simplified 47.3

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

   11. Taylor expanded around -inf 47.3

       \[\leadsto \color{blue}{\left(\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}\right)} + \tan x \cdot 0\]

   12. Simplified 42.7

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

   13. Taylor expanded around 0 8.0

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

   14. Simplified 8.0

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

4. Final simplification 6.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -8.784974285695471601363619261390315751079 \cdot 10^{-89} \lor \neg \left(\varepsilon \le 6.726281342629977526189866836658949394819 \cdot 10^{-43}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{\cos \varepsilon}, \frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right) \cdot {\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}}, \mathsf{fma}\left(\frac{{\left(\sin \varepsilon\right)}^{2}}{{\left(\cos \varepsilon\right)}^{2} \cdot \left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right)}, \frac{\sin x}{\cos x} + \frac{{\left(\sin x\right)}^{3}}{{\left(\cos x\right)}^{3}}, \frac{\frac{\sin x}{\cos x}}{1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}}\right) + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right)}\right) - \frac{\sin x}{\cos x}\right) + \tan x \cdot 0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{\cos \varepsilon}, \frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}\right) \cdot {\left(\cos x\right)}^{2}}, \mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\right) + \tan x \cdot 0\\ \end{array}\]

Reproduce

herbie shell --seed 2019235 +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)))