Spherical law of cosines

1. Initial program 74.0%

   \[\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 \]
2. Step-by-step derivation

   1. fma-def74.1%

      \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

   2. associate-*l*74.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

3. Simplified74.1%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
4. Step-by-step derivation

   1. associate-*r*74.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

   2. cos-diff94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

   3. distribute-lft-in94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

5. Applied egg-rr94.2%

   \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

6. Final simplification94.2%

   \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)\right) \cdot R \]

1. Initial program 74.0%

   \[\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 \]
2. Step-by-step derivation

   1. fma-def74.1%

      \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

   2. associate-*l*74.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

3. Simplified74.1%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
4. Step-by-step derivation

   1. associate-*r*74.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

   2. cos-diff94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

   3. distribute-lft-in94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

5. Applied egg-rr94.2%

   \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

6. Taylor expanded in phi2 around inf 94.2%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right) + \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right)} \cdot R \]
7. Step-by-step derivation

   1. distribute-lft-out94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)}\right)\right) \cdot R \]

   2. cos-neg94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\color{blue}{\cos \left(-\lambda_2\right)} \cdot \cos \lambda_1\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

   3. *-commutative94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \left(-\lambda_2\right)\right)} + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

   4. cos-neg94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \color{blue}{\cos \lambda_2}\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

   5. *-commutative94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \cos \phi_1 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right)\right) \cdot R \]

   6. distribute-lft-out94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \color{blue}{\left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right)\right) \cdot R \]

   7. +-commutative94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)}\right)\right)\right) \cdot R \]

   8. *-commutative94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\color{blue}{\sin \lambda_2 \cdot \sin \lambda_1} + \cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)\right) \cdot R \]

   9. fma-def94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \cos \lambda_2\right)}\right)\right)\right) \cdot R \]

8. Simplified94.1%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)\right)} \cdot R \]

9. Final simplification94.1%

   \[\leadsto R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)\right) \]

1. Initial program 74.0%

   \[\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 \]
2. Step-by-step derivation

   1. cos-diff35.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

3. Applied egg-rr94.1%

   \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right) \cdot R \]
4. Step-by-step derivation

   1. cos-neg35.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \lambda_1 \cdot \color{blue}{\cos \left(-\lambda_2\right)} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

   2. *-commutative35.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\color{blue}{\cos \left(-\lambda_2\right) \cdot \cos \lambda_1} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

   3. fma-def35.2%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\mathsf{fma}\left(\cos \left(-\lambda_2\right), \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   4. cos-neg35.2%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \mathsf{fma}\left(\color{blue}{\cos \lambda_2}, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

5. Simplified94.1%

   \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)}\right) \cdot R \]

6. Final simplification94.1%

   \[\leadsto R \cdot \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)\right) \]

1. Initial program 74.0%

   \[\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 \]
2. Step-by-step derivation

   1. fma-def74.1%

      \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

   2. associate-*l*74.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

3. Simplified74.1%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
4. Step-by-step derivation

   1. cos-diff35.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   2. +-commutative35.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

5. Applied egg-rr94.2%

   \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)}\right)\right)\right) \cdot R \]

6. Final simplification94.2%

   \[\leadsto R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \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)\right)\right) \]

1. Initial program 74.0%

   \[\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 \]
2. Step-by-step derivation

   1. fma-def74.1%

      \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

   2. associate-*l*74.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

3. Simplified74.1%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
4. Step-by-step derivation

   1. associate-*r*74.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

   2. cos-diff94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

   3. distribute-lft-in94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

5. Applied egg-rr94.2%

   \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

6. Taylor expanded in phi2 around inf 94.2%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right) + \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right)} \cdot R \]
7. Step-by-step derivation

   1. distribute-lft-out94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)}\right)\right) \cdot R \]

   2. cos-neg94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\color{blue}{\cos \left(-\lambda_2\right)} \cdot \cos \lambda_1\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

   3. *-commutative94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \left(-\lambda_2\right)\right)} + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

   4. cos-neg94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \color{blue}{\cos \lambda_2}\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

   5. *-commutative94.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \cos \phi_1 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right)\right) \cdot R \]

   6. distribute-lft-out94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \color{blue}{\left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right)\right) \cdot R \]

   7. +-commutative94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)}\right)\right)\right) \cdot R \]

   8. *-commutative94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\color{blue}{\sin \lambda_2 \cdot \sin \lambda_1} + \cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)\right) \cdot R \]

   9. fma-def94.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \cos \lambda_2\right)}\right)\right)\right) \cdot R \]

