Average Error: 31.9 → 7.4
Time: 27.2s
Precision: 64
$\tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right) + z\right)$
$\begin{array}{l} \mathbf{if}\;z \le -5.24409163734940734375211746442910245531 \cdot 10^{-32} \lor \neg \left(z \le 1.86406985634181338373775414712502690213 \cdot 10^{-43}\right):\\ \;\;\;\;\frac{\tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right) + \tan z}{1 - \frac{\sin \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right)}{\cos \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right)} \cdot \tan z}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{y - x}{1 + x \cdot y} + \tan z}{1 - \tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right) \cdot \tan z}\\ \end{array}$
\tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right) + z\right)
\begin{array}{l}
\mathbf{if}\;z \le -5.24409163734940734375211746442910245531 \cdot 10^{-32} \lor \neg \left(z \le 1.86406985634181338373775414712502690213 \cdot 10^{-43}\right):\\
\;\;\;\;\frac{\tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right) + \tan z}{1 - \frac{\sin \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right)}{\cos \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right)} \cdot \tan z}\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{y - x}{1 + x \cdot y} + \tan z}{1 - \tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right) \cdot \tan z}\\

\end{array}
double f(double y, double x, double z) {
double r1272628 = y;
double r1272629 = x;
double r1272630 = r1272628 - r1272629;
double r1272631 = 1.0;
double r1272632 = r1272629 * r1272628;
double r1272633 = r1272631 + r1272632;
double r1272634 = r1272630 / r1272633;
double r1272635 = atan(r1272634);
double r1272636 = z;
double r1272637 = r1272635 + r1272636;
double r1272638 = tan(r1272637);
return r1272638;
}


double f(double y, double x, double z) {
double r1272639 = z;
double r1272640 = -5.244091637349407e-32;
bool r1272641 = r1272639 <= r1272640;
double r1272642 = 1.8640698563418134e-43;
bool r1272643 = r1272639 <= r1272642;
double r1272644 = !r1272643;
bool r1272645 = r1272641 || r1272644;
double r1272646 = y;
double r1272647 = x;
double r1272648 = r1272646 - r1272647;
double r1272649 = 1.0;
double r1272650 = r1272647 * r1272646;
double r1272651 = r1272649 + r1272650;
double r1272652 = r1272648 / r1272651;
double r1272653 = atan(r1272652);
double r1272654 = tan(r1272653);
double r1272655 = tan(r1272639);
double r1272656 = r1272654 + r1272655;
double r1272657 = 1.0;
double r1272658 = sin(r1272653);
double r1272659 = cos(r1272653);
double r1272660 = r1272658 / r1272659;
double r1272661 = r1272660 * r1272655;
double r1272662 = r1272657 - r1272661;
double r1272663 = r1272656 / r1272662;
double r1272664 = r1272652 + r1272655;
double r1272665 = r1272654 * r1272655;
double r1272666 = r1272657 - r1272665;
double r1272667 = r1272664 / r1272666;
double r1272668 = r1272645 ? r1272663 : r1272667;
return r1272668;
}



# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Split input into 2 regimes
2. ## if z < -5.244091637349407e-32 or 1.8640698563418134e-43 < z

1. Initial program 31.0

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

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

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

## if -5.244091637349407e-32 < z < 1.8640698563418134e-43

1. Initial program 33.0

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

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

$\leadsto \frac{\color{blue}{\frac{y - x}{1 + x \cdot y}} + \tan z}{1 - \tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right) \cdot \tan z}$
3. Recombined 2 regimes into one program.
4. Final simplification7.4

$\leadsto \begin{array}{l} \mathbf{if}\;z \le -5.24409163734940734375211746442910245531 \cdot 10^{-32} \lor \neg \left(z \le 1.86406985634181338373775414712502690213 \cdot 10^{-43}\right):\\ \;\;\;\;\frac{\tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right) + \tan z}{1 - \frac{\sin \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right)}{\cos \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right)} \cdot \tan z}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{y - x}{1 + x \cdot y} + \tan z}{1 - \tan \left(\tan^{-1} \left(\frac{y - x}{1 + x \cdot y}\right)\right) \cdot \tan z}\\ \end{array}$

# Reproduce

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