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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -3.6369613603042125 \cdot 10^{-157}:\\ \;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*\\ \mathbf{elif}\;\varepsilon \le 6.73582727739693 \cdot 10^{-98}:\\ \;\;\;\;(\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*\\ \end{array}\]

double f(double x, double eps) {
        double r9915441 = x;
        double r9915442 = eps;
        double r9915443 = r9915441 + r9915442;
        double r9915444 = tan(r9915443);
        double r9915445 = tan(r9915441);
        double r9915446 = r9915444 - r9915445;
        return r9915446;
}

↓

double f(double x, double eps) {
        double r9915447 = eps;
        double r9915448 = -3.6369613603042125e-157;
        bool r9915449 = r9915447 <= r9915448;
        double r9915450 = x;
        double r9915451 = sin(r9915450);
        double r9915452 = cos(r9915450);
        double r9915453 = r9915451 / r9915452;
        double r9915454 = r9915453 * r9915453;
        double r9915455 = sin(r9915447);
        double r9915456 = cos(r9915447);
        double r9915457 = r9915455 / r9915456;
        double r9915458 = 1.0;
        double r9915459 = r9915454 * r9915453;
        double r9915460 = r9915455 * r9915455;
        double r9915461 = r9915460 * r9915455;
        double r9915462 = r9915459 * r9915461;
        double r9915463 = r9915456 * r9915456;
        double r9915464 = r9915456 * r9915463;
        double r9915465 = r9915462 / r9915464;
        double r9915466 = r9915458 - r9915465;
        double r9915467 = r9915457 / r9915466;
        double r9915468 = r9915460 / r9915463;
        double r9915469 = r9915468 / r9915466;
        double r9915470 = r9915464 * r9915466;
        double r9915471 = r9915461 / r9915470;
        double r9915472 = fma(r9915454, r9915471, r9915467);
        double r9915473 = r9915453 / r9915466;
        double r9915474 = r9915472 + r9915473;
        double r9915475 = fma(r9915453, r9915469, r9915474);
        double r9915476 = fma(r9915459, r9915469, r9915475);
        double r9915477 = r9915476 - r9915453;
        double r9915478 = fma(r9915454, r9915467, r9915477);
        double r9915479 = 6.73582727739693e-98;
        bool r9915480 = r9915447 <= r9915479;
        double r9915481 = r9915450 * r9915447;
        double r9915482 = r9915450 + r9915447;
        double r9915483 = fma(r9915481, r9915482, r9915447);
        double r9915484 = r9915480 ? r9915483 : r9915478;
        double r9915485 = r9915449 ? r9915478 : r9915484;
        return r9915485;
}

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -3.6369613603042125 \cdot 10^{-157}:\\
\;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*\\

\mathbf{elif}\;\varepsilon \le 6.73582727739693 \cdot 10^{-98}:\\
\;\;\;\;(\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon)_*\\

\mathbf{else}:\\
\;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*\\

\end{array}

Original	37.0
Target	15.1
Herbie	15.3

Derivation

Split input into 2 regimes
if eps < -3.6369613603042125e-157 or 6.73582727739693e-98 < eps
1. Initial program 31.8
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum10.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip3--10.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/10.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-neg10.3
  \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\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) + \left(-\tan x\right))_*}\]
8. Simplified10.3
  \[\leadsto (\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)} \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(-\tan x\right))_*\]
9. Taylor expanded around -inf 10.5
  \[\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. Simplified9.1
  \[\leadsto \color{blue}{(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \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((\left(\frac{\sin x}{\cos x}\right) \cdot \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((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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))_* + \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))_* - \frac{\sin x}{\cos x}\right))_*}\]
if -3.6369613603042125e-157 < eps < 6.73582727739693e-98
1. Initial program 49.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 30.4
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified30.3
  \[\leadsto \color{blue}{(\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon)_*}\]
Recombined 2 regimes into one program.
Final simplification15.3
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -3.6369613603042125 \cdot 10^{-157}:\\ \;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*\\ \mathbf{elif}\;\varepsilon \le 6.73582727739693 \cdot 10^{-98}:\\ \;\;\;\;(\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\left(\sin \varepsilon \cdot \sin \varepsilon\right) \cdot \sin \varepsilon}{\left(\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}\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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \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)}{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}}\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*\\ \end{array}\]

Error

Target

Derivation

`if eps < -3.6369613603042125e-157 or 6.73582727739693e-98 < eps`

`if -3.6369613603042125e-157 < eps < 6.73582727739693e-98`

Reproduce