Initial program 0.8
\[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
- Using strategy
rm Applied sub-neg0.8
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)}}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
Applied sin-sum0.7
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \cos \left(-\lambda_2\right) + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
Simplified0.7
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\color{blue}{\sin \lambda_1 \cdot \cos \lambda_2} + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
- Using strategy
rm Applied sub-neg0.7
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)}}\]
Applied cos-sum0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\cos \phi_1 + \cos \phi_2 \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \left(-\lambda_2\right) - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}}\]
Simplified0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\cos \phi_1 + \cos \phi_2 \cdot \left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}\]
- Using strategy
rm Applied flip3-+0.3
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\color{blue}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)}^{3}}{\cos \phi_1 \cdot \cos \phi_1 + \left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) - \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)\right)}}}\]
Simplified0.3
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)}^{3}}{\color{blue}{\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + \cos \phi_1 \cdot \cos \phi_1}}}\]
- Using strategy
rm Applied *-un-lft-identity0.3
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)}^{3}}{\color{blue}{1 \cdot \left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + \cos \phi_1 \cdot \cos \phi_1\right)}}}\]
Applied sum-cubes0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{\color{blue}{\left(\cos \phi_1 \cdot \cos \phi_1 + \left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) - \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)\right)\right) \cdot \left(\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)}}{1 \cdot \left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + \cos \phi_1 \cdot \cos \phi_1\right)}}\]
Applied times-frac0.3
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\color{blue}{\frac{\cos \phi_1 \cdot \cos \phi_1 + \left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) - \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)\right)}{1} \cdot \frac{\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + \cos \phi_1 \cdot \cos \phi_1}}}\]
Simplified0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\color{blue}{\left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + {\left(\cos \phi_1\right)}^{2}\right)} \cdot \frac{\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + \cos \phi_1 \cdot \cos \phi_1}}\]
Final simplification0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + {\left(\cos \phi_1\right)}^{2}\right) \cdot \frac{\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) - \cos \phi_1\right) + \cos \phi_1 \cdot \cos \phi_1}}\]