Bearing on a great circle Percentage Accurate: 79.4% → 99.7%
Time: 36.7s
Alternatives: 26
Speedup: TODO×
Specification ? \[\begin{array}{l}
t_0 := \lambda_1 - \lambda_2\\
t_1 := \cos \phi_2\\
\tan^{-1}_* \frac{\sin t_0 \cdot t_1}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot t_1\right) \cdot \cos t_0}
\end{array}
\]
Local Percentage Accuracy vs ?
The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples. Accuracy vs Speed? The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs. Alternative 1? \[\begin{array}{l}
t_0 := \cos \lambda_2 \cdot \cos \lambda_1\\
t_1 := \sin \lambda_1 \cdot \sin \lambda_2\\
\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \frac{\left(t_0 + t_1\right) \cdot \left(t_1 - t_0\right)}{t_0 - t_1}}
\end{array}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Step-by-step derivation sin-diff90.3%
\[\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)}
\]
cancel-sign-sub-inv90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Step-by-step derivation cos-diff99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}}
\]
flip-+99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_2 \cdot \cos \lambda_1} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Applied egg-rr 99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Step-by-step derivation difference-of-squares99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
fma-udef99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Simplified99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Taylor expanded in lambda1 around inf 99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1 + \cos \lambda_2 \cdot \cos \lambda_1\right)}}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Final simplification99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2 - \cos \lambda_2 \cdot \cos \lambda_1\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Alternative 2? \[\begin{array}{l}
t_0 := \cos \phi_2 \cdot \sin \phi_1\\
\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(t_0 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + t_0 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}
\end{array}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Step-by-step derivation sin-diff90.3%
\[\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)}
\]
cancel-sign-sub-inv90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Step-by-step derivation cos-diff99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}}
\]
distribute-lft-in99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\left(\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} + \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}
\]
Applied egg-rr 99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\left(\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}}
\]
Final simplification99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) + \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}
\]
Alternative 3? \[\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Step-by-step derivation sin-diff90.3%
\[\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)}
\]
cancel-sign-sub-inv90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Step-by-step derivation cos-diff99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}}
\]
flip-+99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_2 \cdot \cos \lambda_1} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Applied egg-rr 99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Step-by-step derivation difference-of-squares99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
fma-udef99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Simplified99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Taylor expanded in phi1 around inf 99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\sin \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_2 \cdot \sin \lambda_1\right)\right)}}
\]
Final simplification99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}
\]
Alternative 4? \[\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right)}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Step-by-step derivation sin-diff90.3%
\[\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)}
\]
cancel-sign-sub-inv90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Step-by-step derivation cos-diff99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}}
\]
+-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right)}}
\]
*-commutative99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \left(\sin \lambda_1 \cdot \sin \lambda_2 + \color{blue}{\cos \lambda_2 \cdot \cos \lambda_1}\right)}
\]
Applied egg-rr 99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_2 \cdot \cos \lambda_1\right)}}
\]
Final simplification99.7%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right)}
\]
Alternative 5? \[\begin{array}{l}
t_0 := \cos \phi_1 \cdot \sin \phi_2\\
t_1 := \mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2\\
\mathbf{if}\;\phi_2 \leq -6.5 \cdot 10^{-6}:\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{t_0 - \frac{\cos \phi_2}{\frac{\frac{1}{\cos \left(\lambda_2 - \lambda_1\right)}}{\sin \phi_1}}}\\
\mathbf{elif}\;\phi_2 \leq 4.2 \cdot 10^{-7}:\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{t_0 - \sin \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{t_0 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\end{array}
\]
Derivation Split input into 3 regimes if phi2 < -6.4999999999999996e-6 Initial program 72.8%
\[\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)}
\]
Step-by-step derivation sin-diff90.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)}
\]
cancel-sign-sub-inv90.0%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Step-by-step derivation cos-diff99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}}
\]
flip-+99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
*-commutative99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_2 \cdot \cos \lambda_1} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Applied egg-rr 99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Step-by-step derivation difference-of-squares99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
fma-udef99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Simplified99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Taylor expanded in lambda1 around inf 99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1 + \cos \lambda_2 \cdot \cos \lambda_1\right)}}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Step-by-step derivation associate-*r/99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\frac{\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1 + \cos \lambda_2 \cdot \cos \lambda_1\right)\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
+-commutative99.4%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_2 \cdot \sin \lambda_1\right)}\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
cos-diff90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \color{blue}{\cos \left(\lambda_2 - \lambda_1\right)}\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)}{\color{blue}{\cos \lambda_2 \cdot \cos \lambda_1} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \color{blue}{\sin \lambda_2 \cdot \sin \lambda_1}}}
\]
Applied egg-rr 90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\frac{\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \left(\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1}}}
\]
Step-by-step derivation associate-/l*90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\frac{\sin \phi_1 \cdot \cos \phi_2}{\frac{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1}{\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)}}}}
\]
*-commutative90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\color{blue}{\cos \phi_2 \cdot \sin \phi_1}}{\frac{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1}{\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)}}}
\]
associate-/l*90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\frac{\cos \phi_2}{\frac{\frac{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1}{\left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)}}{\sin \phi_1}}}}
\]
associate-/r*90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\cos \phi_2}{\frac{\color{blue}{\frac{\frac{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_2 \cdot \sin \lambda_1}}{\cos \left(\lambda_2 - \lambda_1\right)}}}{\sin \phi_1}}}
\]
*-inverses90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\cos \phi_2}{\frac{\frac{\color{blue}{1}}{\cos \left(\lambda_2 - \lambda_1\right)}}{\sin \phi_1}}}
\]
Simplified90.1%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\frac{\cos \phi_2}{\frac{\frac{1}{\cos \left(\lambda_2 - \lambda_1\right)}}{\sin \phi_1}}}}
\]
if -6.4999999999999996e-6 < phi2 < 4.2e-7 Initial program 82.7%
\[\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)}
\]
Step-by-step derivation sin-diff90.2%
\[\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)}
\]
cancel-sign-sub-inv90.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Step-by-step derivation cos-diff99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}}
\]
flip-+99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
*-commutative99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1\right)} - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_2 \cdot \cos \lambda_1} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Applied egg-rr 99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\left(\cos \lambda_2 \cdot \cos \lambda_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Step-by-step derivation difference-of-squares99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} + \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
fma-udef99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\color{blue}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right)} \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_2 \cdot \cos \lambda_1 - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
*-commutative99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 \frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \lambda_2}}
\]
Simplified99.9%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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}{\frac{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2\right)}{\cos \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \lambda_2}}}
\]
Taylor expanded in phi2 around 0 99.8%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\sin \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_2 \cdot \sin \lambda_1\right)}}
\]
if 4.2e-7 < phi2 Initial program 78.7%
\[\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)}
\]
Step-by-step derivation sin-diff56.1%
\[\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}{\sin \phi_2}
\]
sub-neg56.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Applied egg-rr 90.9%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\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)}
\]
Step-by-step derivation sub-neg56.1%
\[\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}{\sin \phi_2}
\]
Simplified90.9%
\[\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)}
\]
Recombined 3 regimes into one program. Final simplification94.9%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_2 \leq -6.5 \cdot 10^{-6}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \frac{\cos \phi_2}{\frac{\frac{1}{\cos \left(\lambda_2 - \lambda_1\right)}}{\sin \phi_1}}}\\
\mathbf{elif}\;\phi_2 \leq 4.2 \cdot 10^{-7}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\end{array}
\]
Alternative 6? \[\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Step-by-step derivation sin-diff90.3%
\[\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)}
\]
cancel-sign-sub-inv90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Final simplification90.3%
\[\leadsto \tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
Alternative 7? \[\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \cos \phi_2 \cdot \left(\sin \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Step-by-step derivation sin-diff90.3%
\[\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)}
\]
cancel-sign-sub-inv90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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)}
\]
Taylor expanded in lambda1 around 0 90.3%
\[\leadsto \color{blue}{\tan^{-1}_* \frac{\cos \phi_2 \cdot \mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, -1 \cdot \left(\sin \lambda_2 \cdot \cos \lambda_1\right)\right)}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)}}
\]
Step-by-step derivation *-commutative90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, -1 \cdot \left(\sin \lambda_2 \cdot \cos \lambda_1\right)\right)}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\left(\cos \phi_2 \cdot \sin \phi_1\right)}}
\]
fma-udef90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + -1 \cdot \left(\sin \lambda_2 \cdot \cos \lambda_1\right)\right)}}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)}
\]
neg-mul-190.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \color{blue}{\left(-\sin \lambda_2 \cdot \cos \lambda_1\right)}\right)}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)}
\]
sub-neg90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_2 \cdot \cos \lambda_1\right)}}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \sin \phi_1\right)}
\]
*-commutative90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_2 \cdot \cos \lambda_1\right)}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \cos \phi_2\right)}}
\]
associate-*r*90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_2 \cdot \cos \lambda_1\right)}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1\right) \cdot \cos \phi_2}}
\]
*-commutative90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_2 \cdot \cos \lambda_1\right)}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \phi_2 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1\right)}}
\]
Simplified90.3%
\[\leadsto \color{blue}{\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \sin \lambda_2 \cdot \cos \lambda_1\right)}{\cos \phi_1 \cdot \sin \phi_2 - \cos \phi_2 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1\right)}}
\]
Final simplification90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \cos \phi_2 \cdot \left(\sin \phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}
\]
Alternative 8? \[\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Step-by-step derivation sin-diff60.3%
\[\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}{\sin \phi_2}
\]
sub-neg60.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Applied egg-rr 90.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\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)}
\]
Step-by-step derivation sub-neg60.3%
\[\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}{\sin \phi_2}
\]
Simplified90.3%
\[\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)}
\]
Final simplification90.3%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
Alternative 9? \[\begin{array}{l}
t_0 := \cos \left(\lambda_1 - \lambda_2\right)\\
t_1 := \cos \phi_1 \cdot \sin \phi_2\\
t_2 := \sin \left(\lambda_1 - \lambda_2\right)\\
t_3 := \cos \phi_2 \cdot \sin \phi_1\\
\mathbf{if}\;\phi_1 \leq -0.0026:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot t_2}{\mathsf{fma}\left(\sin \phi_1, \cos \phi_2 \cdot \left(-t_0\right), t_1\right)}\\
\mathbf{elif}\;\phi_1 \leq 8500:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right) - t_3 \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(t_2\right)\right)}{t_1 - t_3 \cdot t_0}\\
\end{array}
\]
Derivation Split input into 3 regimes if phi1 < -0.0025999999999999999 Initial program 82.1%
\[\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)}
\]
Step-by-step derivation sub-neg82.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \phi_1 \cdot \sin \phi_2 + \left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
+-commutative82.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) + \cos \phi_1 \cdot \sin \phi_2}}
\]
associate-*l*82.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\left(-\color{blue}{\sin \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right) + \cos \phi_1 \cdot \sin \phi_2}
\]
distribute-rgt-neg-in82.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_1 \cdot \left(-\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)} + \cos \phi_1 \cdot \sin \phi_2}
\]
fma-def82.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sin \phi_1, -\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right), \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
*-commutative82.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left(\sin \phi_1, -\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}, \cos \phi_1 \cdot \sin \phi_2\right)}
\]
Applied egg-rr 82.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sin \phi_1, -\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2, \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
if -0.0025999999999999999 < phi1 < 8500 Initial program 79.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)}
\]
Step-by-step derivation add-cube-cbrt79.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \sqrt[3]{\cos \phi_1}\right)} \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
associate-*l*79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)} - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
fma-neg79.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
pow279.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left(\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2}}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}
\]
*-commutative79.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in79.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in79.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}\right)}
\]
Applied egg-rr 79.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)\right)}}
\]
Step-by-step derivation fma-udef79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right) + \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}}
\]
+-commutative79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right) + {\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)}}
\]
Simplified79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot {\left(\sqrt[3]{\cos \phi_1}\right)}^{3}}}
\]
Taylor expanded in phi1 around 0 79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot {\phi_1}^{2}\right)}}
\]
Step-by-step derivation unpow279.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \color{blue}{\left(\phi_1 \cdot \phi_1\right)}\right)}
\]
Simplified79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}}
\]
Step-by-step derivation sin-diff94.3%
\[\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}{\sin \phi_2}
\]
sub-neg94.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Applied egg-rr 98.5%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}
\]
Step-by-step derivation sub-neg94.3%
\[\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}{\sin \phi_2}
\]
Simplified98.5%
\[\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 \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}
\]
if 8500 < phi1 Initial program 74.7%
\[\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)}
\]
Step-by-step derivation expm1-log1p-u74.7%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \left(\lambda_1 - \lambda_2\right)\right)\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 egg-rr 74.7%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \left(\lambda_1 - \lambda_2\right)\right)\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)}
\]
Recombined 3 regimes into one program. Final simplification89.0%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -0.0026:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\mathsf{fma}\left(\sin \phi_1, \cos \phi_2 \cdot \left(-\cos \left(\lambda_1 - \lambda_2\right)\right), \cos \phi_1 \cdot \sin \phi_2\right)}\\
\mathbf{elif}\;\phi_1 \leq 8500:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right) - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\sin \left(\lambda_1 - \lambda_2\right)\right)\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\end{array}
\]
Alternative 10? \[\begin{array}{l}
t_0 := \cos \left(\lambda_1 - \lambda_2\right)\\
t_1 := \cos \phi_1 \cdot \sin \phi_2\\
t_2 := \sin \left(\lambda_1 - \lambda_2\right)\\
\mathbf{if}\;\phi_1 \leq -3.4 \cdot 10^{-15}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot t_2}{\mathsf{fma}\left(\sin \phi_1, \cos \phi_2 \cdot \left(-t_0\right), t_1\right)}\\
\mathbf{elif}\;\phi_1 \leq 1.7 \cdot 10^{-11}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(t_2\right)\right)}{t_1 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot t_0}\\
\end{array}
\]
Derivation Split input into 3 regimes if phi1 < -3.4e-15 Initial program 83.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)}
\]
Step-by-step derivation sub-neg83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \phi_1 \cdot \sin \phi_2 + \left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
+-commutative83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) + \cos \phi_1 \cdot \sin \phi_2}}
\]
associate-*l*83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\left(-\color{blue}{\sin \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right) + \cos \phi_1 \cdot \sin \phi_2}
\]
distribute-rgt-neg-in83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_1 \cdot \left(-\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)} + \cos \phi_1 \cdot \sin \phi_2}
\]
fma-def83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sin \phi_1, -\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right), \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
*-commutative83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left(\sin \phi_1, -\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}, \cos \phi_1 \cdot \sin \phi_2\right)}
\]
Applied egg-rr 83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sin \phi_1, -\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2, \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
if -3.4e-15 < phi1 < 1.6999999999999999e-11 Initial program 79.1%
\[\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)}
\]
Taylor expanded in phi1 around 0 77.6%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff99.6%
\[\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)}
\]
cancel-sign-sub-inv99.6%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def99.7%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 98.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
if 1.6999999999999999e-11 < phi1 Initial program 74.4%
\[\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)}
\]
Step-by-step derivation expm1-log1p-u74.4%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \left(\lambda_1 - \lambda_2\right)\right)\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 egg-rr 74.4%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \left(\lambda_1 - \lambda_2\right)\right)\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)}
\]
Recombined 3 regimes into one program. Final simplification88.1%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -3.4 \cdot 10^{-15}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\mathsf{fma}\left(\sin \phi_1, \cos \phi_2 \cdot \left(-\cos \left(\lambda_1 - \lambda_2\right)\right), \cos \phi_1 \cdot \sin \phi_2\right)}\\
\mathbf{elif}\;\phi_1 \leq 1.7 \cdot 10^{-11}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\sin \left(\lambda_1 - \lambda_2\right)\right)\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\end{array}
\]
Alternative 11? \[\begin{array}{l}
t_0 := \cos \left(\lambda_1 - \lambda_2\right)\\
t_1 := \cos \phi_1 \cdot \sin \phi_2\\
t_2 := \cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)\\
\mathbf{if}\;\phi_1 \leq -9.2 \cdot 10^{-14}:\\
\;\;\;\;\tan^{-1}_* \frac{t_2}{\mathsf{fma}\left(\sin \phi_1, \cos \phi_2 \cdot \left(-t_0\right), t_1\right)}\\
\mathbf{elif}\;\phi_1 \leq 6.2 \cdot 10^{-13}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{t_2}{t_1 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot t_0}\\
\end{array}
\]
Derivation Split input into 3 regimes if phi1 < -9.19999999999999993e-14 Initial program 83.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)}
\]
Step-by-step derivation sub-neg83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \phi_1 \cdot \sin \phi_2 + \left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
+-commutative83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) + \cos \phi_1 \cdot \sin \phi_2}}
\]
associate-*l*83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\left(-\color{blue}{\sin \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\right) + \cos \phi_1 \cdot \sin \phi_2}
\]
distribute-rgt-neg-in83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_1 \cdot \left(-\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)} + \cos \phi_1 \cdot \sin \phi_2}
\]
fma-def83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sin \phi_1, -\cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right), \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
*-commutative83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left(\sin \phi_1, -\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}, \cos \phi_1 \cdot \sin \phi_2\right)}
\]
Applied egg-rr 83.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sin \phi_1, -\cos \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2, \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
if -9.19999999999999993e-14 < phi1 < 6.1999999999999998e-13 Initial program 79.1%
\[\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)}
\]
Taylor expanded in phi1 around 0 77.6%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff99.6%
\[\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)}
\]
cancel-sign-sub-inv99.6%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def99.7%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 98.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
if 6.1999999999999998e-13 < phi1 Initial program 74.4%
\[\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)}
\]
Recombined 3 regimes into one program. Final simplification88.1%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -9.2 \cdot 10^{-14}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\mathsf{fma}\left(\sin \phi_1, \cos \phi_2 \cdot \left(-\cos \left(\lambda_1 - \lambda_2\right)\right), \cos \phi_1 \cdot \sin \phi_2\right)}\\
\mathbf{elif}\;\phi_1 \leq 6.2 \cdot 10^{-13}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\end{array}
\]
Alternative 12? \[\begin{array}{l}
t_0 := \cos \phi_1 \cdot \sin \phi_2\\
\mathbf{if}\;\lambda_1 \leq -5.5 \cdot 10^{+138}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\mathbf{elif}\;\lambda_1 \leq -0.7:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1 \cdot \cos \phi_2}{t_0 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\mathbf{elif}\;\lambda_1 \leq 6.4 \cdot 10^{+16}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{t_0 - \sin \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \phi_2\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Derivation Split input into 4 regimes if lambda1 < -5.4999999999999999e138 Initial program 46.4%
\[\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)}
\]
Taylor expanded in phi1 around 0 39.8%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff75.9%
\[\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}{\sin \phi_2}
\]
sub-neg75.9%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Applied egg-rr 75.9%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Step-by-step derivation sub-neg75.9%
\[\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}{\sin \phi_2}
\]
Simplified75.9%
\[\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}{\sin \phi_2}
\]
if -5.4999999999999999e138 < lambda1 < -0.69999999999999996 Initial program 63.4%
\[\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)}
\]
Taylor expanded in lambda2 around 0 62.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \lambda_1} \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)}
\]
if -0.69999999999999996 < lambda1 < 6.4e16 Initial program 99.4%
\[\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)}
\]
Taylor expanded in lambda1 around 0 98.8%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(-\lambda_2\right)\right)}}
\]
Step-by-step derivation *-commutative98.8%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2 \cdot \cos \phi_1} - \sin \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(-\lambda_2\right)\right)}
\]
cos-neg98.8%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\sin \phi_2 \cdot \cos \phi_1 - \sin \phi_1 \cdot \left(\cos \phi_2 \cdot \color{blue}{\cos \lambda_2}\right)}
\]
Simplified98.8%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2 \cdot \cos \phi_1 - \sin \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \lambda_2\right)}}
\]
if 6.4e16 < lambda1 Initial program 59.8%
\[\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)}
\]
Taylor expanded in phi1 around 0 44.6%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff82.5%
\[\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)}
\]
cancel-sign-sub-inv82.5%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def82.5%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 67.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Recombined 4 regimes into one program. Final simplification84.0%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\lambda_1 \leq -5.5 \cdot 10^{+138}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\mathbf{elif}\;\lambda_1 \leq -0.7:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1 \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\mathbf{elif}\;\lambda_1 \leq 6.4 \cdot 10^{+16}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \left(\cos \lambda_2 \cdot \cos \phi_2\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Alternative 13? \[\begin{array}{l}
\mathbf{if}\;\phi_1 \leq -3.8 \cdot 10^{-15} \lor \neg \left(\phi_1 \leq 2.35 \cdot 10^{-14}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Derivation Split input into 2 regimes if phi1 < -3.8000000000000002e-15 or 2.3500000000000001e-14 < phi1 Initial program 78.9%
\[\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)}
\]
if -3.8000000000000002e-15 < phi1 < 2.3500000000000001e-14 Initial program 79.1%
\[\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)}
\]
Taylor expanded in phi1 around 0 77.6%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff99.6%
\[\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)}
\]
cancel-sign-sub-inv99.6%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def99.7%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 98.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Recombined 2 regimes into one program. Final simplification88.1%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -3.8 \cdot 10^{-15} \lor \neg \left(\phi_1 \leq 2.35 \cdot 10^{-14}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Alternative 14? \[\begin{array}{l}
t_0 := \cos \left(\lambda_2 - \lambda_1\right)\\
t_1 := \cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)\\
\mathbf{if}\;\phi_1 \leq -2 \cdot 10^{-14}:\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{\sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot t_0}\\
\mathbf{elif}\;\phi_1 \leq 65000000000:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot t_0}\\
\end{array}
\]
Derivation Split input into 3 regimes if phi1 < -2e-14 Initial program 83.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)}
\]
Step-by-step derivation add-cube-cbrt83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \sqrt[3]{\cos \phi_1}\right)} \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
associate-*l*83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)} - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
fma-neg83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
pow283.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left(\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2}}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}
\]
*-commutative83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}\right)}
\]
Applied egg-rr 83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)\right)}}
\]
Step-by-step derivation fma-udef83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right) + \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}}
\]
+-commutative83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right) + {\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)}}
\]
Simplified83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot {\left(\sqrt[3]{\cos \phi_1}\right)}^{3}}}
\]
Taylor expanded in phi1 around 0 29.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot {\phi_1}^{2}\right)}}
\]
Step-by-step derivation unpow229.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \color{blue}{\left(\phi_1 \cdot \phi_1\right)}\right)}
\]
Simplified29.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}}
\]
Taylor expanded in phi1 around 0 54.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \color{blue}{\sin \phi_2}}
\]
if -2e-14 < phi1 < 6.5e10 Initial program 78.7%
\[\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)}
\]
Taylor expanded in phi1 around 0 75.9%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff98.6%
\[\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)}
\]
cancel-sign-sub-inv98.6%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1\right) \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)}
\]
fma-def98.6%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \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 egg-rr 95.8%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \left(-\cos \lambda_1\right) \cdot \sin \lambda_2\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
if 6.5e10 < phi1 Initial program 74.7%
\[\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)}
\]
Taylor expanded in phi2 around 0 53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1}}
\]
Step-by-step derivation sub-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \sin \phi_1}
\]
+-commutative53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \sin \phi_1}
\]
neg-mul-153.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \sin \phi_1}
\]
neg-mul-153.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \sin \phi_1}
\]
remove-double-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \sin \phi_1}
\]
mul-1-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \sin \phi_1}
\]
distribute-neg-in53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \sin \phi_1}
\]
+-commutative53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \sin \phi_1}
\]
cos-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \sin \phi_1}
\]
+-commutative53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \sin \phi_1}
\]
mul-1-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \sin \phi_1}
\]
unsub-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \sin \phi_1}
\]
Simplified53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \sin \phi_1}}
\]
Recombined 3 regimes into one program. Final simplification75.2%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -2 \cdot 10^{-14}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\mathbf{elif}\;\phi_1 \leq 65000000000:\\
\;\;\;\;\tan^{-1}_* \frac{\mathsf{fma}\left(\sin \lambda_1, \cos \lambda_2, \cos \lambda_1 \cdot \left(-\sin \lambda_2\right)\right) \cdot \cos \phi_2}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\end{array}
\]
Alternative 15? \[\begin{array}{l}
\mathbf{if}\;\phi_1 \leq -6 \cdot 10^{-14} \lor \neg \left(\phi_1 \leq 8500\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\end{array}
\]
Derivation Split input into 2 regimes if phi1 < -5.9999999999999997e-14 or 8500 < phi1 Initial program 79.3%
\[\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)}
\]
Taylor expanded in phi2 around 0 53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1}}
\]
Step-by-step derivation sub-neg53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \sin \phi_1}
\]
+-commutative53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \sin \phi_1}
\]
neg-mul-153.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \sin \phi_1}
\]
neg-mul-153.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \sin \phi_1}
\]
remove-double-neg53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \sin \phi_1}
\]
mul-1-neg53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \sin \phi_1}
\]
distribute-neg-in53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \sin \phi_1}
\]
+-commutative53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \sin \phi_1}
\]
cos-neg53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \sin \phi_1}
\]
+-commutative53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \sin \phi_1}
\]
mul-1-neg53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \sin \phi_1}
\]
unsub-neg53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \sin \phi_1}
\]
Simplified53.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \sin \phi_1}}
\]
if -5.9999999999999997e-14 < phi1 < 8500 Initial program 78.7%
\[\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)}
\]
Taylor expanded in phi1 around 0 75.9%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff95.8%
\[\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}{\sin \phi_2}
\]
sub-neg95.8%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Applied egg-rr 95.8%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Step-by-step derivation sub-neg95.8%
\[\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}{\sin \phi_2}
\]
Simplified95.8%
\[\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}{\sin \phi_2}
\]
Recombined 2 regimes into one program. Final simplification74.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -6 \cdot 10^{-14} \lor \neg \left(\phi_1 \leq 8500\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\end{array}
\]
Alternative 16? \[\begin{array}{l}
t_0 := \cos \left(\lambda_2 - \lambda_1\right)\\
t_1 := \cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)\\
\mathbf{if}\;\phi_1 \leq -7 \cdot 10^{-15}:\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{\sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot t_0}\\
\mathbf{elif}\;\phi_1 \leq 8500:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot t_0}\\
\end{array}
\]
Derivation Split input into 3 regimes if phi1 < -7.0000000000000001e-15 Initial program 83.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)}
\]
Step-by-step derivation add-cube-cbrt83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \sqrt[3]{\cos \phi_1}\right)} \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
associate-*l*83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)} - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
fma-neg83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
pow283.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left(\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2}}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}
\]
*-commutative83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}\right)}
\]
Applied egg-rr 83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)\right)}}
\]
Step-by-step derivation fma-udef83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right) + \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}}
\]
+-commutative83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right) + {\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)}}
\]
Simplified83.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot {\left(\sqrt[3]{\cos \phi_1}\right)}^{3}}}
\]
Taylor expanded in phi1 around 0 29.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot {\phi_1}^{2}\right)}}
\]
Step-by-step derivation unpow229.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \color{blue}{\left(\phi_1 \cdot \phi_1\right)}\right)}
\]
Simplified29.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}}
\]
Taylor expanded in phi1 around 0 54.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \color{blue}{\sin \phi_2}}
\]
if -7.0000000000000001e-15 < phi1 < 8500 Initial program 78.7%
\[\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)}
\]
Taylor expanded in phi1 around 0 75.9%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff95.8%
\[\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}{\sin \phi_2}
\]
sub-neg95.8%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Applied egg-rr 95.8%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Step-by-step derivation sub-neg95.8%
\[\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}{\sin \phi_2}
\]
Simplified95.8%
\[\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}{\sin \phi_2}
\]
if 8500 < phi1 Initial program 74.7%
\[\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)}
\]
Taylor expanded in phi2 around 0 53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1}}
\]
Step-by-step derivation sub-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \sin \phi_1}
\]
+-commutative53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \sin \phi_1}
\]
neg-mul-153.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \sin \phi_1}
\]
neg-mul-153.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \sin \phi_1}
\]
remove-double-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \sin \phi_1}
\]
mul-1-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \sin \phi_1}
\]
distribute-neg-in53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \sin \phi_1}
\]
+-commutative53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \sin \phi_1}
\]
cos-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \sin \phi_1}
\]
+-commutative53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \sin \phi_1}
\]
mul-1-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \sin \phi_1}
\]
unsub-neg53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \sin \phi_1}
\]
Simplified53.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \sin \phi_1}}
\]
Recombined 3 regimes into one program. Final simplification75.2%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -7 \cdot 10^{-15}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2 - \left(\cos \phi_2 \cdot \sin \phi_1\right) \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\mathbf{elif}\;\phi_1 \leq 8500:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 \cdot \sin \phi_2 - \sin \phi_1 \cdot \cos \left(\lambda_2 - \lambda_1\right)}\\
\end{array}
\]
Alternative 17? \[\begin{array}{l}
\mathbf{if}\;\phi_1 \leq -2.4 \cdot 10^{-13} \lor \neg \left(\phi_1 \leq 24500000\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_1 \cdot \left(-\cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\end{array}
\]
Derivation Split input into 2 regimes if phi1 < -2.3999999999999999e-13 or 2.45e7 < phi1 Initial program 79.3%
\[\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)}
\]
Taylor expanded in phi2 around 0 49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-1 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1\right)}}
\]
Step-by-step derivation mul-1-neg49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1}}
\]
distribute-rgt-neg-in49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1\right)}}
\]
sub-neg49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-149.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-149.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
remove-double-neg49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \left(-\sin \phi_1\right)}
\]
distribute-neg-in49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
cos-neg49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
unsub-neg49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
Simplified49.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(-\sin \phi_1\right)}}
\]
if -2.3999999999999999e-13 < phi1 < 2.45e7 Initial program 78.7%
\[\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)}
\]
Taylor expanded in phi1 around 0 75.9%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Step-by-step derivation sin-diff95.8%
\[\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}{\sin \phi_2}
\]
sub-neg95.8%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Applied egg-rr 95.8%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \left(-\cos \lambda_1 \cdot \sin \lambda_2\right)\right)} \cdot \cos \phi_2}{\sin \phi_2}
\]
Step-by-step derivation sub-neg95.8%
\[\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}{\sin \phi_2}
\]
Simplified95.8%
\[\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}{\sin \phi_2}
\]
Recombined 2 regimes into one program. Final simplification73.0%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -2.4 \cdot 10^{-13} \lor \neg \left(\phi_1 \leq 24500000\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_1 \cdot \left(-\cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\sin \phi_2}\\
\end{array}
\]
Alternative 18? \[\begin{array}{l}
t_0 := \cos \left(\lambda_2 - \lambda_1\right)\\
t_1 := \cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)\\
\mathbf{if}\;\phi_1 \leq -0.042 \lor \neg \left(\phi_1 \leq 5.1 \cdot 10^{+17}\right):\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{\sin \phi_1 \cdot \left(-t_0\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{t_1}{\sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right) - \phi_1 \cdot \left(\cos \phi_2 \cdot t_0\right)}\\
\end{array}
\]
Derivation Split input into 2 regimes if phi1 < -0.0420000000000000026 or 5.1e17 < phi1 Initial program 78.1%
\[\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)}
\]
Taylor expanded in phi2 around 0 49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-1 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1\right)}}
\]
Step-by-step derivation mul-1-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1}}
\]
distribute-rgt-neg-in49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1\right)}}
\]
sub-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-149.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-149.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
remove-double-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \left(-\sin \phi_1\right)}
\]
distribute-neg-in49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
cos-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
unsub-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
Simplified49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(-\sin \phi_1\right)}}
\]
if -0.0420000000000000026 < phi1 < 5.1e17 Initial program 79.8%
\[\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)}
\]
Step-by-step derivation add-cube-cbrt79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \sqrt[3]{\cos \phi_1}\right)} \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
associate-*l*79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}\right) \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)} - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\]
fma-neg79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left(\sqrt[3]{\cos \phi_1} \cdot \sqrt[3]{\cos \phi_1}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
pow279.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left(\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2}}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}
\]
*-commutative79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, -\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1 \cdot \cos \phi_2\right)}\right)}
\]
distribute-rgt-neg-in79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}\right)}
\]
Applied egg-rr 79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\mathsf{fma}\left({\left(\sqrt[3]{\cos \phi_1}\right)}^{2}, \sqrt[3]{\cos \phi_1} \cdot \sin \phi_2, \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)\right)}}
\]
Step-by-step derivation fma-udef79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{{\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right) + \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right)}}
\]
+-commutative79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \left(-\cos \phi_2\right)\right) + {\left(\sqrt[3]{\cos \phi_1}\right)}^{2} \cdot \left(\sqrt[3]{\cos \phi_1} \cdot \sin \phi_2\right)}}
\]
Simplified79.7%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot {\left(\sqrt[3]{\cos \phi_1}\right)}^{3}}}
\]
Taylor expanded in phi1 around 0 79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot {\phi_1}^{2}\right)}}
\]
Step-by-step derivation unpow279.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \color{blue}{\left(\phi_1 \cdot \phi_1\right)}\right)}
\]
Simplified79.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(\cos \phi_2 \cdot \left(-\sin \phi_1\right)\right) + \sin \phi_2 \cdot \color{blue}{\left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}}
\]
Taylor expanded in phi1 around 0 79.3%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-1 \cdot \left(\phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)\right)} + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}
\]
Step-by-step derivation mul-1-neg79.3%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(-\phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)\right)} + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}
\]
*-commutative79.3%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\left(-\color{blue}{\left(\cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right) \cdot \phi_1}\right) + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}
\]
distribute-rgt-neg-in79.3%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right) \cdot \left(-\phi_1\right)} + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}
\]
Simplified79.3%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\left(\cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right) \cdot \left(-\phi_1\right)} + \sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right)}
\]
Recombined 2 regimes into one program. Final simplification65.3%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -0.042 \lor \neg \left(\phi_1 \leq 5.1 \cdot 10^{+17}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_1 \cdot \left(-\cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2 \cdot \left(1 + -0.5 \cdot \left(\phi_1 \cdot \phi_1\right)\right) - \phi_1 \cdot \left(\cos \phi_2 \cdot \cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\end{array}
\]
Alternative 19? \[\begin{array}{l}
t_0 := \cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)\\
\mathbf{if}\;\phi_1 \leq -0.03 \lor \neg \left(\phi_1 \leq 5.1 \cdot 10^{+17}\right):\\
\;\;\;\;\tan^{-1}_* \frac{t_0}{\sin \phi_1 \cdot \left(-\cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{t_0}{\sin \phi_2 - \cos \phi_2 \cdot \left(\phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\\
\end{array}
\]
Derivation Split input into 2 regimes if phi1 < -0.029999999999999999 or 5.1e17 < phi1 Initial program 78.1%
\[\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)}
\]
Taylor expanded in phi2 around 0 49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-1 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1\right)}}
\]
Step-by-step derivation mul-1-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1}}
\]
distribute-rgt-neg-in49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1\right)}}
\]
sub-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-149.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-149.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
remove-double-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \left(-\sin \phi_1\right)}
\]
distribute-neg-in49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
cos-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
unsub-neg49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
Simplified49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(-\sin \phi_1\right)}}
\]
if -0.029999999999999999 < phi1 < 5.1e17 Initial program 79.8%
\[\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)}
\]
Step-by-step derivation add-exp-log41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{e^{\log \left(\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}}
\]
sub-neg41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{e^{\log \color{blue}{\left(\cos \phi_1 \cdot \sin \phi_2 + \left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)\right)}}}
\]
+-commutative41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{e^{\log \color{blue}{\left(\left(-\left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) + \cos \phi_1 \cdot \sin \phi_2\right)}}}
\]
*-commutative41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{e^{\log \left(\left(-\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\sin \phi_1 \cdot \cos \phi_2\right)}\right) + \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
distribute-rgt-neg-in41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{e^{\log \left(\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1 \cdot \cos \phi_2\right)} + \cos \phi_1 \cdot \sin \phi_2\right)}}
\]
fma-def41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{e^{\log \color{blue}{\left(\mathsf{fma}\left(\cos \left(\lambda_1 - \lambda_2\right), -\sin \phi_1 \cdot \cos \phi_2, \cos \phi_1 \cdot \sin \phi_2\right)\right)}}}
\]
distribute-rgt-neg-in41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{e^{\log \left(\mathsf{fma}\left(\cos \left(\lambda_1 - \lambda_2\right), \color{blue}{\sin \phi_1 \cdot \left(-\cos \phi_2\right)}, \cos \phi_1 \cdot \sin \phi_2\right)\right)}}
\]
Applied egg-rr 41.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{e^{\log \left(\mathsf{fma}\left(\cos \left(\lambda_1 - \lambda_2\right), \sin \phi_1 \cdot \left(-\cos \phi_2\right), \cos \phi_1 \cdot \sin \phi_2\right)\right)}}}
\]
Taylor expanded in phi1 around 0 79.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-1 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \phi_1\right)\right) + \sin \phi_2}}
\]
Step-by-step derivation +-commutative79.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2 + -1 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \phi_1\right)\right)}}
\]
mul-1-neg79.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\sin \phi_2 + \color{blue}{\left(-\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \phi_1\right)\right)}}
\]
unsub-neg79.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2 - \cos \left(\lambda_1 - \lambda_2\right) \cdot \left(\cos \phi_2 \cdot \phi_1\right)}}
\]
*-commutative79.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\sin \phi_2 - \color{blue}{\left(\cos \phi_2 \cdot \phi_1\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}}
\]
associate-*l*79.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\sin \phi_2 - \color{blue}{\cos \phi_2 \cdot \left(\phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
Simplified79.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2 - \cos \phi_2 \cdot \left(\phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}}
\]
Recombined 2 regimes into one program. Final simplification65.2%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_1 \leq -0.03 \lor \neg \left(\phi_1 \leq 5.1 \cdot 10^{+17}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_1 \cdot \left(-\cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2 - \cos \phi_2 \cdot \left(\phi_1 \cdot \cos \left(\lambda_1 - \lambda_2\right)\right)}\\
\end{array}
\]
Alternative 20? \[\begin{array}{l}
t_0 := \cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)\\
\mathbf{if}\;\phi_2 \leq -1.75 \cdot 10^{-20} \lor \neg \left(\phi_2 \leq 4.3 \cdot 10^{-7}\right):\\
\;\;\;\;\tan^{-1}_* \frac{t_0}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{t_0}{\sin \phi_1 \cdot \left(-\cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\end{array}
\]
Derivation Split input into 2 regimes if phi2 < -1.75000000000000002e-20 or 4.3000000000000001e-7 < phi2 Initial program 75.9%
\[\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)}
\]
Taylor expanded in phi1 around 0 47.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
if -1.75000000000000002e-20 < phi2 < 4.3000000000000001e-7 Initial program 82.6%
\[\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)}
\]
Taylor expanded in phi2 around 0 81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-1 \cdot \left(\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1\right)}}
\]
Step-by-step derivation mul-1-neg81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{-\cos \left(\lambda_1 - \lambda_2\right) \cdot \sin \phi_1}}
\]
distribute-rgt-neg-in81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_1 - \lambda_2\right) \cdot \left(-\sin \phi_1\right)}}
\]
sub-neg81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\left(-\lambda_2\right) + \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-181.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{-1 \cdot \lambda_2} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
neg-mul-181.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\color{blue}{\left(-\lambda_2\right)} + \lambda_1\right) \cdot \left(-\sin \phi_1\right)}
\]
remove-double-neg81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \color{blue}{\left(-\left(-\lambda_1\right)\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\left(-\lambda_2\right) + \left(-\color{blue}{-1 \cdot \lambda_1}\right)\right) \cdot \left(-\sin \phi_1\right)}
\]
distribute-neg-in81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(-\left(\lambda_2 + -1 \cdot \lambda_1\right)\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(-\color{blue}{\left(-1 \cdot \lambda_1 + \lambda_2\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
cos-neg81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(-1 \cdot \lambda_1 + \lambda_2\right)} \cdot \left(-\sin \phi_1\right)}
\]
+-commutative81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 + -1 \cdot \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
mul-1-neg81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \left(\lambda_2 + \color{blue}{\left(-\lambda_1\right)}\right) \cdot \left(-\sin \phi_1\right)}
\]
unsub-neg81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \color{blue}{\left(\lambda_2 - \lambda_1\right)} \cdot \left(-\sin \phi_1\right)}
\]
Simplified81.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\cos \left(\lambda_2 - \lambda_1\right) \cdot \left(-\sin \phi_1\right)}}
\]
Recombined 2 regimes into one program. Final simplification63.3%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\phi_2 \leq -1.75 \cdot 10^{-20} \lor \neg \left(\phi_2 \leq 4.3 \cdot 10^{-7}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_1 \cdot \left(-\cos \left(\lambda_2 - \lambda_1\right)\right)}\\
\end{array}
\]
Alternative 21? \[\begin{array}{l}
\mathbf{if}\;\lambda_2 \leq -8.2 \cdot 10^{-61} \lor \neg \left(\lambda_2 \leq 2.7 \cdot 10^{-40}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(-\lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1 \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Derivation Split input into 2 regimes if lambda2 < -8.19999999999999998e-61 or 2.7e-40 < lambda2 Initial program 64.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)}
\]
Taylor expanded in phi1 around 0 38.5%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in lambda1 around 0 39.5%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(-\lambda_2\right) \cdot \cos \phi_2}}{\sin \phi_2}
\]
if -8.19999999999999998e-61 < lambda2 < 2.7e-40 Initial program 99.8%
\[\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)}
\]
Taylor expanded in phi1 around 0 64.6%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in lambda2 around 0 57.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\cos \phi_2 \cdot \sin \lambda_1}}{\sin \phi_2}
\]
Step-by-step derivation *-commutative57.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \lambda_1 \cdot \cos \phi_2}}{\sin \phi_2}
\]
Simplified57.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \lambda_1 \cdot \cos \phi_2}}{\sin \phi_2}
\]
Recombined 2 regimes into one program. Final simplification46.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\lambda_2 \leq -8.2 \cdot 10^{-61} \lor \neg \left(\lambda_2 \leq 2.7 \cdot 10^{-40}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(-\lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1 \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Alternative 22? \[\begin{array}{l}
\mathbf{if}\;\lambda_2 \leq -4.1 \cdot 10^{-27} \lor \neg \left(\lambda_2 \leq 2.3 \cdot 10^{-25}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\sin \left(-\lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1 \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Derivation Split input into 2 regimes if lambda2 < -4.0999999999999999e-27 or 2.2999999999999999e-25 < lambda2 Initial program 62.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)}
\]
Taylor expanded in phi1 around 0 37.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in phi2 around 0 26.6%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(\lambda_1 - \lambda_2\right)}}{\sin \phi_2}
\]
Taylor expanded in lambda1 around 0 28.6%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(-\lambda_2\right)}}{\sin \phi_2}
\]
if -4.0999999999999999e-27 < lambda2 < 2.2999999999999999e-25 Initial program 99.8%
\[\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)}
\]
Taylor expanded in phi1 around 0 64.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in lambda2 around 0 56.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\cos \phi_2 \cdot \sin \lambda_1}}{\sin \phi_2}
\]
Step-by-step derivation *-commutative56.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \lambda_1 \cdot \cos \phi_2}}{\sin \phi_2}
\]
Simplified56.2%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \lambda_1 \cdot \cos \phi_2}}{\sin \phi_2}
\]
Recombined 2 regimes into one program. Final simplification40.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\lambda_2 \leq -4.1 \cdot 10^{-27} \lor \neg \left(\lambda_2 \leq 2.3 \cdot 10^{-25}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\sin \left(-\lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1 \cdot \cos \phi_2}{\sin \phi_2}\\
\end{array}
\]
Alternative 23? \[\tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Taylor expanded in phi1 around 0 49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Final simplification49.2%
\[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2}
\]
Alternative 24? \[\begin{array}{l}
\mathbf{if}\;\lambda_2 \leq -2.9 \cdot 10^{-64} \lor \neg \left(\lambda_2 \leq 1.15 \cdot 10^{-39}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\sin \left(-\lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1}{\sin \phi_2}\\
\end{array}
\]
Derivation Split input into 2 regimes if lambda2 < -2.8999999999999999e-64 or 1.15000000000000004e-39 < lambda2 Initial program 64.7%
\[\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)}
\]
Taylor expanded in phi1 around 0 38.4%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in phi2 around 0 27.0%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(\lambda_1 - \lambda_2\right)}}{\sin \phi_2}
\]
Taylor expanded in lambda1 around 0 28.9%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(-\lambda_2\right)}}{\sin \phi_2}
\]
if -2.8999999999999999e-64 < lambda2 < 1.15000000000000004e-39 Initial program 99.8%
\[\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)}
\]
Taylor expanded in phi1 around 0 65.0%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in phi2 around 0 39.5%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(\lambda_1 - \lambda_2\right)}}{\sin \phi_2}
\]
Taylor expanded in lambda2 around 0 39.9%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \lambda_1}}{\sin \phi_2}
\]
Recombined 2 regimes into one program. Final simplification33.4%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\lambda_2 \leq -2.9 \cdot 10^{-64} \lor \neg \left(\lambda_2 \leq 1.15 \cdot 10^{-39}\right):\\
\;\;\;\;\tan^{-1}_* \frac{\sin \left(-\lambda_2\right)}{\sin \phi_2}\\
\mathbf{else}:\\
\;\;\;\;\tan^{-1}_* \frac{\sin \lambda_1}{\sin \phi_2}\\
\end{array}
\]
Alternative 25? \[\tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Taylor expanded in phi1 around 0 49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in phi2 around 0 32.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(\lambda_1 - \lambda_2\right)}}{\sin \phi_2}
\]
Final simplification32.1%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right)}{\sin \phi_2}
\]
Alternative 26? \[\tan^{-1}_* \frac{\sin \lambda_1}{\sin \phi_2}
\]
Derivation Initial program 79.0%
\[\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)}
\]
Taylor expanded in phi1 around 0 49.2%
\[\leadsto \tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\color{blue}{\sin \phi_2}}
\]
Taylor expanded in phi2 around 0 32.1%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \left(\lambda_1 - \lambda_2\right)}}{\sin \phi_2}
\]
Taylor expanded in lambda2 around 0 26.3%
\[\leadsto \tan^{-1}_* \frac{\color{blue}{\sin \lambda_1}}{\sin \phi_2}
\]
Final simplification26.3%
\[\leadsto \tan^{-1}_* \frac{\sin \lambda_1}{\sin \phi_2}
\]
Reproduce ? herbie shell --seed 2023166
(FPCore (lambda1 lambda2 phi1 phi2)
:name "Bearing on a great circle"
:precision binary64
(atan2 (* (sin (- lambda1 lambda2)) (cos phi2)) (- (* (cos phi1) (sin phi2)) (* (* (sin phi1) (cos phi2)) (cos (- lambda1 lambda2))))))
