Error

Target

Derivation

1. Initial program 14.7

   \[\tan^{-1} \left(N + 1\right) - \tan^{-1} N\]
2. Using strategy rm

3. Applied diff-atan13.7

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

4. Simplified0.4

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

5. Simplified0.4

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

7. Applied add-sqr-sqrt0.4

   \[\leadsto \tan^{-1}_* \frac{1}{\color{blue}{\sqrt{(N \cdot \left(N + 1\right) + 1)_*} \cdot \sqrt{(N \cdot \left(N + 1\right) + 1)_*}}}\]
8. Using strategy rm

9. Applied pow10.4

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

10. Applied pow10.4

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

11. Applied pow-prod-down0.4

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

12. Simplified0.4

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

13. Final simplification0.4

    \[\leadsto \tan^{-1}_* \frac{1}{N + (N \cdot N + 1)_*}\]

Runtime

Time bar (total: 9.8s)Debug logProfile

herbie shell --seed 2018278 +o rules:numerics
(FPCore (N)
  :name "2atan (example 3.5)"

  :herbie-target
  (atan (/ 1 (+ 1 (* N (+ N 1)))))

  (- (atan (+ N 1)) (atan N)))