\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 RR \cdot e^{\log \left(\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)\right)}double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r1289181 = phi1;
double r1289182 = sin(r1289181);
double r1289183 = phi2;
double r1289184 = sin(r1289183);
double r1289185 = r1289182 * r1289184;
double r1289186 = cos(r1289181);
double r1289187 = cos(r1289183);
double r1289188 = r1289186 * r1289187;
double r1289189 = lambda1;
double r1289190 = lambda2;
double r1289191 = r1289189 - r1289190;
double r1289192 = cos(r1289191);
double r1289193 = r1289188 * r1289192;
double r1289194 = r1289185 + r1289193;
double r1289195 = acos(r1289194);
double r1289196 = R;
double r1289197 = r1289195 * r1289196;
return r1289197;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r1289198 = R;
double r1289199 = phi2;
double r1289200 = sin(r1289199);
double r1289201 = phi1;
double r1289202 = sin(r1289201);
double r1289203 = r1289200 * r1289202;
double r1289204 = lambda2;
double r1289205 = cos(r1289204);
double r1289206 = lambda1;
double r1289207 = cos(r1289206);
double r1289208 = r1289205 * r1289207;
double r1289209 = r1289208 * r1289208;
double r1289210 = r1289209 * r1289208;
double r1289211 = sin(r1289206);
double r1289212 = sin(r1289204);
double r1289213 = r1289211 * r1289212;
double r1289214 = r1289213 * r1289213;
double r1289215 = r1289214 * r1289213;
double r1289216 = r1289210 + r1289215;
double r1289217 = cos(r1289201);
double r1289218 = cos(r1289199);
double r1289219 = r1289217 * r1289218;
double r1289220 = r1289216 * r1289219;
double r1289221 = r1289208 * r1289213;
double r1289222 = r1289214 - r1289221;
double r1289223 = r1289209 + r1289222;
double r1289224 = r1289220 / r1289223;
double r1289225 = r1289203 + r1289224;
double r1289226 = acos(r1289225);
double r1289227 = log(r1289226);
double r1289228 = exp(r1289227);
double r1289229 = r1289198 * r1289228;
return r1289229;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



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