Average Error: 16.9 → 3.8
Time: 44.3s
Precision: 64
\[\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 \left(\frac{\pi}{2} - \sin^{-1} \left(\left(\cos \phi_2 \cdot \cos \phi_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_2 \cdot \sin \lambda_1\right) + \sin \phi_2 \cdot \sin \phi_1\right)\right)\]
\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 \left(\frac{\pi}{2} - \sin^{-1} \left(\left(\cos \phi_2 \cdot \cos \phi_1\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 + \sin \lambda_2 \cdot \sin \lambda_1\right) + \sin \phi_2 \cdot \sin \phi_1\right)\right)
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1328100 = phi1;
        double r1328101 = sin(r1328100);
        double r1328102 = phi2;
        double r1328103 = sin(r1328102);
        double r1328104 = r1328101 * r1328103;
        double r1328105 = cos(r1328100);
        double r1328106 = cos(r1328102);
        double r1328107 = r1328105 * r1328106;
        double r1328108 = lambda1;
        double r1328109 = lambda2;
        double r1328110 = r1328108 - r1328109;
        double r1328111 = cos(r1328110);
        double r1328112 = r1328107 * r1328111;
        double r1328113 = r1328104 + r1328112;
        double r1328114 = acos(r1328113);
        double r1328115 = R;
        double r1328116 = r1328114 * r1328115;
        return r1328116;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1328117 = R;
        double r1328118 = atan2(1.0, 0.0);
        double r1328119 = 2.0;
        double r1328120 = r1328118 / r1328119;
        double r1328121 = phi2;
        double r1328122 = cos(r1328121);
        double r1328123 = phi1;
        double r1328124 = cos(r1328123);
        double r1328125 = r1328122 * r1328124;
        double r1328126 = lambda2;
        double r1328127 = cos(r1328126);
        double r1328128 = lambda1;
        double r1328129 = cos(r1328128);
        double r1328130 = r1328127 * r1328129;
        double r1328131 = sin(r1328126);
        double r1328132 = sin(r1328128);
        double r1328133 = r1328131 * r1328132;
        double r1328134 = r1328130 + r1328133;
        double r1328135 = r1328125 * r1328134;
        double r1328136 = sin(r1328121);
        double r1328137 = sin(r1328123);
        double r1328138 = r1328136 * r1328137;
        double r1328139 = r1328135 + r1328138;
        double r1328140 = asin(r1328139);
        double r1328141 = r1328120 - r1328140;
        double r1328142 = r1328117 * r1328141;
        return r1328142;
}

Error

Bits error versus R

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. 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\]
  2. Using strategy rm

  3. 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\]

  4. Applied distribute-lft-in3.7

    \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \color{blue}{\left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right) \cdot R\]
  5. Using strategy rm

  6. Applied add-log-exp3.8

    \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\log \left(e^{\sin \lambda_1 \cdot \sin \lambda_2}\right)}\right)\right) \cdot R\]
  7. Using strategy rm

  8. Applied add-log-exp3.8

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

  9. Simplified3.8

    \[\leadsto \log \color{blue}{\left(e^{\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_2 \cdot \cos \phi_1\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right)} \cdot R\]
  10. Using strategy rm

  11. Applied acos-asin3.8

    \[\leadsto \log \left(e^{\color{blue}{\frac{\pi}{2} - \sin^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_2 \cdot \cos \phi_1\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}}\right) \cdot R\]

  12. Applied exp-diff3.9

    \[\leadsto \log \color{blue}{\left(\frac{e^{\frac{\pi}{2}}}{e^{\sin^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_2 \cdot \cos \phi_1\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}}\right)} \cdot R\]

  13. Applied log-div3.8

    \[\leadsto \color{blue}{\left(\log \left(e^{\frac{\pi}{2}}\right) - \log \left(e^{\sin^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_2 \cdot \cos \phi_1\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right)\right)} \cdot R\]

  14. Simplified3.8

    \[\leadsto \left(\color{blue}{\frac{\pi}{2}} - \log \left(e^{\sin^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_2 \cdot \cos \phi_1\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right)\right) \cdot R\]

  15. Simplified3.8

    \[\leadsto \left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2 + \cos \lambda_1 \cdot \cos \lambda_2\right) + \sin \phi_2 \cdot \sin \phi_1\right)}\right) \cdot R\]

  16. Final simplification3.8

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

Reproduce

herbie shell --seed 2019170 
(FPCore (R lambda1 lambda2 phi1 phi2)
  :name "Spherical law of cosines"
  (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))