8. Simplified94.1%

   \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)\right)} \cdot R \]

9. Taylor expanded in lambda2 around inf 94.1%

   \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1 + \cos \lambda_2 \cdot \cos \lambda_1\right)\right)}\right)\right) \cdot R \]

10. Final simplification94.1%

    \[\leadsto R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\right)\right) \]

1. Split input into 3 regimes

2. if phi2 < -1.6500000000000001e-5

   1. Initial program 74.6%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def74.7%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*74.7%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified74.7%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]

   4. Taylor expanded in lambda1 around 0 60.6%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \left(-\lambda_2\right)\right)}\right)\right) \cdot R \]
   5. Step-by-step derivation

      1. *-commutative60.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \color{blue}{\left(\cos \left(-\lambda_2\right) \cdot \cos \phi_1\right)}\right)\right) \cdot R \]

      2. cos-neg60.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\color{blue}{\cos \lambda_2} \cdot \cos \phi_1\right)\right)\right) \cdot R \]

   6. Simplified60.6%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \phi_1\right)}\right)\right) \cdot R \]

   if -1.6500000000000001e-5 < phi2 < 2.25e-13

   1. Initial program 66.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 \]
   2. Step-by-step derivation

      1. fma-def66.8%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*66.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified66.8%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*66.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. cos-diff87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

      3. distribute-lft-in87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

   5. Applied egg-rr87.8%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right) \cdot R \]

   6. Taylor expanded in phi2 around inf 87.8%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right) + \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right)} \cdot R \]
   7. Step-by-step derivation

      1. distribute-lft-out87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)}\right)\right) \cdot R \]

      2. cos-neg87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\color{blue}{\cos \left(-\lambda_2\right)} \cdot \cos \lambda_1\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

      3. *-commutative87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \left(-\lambda_2\right)\right)} + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

      4. cos-neg87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \color{blue}{\cos \lambda_2}\right) + \cos \phi_1 \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right)\right)\right)\right) \cdot R \]

      5. *-commutative87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \cos \phi_1 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)\right)\right) \cdot R \]

      6. distribute-lft-out87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \color{blue}{\left(\cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right)\right) \cdot R \]

      7. +-commutative87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)}\right)\right)\right) \cdot R \]

      8. *-commutative87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \left(\color{blue}{\sin \lambda_2 \cdot \sin \lambda_1} + \cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)\right) \cdot R \]

      9. fma-def87.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \cos \lambda_2\right)}\right)\right)\right) \cdot R \]

   8. Simplified87.8%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \mathsf{fma}\left(\sin \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)\right)} \cdot R \]

   9. Taylor expanded in phi2 around 0 87.8%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_2 \cdot \sin \lambda_1\right)}\right)\right) \cdot R \]

   if 2.25e-13 < phi2

   1. Initial program 84.5%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def84.5%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*84.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified84.5%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*84.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt83.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow383.7%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative83.7%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr83.7%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]
   6. Step-by-step derivation

      1. unpow383.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)} \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right) \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)\right) \cdot R \]

      2. add-cube-cbrt84.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)\right) \cdot R \]

      3. associate-*r*84.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]

   7. Applied egg-rr84.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]
3. Recombined 3 regimes into one program.

4. Final simplification79.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_2 \leq -1.65 \cdot 10^{-5}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \lambda_2\right)\right)\right)\\ \mathbf{elif}\;\phi_2 \leq 2.25 \cdot 10^{-13}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right)\\ \end{array} \]

1. Initial program 74.0%

   \[\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 \]
2. Step-by-step derivation

   1. cos-diff35.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   2. +-commutative35.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

3. Applied egg-rr94.1%

   \[\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 \]

4. Final simplification94.1%

   \[\leadsto R \cdot \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right) \]

1. Split input into 3 regimes

