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

Error

Bits error versus y

Bits error versus x

Try it out

Your Program's Arguments

Results

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