Original	36.9
Target	15.1
Herbie	13.9

Derivation

Split input into 2 regimes
if eps < -3.5479355778421913e-28 or 1.146422683164635e-17 < eps
1. Initial program 30.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum1.6
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot1.6
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \tan \varepsilon} - \tan x\]
6. Applied associate-*l/1.6
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}} - \tan x\]
7. Using strategy rm
8. Applied flip3--1.6
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)}^{3}}{1 \cdot 1 + \left(\frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x} + 1 \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)}}} - \tan x\]
9. Applied associate-/r/1.6
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x} + 1 \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)\right)} - \tan x\]
10. Applied fma-neg1.6
  \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)}^{3}}\right) \cdot \left(1 \cdot 1 + \left(\frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x} + 1 \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)\right) + \left(-\tan x\right))_*}\]
if -3.5479355778421913e-28 < eps < 1.146422683164635e-17
1. Initial program 44.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum44.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot44.3
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \tan \varepsilon} - \tan x\]
6. Applied associate-*l/44.3
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}} - \tan x\]
7. Using strategy rm
8. Applied add-sqr-sqrt53.6
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}} - \color{blue}{\sqrt{\tan x} \cdot \sqrt{\tan x}}\]
9. Applied add-sqr-sqrt53.6
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}} \cdot \sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}}}} - \sqrt{\tan x} \cdot \sqrt{\tan x}\]
10. Applied add-cube-cbrt53.9
  \[\leadsto \frac{\color{blue}{\left(\sqrt[3]{\tan x + \tan \varepsilon} \cdot \sqrt[3]{\tan x + \tan \varepsilon}\right) \cdot \sqrt[3]{\tan x + \tan \varepsilon}}}{\sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}} \cdot \sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}}} - \sqrt{\tan x} \cdot \sqrt{\tan x}\]
11. Applied times-frac53.9
  \[\leadsto \color{blue}{\frac{\sqrt[3]{\tan x + \tan \varepsilon} \cdot \sqrt[3]{\tan x + \tan \varepsilon}}{\sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}}} \cdot \frac{\sqrt[3]{\tan x + \tan \varepsilon}}{\sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}}}} - \sqrt{\tan x} \cdot \sqrt{\tan x}\]
12. Applied prod-diff54.0
  \[\leadsto \color{blue}{(\left(\frac{\sqrt[3]{\tan x + \tan \varepsilon} \cdot \sqrt[3]{\tan x + \tan \varepsilon}}{\sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}}}\right) \cdot \left(\frac{\sqrt[3]{\tan x + \tan \varepsilon}}{\sqrt{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x}}}\right) + \left(-\sqrt{\tan x} \cdot \sqrt{\tan x}\right))_* + (\left(-\sqrt{\tan x}\right) \cdot \left(\sqrt{\tan x}\right) + \left(\sqrt{\tan x} \cdot \sqrt{\tan x}\right))_*}\]
13. Simplified53.8
  \[\leadsto \color{blue}{\left(\frac{\tan \varepsilon + \tan x}{(\left(-\tan \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x}\right) + 1)_*} - \tan x\right)} + (\left(-\sqrt{\tan x}\right) \cdot \left(\sqrt{\tan x}\right) + \left(\sqrt{\tan x} \cdot \sqrt{\tan x}\right))_*\]
14. Simplified44.3
  \[\leadsto \left(\frac{\tan \varepsilon + \tan x}{(\left(-\tan \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x}\right) + 1)_*} - \tan x\right) + \color{blue}{0}\]
15. Taylor expanded around 0 27.7
  \[\leadsto \color{blue}{\left(x \cdot {\varepsilon}^{2} + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \varepsilon\right)\right)} + 0\]
16. Simplified27.7
  \[\leadsto \color{blue}{(\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*} + 0\]
Recombined 2 regimes into one program.
Final simplification13.9
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -3.5479355778421913 \cdot 10^{-28} \lor \neg \left(\varepsilon \le 1.146422683164635 \cdot 10^{-17}\right):\\ \;\;\;\;(\left(\frac{\tan \varepsilon + \tan x}{1 - {\left(\frac{\tan \varepsilon \cdot \sin x}{\cos x}\right)}^{3}}\right) \cdot \left(1 + \left(\frac{\tan \varepsilon \cdot \sin x}{\cos x} + \frac{\tan \varepsilon \cdot \sin x}{\cos x} \cdot \frac{\tan \varepsilon \cdot \sin x}{\cos x}\right)\right) + \left(-\tan x\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*\\ \end{array}\]

Error

Target

Derivation

`if eps < -3.5479355778421913e-28 or 1.146422683164635e-17 < eps`

`if -3.5479355778421913e-28 < eps < 1.146422683164635e-17`

Runtime