?

Average Accuracy: 99.8% → 99.7%
Time: 39.8s
Precision: binary64
Cost: 142464

?

\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(\mathsf{asin.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right) \]
\[\begin{array}{l} t_1 := \mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\\ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{pow.f64}\left(t_1, 2\right)\right), \mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right)\right), \mathsf{cbrt.f64}\left(t_1\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \end{array} \]
(FPCore (lambda1 phi1 phi2 delta theta)
 :precision binary64
 (+.f64
  lambda1
  (atan2.f64
   (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1))
   (-.f64
    (cos.f64 delta)
    (*.f64
     (sin.f64 phi1)
     (sin.f64
      (asin.f64
       (+.f64
        (*.f64 (sin.f64 phi1) (cos.f64 delta))
        (*.f64 (*.f64 (cos.f64 phi1) (sin.f64 delta)) (cos.f64 theta))))))))))
(FPCore (lambda1 phi1 phi2 delta theta)
 :precision binary64
 (let* ((t_1
         (fma.f64
          (sin.f64 phi1)
          (cos.f64 delta)
          (*.f64 (cos.f64 phi1) (*.f64 (sin.f64 delta) (cos.f64 theta))))))
   (+.f64
    lambda1
    (atan2.f64
     (*.f64 (*.f64 (sin.f64 theta) (sin.f64 delta)) (cos.f64 phi1))
     (fma.f64
      (*.f64 (cbrt.f64 (pow.f64 t_1 2)) (neg.f64 (sin.f64 phi1)))
      (cbrt.f64 t_1)
      (cos.f64 delta))))))
\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(\mathsf{asin.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right)
\begin{array}{l}
t_1 := \mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\\
\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{pow.f64}\left(t_1, 2\right)\right), \mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right)\right), \mathsf{cbrt.f64}\left(t_1\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right)
\end{array}

Error?

Derivation?

  1. Initial program 99.8%

    \[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(\mathsf{asin.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right) \]
  2. Applied egg-rr99.7%

    \[\leadsto \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{log.f64}\left(\mathsf{+.f64}\left(1, \mathsf{expm1.f64}\left(\mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right)}\right)\right) \]
    Proof

    [Start]99.8

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(\mathsf{asin.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right) \]

    log1p-expm1-u [=>]99.7

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{log1p.f64}\left(\mathsf{expm1.f64}\left(\mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(\mathsf{asin.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right)}\right)\right) \]

    log1p-udef [=>]99.7

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{log.f64}\left(\mathsf{+.f64}\left(1, \mathsf{expm1.f64}\left(\mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(\mathsf{asin.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)}\right)\right) \]

    sin-asin [=>]99.7

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{log.f64}\left(\mathsf{+.f64}\left(1, \mathsf{expm1.f64}\left(\mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(theta\right)\right)\right)}\right)\right)\right)\right)\right)\right)\right) \]
  3. Applied egg-rr99.7%

    \[\leadsto \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{fma.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right), \mathsf{cbrt.f64}\left(\mathsf{pow.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right)\right)\right), 2\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right)\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)}\right)\right) \]
    Proof

    [Start]99.7

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{log.f64}\left(\mathsf{+.f64}\left(1, \mathsf{expm1.f64}\left(\mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right) \]

    log1p-def [=>]99.8

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{log1p.f64}\left(\mathsf{expm1.f64}\left(\mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)}\right)\right) \]

    log1p-expm1-u [<=]99.8

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)}\right)\right) \]

    sub-neg [=>]99.8

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)}\right)\right) \]

    +-commutative [=>]99.8

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)}\right)\right) \]

    distribute-lft-neg-in [=>]99.8

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)}, \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \]

    add-cube-cbrt [=>]99.7

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)}\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \]

    associate-*r* [=>]99.6

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right), \mathsf{*.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)}, \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \]
  4. Simplified99.7%

    \[\leadsto \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \color{blue}{\mathsf{fma.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{neg.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{pow.f64}\left(\mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right)\right)\right), 2\right)\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right)\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)}\right)\right) \]
    Proof

    [Start]99.7

    \[ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right), \mathsf{cbrt.f64}\left(\mathsf{pow.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right)\right)\right), 2\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right)\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \]
  5. Final simplification99.7%

    \[\leadsto \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{pow.f64}\left(\mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right), 2\right)\right), \mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \]

Alternatives

