Error

Target

Derivation

1. Split input into 3 regimes

2. if eps < -1.0227983164462347e-17

   1. Initial program 29.0

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

   3. Applied tan-sum1.0

      \[\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.1

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

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

   8. Applied flip--31.2

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

   9. Applied associate-/r/31.2

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

   10. Applied prod-diff31.2

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

   11. Simplified31.1

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

   12. Simplified1.0

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

   if -1.0227983164462347e-17 < eps < 7.055752543575732e-17

   1. Initial program 44.9

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

   3. Applied tan-sum44.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-exp44.9

      \[\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.9

      \[\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.9

      \[\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.3

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

   if 7.055752543575732e-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 -1.0227983164462347 \cdot 10^{-17}:\\ \;\;\;\;\frac{(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon + \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 7.055752543575732 \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.5m)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)))