- Split input into 3 regimes
if eps < -4.374462096754248e-143
Initial program 31.9
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-quot31.8
\[\leadsto \tan \left(x + \varepsilon\right) - \color{blue}{\frac{\sin x}{\cos x}}\]
Applied tan-sum10.7
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \frac{\sin x}{\cos x}\]
Applied frac-sub10.7
\[\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}}\]
if -4.374462096754248e-143 < eps < 1.1868227357344406e-30
Initial program 47.8
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum47.8
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
Taylor expanded around 0 31.8
\[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
Simplified31.7
\[\leadsto \color{blue}{\varepsilon + \left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)}\]
if 1.1868227357344406e-30 < eps
Initial program 29.0
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum1.9
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
- Using strategy
rm Applied tan-quot2.0
\[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
Applied tan-quot2.0
\[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \tan x\]
Applied frac-times2.0
\[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}} - \tan x\]
- Using strategy
rm Applied flip--2.1
\[\leadsto \color{blue}{\frac{\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} + \tan x}}\]
- Recombined 3 regimes into one program.
Final simplification15.9
\[\leadsto \begin{array}{l}
\mathbf{if}\;\varepsilon \le -4.374462096754248 \cdot 10^{-143}:\\
\;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\
\mathbf{elif}\;\varepsilon \le 1.1868227357344406 \cdot 10^{-30}:\\
\;\;\;\;\varepsilon + \left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\frac{\tan \varepsilon + \tan x}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}} \cdot \frac{\tan \varepsilon + \tan x}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}} + \tan x}\\
\end{array}\]