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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -6.4253650413344779 \cdot 10^{-20}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\sin x \cdot \tan \varepsilon\right)}{\cos x}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\\ \mathbf{elif}\;\varepsilon \le 7.60268013552436 \cdot 10^{-69}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \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.4253650413344779 \cdot 10^{-20}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\sin x \cdot \tan \varepsilon\right)}{\cos x}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\\

\mathbf{elif}\;\varepsilon \le 7.60268013552436 \cdot 10^{-69}:\\
\;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\

\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 r138315 = x;
        double r138316 = eps;
        double r138317 = r138315 + r138316;
        double r138318 = tan(r138317);
        double r138319 = tan(r138315);
        double r138320 = r138318 - r138319;
        return r138320;
}

↓

double f(double x, double eps) {
        double r138321 = eps;
        double r138322 = -6.425365041334478e-20;
        bool r138323 = r138321 <= r138322;
        double r138324 = x;
        double r138325 = tan(r138324);
        double r138326 = tan(r138321);
        double r138327 = r138325 + r138326;
        double r138328 = 1.0;
        double r138329 = r138325 * r138326;
        double r138330 = sin(r138324);
        double r138331 = r138330 * r138326;
        double r138332 = r138329 * r138331;
        double r138333 = cos(r138324);
        double r138334 = r138332 / r138333;
        double r138335 = r138328 - r138334;
        double r138336 = r138327 / r138335;
        double r138337 = r138328 + r138329;
        double r138338 = r138336 * r138337;
        double r138339 = r138338 - r138325;
        double r138340 = 7.60268013552436e-69;
        bool r138341 = r138321 <= r138340;
        double r138342 = 2.0;
        double r138343 = pow(r138321, r138342);
        double r138344 = r138324 * r138343;
        double r138345 = pow(r138324, r138342);
        double r138346 = r138345 * r138321;
        double r138347 = r138321 + r138346;
        double r138348 = r138344 + r138347;
        double r138349 = r138327 * r138333;
        double r138350 = r138328 - r138329;
        double r138351 = r138350 * r138330;
        double r138352 = r138349 - r138351;
        double r138353 = r138350 * r138333;
        double r138354 = r138352 / r138353;
        double r138355 = r138341 ? r138348 : r138354;
        double r138356 = r138323 ? r138339 : r138355;
        return r138356;
}

Original	37.0
Target	15.0
Herbie	15.4

Derivation

Split input into 3 regimes
if eps < -6.425365041334478e-20
1. Initial program 30.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum1.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--1.4
  \[\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/1.4
  \[\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. Simplified1.4
  \[\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-quot1.4
  \[\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/1.4
  \[\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\]
11. Applied associate-*r/1.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\sin x \cdot \tan \varepsilon\right)}{\cos x}}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\]
if -6.425365041334478e-20 < eps < 7.60268013552436e-69
1. Initial program 46.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum46.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--46.4
  \[\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/46.4
  \[\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. Simplified46.4
  \[\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. Taylor expanded around 0 31.2
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
if 7.60268013552436e-69 < eps
1. Initial program 29.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-quot29.6
  \[\leadsto \tan \left(x + \varepsilon\right) - \color{blue}{\frac{\sin x}{\cos x}}\]
4. Applied tan-sum5.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \frac{\sin x}{\cos x}\]
5. Applied frac-sub5.1
  \[\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 simplification15.4
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -6.4253650413344779 \cdot 10^{-20}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\sin x \cdot \tan \varepsilon\right)}{\cos x}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\\ \mathbf{elif}\;\varepsilon \le 7.60268013552436 \cdot 10^{-69}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \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.425365041334478e-20`

`if -6.425365041334478e-20 < eps < 7.60268013552436e-69`

`if 7.60268013552436e-69 < eps`

Reproduce

In
Out