\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)}^{3} + {\left(\sin \lambda_1 \cdot \sin \lambda_2\right)}^{3}\right)}{\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \left(\cos \lambda_1 \cdot \cos \lambda_2\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 r24642 = phi1;
double r24643 = sin(r24642);
double r24644 = phi2;
double r24645 = sin(r24644);
double r24646 = r24643 * r24645;
double r24647 = cos(r24642);
double r24648 = cos(r24644);
double r24649 = r24647 * r24648;
double r24650 = lambda1;
double r24651 = lambda2;
double r24652 = r24650 - r24651;
double r24653 = cos(r24652);
double r24654 = r24649 * r24653;
double r24655 = r24646 + r24654;
double r24656 = acos(r24655);
double r24657 = R;
double r24658 = r24656 * r24657;
return r24658;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r24659 = phi1;
double r24660 = sin(r24659);
double r24661 = phi2;
double r24662 = sin(r24661);
double r24663 = r24660 * r24662;
double r24664 = cos(r24659);
double r24665 = cos(r24661);
double r24666 = r24664 * r24665;
double r24667 = lambda1;
double r24668 = cos(r24667);
double r24669 = lambda2;
double r24670 = cos(r24669);
double r24671 = r24668 * r24670;
double r24672 = 3.0;
double r24673 = pow(r24671, r24672);
double r24674 = sin(r24667);
double r24675 = sin(r24669);
double r24676 = r24674 * r24675;
double r24677 = pow(r24676, r24672);
double r24678 = r24673 + r24677;
double r24679 = r24666 * r24678;
double r24680 = r24671 * r24671;
double r24681 = r24676 * r24676;
double r24682 = r24671 * r24676;
double r24683 = r24681 - r24682;
double r24684 = r24680 + r24683;
double r24685 = r24679 / r24684;
double r24686 = r24663 + r24685;
double r24687 = acos(r24686);
double r24688 = R;
double r24689 = r24687 * r24688;
return r24689;
}



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.7
rmApplied flip3-+3.8
Applied associate-*r/3.8
Final simplification3.8
herbie shell --seed 2019351
(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))