Initial program 16.8
\[\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
\]
Applied egg-rr3.8
\[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)}\right) \cdot R
\]
Taylor expanded in phi1 around 0 3.8
\[\leadsto \color{blue}{\cos^{-1} \left(\cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_2 \cdot \sin \lambda_1\right)\right) + \sin \phi_1 \cdot \sin \phi_2\right)} \cdot R
\]
Simplified3.8
\[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\cos \phi_2, \cos \phi_1 \cdot \mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_2 \cdot \cos \lambda_1\right), \sin \phi_1 \cdot \sin \phi_2\right)\right)} \cdot R
\]
Proof
(acos.f64 (fma.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (fma.f64 (sin.f64 lambda2) (sin.f64 lambda1) (*.f64 (cos.f64 lambda2) (cos.f64 lambda1)))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))): 0 points increase in error, 0 points decrease in error
(acos.f64 (fma.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sin.f64 lambda2) (sin.f64 lambda1)) (*.f64 (cos.f64 lambda2) (cos.f64 lambda1))))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))): 3 points increase in error, 5 points decrease in error
(acos.f64 (fma.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 lambda1) (sin.f64 lambda2))) (*.f64 (cos.f64 lambda2) (cos.f64 lambda1)))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))): 0 points increase in error, 0 points decrease in error
(acos.f64 (fma.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (+.f64 (*.f64 (sin.f64 lambda1) (sin.f64 lambda2)) (Rewrite=> *-commutative_binary64 (*.f64 (cos.f64 lambda1) (cos.f64 lambda2))))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))): 0 points increase in error, 0 points decrease in error
(acos.f64 (fma.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (cos.f64 lambda1) (cos.f64 lambda2)) (*.f64 (sin.f64 lambda1) (sin.f64 lambda2))))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))): 0 points increase in error, 0 points decrease in error
(acos.f64 (fma.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 lambda2) (cos.f64 lambda1))) (*.f64 (sin.f64 lambda1) (sin.f64 lambda2)))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))): 0 points increase in error, 0 points decrease in error
(acos.f64 (fma.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (+.f64 (*.f64 (cos.f64 lambda2) (cos.f64 lambda1)) (Rewrite=> *-commutative_binary64 (*.f64 (sin.f64 lambda2) (sin.f64 lambda1))))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))): 0 points increase in error, 0 points decrease in error
(acos.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (cos.f64 phi2) (*.f64 (cos.f64 phi1) (+.f64 (*.f64 (cos.f64 lambda2) (cos.f64 lambda1)) (*.f64 (sin.f64 lambda2) (sin.f64 lambda1))))) (*.f64 (sin.f64 phi1) (sin.f64 phi2))))): 2 points increase in error, 5 points decrease in error
Final simplification3.8
\[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\cos \phi_2, \cos \phi_1 \cdot \mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_2 \cdot \cos \lambda_1\right), \sin \phi_1 \cdot \sin \phi_2\right)\right) \cdot R
\]