2. if phi1 < -4.8e6

   1. Initial program 73.4%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def73.5%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*73.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified73.5%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*73.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt73.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow373.1%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative73.1%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr73.1%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]
   6. Step-by-step derivation

      1. unpow373.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)} \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right) \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)\right) \cdot R \]

      2. add-cube-cbrt73.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)\right) \cdot R \]

      3. associate-*r*73.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]

   7. Applied egg-rr73.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]

   if -4.8e6 < phi1 < 3.50000000000000019e-11

   1. Initial program 72.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 72.2%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]
   3. Step-by-step derivation

      1. cos-diff44.5%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      2. +-commutative44.5%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   4. Applied egg-rr89.4%

      \[\leadsto \cos^{-1} \left(\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 \]

   if 3.50000000000000019e-11 < phi1

   1. Initial program 77.6%

      \[\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 \]
   2. Step-by-step derivation

      1. add-log-exp77.7%

         \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\log \left(e^{\cos \left(\lambda_1 - \lambda_2\right)}\right)}\right) \cdot R \]

   3. Applied egg-rr77.7%

      \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\log \left(e^{\cos \left(\lambda_1 - \lambda_2\right)}\right)}\right) \cdot R \]
3. Recombined 3 regimes into one program.

4. Final simplification83.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_1 \leq -4800000:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right)\\ \mathbf{elif}\;\phi_1 \leq 3.5 \cdot 10^{-11}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right) + \phi_1 \cdot \sin \phi_2\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \log \left(e^{\cos \left(\lambda_1 - \lambda_2\right)}\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < -8.0000000000000001e27

   1. Initial program 61.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.4%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 33.0%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]
   4. Step-by-step derivation

      1. cos-diff46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   5. Applied egg-rr56.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right) \cdot R \]
   6. Step-by-step derivation

      1. cos-neg46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \lambda_1 \cdot \color{blue}{\cos \left(-\lambda_2\right)} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

      2. *-commutative46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\color{blue}{\cos \left(-\lambda_2\right) \cdot \cos \lambda_1} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

      3. fma-def46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\mathsf{fma}\left(\cos \left(-\lambda_2\right), \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      4. cos-neg46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \mathsf{fma}\left(\color{blue}{\cos \lambda_2}, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

   7. Simplified56.2%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)}\right) \cdot R \]

   if -8.0000000000000001e27 < lambda2

   1. Initial program 78.1%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def78.2%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified78.2%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr77.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]
   6. Step-by-step derivation

      1. unpow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)} \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right) \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)\right) \cdot R \]

      2. add-cube-cbrt78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)\right) \cdot R \]

      3. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]

   7. Applied egg-rr78.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification72.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq -8 \cdot 10^{+27}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) + \phi_1 \cdot \phi_2\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < -1.74999999999999989e29

   1. Initial program 61.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.4%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 33.0%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]
   4. Step-by-step derivation

      1. cos-diff46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      2. +-commutative46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   5. Applied egg-rr56.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \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 \]

   if -1.74999999999999989e29 < lambda2

   1. Initial program 78.1%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def78.2%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified78.2%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr77.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]
   6. Step-by-step derivation

      1. unpow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)} \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right) \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)\right) \cdot R \]

      2. add-cube-cbrt78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)\right) \cdot R \]

      3. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]

   7. Applied egg-rr78.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification72.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq -1.75 \cdot 10^{+29}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right) + \phi_1 \cdot \phi_2\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < -1.74999999999999989e29

   1. Initial program 61.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.4%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 33.0%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 27.9%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]
   5. Step-by-step derivation

      1. cos-diff46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   6. Applied egg-rr46.3%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]
   7. Step-by-step derivation

      1. cos-neg46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \lambda_1 \cdot \color{blue}{\cos \left(-\lambda_2\right)} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

      2. *-commutative46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\color{blue}{\cos \left(-\lambda_2\right) \cdot \cos \lambda_1} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

      3. fma-def46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\mathsf{fma}\left(\cos \left(-\lambda_2\right), \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      4. cos-neg46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \mathsf{fma}\left(\color{blue}{\cos \lambda_2}, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1\right) \cdot R \]

   8. Simplified46.3%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   if -1.74999999999999989e29 < lambda2

   1. Initial program 78.1%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def78.2%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified78.2%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr77.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]
   6. Step-by-step derivation

      1. unpow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)} \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right) \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)\right) \cdot R \]

      2. add-cube-cbrt78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)\right) \cdot R \]

      3. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]

   7. Applied egg-rr78.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification70.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq -1.75 \cdot 10^{+29}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < -4.2000000000000003e29

   1. Initial program 61.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.4%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 33.0%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 27.9%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]
   5. Step-by-step derivation

      1. cos-diff46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      2. +-commutative46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   6. Applied egg-rr46.3%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   if -4.2000000000000003e29 < lambda2

   1. Initial program 78.1%

      \[\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 \]
   2. Step-by-step derivation

      1. add-cbrt-cube29.9%

         \[\leadsto \color{blue}{\sqrt[3]{\left(\left(\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\right) \cdot \left(\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\right)\right) \cdot \left(\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\right)}} \]

      2. pow329.9%

         \[\leadsto \sqrt[3]{\color{blue}{{\left(\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\right)}^{3}}} \]

   3. Applied egg-rr29.9%

      \[\leadsto \color{blue}{\sqrt[3]{{\left(\cos^{-1} \left(\mathsf{fma}\left(\cos \left(\lambda_1 - \lambda_2\right), \cos \phi_1 \cdot \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right) \cdot R\right)}^{3}}} \]

   4. Taylor expanded in lambda1 around 0 78.1%

      \[\leadsto \color{blue}{R \cdot \cos^{-1} \left(\mathsf{fma}\left(\cos \left(\lambda_1 - \lambda_2\right), \cos \phi_2 \cdot \cos \phi_1, \sin \phi_1 \cdot \sin \phi_2\right)\right)} \]
   5. Step-by-step derivation

      1. fma-udef78.1%

         \[\leadsto R \cdot \cos^{-1} \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \cos \phi_1\right) + \sin \phi_1 \cdot \sin \phi_2\right)} \]

      2. associate-*r*78.2%

         \[\leadsto R \cdot \cos^{-1} \left(\color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2\right) \cdot \cos \phi_1} + \sin \phi_1 \cdot \sin \phi_2\right) \]

      3. *-commutative78.2%

         \[\leadsto R \cdot \cos^{-1} \left(\color{blue}{\cos \phi_1 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2\right)} + \sin \phi_1 \cdot \sin \phi_2\right) \]

      4. fma-def78.2%

         \[\leadsto R \cdot \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\cos \phi_1, \cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)} \]

   6. Simplified78.2%

      \[\leadsto \color{blue}{R \cdot \cos^{-1} \left(\mathsf{fma}\left(\cos \phi_1, \cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right), \sin \phi_1 \cdot \sin \phi_2\right)\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq -4.2 \cdot 10^{+29}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\cos \phi_1, \cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right), \sin \phi_1 \cdot \sin \phi_2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < -3.99999999999999966e29

   1. Initial program 61.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.4%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 33.0%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 27.9%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]
   5. Step-by-step derivation

      1. cos-diff46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      2. +-commutative46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   6. Applied egg-rr46.3%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   if -3.99999999999999966e29 < lambda2

   1. Initial program 78.1%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def78.2%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified78.2%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq -4 \cdot 10^{+29}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < -2.7e29

   1. Initial program 61.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.4%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 33.0%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 27.9%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]
   5. Step-by-step derivation

      1. cos-diff46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      2. +-commutative46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   6. Applied egg-rr46.3%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   if -2.7e29 < lambda2

   1. Initial program 78.1%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def78.2%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified78.2%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative77.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr77.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]
   6. Step-by-step derivation

      1. unpow377.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)} \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right) \cdot \sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)\right) \cdot R \]

      2. add-cube-cbrt78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)\right) \cdot R \]

      3. associate-*r*78.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]

   7. Applied egg-rr78.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification70.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq -2.7 \cdot 10^{+29}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < -4.2000000000000003e29

   1. Initial program 61.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.4%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 33.0%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 27.9%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]
   5. Step-by-step derivation

      1. cos-diff46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

      2. +-commutative46.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   6. Applied egg-rr46.3%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)} \cdot \cos \phi_1\right) \cdot R \]

   if -4.2000000000000003e29 < lambda2

   1. Initial program 78.1%

      \[\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 \]
