Average Error: 7.2 → 3.9
Time: 6.9s
Precision: 64
$\tan^{-1} y - \tan^{-1} x$
$\tan^{-1}_* \frac{y - x}{1 + y \cdot x}$
\tan^{-1} y - \tan^{-1} x
\tan^{-1}_* \frac{y - x}{1 + y \cdot x}
double f(double y, double x) {
double r1258191 = y;
double r1258192 = atan(r1258191);
double r1258193 = x;
double r1258194 = atan(r1258193);
double r1258195 = r1258192 - r1258194;
return r1258195;
}


double f(double y, double x) {
double r1258196 = y;
double r1258197 = x;
double r1258198 = r1258196 - r1258197;
double r1258199 = 1.0;
double r1258200 = r1258196 * r1258197;
double r1258201 = r1258199 + r1258200;
double r1258202 = atan2(r1258198, r1258201);
return r1258202;
}



# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 7.2

$\tan^{-1} y - \tan^{-1} x$
2. Using strategy rm
3. Applied diff-atan3.9

$\leadsto \color{blue}{\tan^{-1}_* \frac{y - x}{1 + y \cdot x}}$
4. Final simplification3.9

$\leadsto \tan^{-1}_* \frac{y - x}{1 + y \cdot x}$

# Reproduce

herbie shell --seed 1
(FPCore (y x)
:name "atan(y) - atan(x)"
:precision binary64
(- (atan y) (atan x)))