Original	37.1
Target	15.0
Herbie	14.6

Derivation

Split input into 3 regimes
if eps < -3.848860041120697e-74
1. Initial program 31.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Initial simplification31.0
  \[\leadsto \tan \left(\varepsilon + x\right) - \tan x\]
3. Using strategy rm
4. Applied tan-sum5.9
  \[\leadsto \color{blue}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x}} - \tan x\]
5. Using strategy rm
6. Applied tan-quot5.9
  \[\leadsto \frac{\tan \varepsilon + \tan x}{1 - \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}} \cdot \tan x} - \tan x\]
7. Applied associate-*l/5.9
  \[\leadsto \frac{\tan \varepsilon + \tan x}{1 - \color{blue}{\frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}} - \tan x\]
8. Using strategy rm
9. Applied *-un-lft-identity5.9
  \[\leadsto \frac{\tan \varepsilon + \tan x}{1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}} - \color{blue}{1 \cdot \tan x}\]
10. Applied flip--5.9
  \[\leadsto \frac{\tan \varepsilon + \tan x}{\color{blue}{\frac{1 \cdot 1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon} \cdot \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}{1 + \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}}} - 1 \cdot \tan x\]
11. Applied associate-/r/5.9
  \[\leadsto \color{blue}{\frac{\tan \varepsilon + \tan x}{1 \cdot 1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon} \cdot \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}} \cdot \left(1 + \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right)} - 1 \cdot \tan x\]
12. Applied prod-diff5.9
  \[\leadsto \color{blue}{(\left(\frac{\tan \varepsilon + \tan x}{1 \cdot 1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon} \cdot \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}\right) \cdot \left(1 + \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right) + \left(-\tan x \cdot 1\right))_* + (\left(-\tan x\right) \cdot 1 + \left(\tan x \cdot 1\right))_*}\]
13. Simplified5.9
  \[\leadsto (\left(\frac{\tan \varepsilon + \tan x}{1 \cdot 1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon} \cdot \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}\right) \cdot \left(1 + \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right) + \left(-\tan x \cdot 1\right))_* + \color{blue}{(-1 \cdot \left(\tan x\right) + \left(\tan x\right))_*}\]
if -3.848860041120697e-74 < eps < 1.0275046713596955e-89
1. Initial program 48.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Initial simplification48.0
  \[\leadsto \tan \left(\varepsilon + x\right) - \tan x\]
3. Using strategy rm
4. Applied tan-sum48.0
  \[\leadsto \color{blue}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x}} - \tan x\]
5. Using strategy rm
6. Applied tan-quot48.0
  \[\leadsto \frac{\tan \varepsilon + \tan x}{1 - \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}} \cdot \tan x} - \tan x\]
7. Applied associate-*l/48.0
  \[\leadsto \frac{\tan \varepsilon + \tan x}{1 - \color{blue}{\frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}} - \tan x\]
8. Taylor expanded around 0 27.8
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \varepsilon\right)}\]
9. Simplified27.8
  \[\leadsto \color{blue}{(\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*}\]
if 1.0275046713596955e-89 < eps
1. Initial program 30.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Initial simplification30.3
  \[\leadsto \tan \left(\varepsilon + x\right) - \tan x\]
3. Using strategy rm
4. Applied tan-sum7.3
  \[\leadsto \color{blue}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x}} - \tan x\]
5. Using strategy rm
6. Applied tan-quot7.3
  \[\leadsto \frac{\tan \varepsilon + \tan x}{1 - \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}} \cdot \tan x} - \tan x\]
7. Applied associate-*l/7.3
  \[\leadsto \frac{\tan \varepsilon + \tan x}{1 - \color{blue}{\frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}} - \tan x\]
8. Using strategy rm
9. Applied flip-+7.4
  \[\leadsto \frac{\color{blue}{\frac{\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan x}{\tan \varepsilon - \tan x}}}{1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}} - \tan x\]
Recombined 3 regimes into one program.
Final simplification14.6
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -3.848860041120697 \cdot 10^{-74}:\\ \;\;\;\;(-1 \cdot \left(\tan x\right) + \left(\tan x\right))_* + (\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon} \cdot \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}}\right) \cdot \left(1 + \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right) + \left(-\tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 1.0275046713596955 \cdot 10^{-89}:\\ \;\;\;\;(\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan x}{\tan \varepsilon - \tan x}}{1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}} - \tan x\\ \end{array}\]

Error

Target

Derivation

`if eps < -3.848860041120697e-74`

`if -3.848860041120697e-74 < eps < 1.0275046713596955e-89`

`if 1.0275046713596955e-89 < eps`

Runtime