3. Recombined 2 regimes into one program.

4. Final simplification70.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq -4.2 \cdot 10^{+29}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \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)\\ \end{array} \]

1. Split input into 3 regimes

2. if lambda2 < 3.49999999999999996e-4

   1. Initial program 77.3%

      \[\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 \]

   2. Taylor expanded in lambda2 around 0 60.1%

      \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_1}\right) \cdot R \]

   if 3.49999999999999996e-4 < lambda2 < 2.3999999999999999e197

   1. Initial program 64.4%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def64.4%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*64.4%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified64.4%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]

   4. Taylor expanded in phi2 around 0 40.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right)\right) \cdot R \]
   5. Step-by-step derivation

      1. sub-neg40.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      2. +-commutative40.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      3. neg-mul-140.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      4. neg-mul-140.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      5. remove-double-neg40.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      6. mul-1-neg40.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      7. distribute-neg-in40.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      8. +-commutative40.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      9. cos-neg40.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      10. +-commutative40.2%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      11. mul-1-neg40.2%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      12. unsub-neg40.2%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

   6. Simplified40.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \cos \phi_1}\right)\right) \cdot R \]

   if 2.3999999999999999e197 < lambda2

   1. Initial program 67.5%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def67.6%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*67.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified67.6%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*67.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt67.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow367.3%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative67.3%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr67.3%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]

   6. Taylor expanded in phi1 around 0 25.6%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\color{blue}{\left({\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2\right)}^{0.3333333333333333}\right)}}^{3}\right)\right) \cdot R \]
   7. Step-by-step derivation

      1. unpow1/351.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}\right)}}^{3}\right)\right) \cdot R \]

      2. *-commutative51.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   8. Simplified51.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\color{blue}{\left(\sqrt[3]{\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}}^{3}\right)\right) \cdot R \]

   9. Taylor expanded in lambda1 around 0 51.3%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{1}^{0.3333333333333333} \cdot \left(\cos \phi_2 \cdot \cos \left(-\lambda_2\right)\right)}\right)\right) \cdot R \]
   10. Step-by-step derivation

       1. pow-base-151.3%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{1} \cdot \left(\cos \phi_2 \cdot \cos \left(-\lambda_2\right)\right)\right)\right) \cdot R \]

       2. *-lft-identity51.3%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \cos \left(-\lambda_2\right)}\right)\right) \cdot R \]

       3. cos-neg51.3%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \color{blue}{\cos \lambda_2}\right)\right) \cdot R \]

   11. Simplified51.3%

       \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \cos \lambda_2}\right)\right) \cdot R \]
