Error

Target

Derivation

1. Split input into 3 regimes

2. if eps < -1.773639946594851e-15

   1. Initial program 30.8

      \[\tan \left(x + \varepsilon\right) - \tan x\]
   2. Using strategy rm

   3. Applied tan-sum0.7

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
   4. Using strategy rm

   5. Applied flip3--0.7

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]

   6. Applied associate-/r/0.7

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]

   7. Applied fma-neg0.7

      \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\right) \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*}\]

   8. Simplified0.7

      \[\leadsto (\color{blue}{\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right)} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*\]
   9. Using strategy rm

   10. Applied associate-*l*0.7

       \[\leadsto (\left(\frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\left(\tan \varepsilon \cdot \left(\tan x \cdot \left(\tan \varepsilon \cdot \tan x\right)\right)\right)} \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right) \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*\]

   if -1.773639946594851e-15 < eps < 2.7756310660190313e-34

   1. Initial program 45.1

      \[\tan \left(x + \varepsilon\right) - \tan x\]
   2. Using strategy rm

   3. Applied tan-sum45.1

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
   4. Using strategy rm

   5. Applied flip3--45.1

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]

   6. Applied associate-/r/45.1

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]

   7. Applied fma-neg45.1

      \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\right) \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*}\]

   8. Simplified45.1

      \[\leadsto (\color{blue}{\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right)} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*\]

   9. Taylor expanded around -inf 45.1

      \[\leadsto \color{blue}{\left(\frac{{\left(\sin x\right)}^{2} \cdot \sin \varepsilon}{{\left(\cos x\right)}^{2} \cdot \left(\cos \varepsilon \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{3} \cdot \left({\left(\cos \varepsilon\right)}^{2} \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{\sin x \cdot {\left(\sin \varepsilon\right)}^{2}}{\cos x \cdot \left({\left(\cos \varepsilon\right)}^{2} \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{2} \cdot \left({\left(\cos \varepsilon\right)}^{3} \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right) \cdot \cos \varepsilon} + \frac{\sin x}{\cos x \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)}\right)\right)\right)\right)\right) - \frac{\sin x}{\cos x}}\]

   10. Simplified40.5

       \[\leadsto \color{blue}{(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right) + \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon} + \frac{\frac{\sin x}{\cos x}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right))_*\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*}\]

   11. Taylor expanded around 0 10.7

       \[\leadsto (\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \color{blue}{\left(x \cdot {\varepsilon}^{2} + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \varepsilon\right)\right)})_*\]

   12. Simplified10.7

       \[\leadsto (\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \color{blue}{\left((\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*\right)})_*\]

   if 2.7756310660190313e-34 < eps

   1. Initial program 28.8

      \[\tan \left(x + \varepsilon\right) - \tan x\]
   2. Using strategy rm

   3. Applied tan-sum2.9

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
   4. Using strategy rm

   5. Applied flip3--3.0

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]

   6. Applied associate-/r/3.0

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]

   7. Applied fma-neg2.9

      \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\right) \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*}\]

   8. Simplified2.9

      \[\leadsto (\color{blue}{\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right)} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*\]

   9. Taylor expanded around -inf 3.2

      \[\leadsto \color{blue}{\left(\frac{{\left(\sin x\right)}^{2} \cdot \sin \varepsilon}{{\left(\cos x\right)}^{2} \cdot \left(\cos \varepsilon \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{2}}{{\left(\cos x\right)}^{3} \cdot \left({\left(\cos \varepsilon\right)}^{2} \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{\sin x \cdot {\left(\sin \varepsilon\right)}^{2}}{\cos x \cdot \left({\left(\cos \varepsilon\right)}^{2} \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{{\left(\sin x\right)}^{2} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{2} \cdot \left({\left(\cos \varepsilon\right)}^{3} \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)\right)} + \left(\frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right) \cdot \cos \varepsilon} + \frac{\sin x}{\cos x \cdot \left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right)}\right)\right)\right)\right)\right) - \frac{\sin x}{\cos x}}\]

   10. Simplified2.8

       \[\leadsto \color{blue}{(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \left((\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon}\right) + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right) + \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon} + \frac{\frac{\sin x}{\cos x}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right))_*\right))_*\right))_* - \frac{\sin x}{\cos x}\right))_*}\]
   11. Using strategy rm

   12. Applied fma-udef2.8

       \[\leadsto (\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \left(\color{blue}{\left(\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon} + (\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right) + \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon} + \frac{\frac{\sin x}{\cos x}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right))_*\right))_*\right)} - \frac{\sin x}{\cos x}\right))_*\]

   13. Applied associate--l+2.8

       \[\leadsto (\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \color{blue}{\left(\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon} + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right) + \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon} + \frac{\frac{\sin x}{\cos x}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\left(\cos \varepsilon \cdot \cos \varepsilon\right) \cdot \cos \varepsilon}{\sin \varepsilon \cdot \sin \varepsilon}}}\right))_*\right))_* - \frac{\sin x}{\cos x}\right)\right)})_*\]
3. Recombined 3 regimes into one program.

4. Final simplification5.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.773639946594851 \cdot 10^{-15}:\\ \;\;\;\;(\left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\left(\tan x \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \tan \varepsilon\right)}\right) \cdot \left(\left(\tan x \cdot \tan \varepsilon + \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) + 1\right) + \left(-\tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 2.7756310660190313 \cdot 10^{-34}:\\ \;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \left((\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right) + \left(\left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon} + \left((\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon \cdot \sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon \cdot \cos \varepsilon}\right) + \left((\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}}\right) + \left(\frac{\frac{\sin x}{\cos x}}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}} + \frac{\frac{\sin \varepsilon}{1 - \left(\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\sin \varepsilon}{\frac{\cos \varepsilon \cdot \left(\cos \varepsilon \cdot \cos \varepsilon\right)}{\sin \varepsilon \cdot \sin \varepsilon}}}}{\cos \varepsilon}\right))_*\right))_* - \frac{\sin x}{\cos x}\right)\right))_*\\ \end{array}\]

Reproduce

herbie shell --seed 2019050 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))