\[\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 r159689 = x;
        double r159690 = eps;
        double r159691 = r159689 + r159690;
        double r159692 = tan(r159691);
        double r159693 = tan(r159689);
        double r159694 = r159692 - r159693;
        return r159694;
}

↓

double f(double x, double eps) {
        double r159695 = eps;
        double r159696 = -6.844251912285021e-54;
        bool r159697 = r159695 <= r159696;
        double r159698 = x;
        double r159699 = tan(r159698);
        double r159700 = tan(r159695);
        double r159701 = r159699 + r159700;
        double r159702 = 1.0;
        double r159703 = r159699 * r159700;
        double r159704 = r159702 - r159703;
        double r159705 = r159701 / r159704;
        double r159706 = r159705 * r159705;
        double r159707 = r159699 * r159699;
        double r159708 = r159706 - r159707;
        double r159709 = r159705 + r159699;
        double r159710 = r159708 / r159709;
        double r159711 = 7.898055614722725e-140;
        bool r159712 = r159695 <= r159711;
        double r159713 = r159695 * r159698;
        double r159714 = r159698 + r159695;
        double r159715 = r159713 * r159714;
        double r159716 = r159715 + r159695;
        double r159717 = cos(r159698);
        double r159718 = r159701 * r159717;
        double r159719 = sin(r159698);
        double r159720 = r159704 * r159719;
        double r159721 = r159718 - r159720;
        double r159722 = r159704 * r159717;
        double r159723 = r159721 / r159722;
        double r159724 = r159712 ? r159716 : r159723;
        double r159725 = r159697 ? r159710 : r159724;
        return r159725;
}

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