\[\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\]

↓

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

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1053856 = phi1;
        double r1053857 = sin(r1053856);
        double r1053858 = phi2;
        double r1053859 = sin(r1053858);
        double r1053860 = r1053857 * r1053859;
        double r1053861 = cos(r1053856);
        double r1053862 = cos(r1053858);
        double r1053863 = r1053861 * r1053862;
        double r1053864 = lambda1;
        double r1053865 = lambda2;
        double r1053866 = r1053864 - r1053865;
        double r1053867 = cos(r1053866);
        double r1053868 = r1053863 * r1053867;
        double r1053869 = r1053860 + r1053868;
        double r1053870 = acos(r1053869);
        double r1053871 = R;
        double r1053872 = r1053870 * r1053871;
        return r1053872;
}

↓

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1053873 = R;
        double r1053874 = phi1;
        double r1053875 = cos(r1053874);
        double r1053876 = phi2;
        double r1053877 = cos(r1053876);
        double r1053878 = r1053875 * r1053877;
        double r1053879 = lambda2;
        double r1053880 = cos(r1053879);
        double r1053881 = lambda1;
        double r1053882 = cos(r1053881);
        double r1053883 = r1053880 * r1053882;
        double r1053884 = sin(r1053879);
        double r1053885 = sin(r1053881);
        double r1053886 = r1053884 * r1053885;
        double r1053887 = exp(r1053886);
        double r1053888 = log(r1053887);
        double r1053889 = r1053883 + r1053888;
        double r1053890 = r1053878 * r1053889;
        double r1053891 = sin(r1053876);
        double r1053892 = sin(r1053874);
        double r1053893 = r1053891 * r1053892;
        double r1053894 = r1053890 + r1053893;
        double r1053895 = acos(r1053894);
        double r1053896 = exp(r1053895);
        double r1053897 = log(r1053896);
        double r1053898 = r1053873 * r1053897;
        return r1053898;
}

\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

↓

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

Derivation

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

Error

Derivation

Reproduce