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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.521553231728933 \cdot 10^{-16}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)} \cdot \left(\left(\tan x \cdot \tan \varepsilon + \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) + 1\right) - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.3390367256703872 \cdot 10^{-42}:\\ \;\;\;\;\varepsilon \cdot \left(\left(x + \varepsilon\right) \cdot x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\tan \varepsilon\right)}^{3} + {\left(\tan x\right)}^{3}}{\left(\left(\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan \varepsilon\right) + \tan x \cdot \tan x\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)} - \tan x\\ \end{array}\]

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

↓

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

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

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

\end{array}

double f(double x, double eps) {
        double r9279517 = x;
        double r9279518 = eps;
        double r9279519 = r9279517 + r9279518;
        double r9279520 = tan(r9279519);
        double r9279521 = tan(r9279517);
        double r9279522 = r9279520 - r9279521;
        return r9279522;
}

↓

double f(double x, double eps) {
        double r9279523 = eps;
        double r9279524 = -2.521553231728933e-16;
        bool r9279525 = r9279523 <= r9279524;
        double r9279526 = tan(r9279523);
        double r9279527 = x;
        double r9279528 = tan(r9279527);
        double r9279529 = r9279526 + r9279528;
        double r9279530 = 1.0;
        double r9279531 = r9279528 * r9279526;
        double r9279532 = r9279531 * r9279531;
        double r9279533 = r9279531 * r9279532;
        double r9279534 = r9279530 - r9279533;
        double r9279535 = r9279529 / r9279534;
        double r9279536 = r9279531 + r9279532;
        double r9279537 = r9279536 + r9279530;
        double r9279538 = r9279535 * r9279537;
        double r9279539 = r9279538 - r9279528;
        double r9279540 = 1.3390367256703872e-42;
        bool r9279541 = r9279523 <= r9279540;
        double r9279542 = r9279527 + r9279523;
        double r9279543 = r9279542 * r9279527;
        double r9279544 = r9279523 * r9279543;
        double r9279545 = r9279544 + r9279523;
        double r9279546 = 3.0;
        double r9279547 = pow(r9279526, r9279546);
        double r9279548 = pow(r9279528, r9279546);
        double r9279549 = r9279547 + r9279548;
        double r9279550 = r9279526 * r9279526;
        double r9279551 = r9279550 - r9279531;
        double r9279552 = r9279528 * r9279528;
        double r9279553 = r9279551 + r9279552;
        double r9279554 = r9279530 - r9279531;
        double r9279555 = r9279553 * r9279554;
        double r9279556 = r9279549 / r9279555;
        double r9279557 = r9279556 - r9279528;
        double r9279558 = r9279541 ? r9279545 : r9279557;
        double r9279559 = r9279525 ? r9279539 : r9279558;
        return r9279559;
}

Original	37.1
Target	15.4
Herbie	15.3

Derivation

Split input into 3 regimes
if eps < -2.521553231728933e-16
1. Initial program 30.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum0.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip3--1.0
  \[\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/1.0
  \[\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. Simplified0.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}} \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\]
if -2.521553231728933e-16 < eps < 1.3390367256703872e-42
1. Initial program 45.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 31.3
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified31.3
  \[\leadsto \color{blue}{\varepsilon + \varepsilon \cdot \left(x \cdot \left(x + \varepsilon\right)\right)}\]
if 1.3390367256703872e-42 < eps
1. Initial program 30.1
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum3.2
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip3-+3.3
  \[\leadsto \frac{\color{blue}{\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\tan x \cdot \tan x + \left(\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan \varepsilon\right)}}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]
6. Applied associate-/l/3.3
  \[\leadsto \color{blue}{\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan x + \left(\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan \varepsilon\right)\right)}} - \tan x\]
Recombined 3 regimes into one program.
Final simplification15.3
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.521553231728933 \cdot 10^{-16}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)} \cdot \left(\left(\tan x \cdot \tan \varepsilon + \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) + 1\right) - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.3390367256703872 \cdot 10^{-42}:\\ \;\;\;\;\varepsilon \cdot \left(\left(x + \varepsilon\right) \cdot x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\tan \varepsilon\right)}^{3} + {\left(\tan x\right)}^{3}}{\left(\left(\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan \varepsilon\right) + \tan x \cdot \tan x\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)} - \tan x\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -2.521553231728933e-16`

`if -2.521553231728933e-16 < eps < 1.3390367256703872e-42`

`if 1.3390367256703872e-42 < eps`

Reproduce

In
Out