Initial program 38.9
\[R \cdot \sqrt{\left(\left(\lambda_1 - \lambda_2\right) \cdot \cos \left(\frac{\phi_1 + \phi_2}{2}\right)\right) \cdot \left(\left(\lambda_1 - \lambda_2\right) \cdot \cos \left(\frac{\phi_1 + \phi_2}{2}\right)\right) + \left(\phi_1 - \phi_2\right) \cdot \left(\phi_1 - \phi_2\right)}
\]
Simplified3.9
\[\leadsto \color{blue}{R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \cos \left(\frac{\phi_1 + \phi_2}{2}\right), \phi_1 - \phi_2\right)}
\]
Proof
(*.f64 R (hypot.f64 (*.f64 (-.f64 lambda1 lambda2) (cos.f64 (/.f64 (+.f64 phi1 phi2) 2))) (-.f64 phi1 phi2))): 0 points increase in error, 0 points decrease in error
(*.f64 R (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 (*.f64 (-.f64 lambda1 lambda2) (cos.f64 (/.f64 (+.f64 phi1 phi2) 2))) (*.f64 (-.f64 lambda1 lambda2) (cos.f64 (/.f64 (+.f64 phi1 phi2) 2)))) (*.f64 (-.f64 phi1 phi2) (-.f64 phi1 phi2)))))): 163 points increase in error, 0 points decrease in error
Applied egg-rr3.9
\[\leadsto R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(\left(\phi_1 + \phi_2\right) \cdot 0.5\right)\right)\right)}, \phi_1 - \phi_2\right)
\]
Applied egg-rr0.1
\[\leadsto R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\left(\cos \left(\phi_2 \cdot 0.5\right) \cdot \cos \left(\phi_1 \cdot 0.5\right) - \sin \left(\phi_2 \cdot 0.5\right) \cdot \sin \left(\phi_1 \cdot 0.5\right)\right)}, \phi_1 - \phi_2\right)
\]
Applied egg-rr0.1
\[\leadsto R \cdot \mathsf{hypot}\left(\color{blue}{\left(\cos \left(\phi_2 \cdot 0.5\right) \cdot \cos \left(0.5 \cdot \phi_1\right)\right) \cdot \left(\lambda_1 - \lambda_2\right) + \left(\sin \left(\phi_2 \cdot 0.5\right) \cdot \left(-\sin \left(0.5 \cdot \phi_1\right)\right)\right) \cdot \left(\lambda_1 - \lambda_2\right)}, \phi_1 - \phi_2\right)
\]
Simplified0.1
\[\leadsto R \cdot \mathsf{hypot}\left(\color{blue}{\left(\lambda_1 - \lambda_2\right) \cdot \mathsf{fma}\left(\sin \left(0.5 \cdot \phi_2\right), -\sin \left(0.5 \cdot \phi_1\right), \cos \left(0.5 \cdot \phi_2\right) \cdot \cos \left(0.5 \cdot \phi_1\right)\right)}, \phi_1 - \phi_2\right)
\]
Proof
(*.f64 (-.f64 lambda1 lambda2) (fma.f64 (sin.f64 (*.f64 1/2 phi2)) (neg.f64 (sin.f64 (*.f64 1/2 phi1))) (*.f64 (cos.f64 (*.f64 1/2 phi2)) (cos.f64 (*.f64 1/2 phi1))))): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 lambda1 lambda2) (fma.f64 (sin.f64 (Rewrite<= *-commutative_binary64 (*.f64 phi2 1/2))) (neg.f64 (sin.f64 (*.f64 1/2 phi1))) (*.f64 (cos.f64 (*.f64 1/2 phi2)) (cos.f64 (*.f64 1/2 phi1))))): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 lambda1 lambda2) (fma.f64 (sin.f64 (*.f64 phi2 1/2)) (neg.f64 (sin.f64 (*.f64 1/2 phi1))) (*.f64 (cos.f64 (Rewrite<= *-commutative_binary64 (*.f64 phi2 1/2))) (cos.f64 (*.f64 1/2 phi1))))): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 lambda1 lambda2) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sin.f64 (*.f64 phi2 1/2)) (neg.f64 (sin.f64 (*.f64 1/2 phi1)))) (*.f64 (cos.f64 (*.f64 phi2 1/2)) (cos.f64 (*.f64 1/2 phi1)))))): 8 points increase in error, 8 points decrease in error
(*.f64 (-.f64 lambda1 lambda2) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (cos.f64 (*.f64 phi2 1/2)) (cos.f64 (*.f64 1/2 phi1))) (*.f64 (sin.f64 (*.f64 phi2 1/2)) (neg.f64 (sin.f64 (*.f64 1/2 phi1))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 (cos.f64 (*.f64 phi2 1/2)) (cos.f64 (*.f64 1/2 phi1))) (-.f64 lambda1 lambda2)) (*.f64 (*.f64 (sin.f64 (*.f64 phi2 1/2)) (neg.f64 (sin.f64 (*.f64 1/2 phi1)))) (-.f64 lambda1 lambda2)))): 10 points increase in error, 13 points decrease in error
Final simplification0.1
\[\leadsto R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \mathsf{fma}\left(\sin \left(0.5 \cdot \phi_2\right), -\sin \left(0.5 \cdot \phi_1\right), \cos \left(0.5 \cdot \phi_1\right) \cdot \cos \left(0.5 \cdot \phi_2\right)\right), \phi_1 - \phi_2\right)
\]