Destination given bearing on a great circle

Average Error: 0.2 → 0.2

Time: 14.0s

Precision: 64

• unused variable phi2

Math

\[\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{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\left(\cos delta - \sin \phi_1 \cdot \left(\cos \left(\log \left(\sqrt{e^{\sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}}\right)\right) \cdot \sin \left(\frac{1}{2} \cdot \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)\right)\right) - \log \left(e^{\sin \phi_1 \cdot \left(\cos \left(\log \left(\sqrt{e^{\sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}}\right)\right) \cdot \sin \left(\log \left(\sqrt{e^{\sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}}\right)\right)\right)}\right)}\]

C

double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r94460 = lambda1;
        double r94461 = theta;
        double r94462 = sin(r94461);
        double r94463 = delta;
        double r94464 = sin(r94463);
        double r94465 = r94462 * r94464;
        double r94466 = phi1;
        double r94467 = cos(r94466);
        double r94468 = r94465 * r94467;
        double r94469 = cos(r94463);
        double r94470 = sin(r94466);
        double r94471 = r94470 * r94469;
        double r94472 = r94467 * r94464;
        double r94473 = cos(r94461);
        double r94474 = r94472 * r94473;
        double r94475 = r94471 + r94474;
        double r94476 = asin(r94475);
        double r94477 = sin(r94476);
        double r94478 = r94470 * r94477;
        double r94479 = r94469 - r94478;
        double r94480 = atan2(r94468, r94479);
        double r94481 = r94460 + r94480;
        return r94481;
}

↓

double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r94482 = lambda1;
        double r94483 = theta;
        double r94484 = sin(r94483);
        double r94485 = delta;
        double r94486 = sin(r94485);
        double r94487 = r94484 * r94486;
        double r94488 = phi1;
        double r94489 = cos(r94488);
        double r94490 = r94487 * r94489;
        double r94491 = cos(r94485);
        double r94492 = sin(r94488);
        double r94493 = r94492 * r94491;
        double r94494 = r94489 * r94486;
        double r94495 = cos(r94483);
        double r94496 = r94494 * r94495;
        double r94497 = r94493 + r94496;
        double r94498 = asin(r94497);
        double r94499 = exp(r94498);
        double r94500 = sqrt(r94499);
        double r94501 = log(r94500);
        double r94502 = cos(r94501);
        double r94503 = 1.0;
        double r94504 = 2.0;
        double r94505 = r94503 / r94504;
        double r94506 = r94505 * r94498;
        double r94507 = sin(r94506);
        double r94508 = r94502 * r94507;
        double r94509 = r94492 * r94508;
        double r94510 = r94491 - r94509;
        double r94511 = sin(r94501);
        double r94512 = r94502 * r94511;
        double r94513 = r94492 * r94512;
        double r94514 = exp(r94513);
        double r94515 = log(r94514);
        double r94516 = r94510 - r94515;
        double r94517 = atan2(r94490, r94516);
        double r94518 = r94482 + r94517;
        return r94518;
}

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-exp 0.2

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

5. Applied add-log-exp 0.2

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

7. Applied add-sqr-sqrt 0.2

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

8. Applied log-prod 0.2

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

9. Applied sin-sum 0.2

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

10. Applied distribute-lft-in 0.2

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

11. Applied exp-sum 0.2

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

12. Applied log-prod 0.2

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

13. Applied associate--r+ 0.2

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

14. Simplified 0.2

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

16. Applied pow1 0.2

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

17. Applied sqrt-pow1 0.2

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

18. Applied log-pow 0.2

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

19. Simplified 0.2

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

20. Final simplification 0.2

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

Reproduce

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