3. Recombined 3 regimes into one program.

4. Final simplification55.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq 0.00035:\\ \;\;\;\;R \cdot \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_1\right)\\ \mathbf{elif}\;\lambda_2 \leq 2.4 \cdot 10^{+197}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \cos \lambda_2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < 1.4000000000000001e-36

   1. Initial program 77.2%

      \[\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 \]

   2. Taylor expanded in lambda2 around 0 59.6%

      \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_1}\right) \cdot R \]

   if 1.4000000000000001e-36 < lambda2

   1. Initial program 66.5%

      \[\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 \]

   2. Taylor expanded in lambda1 around 0 64.4%

      \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \left(-\lambda_2\right)}\right) \cdot R \]
   3. Step-by-step derivation

      1. cos-neg28.1%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]

   4. Simplified64.4%

      \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification61.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq 1.4 \cdot 10^{-36}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_1\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_2\right)\\ \end{array} \]

1. Initial program 74.0%

   \[\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 \]

2. Final simplification74.0%

   \[\leadsto R \cdot \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) \]

1. Split input into 2 regimes

2. if phi1 < -4.8e6

   1. Initial program 73.4%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def73.5%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*73.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified73.5%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]

   4. Taylor expanded in phi2 around 0 37.6%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right)\right) \cdot R \]
   5. Step-by-step derivation

      1. sub-neg37.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      2. +-commutative37.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      3. neg-mul-137.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      4. neg-mul-137.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      5. remove-double-neg37.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      6. mul-1-neg37.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      7. distribute-neg-in37.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      8. +-commutative37.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      9. cos-neg37.6%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      10. +-commutative37.6%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      11. mul-1-neg37.6%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      12. unsub-neg37.6%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

   6. Simplified37.6%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \cos \phi_1}\right)\right) \cdot R \]

   if -4.8e6 < phi1

   1. Initial program 74.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 55.9%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]