Alternative 1
Accuracy99.7%
Cost142464
\[\begin{array}{l} t_1 := \mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\\ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{pow.f64}\left(t_1, 2\right)\right), \mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right)\right), \mathsf{cbrt.f64}\left(t_1\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \end{array} \]
Alternative 2
Accuracy99.7%
Cost90752
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{expm1.f64}\left(\mathsf{log1p.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{fma.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{sin.f64}\left(\phi_1\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right)\right)\right)\right)\right)\right)\right) \]
Alternative 3
Accuracy99.7%
Cost84608
\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\\ \mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), t_1\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right), \mathsf{log.f64}\left(\mathsf{+.f64}\left(1, \mathsf{expm1.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(theta\right), t_1\right)\right)\right)\right)\right)\right)\right)\right)\right) \end{array} \]
Alternative 4
Accuracy99.8%
Cost84288
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{fma.f64}\left(\mathsf{fma.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sin.f64}\left(\phi_1\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right) \]
Alternative 5
Accuracy99.8%
Cost71680
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right)\right)\right)\right) \]
Alternative 6
Accuracy99.8%
Cost71680
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(theta\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right)\right)\right)\right) \]
Alternative 7
Accuracy94.3%
Cost65152
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(\phi_1\right)\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\right)\right)\right)\right) \]
Alternative 8
Accuracy89.5%
Cost45960
\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{sin.f64}\left(delta\right), \frac{-5332261958806667}{288230376151711744}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(t_1, \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\phi_1, \phi_1\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{sin.f64}\left(delta\right), \frac{-1320736327839163}{33018408195979077897021236557282287907427957877257595132997544314167118909795303717151078492978574243417149687078570542430146722468917846078158686153933723556774167749937817760545719854776652565814014556763199275259251768296972608677399806172939779780596161306108624896}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(t_1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, \mathsf{cos.f64}\left(\mathsf{+.f64}\left(\phi_1, \phi_1\right)\right)\right), 2\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\\ \end{array} \]
Alternative 9
Accuracy89.5%
Cost45704
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{sin.f64}\left(delta\right), \frac{-5332261958806667}{288230376151711744}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{*.f64}\left(\phi_1, \phi_1\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{sin.f64}\left(delta\right), \frac{-1320736327839163}{33018408195979077897021236557282287907427957877257595132997544314167118909795303717151078492978574243417149687078570542430146722468917846078158686153933723556774167749937817760545719854776652565814014556763199275259251768296972608677399806172939779780596161306108624896}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{*.f64}\left(delta, \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\phi_1\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\\ \end{array} \]
Alternative 10
Accuracy92.1%
Cost39424
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{+.f64}\left(\mathsf{cos.f64}\left(delta\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(\phi_1, 2\right)\right), -1\right), 2\right)\right)\right)\right) \]
Alternative 11
Accuracy75.2%
Cost32649
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{sin.f64}\left(delta\right), \frac{-1261007895663739}{4503599627370496}\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{sin.f64}\left(delta\right), \frac{348449143727041}{696898287454081973172991196020261297061888}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(theta, \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\lambda_1\\ \end{array} \]
Alternative 12
Accuracy88.2%
Cost32512
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(delta\right), \mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{cos.f64}\left(\phi_1\right)\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right) \]
Alternative 13
Accuracy86.0%
Cost25984
\[\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right) \]
Alternative 14
Accuracy79.4%
Cost19849
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(delta, -1419999999999999983727607138668932362056590686158848\right) \lor \neg \mathsf{<=.f64}\left(delta, 325000000000000006850731374841046237184\right):\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(theta, \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\lambda_1, \mathsf{atan2.f64}\left(\mathsf{*.f64}\left(\mathsf{sin.f64}\left(theta\right), \mathsf{sin.f64}\left(delta\right)\right), 1\right)\right)\\ \end{array} \]
Alternative 15
Accuracy69.6%
Cost19720
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\lambda_1, \frac{-6491683198595055}{1081947199765842424529591879509026010150599323721976877318063532086628152436172512203606540057921920808293160946190599534351047801861499980289103827892100253508375928829962412377562148201321351276593628996016513851695161943555198441141036848674890703850575013678567420592128}\right):\\ \;\;\;\;\lambda_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\lambda_1, \frac{533661513344723}{5231975621026695903068481684863290090631859432155925817596437443214604741820977160611320209061014932263645863855239974732359107840294502166008094518895788478483675671300894035850134084503110909120094815504417224113077119759472054472248800754920440876255467030120381917802944253736633001385354330112}\right):\\ \;\;\;\;\mathsf{atan2.f64}\left(\mathsf{*.f64}\left(theta, \mathsf{sin.f64}\left(delta\right)\right), \mathsf{cos.f64}\left(delta\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\lambda_1\\ \end{array} \]
Alternative 16
Accuracy69.3%
Cost64
\[\lambda_1 \]

Error

Reproduce?

herbie shell --seed 2023144 
(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))))))))))