Average Error: 40.8 → 40.6
Time: 25.2s
Precision: 64
$\tan \left(\tan^{-1} x + z \cdot \left(\tan^{-1} y - \tan^{-1} x\right)\right)$
$\frac{\sin \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}{\cos \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}$
\tan \left(\tan^{-1} x + z \cdot \left(\tan^{-1} y - \tan^{-1} x\right)\right)
\frac{\sin \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}{\cos \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}
double f(double x, double z, double y) {
double r1280296 = x;
double r1280297 = atan(r1280296);
double r1280298 = z;
double r1280299 = y;
double r1280300 = atan(r1280299);
double r1280301 = r1280300 - r1280297;
double r1280302 = r1280298 * r1280301;
double r1280303 = r1280297 + r1280302;
double r1280304 = tan(r1280303);
return r1280304;
}


double f(double x, double z, double y) {
double r1280305 = x;
double r1280306 = atan(r1280305);
double r1280307 = z;
double r1280308 = y;
double r1280309 = r1280308 - r1280305;
double r1280310 = r1280305 * r1280308;
double r1280311 = 1.0;
double r1280312 = r1280310 + r1280311;
double r1280313 = atan2(r1280309, r1280312);
double r1280314 = r1280307 * r1280313;
double r1280315 = r1280306 + r1280314;
double r1280316 = sin(r1280315);
double r1280317 = cos(r1280315);
double r1280318 = r1280316 / r1280317;
return r1280318;
}



# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 40.8

$\tan \left(\tan^{-1} x + z \cdot \left(\tan^{-1} y - \tan^{-1} x\right)\right)$
2. Using strategy rm
3. Applied diff-atan40.6

$\leadsto \tan \left(\tan^{-1} x + z \cdot \color{blue}{\tan^{-1}_* \frac{y - x}{1 + y \cdot x}}\right)$
4. Using strategy rm
5. Applied tan-quot40.6

$\leadsto \color{blue}{\frac{\sin \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{1 + y \cdot x}\right)}{\cos \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{1 + y \cdot x}\right)}}$
6. Simplified40.6

$\leadsto \frac{\color{blue}{\sin \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}}{\cos \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{1 + y \cdot x}\right)}$
7. Simplified40.6

$\leadsto \frac{\sin \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}{\color{blue}{\cos \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}}$
8. Final simplification40.6

$\leadsto \frac{\sin \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}{\cos \left(\tan^{-1} x + z \cdot \tan^{-1}_* \frac{y - x}{x \cdot y + 1}\right)}$

# Reproduce

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