3. Recombined 2 regimes into one program.

4. Final simplification52.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_1 \leq -4800000:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if phi2 < 2.9000000000000002e-6

   1. Initial program 69.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 \]
   2. Step-by-step derivation

      1. fma-def69.9%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*69.9%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified69.9%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]

   4. Taylor expanded in phi2 around 0 49.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right)\right) \cdot R \]
   5. Step-by-step derivation

      1. sub-neg49.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      2. +-commutative49.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      3. neg-mul-149.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      4. neg-mul-149.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      5. remove-double-neg49.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      6. mul-1-neg49.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      7. distribute-neg-in49.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      8. +-commutative49.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      9. cos-neg49.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      10. +-commutative49.2%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

      11. mul-1-neg49.2%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \cos \phi_1\right)\right) \cdot R \]

      12. unsub-neg49.2%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \cos \phi_1\right)\right) \cdot R \]

   6. Simplified49.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \cos \phi_1}\right)\right) \cdot R \]

   if 2.9000000000000002e-6 < phi2

   1. Initial program 84.2%

      \[\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 \]
   2. Step-by-step derivation

      1. fma-def84.3%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*84.3%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified84.3%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]

   4. Taylor expanded in phi1 around 0 52.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}\right)\right) \cdot R \]
   5. Step-by-step derivation

      1. sub-neg52.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \cos \phi_2\right)\right) \cdot R \]

      2. +-commutative52.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \cos \phi_2\right)\right) \cdot R \]

      3. neg-mul-152.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \cos \phi_2\right)\right) \cdot R \]

      4. neg-mul-152.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \cos \phi_2\right)\right) \cdot R \]

      5. remove-double-neg52.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \cos \phi_2\right)\right) \cdot R \]

      6. mul-1-neg52.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \cos \phi_2\right)\right) \cdot R \]

      7. distribute-neg-in52.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \cos \phi_2\right)\right) \cdot R \]

      8. +-commutative52.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \cos \phi_2\right)\right) \cdot R \]

      9. cos-neg52.5%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \cos \phi_2\right)\right) \cdot R \]

      10. +-commutative52.5%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \cos \phi_2\right)\right) \cdot R \]

      11. mul-1-neg52.5%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \cos \phi_2\right)\right) \cdot R \]

      12. unsub-neg52.5%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \cos \phi_2\right)\right) \cdot R \]

   6. Simplified52.5%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \cos \phi_2}\right)\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification50.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_2 \leq 2.9 \cdot 10^{-6}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if phi2 < 4.8e6

   1. Initial program 70.1%

      \[\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 \]

   2. Taylor expanded in phi2 around 0 47.1%

      \[\leadsto \cos^{-1} \left(\color{blue}{\sin \phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   if 4.8e6 < phi2

   1. Initial program 83.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 \]
   2. Step-by-step derivation

      1. fma-def83.9%

         \[\leadsto \cos^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)} \cdot R \]

      2. associate-*l*83.9%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right)\right) \cdot R \]

   3. Simplified83.9%

      \[\leadsto \color{blue}{\cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)\right) \cdot R} \]
   4. Step-by-step derivation

      1. associate-*r*83.9%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)\right) \cdot R \]

      2. add-cube-cbrt83.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)} \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot \sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)\right) \cdot R \]

      3. pow383.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}^{3}}\right)\right) \cdot R \]

      4. *-commutative83.2%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   5. Applied egg-rr83.2%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)}\right)}^{3}}\right)\right) \cdot R \]

   6. Taylor expanded in phi1 around 0 20.8%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\color{blue}{\left({\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2\right)}^{0.3333333333333333}\right)}}^{3}\right)\right) \cdot R \]
   7. Step-by-step derivation

      1. unpow1/350.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\color{blue}{\left(\sqrt[3]{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}\right)}}^{3}\right)\right) \cdot R \]

      2. *-commutative50.8%

         \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\left(\sqrt[3]{\color{blue}{\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}}\right)}^{3}\right)\right) \cdot R \]

   8. Simplified50.8%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, {\color{blue}{\left(\sqrt[3]{\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\right)}}^{3}\right)\right) \cdot R \]

   9. Taylor expanded in lambda2 around 0 36.7%

      \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{{1}^{0.3333333333333333} \cdot \left(\cos \phi_2 \cdot \cos \lambda_1\right)}\right)\right) \cdot R \]
   10. Step-by-step derivation

       1. pow-base-136.7%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{1} \cdot \left(\cos \phi_2 \cdot \cos \lambda_1\right)\right)\right) \cdot R \]

       2. *-lft-identity36.7%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \phi_2 \cdot \cos \lambda_1}\right)\right) \cdot R \]

       3. *-commutative36.7%

          \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \lambda_1 \cdot \cos \phi_2}\right)\right) \cdot R \]

   11. Simplified36.7%

       \[\leadsto \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \color{blue}{\cos \lambda_1 \cdot \cos \phi_2}\right)\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification44.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_2 \leq 4800000:\\ \;\;\;\;R \cdot \cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right) + \sin \phi_1 \cdot \phi_2\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \sin \phi_2, \cos \phi_2 \cdot \cos \lambda_1\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if phi2 < 0.0100000000000000002

   1. Initial program 69.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 \]

   2. Taylor expanded in phi2 around 0 46.5%

      \[\leadsto \cos^{-1} \left(\color{blue}{\sin \phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   if 0.0100000000000000002 < phi2

   1. Initial program 84.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.9%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]
3. Recombined 2 regimes into one program.

4. Final simplification45.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_2 \leq 0.01:\\ \;\;\;\;R \cdot \cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right) + \sin \phi_1 \cdot \phi_2\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < 7.2e5

   1. Initial program 77.1%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 49.3%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in lambda2 around 0 37.4%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_1}\right) \cdot R \]

   if 7.2e5 < lambda2

   1. Initial program 65.6%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 41.7%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 30.3%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in lambda1 around 0 30.6%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \left(-\lambda_2\right)}\right) \cdot R \]
   5. Step-by-step derivation

      1. cos-neg30.6%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]

   6. Simplified30.6%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification35.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq 720000:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_1\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_2\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < 4.4999999999999999e-44

   1. Initial program 77.9%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 49.2%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in lambda2 around 0 37.0%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_1}\right) \cdot R \]

   if 4.4999999999999999e-44 < lambda2

   1. Initial program 65.3%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 42.9%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in lambda1 around 0 39.9%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \left(-\lambda_2\right)}\right) \cdot R \]
   4. Step-by-step derivation

      1. cos-neg27.3%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]

   5. Simplified39.9%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification37.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq 4.5 \cdot 10^{-44}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_1\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_2\right)\\ \end{array} \]

