Initial program 0.2
\[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}
\]
Simplified0.2
\[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right)}}
\]
Proof
(+.f64 lambda1 (atan2.f64 (*.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (sin.f64 theta))) (-.f64 (cos.f64 delta) (*.f64 (sin.f64 phi1) (sin.f64 (asin.f64 (fma.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta)) (*.f64 (cos.f64 delta) (sin.f64 phi1))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (sin.f64 delta) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 theta) (cos.f64 phi1)))) (-.f64 (cos.f64 delta) (*.f64 (sin.f64 phi1) (sin.f64 (asin.f64 (fma.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta)) (*.f64 (cos.f64 delta) (sin.f64 phi1))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sin.f64 delta) (sin.f64 theta)) (cos.f64 phi1))) (-.f64 (cos.f64 delta) (*.f64 (sin.f64 phi1) (sin.f64 (asin.f64 (fma.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta)) (*.f64 (cos.f64 delta) (sin.f64 phi1))))))))): 3 points increase in error, 1 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 theta) (sin.f64 delta))) (cos.f64 phi1)) (-.f64 (cos.f64 delta) (*.f64 (sin.f64 phi1) (sin.f64 (asin.f64 (fma.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta)) (*.f64 (cos.f64 delta) (sin.f64 phi1))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (-.f64 (cos.f64 delta) (*.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (sin.f64 phi1)))) (sin.f64 (asin.f64 (fma.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta)) (*.f64 (cos.f64 delta) (sin.f64 phi1))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (-.f64 (cos.f64 delta) (*.f64 (neg.f64 (neg.f64 (sin.f64 phi1))) (sin.f64 (asin.f64 (fma.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta)) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 phi1) (cos.f64 delta)))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (-.f64 (cos.f64 delta) (*.f64 (neg.f64 (neg.f64 (sin.f64 phi1))) (sin.f64 (asin.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta))) (*.f64 (sin.f64 phi1) (cos.f64 delta)))))))))): 1 points increase in error, 1 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (-.f64 (cos.f64 delta) (*.f64 (neg.f64 (neg.f64 (sin.f64 phi1))) (sin.f64 (asin.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sin.f64 delta) (cos.f64 phi1)) (cos.f64 theta))) (*.f64 (sin.f64 phi1) (cos.f64 delta))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (-.f64 (cos.f64 delta) (*.f64 (neg.f64 (neg.f64 (sin.f64 phi1))) (sin.f64 (asin.f64 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 phi1) (sin.f64 delta))) (cos.f64 theta)) (*.f64 (sin.f64 phi1) (cos.f64 delta))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (-.f64 (cos.f64 delta) (*.f64 (neg.f64 (neg.f64 (sin.f64 phi1))) (sin.f64 (asin.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (sin.f64 phi1) (cos.f64 delta)) (*.f64 (*.f64 (cos.f64 phi1) (sin.f64 delta)) (cos.f64 theta)))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (Rewrite=> cancel-sign-sub_binary64 (+.f64 (cos.f64 delta) (*.f64 (neg.f64 (sin.f64 phi1)) (sin.f64 (asin.f64 (+.f64 (*.f64 (sin.f64 phi1) (cos.f64 delta)) (*.f64 (*.f64 (cos.f64 phi1) (sin.f64 delta)) (cos.f64 theta)))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 lambda1 (atan2.f64 (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1)) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (cos.f64 delta) (*.f64 (sin.f64 phi1) (sin.f64 (asin.f64 (+.f64 (*.f64 (sin.f64 phi1) (cos.f64 delta)) (*.f64 (*.f64 (cos.f64 phi1) (sin.f64 delta)) (cos.f64 theta)))))))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.1
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\cos delta, \sin \phi_1, \left(\sin delta \cdot \cos theta\right) \cdot \cos \phi_1\right), -\sin \phi_1, \cos delta\right)}}
\]
Applied egg-rr0.1
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\mathsf{fma}\left(\mathsf{fma}\left(\cos delta, \sin \phi_1, \color{blue}{{\left(\cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)\right)}^{1}}\right), -\sin \phi_1, \cos delta\right)}
\]
Final simplification0.1
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\mathsf{fma}\left(\mathsf{fma}\left(\cos delta, \sin \phi_1, \cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}
\]