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.7
\[\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)))))): 141 points increase in error, 0 points decrease in error
Applied egg-rr3.7
\[\leadsto R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\log \left(e^{\cos \left(\left(\phi_1 + \phi_2\right) \cdot 0.5\right)}\right)}, \phi_1 - \phi_2\right)
\]
Applied egg-rr0.2
\[\leadsto R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \log \left(e^{\color{blue}{\cos \left(\phi_1 \cdot 0.5\right) \cdot \cos \left(\phi_2 \cdot 0.5\right) - \sin \left(\phi_1 \cdot 0.5\right) \cdot \sin \left(\phi_2 \cdot 0.5\right)}}\right), \phi_1 - \phi_2\right)
\]
Simplified0.2
\[\leadsto R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \log \left(e^{\color{blue}{\mathsf{fma}\left(\cos \left(0.5 \cdot \phi_2\right), \cos \left(0.5 \cdot \phi_1\right), -\sin \left(0.5 \cdot \phi_2\right) \cdot \sin \left(0.5 \cdot \phi_1\right)\right)}}\right), \phi_1 - \phi_2\right)
\]
Proof
(fma.f64 (cos.f64 (*.f64 1/2 phi2)) (cos.f64 (*.f64 1/2 phi1)) (neg.f64 (*.f64 (sin.f64 (*.f64 1/2 phi2)) (sin.f64 (*.f64 1/2 phi1))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (cos.f64 (*.f64 1/2 phi2)) (cos.f64 (*.f64 1/2 phi1))) (*.f64 (sin.f64 (*.f64 1/2 phi2)) (sin.f64 (*.f64 1/2 phi1))))): 7 points increase in error, 9 points decrease in error
(-.f64 (*.f64 (cos.f64 (Rewrite<= *-commutative_binary64 (*.f64 phi2 1/2))) (cos.f64 (*.f64 1/2 phi1))) (*.f64 (sin.f64 (*.f64 1/2 phi2)) (sin.f64 (*.f64 1/2 phi1)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (cos.f64 (*.f64 phi2 1/2)) (cos.f64 (Rewrite<= *-commutative_binary64 (*.f64 phi1 1/2)))) (*.f64 (sin.f64 (*.f64 1/2 phi2)) (sin.f64 (*.f64 1/2 phi1)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> *-commutative_binary64 (*.f64 (cos.f64 (*.f64 phi1 1/2)) (cos.f64 (*.f64 phi2 1/2)))) (*.f64 (sin.f64 (*.f64 1/2 phi2)) (sin.f64 (*.f64 1/2 phi1)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (cos.f64 (*.f64 phi1 1/2)) (cos.f64 (*.f64 phi2 1/2))) (*.f64 (sin.f64 (Rewrite<= *-commutative_binary64 (*.f64 phi2 1/2))) (sin.f64 (*.f64 1/2 phi1)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (cos.f64 (*.f64 phi1 1/2)) (cos.f64 (*.f64 phi2 1/2))) (*.f64 (sin.f64 (*.f64 phi2 1/2)) (sin.f64 (Rewrite<= *-commutative_binary64 (*.f64 phi1 1/2))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (cos.f64 (*.f64 phi1 1/2)) (cos.f64 (*.f64 phi2 1/2))) (Rewrite=> *-commutative_binary64 (*.f64 (sin.f64 (*.f64 phi1 1/2)) (sin.f64 (*.f64 phi2 1/2))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.1
\[\leadsto R \cdot \mathsf{hypot}\left(\left(\lambda_1 - \lambda_2\right) \cdot \color{blue}{\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)
\]
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_2\right) \cdot \cos \left(0.5 \cdot \phi_1\right)\right), \phi_1 - \phi_2\right)
\]