1. Initial program 74.0%

   \[\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 \]

2. Taylor expanded in phi1 around 0 47.3%

   \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

3. Final simplification47.3%

   \[\leadsto R \cdot \cos^{-1} \left(\phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \]

1. Split input into 2 regimes

2. if lambda2 < 1.99999999999999997e-45

   1. Initial program 77.7%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 48.9%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 35.1%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in lambda2 around 0 25.2%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_1}\right) \cdot R \]

   if 1.99999999999999997e-45 < lambda2

   1. Initial program 65.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 \]

   2. Taylor expanded in phi1 around 0 43.7%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 28.8%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in lambda1 around 0 27.0%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \left(-\lambda_2\right)}\right) \cdot R \]
   5. Step-by-step derivation

      1. cos-neg27.0%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]

   6. Simplified27.0%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification25.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq 2 \cdot 10^{-45}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_1\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \lambda_2\right)\\ \end{array} \]

1. Initial program 74.0%

   \[\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 \]

2. Taylor expanded in phi1 around 0 47.3%

   \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

3. Taylor expanded in phi2 around 0 33.1%

   \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

4. Final simplification33.1%

   \[\leadsto R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \]

1. Split input into 2 regimes

2. if phi2 < 5.0000000000000002e-84

   1. Initial program 70.5%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 51.2%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 39.7%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 37.0%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]

   if 5.0000000000000002e-84 < phi2

   1. Initial program 80.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 \]

   2. Taylor expanded in phi1 around 0 39.9%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 20.8%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi1 around 0 20.4%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification31.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_2 \leq 5 \cdot 10^{-84}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right) + \phi_1 \cdot \phi_2\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if phi1 < -1.29999999999999992e-5

   1. Initial program 73.4%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 10.1%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 10.1%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 10.1%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]

   5. Taylor expanded in lambda2 around 0 7.0%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \phi_1 \cdot \cos \lambda_1}\right) \cdot R \]

   if -1.29999999999999992e-5 < phi1

   1. Initial program 74.2%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 55.9%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 38.5%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 31.0%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]

   5. Taylor expanded in phi1 around 0 24.2%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification21.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\phi_1 \leq -1.3 \cdot 10^{-5}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \cos \lambda_1\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\cos \left(\lambda_1 - \lambda_2\right) + \phi_1 \cdot \phi_2\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if lambda2 < 1.99999999999999997e-45

   1. Initial program 77.7%

      \[\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 \]

   2. Taylor expanded in phi1 around 0 48.9%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 35.1%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 27.8%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]

   5. Taylor expanded in lambda2 around 0 19.7%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \phi_1 \cdot \cos \lambda_1}\right) \cdot R \]

   if 1.99999999999999997e-45 < lambda2

   1. Initial program 65.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 \]

   2. Taylor expanded in phi1 around 0 43.7%

      \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

   3. Taylor expanded in phi2 around 0 28.8%

      \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

   4. Taylor expanded in phi2 around 0 25.5%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]

   5. Taylor expanded in lambda1 around 0 23.7%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \phi_1 \cdot \cos \left(-\lambda_2\right)}\right) \cdot R \]
   6. Step-by-step derivation

      1. cos-neg23.7%

         \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \color{blue}{\cos \lambda_2}\right) \cdot R \]

   7. Simplified23.7%

      \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \phi_1 \cdot \cos \lambda_2}\right) \cdot R \]
