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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.1488643550373863 \cdot 10^{-31}:\\ \;\;\;\;\frac{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} \cdot \frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x \cdot \tan x}{\tan x + \frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}}}\\ \mathbf{elif}\;\varepsilon \le 5.947598887208492 \cdot 10^{-69}:\\ \;\;\;\;\varepsilon + x \cdot \left(\varepsilon \cdot \left(\varepsilon + x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan x + \tan \varepsilon\right) - \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 r8247071 = x;
        double r8247072 = eps;
        double r8247073 = r8247071 + r8247072;
        double r8247074 = tan(r8247073);
        double r8247075 = tan(r8247071);
        double r8247076 = r8247074 - r8247075;
        return r8247076;
}

↓

double f(double x, double eps) {
        double r8247077 = eps;
        double r8247078 = -1.1488643550373863e-31;
        bool r8247079 = r8247077 <= r8247078;
        double r8247080 = 1.0;
        double r8247081 = x;
        double r8247082 = tan(r8247081);
        double r8247083 = tan(r8247077);
        double r8247084 = r8247082 * r8247083;
        double r8247085 = r8247080 - r8247084;
        double r8247086 = r8247082 + r8247083;
        double r8247087 = r8247085 / r8247086;
        double r8247088 = r8247080 / r8247087;
        double r8247089 = r8247088 * r8247088;
        double r8247090 = r8247082 * r8247082;
        double r8247091 = r8247089 - r8247090;
        double r8247092 = r8247082 + r8247088;
        double r8247093 = r8247091 / r8247092;
        double r8247094 = 5.947598887208492e-69;
        bool r8247095 = r8247077 <= r8247094;
        double r8247096 = r8247077 + r8247081;
        double r8247097 = r8247077 * r8247096;
        double r8247098 = r8247081 * r8247097;
        double r8247099 = r8247077 + r8247098;
        double r8247100 = cos(r8247081);
        double r8247101 = r8247100 * r8247086;
        double r8247102 = sin(r8247081);
        double r8247103 = r8247085 * r8247102;
        double r8247104 = r8247101 - r8247103;
        double r8247105 = r8247085 * r8247100;
        double r8247106 = r8247104 / r8247105;
        double r8247107 = r8247095 ? r8247099 : r8247106;
        double r8247108 = r8247079 ? r8247093 : r8247107;
        return r8247108;
}

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.1488643550373863 \cdot 10^{-31}:\\
\;\;\;\;\frac{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} \cdot \frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x \cdot \tan x}{\tan x + \frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}}}\\

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

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

\end{array}

Original	37.0
Target	15.1
Herbie	15.2

Derivation

Split input into 3 regimes
if eps < -1.1488643550373863e-31
1. Initial program 29.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum2.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied *-un-lft-identity2.4
  \[\leadsto \frac{\color{blue}{1 \cdot \left(\tan x + \tan \varepsilon\right)}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]
6. Applied associate-/l*2.5
  \[\leadsto \color{blue}{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}}} - \tan x\]
7. Using strategy rm
8. Applied flip--2.6
  \[\leadsto \color{blue}{\frac{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} \cdot \frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x \cdot \tan x}{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} + \tan x}}\]
if -1.1488643550373863e-31 < eps < 5.947598887208492e-69
1. Initial program 46.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 30.8
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified30.7
  \[\leadsto \color{blue}{\varepsilon + \left(\left(\varepsilon + x\right) \cdot \varepsilon\right) \cdot x}\]
if 5.947598887208492e-69 < eps
1. Initial program 30.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-quot30.3
  \[\leadsto \tan \left(x + \varepsilon\right) - \color{blue}{\frac{\sin x}{\cos x}}\]
4. Applied tan-sum5.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \frac{\sin x}{\cos x}\]
5. Applied frac-sub5.3
  \[\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.2
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.1488643550373863 \cdot 10^{-31}:\\ \;\;\;\;\frac{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} \cdot \frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x \cdot \tan x}{\tan x + \frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}}}\\ \mathbf{elif}\;\varepsilon \le 5.947598887208492 \cdot 10^{-69}:\\ \;\;\;\;\varepsilon + x \cdot \left(\varepsilon \cdot \left(\varepsilon + x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan x + \tan \varepsilon\right) - \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

Target

Derivation

`if eps < -1.1488643550373863e-31`

`if -1.1488643550373863e-31 < eps < 5.947598887208492e-69`

`if 5.947598887208492e-69 < eps`

Reproduce