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;
}



Try it out

Results

 In Out
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)))