Average Error: 0.2 → 0.2
Time: 47.9s
Precision: 64
\[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \left(\sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}\]
↓
\[\tan^{-1}_* \frac{\left(\cos \phi_1 \cdot \sin theta\right) \cdot \sin delta}{\mathsf{fma}\left(1, \cos delta, \left(-\sqrt[3]{\sin \phi_1 \cdot \left(\sin \phi_1 \cdot \sin \phi_1\right)}\right) \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right)} + \lambda_1\]
\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \left(\sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}
↓
\tan^{-1}_* \frac{\left(\cos \phi_1 \cdot \sin theta\right) \cdot \sin delta}{\mathsf{fma}\left(1, \cos delta, \left(-\sqrt[3]{\sin \phi_1 \cdot \left(\sin \phi_1 \cdot \sin \phi_1\right)}\right) \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right)} + \lambda_1
double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r3609189 = lambda1;
        double r3609190 = theta;
        double r3609191 = sin(r3609190);
        double r3609192 = delta;
        double r3609193 = sin(r3609192);
        double r3609194 = r3609191 * r3609193;
        double r3609195 = phi1;
        double r3609196 = cos(r3609195);
        double r3609197 = r3609194 * r3609196;
        double r3609198 = cos(r3609192);
        double r3609199 = sin(r3609195);
        double r3609200 = r3609199 * r3609198;
        double r3609201 = r3609196 * r3609193;
        double r3609202 = cos(r3609190);
        double r3609203 = r3609201 * r3609202;
        double r3609204 = r3609200 + r3609203;
        double r3609205 = asin(r3609204);
        double r3609206 = sin(r3609205);
        double r3609207 = r3609199 * r3609206;
        double r3609208 = r3609198 - r3609207;
        double r3609209 = atan2(r3609197, r3609208);
        double r3609210 = r3609189 + r3609209;
        return r3609210;
}
↓
double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r3609211 = phi1;
        double r3609212 = cos(r3609211);
        double r3609213 = theta;
        double r3609214 = sin(r3609213);
        double r3609215 = r3609212 * r3609214;
        double r3609216 = delta;
        double r3609217 = sin(r3609216);
        double r3609218 = r3609215 * r3609217;
        double r3609219 = 1.0;
        double r3609220 = cos(r3609216);
        double r3609221 = sin(r3609211);
        double r3609222 = r3609221 * r3609221;
        double r3609223 = r3609221 * r3609222;
        double r3609224 = cbrt(r3609223);
        double r3609225 = -r3609224;
        double r3609226 = cos(r3609213);
        double r3609227 = r3609212 * r3609217;
        double r3609228 = r3609220 * r3609221;
        double r3609229 = fma(r3609226, r3609227, r3609228);
        double r3609230 = asin(r3609229);
        double r3609231 = sin(r3609230);
        double r3609232 = r3609225 * r3609231;
        double r3609233 = fma(r3609219, r3609220, r3609232);
        double r3609234 = atan2(r3609218, r3609233);
        double r3609235 = lambda1;
        double r3609236 = r3609234 + r3609235;
        return r3609236;
}

Error

Bits error versus lambda1

Bits error versus phi1

Bits error versus phi2

Bits error versus delta

Bits error versus theta

Derivation

  1. Initial program 0.2

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \left(\sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}\]

  2. Simplified0.2

    \[\leadsto \color{blue}{\tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\cos delta - \sin \phi_1 \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)} + \lambda_1}\]
  3. Using strategy rm

  4. Applied add-log-exp0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\cos delta - \color{blue}{\log \left(e^{\sin \phi_1 \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)}\right)}} + \lambda_1\]
  5. Using strategy rm

  6. Applied add-log-exp0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\cos delta - \log \left(e^{\color{blue}{\log \left(e^{\sin \phi_1}\right)} \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)}\right)} + \lambda_1\]

  7. Applied exp-to-pow0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\cos delta - \log \color{blue}{\left({\left(e^{\sin \phi_1}\right)}^{\left(\sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right)}\right)}} + \lambda_1\]

  8. Applied log-pow0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\cos delta - \color{blue}{\sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right) \cdot \log \left(e^{\sin \phi_1}\right)}} + \lambda_1\]

  9. Applied *-un-lft-identity0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\color{blue}{1 \cdot \cos delta} - \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right) \cdot \log \left(e^{\sin \phi_1}\right)} + \lambda_1\]

  10. Applied prod-diff0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\color{blue}{\mathsf{fma}\left(1, \cos delta, -\log \left(e^{\sin \phi_1}\right) \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right) + \mathsf{fma}\left(-\log \left(e^{\sin \phi_1}\right), \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right), \log \left(e^{\sin \phi_1}\right) \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right)}} + \lambda_1\]

  11. Simplified0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\mathsf{fma}\left(1, \cos delta, -\log \left(e^{\sin \phi_1}\right) \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right) + \color{blue}{0}} + \lambda_1\]
  12. Using strategy rm

  13. Applied add-cbrt-cube0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\mathsf{fma}\left(1, \cos delta, -\color{blue}{\sqrt[3]{\left(\log \left(e^{\sin \phi_1}\right) \cdot \log \left(e^{\sin \phi_1}\right)\right) \cdot \log \left(e^{\sin \phi_1}\right)}} \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right) + 0} + \lambda_1\]

  14. Simplified0.2

    \[\leadsto \tan^{-1}_* \frac{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}{\mathsf{fma}\left(1, \cos delta, -\sqrt[3]{\color{blue}{\sin \phi_1 \cdot \left(\sin \phi_1 \cdot \sin \phi_1\right)}} \cdot \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \cos delta \cdot \sin \phi_1\right)\right)\right)\right) + 0} + \lambda_1\]

  15. Final simplification0.2

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

Reproduce

herbie shell --seed 2019158 +o rules:numerics
(FPCore (lambda1 phi1 phi2 delta theta)
  :name "Destination given bearing on a great circle"
  (+ lambda1 (atan2 (* (* (sin theta) (sin delta)) (cos phi1)) (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))