Average Error: 15.2 → 0.4
Time: 8.6s
Precision: 64
\[\tan^{-1} \left(x + 1\right) - \tan^{-1} x\]
\[\tan^{-1}_* \frac{1}{x \cdot \left(1 + x\right) + 1}\]
\tan^{-1} \left(x + 1\right) - \tan^{-1} x
\tan^{-1}_* \frac{1}{x \cdot \left(1 + x\right) + 1}
double f(double x) {
        double r3768487 = x;
        double r3768488 = 1.0;
        double r3768489 = r3768487 + r3768488;
        double r3768490 = atan(r3768489);
        double r3768491 = atan(r3768487);
        double r3768492 = r3768490 - r3768491;
        return r3768492;
}

double f(double x) {
        double r3768493 = 1.0;
        double r3768494 = x;
        double r3768495 = r3768493 + r3768494;
        double r3768496 = r3768494 * r3768495;
        double r3768497 = 1.0;
        double r3768498 = r3768496 + r3768497;
        double r3768499 = atan2(r3768493, r3768498);
        return r3768499;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 15.2

    \[\tan^{-1} \left(x + 1\right) - \tan^{-1} x\]
  2. Using strategy rm
  3. Applied diff-atan14.0

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

    \[\leadsto \tan^{-1}_* \frac{\color{blue}{1}}{1 + \left(x + 1\right) \cdot x}\]
  5. Final simplification0.4

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

Reproduce

herbie shell --seed 1 
(FPCore (x)
  :name "atan(x+1)-atan(x)"
  (- (atan (+ x 1.0)) (atan x)))