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 r93045 = lambda1;
        double r93046 = theta;
        double r93047 = sin(r93046);
        double r93048 = delta;
        double r93049 = sin(r93048);
        double r93050 = r93047 * r93049;
        double r93051 = phi1;
        double r93052 = cos(r93051);
        double r93053 = r93050 * r93052;
        double r93054 = cos(r93048);
        double r93055 = sin(r93051);
        double r93056 = r93055 * r93054;
        double r93057 = r93052 * r93049;
        double r93058 = cos(r93046);
        double r93059 = r93057 * r93058;
        double r93060 = r93056 + r93059;
        double r93061 = asin(r93060);
        double r93062 = sin(r93061);
        double r93063 = r93055 * r93062;
        double r93064 = r93054 - r93063;
        double r93065 = atan2(r93053, r93064);
        double r93066 = r93045 + r93065;
        return r93066;
}

↓

double f(double lambda1, double phi1, double __attribute__((unused)) phi2, double delta, double theta) {
        double r93067 = lambda1;
        double r93068 = theta;
        double r93069 = sin(r93068);
        double r93070 = delta;
        double r93071 = sin(r93070);
        double r93072 = r93069 * r93071;
        double r93073 = phi1;
        double r93074 = cos(r93073);
        double r93075 = r93072 * r93074;
        double r93076 = cos(r93070);
        double r93077 = sin(r93073);
        double r93078 = r93077 * r93076;
        double r93079 = r93074 * r93071;
        double r93080 = cos(r93068);
        double r93081 = r93079 * r93080;
        double r93082 = r93078 + r93081;
        double r93083 = asin(r93082);
        double r93084 = exp(r93083);
        double r93085 = sqrt(r93084);
        double r93086 = log(r93085);
        double r93087 = cos(r93086);
        double r93088 = 0.5;
        double r93089 = r93088 * r93083;
        double r93090 = sin(r93089);
        double r93091 = r93087 * r93090;
        double r93092 = r93077 * r93091;
        double r93093 = r93076 - r93092;
        double r93094 = sin(r93086);
        double r93095 = r93087 * r93094;
        double r93096 = r93077 * r93095;
        double r93097 = exp(r93096);
        double r93098 = log(r93097);
        double r93099 = r93093 - r93098;
        double r93100 = atan2(r93075, r93099);
        double r93101 = r93067 + r93100;
        return r93101;
}

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))))))))))