\[\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R\]

↓

\[\log \left(e^{\cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1 + \cos \lambda_2 \cdot \cos \lambda_1\right) + \sin \phi_2 \cdot \sin \phi_1\right)}\right) \cdot R\]

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1384462 = phi1;
        double r1384463 = sin(r1384462);
        double r1384464 = phi2;
        double r1384465 = sin(r1384464);
        double r1384466 = r1384463 * r1384465;
        double r1384467 = cos(r1384462);
        double r1384468 = cos(r1384464);
        double r1384469 = r1384467 * r1384468;
        double r1384470 = lambda1;
        double r1384471 = lambda2;
        double r1384472 = r1384470 - r1384471;
        double r1384473 = cos(r1384472);
        double r1384474 = r1384469 * r1384473;
        double r1384475 = r1384466 + r1384474;
        double r1384476 = acos(r1384475);
        double r1384477 = R;
        double r1384478 = r1384476 * r1384477;
        return r1384478;
}

↓

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1384479 = phi1;
        double r1384480 = cos(r1384479);
        double r1384481 = phi2;
        double r1384482 = cos(r1384481);
        double r1384483 = r1384480 * r1384482;
        double r1384484 = lambda2;
        double r1384485 = sin(r1384484);
        double r1384486 = lambda1;
        double r1384487 = sin(r1384486);
        double r1384488 = r1384485 * r1384487;
        double r1384489 = cos(r1384484);
        double r1384490 = cos(r1384486);
        double r1384491 = r1384489 * r1384490;
        double r1384492 = r1384488 + r1384491;
        double r1384493 = r1384483 * r1384492;
        double r1384494 = sin(r1384481);
        double r1384495 = sin(r1384479);
        double r1384496 = r1384494 * r1384495;
        double r1384497 = r1384493 + r1384496;
        double r1384498 = acos(r1384497);
        double r1384499 = exp(r1384498);
        double r1384500 = log(r1384499);
        double r1384501 = R;
        double r1384502 = r1384500 * r1384501;
        return r1384502;
}

\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R

↓

\log \left(e^{\cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1 + \cos \lambda_2 \cdot \cos \lambda_1\right) + \sin \phi_2 \cdot \sin \phi_1\right)}\right) \cdot R

Derivation

Initial program 16.7
\[\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R\]
Using strategy rm
Applied cos-diff3.8
\[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \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)}\right) \cdot R\]
Using strategy rm
Applied add-log-exp3.8
\[\leadsto \color{blue}{\log \left(e^{\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right)} \cdot R\]
Final simplification3.8
\[\leadsto \log \left(e^{\cos^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1 + \cos \lambda_2 \cdot \cos \lambda_1\right) + \sin \phi_2 \cdot \sin \phi_1\right)}\right) \cdot R\]

Error

Derivation

Reproduce