Average Error: 37.3 → 8.3
Time: 4.0m
Precision: 64
Internal Precision: 2368
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\left(\left(\frac{\left(x \cdot x\right) \cdot {\varepsilon}^{3}}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \frac{\varepsilon}{1 - {\left(\varepsilon \cdot x\right)}^{3}}\right) + \left(\frac{x}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \left(-x\right)\right)\right) + \frac{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \le -2.084504492194263 \cdot 10^{-45}:\\ \;\;\;\;\left(\left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1\right) \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} - \tan x\right) + \frac{\left(\sqrt[3]{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \sqrt[3]{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \sqrt[3]{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\\ \mathbf{elif}\;\left(\left(\frac{\left(x \cdot x\right) \cdot {\varepsilon}^{3}}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \frac{\varepsilon}{1 - {\left(\varepsilon \cdot x\right)}^{3}}\right) + \left(\frac{x}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \left(-x\right)\right)\right) + \frac{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \le 4.215177757707313 \cdot 10^{-42}:\\ \;\;\;\;\left(\left(\frac{\left(x \cdot x\right) \cdot {\varepsilon}^{3}}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \frac{\varepsilon}{1 - {\left(\varepsilon \cdot x\right)}^{3}}\right) + \left(\frac{x}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \left(-x\right)\right)\right) + \frac{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1\right) \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} - \tan x\right) + \frac{\frac{\left(\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan x\right) \cdot \left(\sin \varepsilon \cdot \tan x\right)}{\cos \varepsilon \cdot \left(\tan \varepsilon - \tan x\right)}}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\\ \end{array}\]

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original37.3
Target15.3
Herbie8.3
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 3 regimes

  2. if (+ (/ (* (* (tan eps) (tan x)) (+ (tan eps) (tan x))) (- 1 (pow (* (tan eps) (tan x)) 3))) (+ (+ (/ (* (pow eps 3) (* x x)) (- 1 (pow (* x eps) 3))) (/ eps (- 1 (pow (* x eps) 3)))) (+ (/ x (- 1 (pow (* x eps) 3))) (- x)))) < -2.084504492194263e-45

    1. Initial program 19.2

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

    3. Applied tan-sum11.1

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

    5. Applied flip3--11.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/11.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. Simplified11.1

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

    9. Applied distribute-lft-in11.1

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

    10. Applied associate--l+9.4

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

    11. Simplified9.4

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

    13. Applied add-cube-cbrt9.4

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

    if -2.084504492194263e-45 < (+ (/ (* (* (tan eps) (tan x)) (+ (tan eps) (tan x))) (- 1 (pow (* (tan eps) (tan x)) 3))) (+ (+ (/ (* (pow eps 3) (* x x)) (- 1 (pow (* x eps) 3))) (/ eps (- 1 (pow (* x eps) 3)))) (+ (/ x (- 1 (pow (* x eps) 3))) (- x)))) < 4.215177757707313e-42

    1. Initial program 40.2

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

    3. Applied tan-sum40.2

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

    5. Applied flip3--40.2

      \[\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/40.2

      \[\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. Simplified40.2

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

    9. Applied distribute-lft-in40.2

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

    10. Applied associate--l+37.5

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

    11. Simplified37.5

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

    12. Taylor expanded around 0 56.9

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

    13. Simplified0.1

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

    if 4.215177757707313e-42 < (+ (/ (* (* (tan eps) (tan x)) (+ (tan eps) (tan x))) (- 1 (pow (* (tan eps) (tan x)) 3))) (+ (+ (/ (* (pow eps 3) (* x x)) (- 1 (pow (* x eps) 3))) (/ eps (- 1 (pow (* x eps) 3)))) (+ (/ x (- 1 (pow (* x eps) 3))) (- x))))

    1. Initial program 39.2

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

    3. Applied tan-sum14.4

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

    5. Applied flip3--14.5

      \[\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/14.5

      \[\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. Simplified14.5

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

    9. Applied distribute-lft-in14.5

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

    10. Applied associate--l+12.4

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

    11. Simplified12.4

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

    13. Applied flip-+12.4

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

    14. Applied tan-quot12.4

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

    15. Applied associate-*l/12.4

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

    16. Applied frac-times12.4

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

  4. Final simplification8.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(\frac{\left(x \cdot x\right) \cdot {\varepsilon}^{3}}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \frac{\varepsilon}{1 - {\left(\varepsilon \cdot x\right)}^{3}}\right) + \left(\frac{x}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \left(-x\right)\right)\right) + \frac{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \le -2.084504492194263 \cdot 10^{-45}:\\ \;\;\;\;\left(\left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1\right) \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} - \tan x\right) + \frac{\left(\sqrt[3]{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \sqrt[3]{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \sqrt[3]{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\\ \mathbf{elif}\;\left(\left(\frac{\left(x \cdot x\right) \cdot {\varepsilon}^{3}}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \frac{\varepsilon}{1 - {\left(\varepsilon \cdot x\right)}^{3}}\right) + \left(\frac{x}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \left(-x\right)\right)\right) + \frac{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \le 4.215177757707313 \cdot 10^{-42}:\\ \;\;\;\;\left(\left(\frac{\left(x \cdot x\right) \cdot {\varepsilon}^{3}}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \frac{\varepsilon}{1 - {\left(\varepsilon \cdot x\right)}^{3}}\right) + \left(\frac{x}{1 - {\left(\varepsilon \cdot x\right)}^{3}} + \left(-x\right)\right)\right) + \frac{\left(\tan x + \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1\right) \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} - \tan x\right) + \frac{\frac{\left(\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan x\right) \cdot \left(\sin \varepsilon \cdot \tan x\right)}{\cos \varepsilon \cdot \left(\tan \varepsilon - \tan x\right)}}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\\ \end{array}\]

Runtime

Time bar (total: 4.0m)Debug logProfile

herbie shell --seed 2018214 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

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

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