3. Recombined 2 regimes into one program.

4. Final simplification20.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\lambda_2 \leq 2 \cdot 10^{-45}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \cos \lambda_1\right)\\ \mathbf{else}:\\ \;\;\;\;R \cdot \cos^{-1} \left(\phi_1 \cdot \phi_2 + \cos \phi_1 \cdot \cos \lambda_2\right)\\ \end{array} \]

1. Initial program 74.0%

   \[\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 \]

2. Taylor expanded in phi1 around 0 47.3%

   \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

3. Taylor expanded in phi2 around 0 33.1%

   \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

4. Taylor expanded in phi2 around 0 27.1%

   \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]

5. Final simplification27.1%

   \[\leadsto R \cdot \cos^{-1} \left(\cos \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right) + \phi_1 \cdot \phi_2\right) \]

1. Initial program 74.0%

   \[\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 \]

2. Taylor expanded in phi1 around 0 47.3%

   \[\leadsto \cos^{-1} \left(\color{blue}{\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 \]

3. Taylor expanded in phi2 around 0 33.1%

   \[\leadsto \cos^{-1} \left(\color{blue}{\phi_1 \cdot \phi_2} + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R \]

4. Taylor expanded in phi2 around 0 27.1%

   \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_1}\right) \cdot R \]

5. Taylor expanded in phi1 around 0 20.2%

   \[\leadsto \cos^{-1} \left(\phi_1 \cdot \phi_2 + \color{blue}{\cos \left(\lambda_1 - \lambda_2\right)}\right) \cdot R \]

6. Final simplification20.2%

   \[\leadsto R \cdot \cos^{-1} \left(\cos \left(\lambda_1 - \lambda_2\right) + \phi_1 \cdot \phi_2\right) \]

herbie shell --seed 2023166 
(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))