Average Error: 37.1 → 0.5
Time: 1.7m
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\mathsf{fma}\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right), \left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right)}{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}}\right), \left(\left(\left(\mathsf{fma}\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right), \left(\frac{\frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}}\right), \left(\frac{\frac{\sin x}{\cos x} \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \left(1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}\right)}\right)\right) + \frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}}\right) + \left(\frac{\left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \left(1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}\right)} - \frac{\sin x}{\cos x}\right)\right) + \frac{\sin \varepsilon}{\left(1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}\right) \cdot \cos \varepsilon}\right)\right)\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\mathsf{fma}\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right), \left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right)}{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}}\right), \left(\left(\left(\mathsf{fma}\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right), \left(\frac{\frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}}\right), \left(\frac{\frac{\sin x}{\cos x} \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \left(1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}\right)}\right)\right) + \frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}}\right) + \left(\frac{\left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \left(1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}\right)} - \frac{\sin x}{\cos x}\right)\right) + \frac{\sin \varepsilon}{\left(1 - \left(\frac{\sin x}{\cos x} \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right)\right) \cdot \frac{\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos \varepsilon}}{\cos \varepsilon}\right) \cdot \cos \varepsilon}\right)\right)
double f(double x, double eps) {
        double r25086352 = x;
        double r25086353 = eps;
        double r25086354 = r25086352 + r25086353;
        double r25086355 = tan(r25086354);
        double r25086356 = tan(r25086352);
        double r25086357 = r25086355 - r25086356;
        return r25086357;
}
↓
double f(double x, double eps) {
        double r25086358 = x;
        double r25086359 = sin(r25086358);
        double r25086360 = cos(r25086358);
        double r25086361 = r25086359 / r25086360;
        double r25086362 = r25086361 * r25086361;
        double r25086363 = eps;
        double r25086364 = sin(r25086363);
        double r25086365 = cos(r25086363);
        double r25086366 = r25086364 / r25086365;
        double r25086367 = 1.0;
        double r25086368 = r25086364 * r25086364;
        double r25086369 = r25086368 * r25086364;
        double r25086370 = r25086361 * r25086362;
        double r25086371 = r25086369 * r25086370;
        double r25086372 = r25086365 * r25086365;
        double r25086373 = r25086372 * r25086365;
        double r25086374 = r25086371 / r25086373;
        double r25086375 = r25086367 - r25086374;
        double r25086376 = r25086366 / r25086375;
        double r25086377 = r25086369 / r25086372;
        double r25086378 = r25086377 / r25086365;
        double r25086379 = r25086370 * r25086378;
        double r25086380 = r25086367 - r25086379;
        double r25086381 = r25086378 / r25086380;
        double r25086382 = r25086361 * r25086368;
        double r25086383 = r25086372 * r25086380;
        double r25086384 = r25086382 / r25086383;
        double r25086385 = fma(r25086362, r25086381, r25086384);
        double r25086386 = r25086361 / r25086380;
        double r25086387 = r25086385 + r25086386;
        double r25086388 = r25086370 * r25086368;
        double r25086389 = r25086388 / r25086383;
        double r25086390 = r25086389 - r25086361;
        double r25086391 = r25086387 + r25086390;
        double r25086392 = r25086380 * r25086365;
        double r25086393 = r25086364 / r25086392;
        double r25086394 = r25086391 + r25086393;
        double r25086395 = fma(r25086362, r25086376, r25086394);
        return r25086395;
}

Error

Bits error versus x

Bits error versus eps

Target

Original37.1
Target15.0
Herbie0.5
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Initial program 37.1

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

  3. Applied tan-sum21.9

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

  5. Applied flip3--22.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/22.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-neg22.0

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

  8. Simplified22.0

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

  9. Taylor expanded around -inf 22.1

    \[\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}}\]

  10. Simplified19.8

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

  11. Taylor expanded around inf 19.8

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

  12. Simplified0.5

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

  13. Final simplification0.5

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

Reproduce

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