\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_1 \cdot \sin \phi_2 + \frac{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \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)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}\right) \cdot Rdouble f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r20975 = phi1;
double r20976 = sin(r20975);
double r20977 = phi2;
double r20978 = sin(r20977);
double r20979 = r20976 * r20978;
double r20980 = cos(r20975);
double r20981 = cos(r20977);
double r20982 = r20980 * r20981;
double r20983 = lambda1;
double r20984 = lambda2;
double r20985 = r20983 - r20984;
double r20986 = cos(r20985);
double r20987 = r20982 * r20986;
double r20988 = r20979 + r20987;
double r20989 = acos(r20988);
double r20990 = R;
double r20991 = r20989 * r20990;
return r20991;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r20992 = phi1;
double r20993 = sin(r20992);
double r20994 = phi2;
double r20995 = sin(r20994);
double r20996 = r20993 * r20995;
double r20997 = cos(r20992);
double r20998 = cos(r20994);
double r20999 = r20997 * r20998;
double r21000 = lambda1;
double r21001 = cos(r21000);
double r21002 = lambda2;
double r21003 = cos(r21002);
double r21004 = r21001 * r21003;
double r21005 = r21004 * r21004;
double r21006 = sin(r21000);
double r21007 = sin(r21002);
double r21008 = r21006 * r21007;
double r21009 = r21008 * r21008;
double r21010 = r21005 - r21009;
double r21011 = r20999 * r21010;
double r21012 = r21004 - r21008;
double r21013 = r21011 / r21012;
double r21014 = r20996 + r21013;
double r21015 = acos(r21014);
double r21016 = R;
double r21017 = r21015 * r21016;
return r21017;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 17.3
rmApplied cos-diff3.8
rmApplied flip-+3.8
Applied associate-*r/3.8
Final simplification3.8
herbie shell --seed 2019353
(FPCore (R lambda1 lambda2 phi1 phi2)
:name "Spherical law of cosines"
:precision binary64
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))