Average Error: 0.2 → 0.2
Time: 49.2s
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)}\]
↓
\[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin delta \cdot \sin theta\right)}{\mathsf{fma}\left(-\sin \left(\log \left(e^{\sin^{-1} \left(\mathsf{fma}\left(\cos theta \cdot \cos \phi_1, \sin delta, \cos delta \cdot \sin \phi_1\right)\right)}\right)\right), \sin \phi_1, \sin \phi_1 \cdot \sin \left(\log \left(e^{\sin^{-1} \left(\mathsf{fma}\left(\cos theta \cdot \cos \phi_1, \sin delta, \cos delta \cdot \sin \phi_1\right)\right)}\right)\right)\right) + \mathsf{fma}\left(1, \cos delta, \left(-\sin \left(\log \left(e^{\sin^{-1} \left(\mathsf{fma}\left(\cos theta \cdot \cos \phi_1, \sin delta, \cos delta \cdot \sin \phi_1\right)\right)}\right)\right)\right) \cdot \sin \phi_1\right)}\]
\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)}
↓
\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin delta \cdot \sin theta\right)}{\mathsf{fma}\left(-\sin \left(\log \left(e^{\sin^{-1} \left(\mathsf{fma}\left(\cos theta \cdot \cos \phi_1, \sin delta, \cos delta \cdot \sin \phi_1\right)\right)}\right)\right), \sin \phi_1, \sin \phi_1 \cdot \sin \left(\log \left(e^{\sin^{-1} \left(\mathsf{fma}\left(\cos theta \cdot \cos \phi_1, \sin delta, \cos delta \cdot \sin \phi_1\right)\right)}\right)\right)\right) + \mathsf{fma}\left(1, \cos delta, \left(-\sin \left(\log \left(e^{\sin^{-1} \left(\mathsf{fma}\left(\cos theta \cdot \cos \phi_1, \sin delta, \cos delta \cdot \sin \phi_1\right)\right)}\right)\right)\right) \cdot \sin \phi_1\right)}
double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r2844200 = lambda1;
        double r2844201 = theta;
        double r2844202 = sin(r2844201);
        double r2844203 = delta;
        double r2844204 = sin(r2844203);
        double r2844205 = r2844202 * r2844204;
        double r2844206 = phi1;
        double r2844207 = cos(r2844206);
        double r2844208 = r2844205 * r2844207;
        double r2844209 = cos(r2844203);
        double r2844210 = sin(r2844206);
        double r2844211 = r2844210 * r2844209;
        double r2844212 = r2844207 * r2844204;
        double r2844213 = cos(r2844201);
        double r2844214 = r2844212 * r2844213;
        double r2844215 = r2844211 + r2844214;
        double r2844216 = asin(r2844215);
        double r2844217 = sin(r2844216);
        double r2844218 = r2844210 * r2844217;
        double r2844219 = r2844209 - r2844218;
        double r2844220 = atan2(r2844208, r2844219);
        double r2844221 = r2844200 + r2844220;
        return r2844221;
}
↓
double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r2844222 = lambda1;
        double r2844223 = phi1;
        double r2844224 = cos(r2844223);
        double r2844225 = delta;
        double r2844226 = sin(r2844225);
        double r2844227 = theta;
        double r2844228 = sin(r2844227);
        double r2844229 = r2844226 * r2844228;
        double r2844230 = r2844224 * r2844229;
        double r2844231 = cos(r2844227);
        double r2844232 = r2844231 * r2844224;
        double r2844233 = cos(r2844225);
        double r2844234 = sin(r2844223);
        double r2844235 = r2844233 * r2844234;
        double r2844236 = fma(r2844232, r2844226, r2844235);
        double r2844237 = asin(r2844236);
        double r2844238 = exp(r2844237);
        double r2844239 = log(r2844238);
        double r2844240 = sin(r2844239);
        double r2844241 = -r2844240;
        double r2844242 = r2844234 * r2844240;
        double r2844243 = fma(r2844241, r2844234, r2844242);
        double r2844244 = 1.0;
        double r2844245 = r2844241 * r2844234;
        double r2844246 = fma(r2844244, r2844233, r2844245);
        double r2844247 = r2844243 + r2844246;
        double r2844248 = atan2(r2844230, r2844247);
        double r2844249 = r2844222 + r2844248;
        return r2844249;
}

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. Using strategy rm

  3. Applied add-log-exp0.2

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

  4. Simplified0.2

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

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

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

  7. Applied prod-diff0.2

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

  8. Final simplification0.2

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

Reproduce

herbie shell --seed 2019143 +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))))))))))