\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\frac{\frac{\pi \cdot \pi}{4} - \sin^{-1} \left(\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right) + \sin \phi_1 \cdot \sin \phi_2\right) \cdot \sin^{-1} \left(\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right) + \sin \phi_1 \cdot \sin \phi_2\right)}{\frac{\pi}{2} + \sin^{-1} \left(\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right) + \sin \phi_1 \cdot \sin \phi_2\right)} \cdot Rdouble f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r26697 = phi1;
double r26698 = sin(r26697);
double r26699 = phi2;
double r26700 = sin(r26699);
double r26701 = r26698 * r26700;
double r26702 = cos(r26697);
double r26703 = cos(r26699);
double r26704 = r26702 * r26703;
double r26705 = lambda1;
double r26706 = lambda2;
double r26707 = r26705 - r26706;
double r26708 = cos(r26707);
double r26709 = r26704 * r26708;
double r26710 = r26701 + r26709;
double r26711 = acos(r26710);
double r26712 = R;
double r26713 = r26711 * r26712;
return r26713;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r26714 = atan2(1.0, 0.0);
double r26715 = r26714 * r26714;
double r26716 = 4.0;
double r26717 = r26715 / r26716;
double r26718 = phi1;
double r26719 = cos(r26718);
double r26720 = phi2;
double r26721 = cos(r26720);
double r26722 = lambda1;
double r26723 = cos(r26722);
double r26724 = lambda2;
double r26725 = cos(r26724);
double r26726 = r26723 * r26725;
double r26727 = sin(r26722);
double r26728 = sin(r26724);
double r26729 = r26727 * r26728;
double r26730 = r26726 + r26729;
double r26731 = r26721 * r26730;
double r26732 = r26719 * r26731;
double r26733 = sin(r26718);
double r26734 = sin(r26720);
double r26735 = r26733 * r26734;
double r26736 = r26732 + r26735;
double r26737 = asin(r26736);
double r26738 = r26737 * r26737;
double r26739 = r26717 - r26738;
double r26740 = 2.0;
double r26741 = r26714 / r26740;
double r26742 = r26741 + r26737;
double r26743 = r26739 / r26742;
double r26744 = R;
double r26745 = r26743 * r26744;
return r26745;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 16.9
rmApplied sub-neg16.9
Applied cos-sum3.7
Simplified3.7
rmApplied acos-asin3.8
Simplified3.8
rmApplied flip--3.9
Simplified3.9
Final simplification3.9
herbie shell --seed 2020046
(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))