Average Error: 0.2 → 0.2
Time: 43.5s
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 delta\right) \cdot \sin theta}{\sqrt[3]{\left(\left(\cos delta - \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right) \cdot \sin \phi_1\right) \cdot \left(\mathsf{fma}\left(1, \cos delta, \left(-\sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right)\right) \cdot \sin \phi_1\right) + \mathsf{fma}\left(-\sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right), \sin \phi_1, \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right) \cdot \sin \phi_1\right)\right)\right) \cdot \left(\cos delta - \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right) \cdot \sin \phi_1\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 delta\right) \cdot \sin theta}{\sqrt[3]{\left(\left(\cos delta - \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right) \cdot \sin \phi_1\right) \cdot \left(\mathsf{fma}\left(1, \cos delta, \left(-\sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right)\right) \cdot \sin \phi_1\right) + \mathsf{fma}\left(-\sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right), \sin \phi_1, \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right) \cdot \sin \phi_1\right)\right)\right) \cdot \left(\cos delta - \sin \left(\sin^{-1} \left(\mathsf{fma}\left(\cos theta, \cos \phi_1 \cdot \sin delta, \sin \phi_1 \cdot \cos delta\right)\right)\right) \cdot \sin \phi_1\right)}} + \lambda_1
double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r4073475 = lambda1;
        double r4073476 = theta;
        double r4073477 = sin(r4073476);
        double r4073478 = delta;
        double r4073479 = sin(r4073478);
        double r4073480 = r4073477 * r4073479;
        double r4073481 = phi1;
        double r4073482 = cos(r4073481);
        double r4073483 = r4073480 * r4073482;
        double r4073484 = cos(r4073478);
        double r4073485 = sin(r4073481);
        double r4073486 = r4073485 * r4073484;
        double r4073487 = r4073482 * r4073479;
        double r4073488 = cos(r4073476);
        double r4073489 = r4073487 * r4073488;
        double r4073490 = r4073486 + r4073489;
        double r4073491 = asin(r4073490);
        double r4073492 = sin(r4073491);
        double r4073493 = r4073485 * r4073492;
        double r4073494 = r4073484 - r4073493;
        double r4073495 = atan2(r4073483, r4073494);
        double r4073496 = r4073475 + r4073495;
        return r4073496;
}
↓
double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r4073497 = phi1;
        double r4073498 = cos(r4073497);
        double r4073499 = delta;
        double r4073500 = sin(r4073499);
        double r4073501 = r4073498 * r4073500;
        double r4073502 = theta;
        double r4073503 = sin(r4073502);
        double r4073504 = r4073501 * r4073503;
        double r4073505 = cos(r4073499);
        double r4073506 = cos(r4073502);
        double r4073507 = sin(r4073497);
        double r4073508 = r4073507 * r4073505;
        double r4073509 = fma(r4073506, r4073501, r4073508);
        double r4073510 = asin(r4073509);
        double r4073511 = sin(r4073510);
        double r4073512 = r4073511 * r4073507;
        double r4073513 = r4073505 - r4073512;
        double r4073514 = 1.0;
        double r4073515 = -r4073511;
        double r4073516 = r4073515 * r4073507;
        double r4073517 = fma(r4073514, r4073505, r4073516);
        double r4073518 = fma(r4073515, r4073507, r4073512);
        double r4073519 = r4073517 + r4073518;
        double r4073520 = r4073513 * r4073519;
        double r4073521 = r4073520 * r4073513;
        double r4073522 = cbrt(r4073521);
        double r4073523 = atan2(r4073504, r4073522);
        double r4073524 = lambda1;
        double r4073525 = r4073523 + r4073524;
        return r4073525;
}

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 theta \cdot \left(\cos \phi_1 \cdot \sin delta\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-cbrt-cube0.2

    \[\leadsto \tan^{-1}_* \frac{\sin theta \cdot \left(\cos \phi_1 \cdot \sin delta\right)}{\color{blue}{\sqrt[3]{\left(\left(\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)\right) \cdot \left(\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)\right)\right) \cdot \left(\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)\right)}}} + \lambda_1\]
  5. Using strategy rm

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

    \[\leadsto \tan^{-1}_* \frac{\sin theta \cdot \left(\cos \phi_1 \cdot \sin delta\right)}{\sqrt[3]{\left(\left(\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)\right) \cdot \left(\color{blue}{1 \cdot \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)\right)\right) \cdot \left(\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)\right)}} + \lambda_1\]

  7. Applied prod-diff0.2

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

  8. Final simplification0.2

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

Reproduce

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