\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(\frac{\left(\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2} + \mathsf{log1p}\left(\mathsf{expm1}\left(\sin \phi_2 \cdot \sin \phi_1\right)\right)\right) \cdot Rdouble f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r1713313 = phi1;
double r1713314 = sin(r1713313);
double r1713315 = phi2;
double r1713316 = sin(r1713315);
double r1713317 = r1713314 * r1713316;
double r1713318 = cos(r1713313);
double r1713319 = cos(r1713315);
double r1713320 = r1713318 * r1713319;
double r1713321 = lambda1;
double r1713322 = lambda2;
double r1713323 = r1713321 - r1713322;
double r1713324 = cos(r1713323);
double r1713325 = r1713320 * r1713324;
double r1713326 = r1713317 + r1713325;
double r1713327 = acos(r1713326);
double r1713328 = R;
double r1713329 = r1713327 * r1713328;
return r1713329;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r1713330 = lambda1;
double r1713331 = cos(r1713330);
double r1713332 = lambda2;
double r1713333 = cos(r1713332);
double r1713334 = r1713331 * r1713333;
double r1713335 = r1713334 * r1713334;
double r1713336 = sin(r1713330);
double r1713337 = sin(r1713332);
double r1713338 = r1713336 * r1713337;
double r1713339 = r1713338 * r1713338;
double r1713340 = r1713335 - r1713339;
double r1713341 = phi1;
double r1713342 = cos(r1713341);
double r1713343 = phi2;
double r1713344 = cos(r1713343);
double r1713345 = r1713342 * r1713344;
double r1713346 = r1713340 * r1713345;
double r1713347 = r1713334 - r1713338;
double r1713348 = r1713346 / r1713347;
double r1713349 = sin(r1713343);
double r1713350 = sin(r1713341);
double r1713351 = r1713349 * r1713350;
double r1713352 = expm1(r1713351);
double r1713353 = log1p(r1713352);
double r1713354 = r1713348 + r1713353;
double r1713355 = acos(r1713354);
double r1713356 = R;
double r1713357 = r1713355 * r1713356;
return r1713357;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 16.8
rmApplied cos-diff3.9
rmApplied log1p-expm1-u3.9
rmApplied flip-+3.9
Applied associate-*r/3.9
Final simplification3.9
herbie shell --seed 2019144 +o rules:numerics
(FPCore (R lambda1 lambda2 phi1 phi2)
:name "Spherical law of cosines"
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))