\[\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 r133153 = x;
        double r133154 = eps;
        double r133155 = r133153 + r133154;
        double r133156 = tan(r133155);
        double r133157 = tan(r133153);
        double r133158 = r133156 - r133157;
        return r133158;
}

↓

double f(double x, double eps) {
        double r133159 = eps;
        double r133160 = -6.425365041334478e-20;
        bool r133161 = r133159 <= r133160;
        double r133162 = x;
        double r133163 = tan(r133162);
        double r133164 = tan(r133159);
        double r133165 = r133163 + r133164;
        double r133166 = 1.0;
        double r133167 = r133163 * r133164;
        double r133168 = sin(r133162);
        double r133169 = r133168 * r133164;
        double r133170 = r133167 * r133169;
        double r133171 = cos(r133162);
        double r133172 = r133170 / r133171;
        double r133173 = r133166 - r133172;
        double r133174 = r133165 / r133173;
        double r133175 = r133166 + r133167;
        double r133176 = r133174 * r133175;
        double r133177 = r133176 - r133163;
        double r133178 = 7.60268013552436e-69;
        bool r133179 = r133159 <= r133178;
        double r133180 = 2.0;
        double r133181 = pow(r133159, r133180);
        double r133182 = r133162 * r133181;
        double r133183 = pow(r133162, r133180);
        double r133184 = r133183 * r133159;
        double r133185 = r133159 + r133184;
        double r133186 = r133182 + r133185;
        double r133187 = r133165 * r133171;
        double r133188 = r133166 - r133167;
        double r133189 = r133188 * r133168;
        double r133190 = r133187 - r133189;
        double r133191 = r133188 * r133171;
        double r133192 = r133190 / r133191;
        double r133193 = r133179 ? r133186 : r133192;
        double r133194 = r133161 ? r133177 : r133193;
        return r133194;
}

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