Error

Target

Derivation

1. Split input into 3 regimes

2. if eps < -3.5084136453538892e-15

   1. Initial program 28.9

      \[\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 add-sqr-sqrt31.0

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \color{blue}{\sqrt{\tan x} \cdot \sqrt{\tan x}}\]

   6. Applied flip--31.0

      \[\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}}} - \sqrt{\tan x} \cdot \sqrt{\tan x}\]

   7. Applied associate-/r/31.0

      \[\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)} - \sqrt{\tan x} \cdot \sqrt{\tan x}\]

   8. Applied prod-diff31.0

      \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\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))_*}\]

   9. Simplified31.0

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

   10. Simplified0.8

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

   if -3.5084136453538892e-15 < eps < 6.918453703437243e-17

   1. Initial program 44.9

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

   3. Applied tan-sum44.8

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

   5. Applied add-log-exp44.8

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
   6. Using strategy rm

   7. Applied tan-quot44.8

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

   8. Applied associate-*l/44.8

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

   9. Taylor expanded around 0 30.4

      \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]

   10. Simplified30.4

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

   if 6.918453703437243e-17 < eps

   1. Initial program 29.9

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

   3. Applied tan-sum0.9

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

   5. Applied add-log-exp1.0

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
   6. Using strategy rm

   7. Applied tan-quot1.0

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

   8. Applied associate-*l/1.0

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\color{blue}{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}}\right)} - \tan x\]
   9. Using strategy rm

   10. Applied add-sqr-sqrt31.7

       \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right)} - \color{blue}{\sqrt{\tan x} \cdot \sqrt{\tan x}}\]

   11. Applied flip--31.7

       \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right) \cdot \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right)}{1 + \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right)}}} - \sqrt{\tan x} \cdot \sqrt{\tan x}\]

   12. Applied associate-/r/31.7

       \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right) \cdot \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right)} \cdot \left(1 + \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right)\right)} - \sqrt{\tan x} \cdot \sqrt{\tan x}\]

   13. Applied prod-diff31.7

       \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right) \cdot \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right)}\right) \cdot \left(1 + \log \left(e^{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}\right)\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))_*}\]

   14. Simplified31.6

       \[\leadsto \color{blue}{\left(\frac{(\left(\frac{\sin x}{\frac{\cos x}{\tan \varepsilon}}\right) \cdot \left(\tan x + \tan \varepsilon\right) + \left(\tan x + \tan \varepsilon\right))_*}{(\left(\frac{\sin x}{\frac{\cos x}{\tan \varepsilon}}\right) \cdot \left(\frac{-\sin x}{\frac{\cos x}{\tan \varepsilon}}\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))_*\]

   15. Simplified0.9

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

4. Final simplification14.8

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

Runtime

Time bar (total: 1.4m)Debug logProfile

herbie shell --seed 2018277 +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)))