\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R\cos^{-1} \left(\sin \phi_2 \cdot \sin \phi_1 + \frac{\left(\left(\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + \left(\left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + \left(\left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right) \cdot Rdouble f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r570373 = phi1;
double r570374 = sin(r570373);
double r570375 = phi2;
double r570376 = sin(r570375);
double r570377 = r570374 * r570376;
double r570378 = cos(r570373);
double r570379 = cos(r570375);
double r570380 = r570378 * r570379;
double r570381 = lambda1;
double r570382 = lambda2;
double r570383 = r570381 - r570382;
double r570384 = cos(r570383);
double r570385 = r570380 * r570384;
double r570386 = r570377 + r570385;
double r570387 = acos(r570386);
double r570388 = R;
double r570389 = r570387 * r570388;
return r570389;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r570390 = phi2;
double r570391 = sin(r570390);
double r570392 = phi1;
double r570393 = sin(r570392);
double r570394 = r570391 * r570393;
double r570395 = lambda2;
double r570396 = cos(r570395);
double r570397 = lambda1;
double r570398 = cos(r570397);
double r570399 = r570396 * r570398;
double r570400 = r570399 * r570399;
double r570401 = r570400 * r570399;
double r570402 = sin(r570397);
double r570403 = sin(r570395);
double r570404 = r570402 * r570403;
double r570405 = r570404 * r570404;
double r570406 = r570405 * r570404;
double r570407 = r570401 + r570406;
double r570408 = cos(r570392);
double r570409 = cos(r570390);
double r570410 = r570408 * r570409;
double r570411 = r570407 * r570410;
double r570412 = r570399 * r570404;
double r570413 = r570405 - r570412;
double r570414 = r570400 + r570413;
double r570415 = r570411 / r570414;
double r570416 = r570394 + r570415;
double r570417 = acos(r570416);
double r570418 = R;
double r570419 = r570417 * r570418;
return r570419;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 16.7
rmApplied cos-diff3.7
rmApplied flip3-+3.8
Applied associate-*r/3.8
Simplified3.7
Final simplification3.7
herbie shell --seed 2019152
(FPCore (R lambda1 lambda2 phi1 phi2)
:name "Spherical law of cosines"
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))