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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.80364681435499689 \cdot 10^{-54} \lor \neg \left(\varepsilon \le 5.66748466896461997 \cdot 10^{-20}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\right)} - \tan x\\ \mathbf{else}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.80364681435499689 \cdot 10^{-54} \lor \neg \left(\varepsilon \le 5.66748466896461997 \cdot 10^{-20}\right):\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\right)} - \tan x\\

\mathbf{else}:\\
\;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\

\end{array}

double f(double x, double eps) {
        double r147612 = x;
        double r147613 = eps;
        double r147614 = r147612 + r147613;
        double r147615 = tan(r147614);
        double r147616 = tan(r147612);
        double r147617 = r147615 - r147616;
        return r147617;
}

↓

double f(double x, double eps) {
        double r147618 = eps;
        double r147619 = -1.803646814354997e-54;
        bool r147620 = r147618 <= r147619;
        double r147621 = 5.66748466896462e-20;
        bool r147622 = r147618 <= r147621;
        double r147623 = !r147622;
        bool r147624 = r147620 || r147623;
        double r147625 = x;
        double r147626 = tan(r147625);
        double r147627 = tan(r147618);
        double r147628 = r147626 + r147627;
        double r147629 = 1.0;
        double r147630 = sin(r147625);
        double r147631 = sin(r147618);
        double r147632 = r147630 * r147631;
        double r147633 = cos(r147625);
        double r147634 = cos(r147618);
        double r147635 = r147633 * r147634;
        double r147636 = r147632 / r147635;
        double r147637 = r147629 - r147636;
        double r147638 = exp(r147637);
        double r147639 = log(r147638);
        double r147640 = r147628 / r147639;
        double r147641 = r147640 - r147626;
        double r147642 = 2.0;
        double r147643 = pow(r147618, r147642);
        double r147644 = r147625 * r147643;
        double r147645 = pow(r147625, r147642);
        double r147646 = r147645 * r147618;
        double r147647 = r147618 + r147646;
        double r147648 = r147644 + r147647;
        double r147649 = r147624 ? r147641 : r147648;
        return r147649;
}

Original	36.8
Target	15.2
Herbie	15.2

Derivation

Split input into 2 regimes
if eps < -1.803646814354997e-54 or 5.66748466896462e-20 < eps
1. Initial program 29.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum2.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot2.8
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied tan-quot2.8
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \tan x\]
7. Applied frac-times2.8
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}} - \tan x\]
8. Using strategy rm
9. Applied add-log-exp2.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\right)}} - \tan x\]
10. Applied add-log-exp2.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\log \left(e^{1}\right)} - \log \left(e^{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\right)} - \tan x\]
11. Applied diff-log3.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\log \left(\frac{e^{1}}{e^{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}}\right)}} - \tan x\]
12. Simplified2.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \color{blue}{\left(e^{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\right)}} - \tan x\]
if -1.803646814354997e-54 < eps < 5.66748466896462e-20
1. Initial program 45.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum45.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot45.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied tan-quot45.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \tan x\]
7. Applied frac-times45.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}} - \tan x\]
8. Taylor expanded around 0 30.9
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
Recombined 2 regimes into one program.
Final simplification15.2
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.80364681435499689 \cdot 10^{-54} \lor \neg \left(\varepsilon \le 5.66748466896461997 \cdot 10^{-20}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\right)} - \tan x\\ \mathbf{else}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -1.803646814354997e-54 or 5.66748466896462e-20 < eps`

`if -1.803646814354997e-54 < eps < 5.66748466896462e-20`

Reproduce

In
Out