Average Error: 15.4 → 0.4
Time: 24.3s
Precision: 64
\[\tan^{-1} \left(N + 1.0\right) - \tan^{-1} N\]
↓
\[\tan^{-1}_* \frac{1.0}{1 + N \cdot \left(1.0 + N\right)}\]
\tan^{-1} \left(N + 1.0\right) - \tan^{-1} N
↓
\tan^{-1}_* \frac{1.0}{1 + N \cdot \left(1.0 + N\right)}
double f(double N) {
        double r6942339 = N;
        double r6942340 = 1.0;
        double r6942341 = r6942339 + r6942340;
        double r6942342 = atan(r6942341);
        double r6942343 = atan(r6942339);
        double r6942344 = r6942342 - r6942343;
        return r6942344;
}
↓
double f(double N) {
        double r6942345 = 1.0;
        double r6942346 = 1.0;
        double r6942347 = N;
        double r6942348 = r6942345 + r6942347;
        double r6942349 = r6942347 * r6942348;
        double r6942350 = r6942346 + r6942349;
        double r6942351 = atan2(r6942345, r6942350);
        return r6942351;
}

Error

Bits error versus N

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original15.4
Target0.4
Herbie0.4
\[\tan^{-1} \left(\frac{1.0}{1.0 + N \cdot \left(N + 1.0\right)}\right)\]

Derivation

  1. Initial program 15.4

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

  3. Applied diff-atan14.3

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

  4. Simplified0.4

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

  5. Final simplification0.4

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

Reproduce

herbie shell --seed 2019165 
(FPCore (N)
  :name "2atan (example 3.5)"

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

  (- (atan (+ N 1.0)) (atan N)))