Error

Target

Derivation

1. Initial program 15.3

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

3. Applied diff-atan14.0

   \[\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. Taylor expanded around 0 0.4

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

9. Final simplification0.4

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

Reproduce

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

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

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