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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -8.784974285695471601363619261390315751079 \cdot 10^{-89}:\\ \;\;\;\;\frac{\frac{\sin \varepsilon}{\cos \varepsilon} + \frac{\sin x}{\cos x}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.738904653256747025452406845907258964244 \cdot 10^{-113}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\left(\tan x + \tan \varepsilon\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x - \left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -8.784974285695471601363619261390315751079 \cdot 10^{-89}:\\
\;\;\;\;\frac{\frac{\sin \varepsilon}{\cos \varepsilon} + \frac{\sin x}{\cos x}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x\\

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

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

\end{array}

double f(double x, double eps) {
        double r145100 = x;
        double r145101 = eps;
        double r145102 = r145100 + r145101;
        double r145103 = tan(r145102);
        double r145104 = tan(r145100);
        double r145105 = r145103 - r145104;
        return r145105;
}

↓

double f(double x, double eps) {
        double r145106 = eps;
        double r145107 = -8.784974285695472e-89;
        bool r145108 = r145106 <= r145107;
        double r145109 = sin(r145106);
        double r145110 = cos(r145106);
        double r145111 = r145109 / r145110;
        double r145112 = x;
        double r145113 = sin(r145112);
        double r145114 = cos(r145112);
        double r145115 = r145113 / r145114;
        double r145116 = r145111 + r145115;
        double r145117 = 1.0;
        double r145118 = r145113 * r145109;
        double r145119 = r145114 * r145110;
        double r145120 = r145118 / r145119;
        double r145121 = r145117 - r145120;
        double r145122 = r145116 / r145121;
        double r145123 = tan(r145112);
        double r145124 = r145122 - r145123;
        double r145125 = 1.738904653256747e-113;
        bool r145126 = r145106 <= r145125;
        double r145127 = 2.0;
        double r145128 = pow(r145106, r145127);
        double r145129 = r145112 * r145128;
        double r145130 = pow(r145112, r145127);
        double r145131 = r145130 * r145106;
        double r145132 = r145106 + r145131;
        double r145133 = r145129 + r145132;
        double r145134 = tan(r145106);
        double r145135 = r145123 + r145134;
        double r145136 = r145123 * r145134;
        double r145137 = r145117 + r145136;
        double r145138 = r145135 * r145137;
        double r145139 = r145138 * r145114;
        double r145140 = r145136 * r145136;
        double r145141 = r145117 - r145140;
        double r145142 = r145141 * r145113;
        double r145143 = r145139 - r145142;
        double r145144 = r145141 * r145114;
        double r145145 = r145143 / r145144;
        double r145146 = r145126 ? r145133 : r145145;
        double r145147 = r145108 ? r145124 : r145146;
        return r145147;
}

Original	36.7
Target	14.9
Herbie	15.9

Derivation

Split input into 3 regimes
if eps < -8.784974285695472e-89
1. Initial program 30.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum6.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around inf 6.8
  \[\leadsto \color{blue}{\frac{\frac{\sin \varepsilon}{\cos \varepsilon} + \frac{\sin x}{\cos x}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}} - \tan x\]
if -8.784974285695472e-89 < eps < 1.738904653256747e-113
1. Initial program 48.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum48.6
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around 0 30.9
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
if 1.738904653256747e-113 < eps
1. Initial program 30.8
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum9.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--9.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/9.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. Simplified9.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-quot9.4
  \[\leadsto \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) - \color{blue}{\frac{\sin x}{\cos x}}\]
10. Applied associate-*l/9.4
  \[\leadsto \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}} - \frac{\sin x}{\cos x}\]
11. Applied frac-sub9.5
  \[\leadsto \color{blue}{\frac{\left(\left(\tan x + \tan \varepsilon\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x - \left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x}}\]
Recombined 3 regimes into one program.
Final simplification15.9
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -8.784974285695471601363619261390315751079 \cdot 10^{-89}:\\ \;\;\;\;\frac{\frac{\sin \varepsilon}{\cos \varepsilon} + \frac{\sin x}{\cos x}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.738904653256747025452406845907258964244 \cdot 10^{-113}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\left(\tan x + \tan \varepsilon\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x - \left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -8.784974285695472e-89`

`if -8.784974285695472e-89 < eps < 1.738904653256747e-113`

`if 1.738904653256747e-113 < eps`

Reproduce

In
Out