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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.698740626985668970197518116300396578201 \cdot 10^{-41}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.483472052463705190339208704273014516534 \cdot 10^{-33}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(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\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.698740626985668970197518116300396578201 \cdot 10^{-41}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\\

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

\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(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\\

\end{array}

double f(double x, double eps) {
        double r184014 = x;
        double r184015 = eps;
        double r184016 = r184014 + r184015;
        double r184017 = tan(r184016);
        double r184018 = tan(r184014);
        double r184019 = r184017 - r184018;
        return r184019;
}

↓

double f(double x, double eps) {
        double r184020 = eps;
        double r184021 = -2.698740626985669e-41;
        bool r184022 = r184020 <= r184021;
        double r184023 = x;
        double r184024 = tan(r184023);
        double r184025 = tan(r184020);
        double r184026 = r184024 + r184025;
        double r184027 = 1.0;
        double r184028 = r184024 * r184025;
        double r184029 = sin(r184023);
        double r184030 = r184029 * r184025;
        double r184031 = cos(r184023);
        double r184032 = r184030 / r184031;
        double r184033 = r184028 * r184032;
        double r184034 = r184027 - r184033;
        double r184035 = r184026 / r184034;
        double r184036 = r184027 + r184028;
        double r184037 = r184035 * r184036;
        double r184038 = r184037 - r184024;
        double r184039 = 1.4834720524637052e-33;
        bool r184040 = r184020 <= r184039;
        double r184041 = r184023 * r184020;
        double r184042 = r184020 + r184023;
        double r184043 = r184041 * r184042;
        double r184044 = r184043 + r184020;
        double r184045 = 3.0;
        double r184046 = pow(r184028, r184045);
        double r184047 = r184027 - r184046;
        double r184048 = r184026 / r184047;
        double r184049 = r184028 * r184028;
        double r184050 = r184027 * r184028;
        double r184051 = r184049 + r184050;
        double r184052 = r184027 + r184051;
        double r184053 = r184048 * r184052;
        double r184054 = r184053 - r184024;
        double r184055 = r184040 ? r184044 : r184054;
        double r184056 = r184022 ? r184038 : r184055;
        return r184056;
}

Original	36.8
Target	15.4
Herbie	14.8

Derivation

Split input into 3 regimes
if eps < -2.698740626985669e-41
1. Initial program 31.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum2.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--2.9
  \[\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}}} - \tan x\]
6. Applied associate-/r/2.9
  \[\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)} - \tan x\]
7. Simplified2.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{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) - \tan x\]
8. Using strategy rm
9. Applied tan-quot2.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\color{blue}{\frac{\sin x}{\cos x}} \cdot \tan \varepsilon\right)} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\]
10. Applied associate-*l/2.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \color{blue}{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\]
if -2.698740626985669e-41 < eps < 1.4834720524637052e-33
1. Initial program 45.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum45.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around 0 30.9
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
5. Simplified30.7
  \[\leadsto \color{blue}{\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon}\]
if 1.4834720524637052e-33 < eps
1. Initial program 28.8
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum2.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip3--2.4
  \[\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/2.4
  \[\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. Simplified2.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - {\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\]
Recombined 3 regimes into one program.
Final simplification14.8
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.698740626985668970197518116300396578201 \cdot 10^{-41}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.483472052463705190339208704273014516534 \cdot 10^{-33}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(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\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -2.698740626985669e-41`

`if -2.698740626985669e-41 < eps < 1.4834720524637052e-33`

`if 1.4834720524637052e-33 < eps`

Reproduce

In
Out