Average Error: 1.0 → 0.2
Time: 11.1s
Precision: 64
\[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
\[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)}^{2} \cdot \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}\]
\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}
\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)}^{2} \cdot \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}
double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r53776 = lambda1;
        double r53777 = phi2;
        double r53778 = cos(r53777);
        double r53779 = lambda2;
        double r53780 = r53776 - r53779;
        double r53781 = sin(r53780);
        double r53782 = r53778 * r53781;
        double r53783 = phi1;
        double r53784 = cos(r53783);
        double r53785 = cos(r53780);
        double r53786 = r53778 * r53785;
        double r53787 = r53784 + r53786;
        double r53788 = atan2(r53782, r53787);
        double r53789 = r53776 + r53788;
        return r53789;
}

double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r53790 = lambda1;
        double r53791 = phi2;
        double r53792 = cos(r53791);
        double r53793 = sin(r53790);
        double r53794 = lambda2;
        double r53795 = cos(r53794);
        double r53796 = r53793 * r53795;
        double r53797 = cos(r53790);
        double r53798 = -r53794;
        double r53799 = sin(r53798);
        double r53800 = r53797 * r53799;
        double r53801 = r53796 + r53800;
        double r53802 = r53792 * r53801;
        double r53803 = r53795 * r53792;
        double r53804 = phi1;
        double r53805 = cos(r53804);
        double r53806 = fma(r53797, r53803, r53805);
        double r53807 = 2.0;
        double r53808 = pow(r53806, r53807);
        double r53809 = r53808 * r53806;
        double r53810 = sin(r53794);
        double r53811 = r53793 * r53810;
        double r53812 = r53792 * r53811;
        double r53813 = 3.0;
        double r53814 = pow(r53812, r53813);
        double r53815 = r53809 + r53814;
        double r53816 = r53792 * r53795;
        double r53817 = fma(r53797, r53816, r53805);
        double r53818 = r53812 - r53806;
        double r53819 = r53812 * r53818;
        double r53820 = fma(r53817, r53817, r53819);
        double r53821 = r53815 / r53820;
        double r53822 = atan2(r53802, r53821);
        double r53823 = r53790 + r53822;
        return r53823;
}

Error

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Derivation

  1. Initial program 1.0

    \[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
  2. Using strategy rm
  3. Applied cos-diff1.0

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}}\]
  4. Applied distribute-lft-in1.0

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \color{blue}{\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}}\]
  5. Applied associate-+r+1.0

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\color{blue}{\left(\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) + \cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}}\]
  6. Simplified1.0

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\color{blue}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)} + \cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\]
  7. Using strategy rm
  8. Applied sub-neg1.0

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \color{blue}{\left(\lambda_1 + \left(-\lambda_2\right)\right)}}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + \cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\]
  9. Applied sin-sum0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \cos \left(-\lambda_2\right) + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + \cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\]
  10. Simplified0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\color{blue}{\sin \lambda_1 \cdot \cos \lambda_2} + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + \cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)}\]
  11. Using strategy rm
  12. Applied flip3-+0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\color{blue}{\frac{{\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) \cdot \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + \left(\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)\right)}}}\]
  13. Simplified0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}}\]
  14. Using strategy rm
  15. Applied add-cube-cbrt0.9

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\color{blue}{\left(\left(\sqrt[3]{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)} \cdot \sqrt[3]{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right) \cdot \sqrt[3]{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right)}}^{3} + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}\]
  16. Applied unpow-prod-down0.9

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{\color{blue}{{\left(\sqrt[3]{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)} \cdot \sqrt[3]{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right)}^{3} \cdot {\left(\sqrt[3]{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right)}^{3}} + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}\]
  17. Simplified0.6

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{\color{blue}{{\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)}^{2}} \cdot {\left(\sqrt[3]{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}\]
  18. Simplified0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)}^{2} \cdot \color{blue}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)} + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}\]
  19. Final simplification0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}{\frac{{\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)}^{2} \cdot \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + {\left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right)}^{3}}{\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \mathsf{fma}\left(\cos \lambda_1, \cos \phi_2 \cdot \cos \lambda_2, \cos \phi_1\right), \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \sin \lambda_2\right) - \mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)\right)\right)}}\]

Reproduce

herbie shell --seed 2020056 +o rules:numerics
(FPCore (lambda1 lambda2 phi1 phi2)
  :name "Midpoint on a great circle"
  :precision binary64
  (+ lambda1 (atan2 (* (cos phi2) (sin (- lambda1 lambda2))) (+ (cos phi1) (* (cos phi2) (cos (- lambda1 lambda2)))))))