2tan (problem 3.3.2)

Average Error: 37.6 → 0.4

Time: 2.1m

Precision: 64

Math

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

↓

\[\left(\tan x - \tan x\right) + \mathsf{fma}\left(\left(\tan \varepsilon \cdot \tan x\right), \left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right), \left(\left(\mathsf{fma}\left(\left(\frac{\sin x \cdot \sin x}{\cos x \cdot \cos x} \cdot \frac{\sin x \cdot \sin x}{\cos x \cdot \cos x}\right), \left(\frac{\frac{{\left(\sin \varepsilon\right)}^{5}}{{\left(\cos \varepsilon\right)}^{5}}}{1 - \left(\frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\right) \cdot \left(\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x}\right)}\right), \left(\mathsf{fma}\left(\left(\frac{{\left(\sin x\right)}^{5}}{{\left(\cos x\right)}^{5}}\right), \left(\frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}{1 - \left(\frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\right) \cdot \left(\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x}\right)}\right), \left(\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{1 - \left(\frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\right) \cdot \left(\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x}\right)}\right)\right)\right)\right) + \left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\right) \cdot \left(\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x}\right)} + \frac{\sin x \cdot \sin x}{\left(1 - \left(\frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\right) \cdot \left(\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x}\right)\right) \cdot \left(\cos x \cdot \cos x\right)} \cdot \frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\right)\right) + \left(\frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)} \cdot \frac{\sin \varepsilon \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\right) \cdot \left(\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\left(\cos x \cdot \cos x\right) \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right)\right)\right)\]

C

double f(double x, double eps) {
        double r17612624 = x;
        double r17612625 = eps;
        double r17612626 = r17612624 + r17612625;
        double r17612627 = tan(r17612626);
        double r17612628 = tan(r17612624);
        double r17612629 = r17612627 - r17612628;
        return r17612629;
}

↓

double f(double x, double eps) {
        double r17612630 = x;
        double r17612631 = tan(r17612630);
        double r17612632 = r17612631 - r17612631;
        double r17612633 = eps;
        double r17612634 = tan(r17612633);
        double r17612635 = r17612634 * r17612631;
        double r17612636 = r17612631 + r17612634;
        double r17612637 = 1.0;
        double r17612638 = r17612635 * r17612635;
        double r17612639 = r17612637 - r17612638;
        double r17612640 = r17612636 / r17612639;
        double r17612641 = sin(r17612630);
        double r17612642 = r17612641 * r17612641;
        double r17612643 = cos(r17612630);
        double r17612644 = r17612643 * r17612643;
        double r17612645 = r17612642 / r17612644;
        double r17612646 = r17612645 * r17612645;
        double r17612647 = sin(r17612633);
        double r17612648 = 5.0;
        double r17612649 = pow(r17612647, r17612648);
        double r17612650 = cos(r17612633);
        double r17612651 = pow(r17612650, r17612648);
        double r17612652 = r17612649 / r17612651;
        double r17612653 = r17612647 * r17612647;
        double r17612654 = r17612647 * r17612653;
        double r17612655 = r17612650 * r17612650;
        double r17612656 = r17612650 * r17612655;
        double r17612657 = r17612654 / r17612656;
        double r17612658 = r17612657 * r17612657;
        double r17612659 = r17612641 * r17612642;
        double r17612660 = r17612644 * r17612643;
        double r17612661 = r17612659 / r17612660;
        double r17612662 = r17612661 * r17612661;
        double r17612663 = r17612658 * r17612662;
        double r17612664 = r17612637 - r17612663;
        double r17612665 = r17612652 / r17612664;
        double r17612666 = pow(r17612641, r17612648);
        double r17612667 = pow(r17612643, r17612648);
        double r17612668 = r17612666 / r17612667;
        double r17612669 = r17612653 * r17612653;
        double r17612670 = r17612655 * r17612655;
        double r17612671 = r17612669 / r17612670;
        double r17612672 = r17612671 / r17612664;
        double r17612673 = r17612653 / r17612655;
        double r17612674 = r17612673 / r17612664;
        double r17612675 = r17612661 * r17612674;
        double r17612676 = fma(r17612668, r17612672, r17612675);
        double r17612677 = fma(r17612646, r17612665, r17612676);
        double r17612678 = r17612647 / r17612650;
        double r17612679 = r17612678 / r17612664;
        double r17612680 = r17612664 * r17612644;
        double r17612681 = r17612642 / r17612680;
        double r17612682 = r17612681 * r17612657;
        double r17612683 = r17612679 + r17612682;
        double r17612684 = r17612677 + r17612683;
        double r17612685 = r17612641 / r17612643;
        double r17612686 = r17612685 / r17612664;
        double r17612687 = r17612686 - r17612685;
        double r17612688 = r17612684 + r17612687;
        double r17612689 = fma(r17612635, r17612640, r17612688);
        double r17612690 = r17612632 + r17612689;
        return r17612690;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.6
Target	15.3
Herbie	0.4

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

Derivation

1. Initial program 37.6

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

3. Applied tan-sum 22.2

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

5. Applied *-un-lft-identity 22.2

   \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \color{blue}{1 \cdot \tan x}\]

6. Applied flip-- 22.2

   \[\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}}} - 1 \cdot \tan x\]

7. Applied associate-/r/ 22.2

   \[\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)} - 1 \cdot \tan x\]

8. Applied prod-diff 22.2

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

9. Simplified 19.9

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

10. Simplified 19.9

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

12. Applied flip3-- 20.0

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

13. Applied associate-/r/ 20.0

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

14. Applied fma-neg 20.0

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

15. Taylor expanded around inf 20.1

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

16. Simplified 0.4

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

17. Final simplification 0.4

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

Reproduce

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