Initial program 13.5
\[\tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
- Using strategy
rm Applied sin-diff_binary647.0
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
Applied flip--_binary649.8
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\frac{\left(\sin \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2\right) - \left(\cos \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \lambda_2}} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
Simplified8.9
\[\leadsto \tan^{-1}_* \frac{\frac{\color{blue}{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \sin \left(-\lambda_2\right) \cdot \cos \lambda_1\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}}{\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \lambda_2} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
Simplified8.9
\[\leadsto \tan^{-1}_* \frac{\frac{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \sin \left(-\lambda_2\right) \cdot \cos \lambda_1\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
- Using strategy
rm Applied cos-diff_binary642.1
\[\leadsto \tan^{-1}_* \frac{\frac{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \sin \left(-\lambda_2\right) \cdot \cos \lambda_1\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \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)}}
\]
Applied distribute-rgt-in_binary642.1
\[\leadsto \tan^{-1}_* \frac{\frac{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \sin \left(-\lambda_2\right) \cdot \cos \lambda_1\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\left(\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right) + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)\right)}}
\]
Simplified2.1
\[\leadsto \tan^{-1}_* \frac{\frac{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \sin \left(-\lambda_2\right) \cdot \cos \lambda_1\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\color{blue}{\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right)} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)\right)}
\]
Simplified2.1
\[\leadsto \tan^{-1}_* \frac{\frac{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \sin \left(-\lambda_2\right) \cdot \cos \lambda_1\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right) + \color{blue}{\left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\right)}
\]
- Using strategy
rm Applied log1p-expm1-u_binary642.1
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\frac{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \sin \left(-\lambda_2\right) \cdot \cos \lambda_1\right) \cdot \mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}{\mathsf{fma}\left(\cos \lambda_2, \sin \lambda_1, \cos \lambda_1 \cdot \sin \lambda_2\right)}\right)\right)} \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right) + \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}
\]
Simplified0.2
\[\leadsto \tan^{-1}_* \frac{\mathsf{log1p}\left(\color{blue}{\mathsf{expm1}\left(\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)}\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right) + \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}
\]
- Using strategy
rm Applied expm1-log1p-u_binary640.2
\[\leadsto \tan^{-1}_* \frac{\mathsf{log1p}\left(\mathsf{expm1}\left(\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right) + \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)\right)}\right)}
\]
Applied expm1-udef_binary640.2
\[\leadsto \tan^{-1}_* \frac{\mathsf{log1p}\left(\mathsf{expm1}\left(\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right) + \color{blue}{\left(e^{\mathsf{log1p}\left(\left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)} - 1\right)}\right)}
\]
Simplified0.2
\[\leadsto \tan^{-1}_* \frac{\mathsf{log1p}\left(\mathsf{expm1}\left(\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right) + \left(\color{blue}{e^{\mathsf{log1p}\left(\sin \lambda_1 \cdot \left(\sin \phi_1 \cdot \left(\sin \lambda_2 \cdot \cos \phi_2\right)\right)\right)}} - 1\right)\right)}
\]
Final simplification0.2
\[\leadsto \tan^{-1}_* \frac{\mathsf{log1p}\left(\mathsf{expm1}\left(\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \lambda_2 \cdot \left(\cos \lambda_1 \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)\right) + \left(e^{\mathsf{log1p}\left(\sin \lambda_1 \cdot \left(\sin \phi_1 \cdot \left(\cos \phi_2 \cdot \sin \lambda_2\right)\right)\right)} - 1\right)\right)}
\]