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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -6.844251912285020723082132168526967873585 \cdot 10^{-54}:\\ \;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\ \mathbf{elif}\;\varepsilon \le 7.898055614722724574412272427378393232998 \cdot 10^{-140}:\\ \;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -6.844251912285020723082132168526967873585 \cdot 10^{-54}:\\
\;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\

\mathbf{elif}\;\varepsilon \le 7.898055614722724574412272427378393232998 \cdot 10^{-140}:\\
\;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\

\mathbf{else}:\\
\;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\

\end{array}

double f(double x, double eps) {
        double r187727 = x;
        double r187728 = eps;
        double r187729 = r187727 + r187728;
        double r187730 = tan(r187729);
        double r187731 = tan(r187727);
        double r187732 = r187730 - r187731;
        return r187732;
}

↓

double f(double x, double eps) {
        double r187733 = eps;
        double r187734 = -6.844251912285021e-54;
        bool r187735 = r187733 <= r187734;
        double r187736 = x;
        double r187737 = tan(r187736);
        double r187738 = tan(r187733);
        double r187739 = r187737 + r187738;
        double r187740 = 1.0;
        double r187741 = r187737 * r187738;
        double r187742 = r187740 - r187741;
        double r187743 = r187739 / r187742;
        double r187744 = r187743 * r187743;
        double r187745 = r187737 * r187737;
        double r187746 = r187744 - r187745;
        double r187747 = r187743 + r187737;
        double r187748 = r187746 / r187747;
        double r187749 = 7.898055614722725e-140;
        bool r187750 = r187733 <= r187749;
        double r187751 = r187733 * r187736;
        double r187752 = r187736 + r187733;
        double r187753 = r187751 * r187752;
        double r187754 = r187753 + r187733;
        double r187755 = cos(r187736);
        double r187756 = r187739 * r187755;
        double r187757 = sin(r187736);
        double r187758 = r187742 * r187757;
        double r187759 = r187756 - r187758;
        double r187760 = r187742 * r187755;
        double r187761 = r187759 / r187760;
        double r187762 = r187750 ? r187754 : r187761;
        double r187763 = r187735 ? r187748 : r187762;
        return r187763;
}

Original	37.5
Target	15.0
Herbie	16.6

Derivation

Split input into 3 regimes
if eps < -6.844251912285021e-54
1. Initial program 30.1
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum4.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--4.4
  \[\leadsto \color{blue}{\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} + \tan x}}\]
if -6.844251912285021e-54 < eps < 7.898055614722725e-140
1. Initial program 48.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 32.2
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified31.9
  \[\leadsto \color{blue}{\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon}\]
if 7.898055614722725e-140 < eps
1. Initial program 32.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-quot32.5
  \[\leadsto \tan \left(x + \varepsilon\right) - \color{blue}{\frac{\sin x}{\cos x}}\]
4. Applied tan-sum12.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \frac{\sin x}{\cos x}\]
5. Applied frac-sub12.0
  \[\leadsto \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}}\]
Recombined 3 regimes into one program.
Final simplification16.6
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -6.844251912285020723082132168526967873585 \cdot 10^{-54}:\\ \;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\ \mathbf{elif}\;\varepsilon \le 7.898055614722724574412272427378393232998 \cdot 10^{-140}:\\ \;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -6.844251912285021e-54`

`if -6.844251912285021e-54 < eps < 7.898055614722725e-140`

`if 7.898055614722725e-140 < eps`

Reproduce

In
Out