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)}
\]
Applied egg-rr0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \color{blue}{\left(\left(\cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right) \cdot \sin \phi_1 + \left(\cos delta \cdot \sin \phi_1\right) \cdot \sin \phi_1\right)}}
\]
Taylor expanded in delta around inf 0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \left(\left(\cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right) \cdot \sin \phi_1 + \color{blue}{\cos delta \cdot {\sin \phi_1}^{2}}\right)}
\]
Simplified0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \left(\left(\cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right) \cdot \sin \phi_1 + \color{blue}{{\sin \phi_1}^{2} \cdot \cos delta}\right)}
\]
Proof
(*.f64 (pow.f64 (sin.f64 phi1) 2) (cos.f64 delta)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))): 0 points increase in error, 0 points decrease in error
Taylor expanded in delta around inf 0.2
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\color{blue}{\cos delta - \left(\sin \phi_1 \cdot \left(\sin delta \cdot \left(\cos \phi_1 \cdot \cos theta\right)\right) + \cos delta \cdot {\sin \phi_1}^{2}\right)}}
\]
Simplified0.1
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\color{blue}{\left(\cos \phi_1 \cdot \cos \phi_1\right) \cdot \cos delta - \cos \phi_1 \cdot \left(\sin delta \cdot \left(\sin \phi_1 \cdot \cos theta\right)\right)}}
\]
Proof
(-.f64 (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi1)) (cos.f64 delta)) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (Rewrite<= 1-sub-sin_binary64 (-.f64 1 (*.f64 (sin.f64 phi1) (sin.f64 phi1)))) (cos.f64 delta)) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 40 points increase in error, 38 points decrease in error
(-.f64 (*.f64 (-.f64 1 (Rewrite<= unpow2_binary64 (pow.f64 (sin.f64 phi1) 2))) (cos.f64 delta)) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (Rewrite=> sub-neg_binary64 (+.f64 1 (neg.f64 (pow.f64 (sin.f64 phi1) 2)))) (cos.f64 delta)) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (pow.f64 (sin.f64 phi1) 2)) 1)) (cos.f64 delta)) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (cos.f64 delta) (*.f64 (neg.f64 (pow.f64 (sin.f64 phi1) 2)) (cos.f64 delta)))) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 16 points increase in error, 13 points decrease in error
(-.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (cos.f64 delta) (*.f64 (pow.f64 (sin.f64 phi1) 2) (cos.f64 delta)))) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (cos.f64 delta) (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2)))) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (cos.f64 theta))))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (cos.f64 delta) (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))) (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (Rewrite=> *-commutative_binary64 (*.f64 (cos.f64 theta) (sin.f64 phi1)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (cos.f64 delta) (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (cos.f64 phi1) (sin.f64 delta)) (*.f64 (cos.f64 theta) (sin.f64 phi1))))): 7 points increase in error, 5 points decrease in error
(-.f64 (-.f64 (cos.f64 delta) (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 delta) (cos.f64 phi1))) (*.f64 (cos.f64 theta) (sin.f64 phi1)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (cos.f64 delta) (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))) (Rewrite=> associate-*l*_binary64 (*.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 theta) (sin.f64 phi1)))))): 1 points increase in error, 8 points decrease in error
(-.f64 (-.f64 (cos.f64 delta) (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))) (*.f64 (sin.f64 delta) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 theta)) (sin.f64 phi1))))): 6 points increase in error, 1 points decrease in error
(-.f64 (-.f64 (cos.f64 delta) (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))) (*.f64 (sin.f64 delta) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 phi1) (*.f64 (cos.f64 phi1) (cos.f64 theta)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 (cos.f64 delta) (+.f64 (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2)) (*.f64 (sin.f64 delta) (*.f64 (sin.f64 phi1) (*.f64 (cos.f64 phi1) (cos.f64 theta))))))): 10 points increase in error, 17 points decrease in error
(-.f64 (cos.f64 delta) (+.f64 (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2)) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (sin.f64 phi1) (*.f64 (cos.f64 phi1) (cos.f64 theta))) (sin.f64 delta))))): 0 points increase in error, 0 points decrease in error
(-.f64 (cos.f64 delta) (+.f64 (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2)) (Rewrite=> associate-*l*_binary64 (*.f64 (sin.f64 phi1) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 theta)) (sin.f64 delta)))))): 3 points increase in error, 1 points decrease in error
(-.f64 (cos.f64 delta) (+.f64 (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2)) (*.f64 (sin.f64 phi1) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta))))))): 0 points increase in error, 0 points decrease in error
(-.f64 (cos.f64 delta) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (sin.f64 phi1) (*.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta)))) (*.f64 (cos.f64 delta) (pow.f64 (sin.f64 phi1) 2))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in phi1 around inf 0.1
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\left(\cos \phi_1 \cdot \cos \phi_1\right) \cdot \cos delta - \color{blue}{\sin \phi_1 \cdot \left(\sin delta \cdot \left(\cos \phi_1 \cdot \cos theta\right)\right)}}
\]
Simplified0.1
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\left(\cos \phi_1 \cdot \cos \phi_1\right) \cdot \cos delta - \color{blue}{\cos theta \cdot \left(\left(\sin \phi_1 \cdot \sin delta\right) \cdot \cos \phi_1\right)}}
\]
Proof
(*.f64 (cos.f64 theta) (*.f64 (*.f64 (sin.f64 phi1) (sin.f64 delta)) (cos.f64 phi1))): 0 points increase in error, 0 points decrease in error
(*.f64 (cos.f64 theta) (Rewrite<= associate-*r*_binary64 (*.f64 (sin.f64 phi1) (*.f64 (sin.f64 delta) (cos.f64 phi1))))): 19 points increase in error, 24 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (sin.f64 phi1) (*.f64 (sin.f64 delta) (cos.f64 phi1))) (cos.f64 theta))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 (sin.f64 phi1) (*.f64 (*.f64 (sin.f64 delta) (cos.f64 phi1)) (cos.f64 theta)))): 23 points increase in error, 16 points decrease in error
(*.f64 (sin.f64 phi1) (Rewrite<= associate-*r*_binary64 (*.f64 (sin.f64 delta) (*.f64 (cos.f64 phi1) (cos.f64 theta))))): 8 points increase in error, 7 points decrease in error
Final simplification0.1
\[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\left(\cos \phi_1 \cdot \cos \phi_1\right) \cdot \cos delta - \cos theta \cdot \left(\cos \phi_1 \cdot \left(\sin delta \cdot \sin \phi_1\right)\right)}
\]