Destination given bearing on a great circle

Percentage Accurate: 99.7% → 99.7%
Time: 28.1s
Alternatives: 14
Speedup: TODO×

Specification

?
\[\begin{array}{l} t_1 := \cos delta\\ t_2 := \sin \phi_1\\ t_3 := \sin delta\\ t_4 := \cos \phi_1\\ \lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot t_3\right) \cdot t_4}{t_1 - t_2 \cdot \sin \sin^{-1} \left(t_2 \cdot t_1 + \left(t_4 \cdot t_3\right) \cdot \cos theta\right)} \end{array} \]

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 14 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Alternative 1?

\[\begin{array}{l} t_1 := \sin delta \cdot \cos \phi_1\\ \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot t_1}{\cos delta - \mathsf{expm1}\left(\mathsf{log1p}\left(\sin \phi_1 \cdot \mathsf{fma}\left(\cos delta, \sin \phi_1, t_1 \cdot \cos theta\right)\right)\right)} \end{array} \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. cancel-sign-sub-inv99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    3. cancel-sign-sub99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(-\left(-\sin \phi_1\right)\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    4. remove-double-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1} \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    5. fma-def99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    6. associate-*l*99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)\right)}} \]
  4. Step-by-step derivation
    1. sin-asin99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
    2. add-sqr-sqrt45.9%

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sqrt{\sin \phi_1 \cdot \sin \phi_1}} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
    4. sqr-neg92.7%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sqrt{\color{blue}{\left(-\sin \phi_1\right) \cdot \left(-\sin \phi_1\right)}} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
    5. sqrt-unprod46.8%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\left(\sqrt{-\sin \phi_1} \cdot \sqrt{-\sin \phi_1}\right)} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
    6. add-sqr-sqrt86.0%

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \cos delta + \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
    8. associate-*r*86.0%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \color{blue}{\left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta}\right)} \]
    9. expm1-log1p-u86.0%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)\right)}} \]
  5. Applied egg-rr99.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \phi_1 \cdot \mathsf{fma}\left(\cos delta, \sin \phi_1, \cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)\right)\right)\right)}} \]
  6. Final simplification99.6%

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

Alternative 2?

\[\begin{array}{l} t_1 := \sin delta \cdot \cos \phi_1\\ \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot t_1}{\cos delta - \sin \phi_1 \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, t_1 \cdot \cos theta\right)} \end{array} \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. cancel-sign-sub-inv99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    3. cancel-sign-sub99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(-\left(-\sin \phi_1\right)\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    4. remove-double-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1} \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    5. fma-def99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    6. associate-*l*99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)\right)}} \]
  4. Taylor expanded in phi1 around inf 99.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\left(\cos delta \cdot \sin \phi_1 + \sin delta \cdot \left(\cos \phi_1 \cdot \cos theta\right)\right) \cdot \sin \phi_1}} \]
  5. Step-by-step derivation
    1. associate-*r*99.6%

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(\cos delta \cdot \sin \phi_1 + \color{blue}{\cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}\right) \cdot \sin \phi_1} \]
    3. fma-udef99.6%

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

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

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \left(\color{blue}{\sin \phi_1 \cdot \cos delta} + \cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)\right)} \]
    7. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \left(\sin \phi_1 \cdot \cos delta + \color{blue}{\left(\sin delta \cdot \cos \phi_1\right) \cdot \cos theta}\right)} \]
    8. associate-*r*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \left(\sin \phi_1 \cdot \cos delta + \color{blue}{\sin delta \cdot \left(\cos \phi_1 \cdot \cos theta\right)}\right)} \]
    9. fma-udef99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \phi_1, \cos delta, \sin delta \cdot \left(\cos \phi_1 \cdot \cos theta\right)\right)}} \]
    10. associate-*r*99.6%

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

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

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

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1 \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos theta \cdot \left(\cos \phi_1 \cdot \sin delta\right)\right)}} \]
  7. Final simplification99.6%

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

Alternative 3?

\[\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \left(\cos delta \cdot \sin \phi_1 + \sin delta \cdot \left(\cos \phi_1 \cdot \cos theta\right)\right)} \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. cancel-sign-sub-inv99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    3. cancel-sign-sub99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(-\left(-\sin \phi_1\right)\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    4. remove-double-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1} \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    5. fma-def99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    6. associate-*l*99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)\right)}} \]
  4. Taylor expanded in delta around inf 99.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(\cos delta \cdot \sin \phi_1 + \sin delta \cdot \left(\cos \phi_1 \cdot \cos theta\right)\right) \cdot \sin \phi_1}} \]
  5. Final simplification99.6%

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

Alternative 4?

\[\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \left(\sin delta \cdot \cos \phi_1 + \cos delta \cdot \sin \phi_1\right)} \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. cancel-sign-sub-inv99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    3. cancel-sign-sub99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(-\left(-\sin \phi_1\right)\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
    4. remove-double-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1} \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    5. fma-def99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    6. associate-*l*99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)\right)}} \]
  4. Taylor expanded in theta around 0 93.4%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \sin \phi_1 \cdot \left(\sin delta \cdot \cos \phi_1 + \cos delta \cdot \sin \phi_1\right)}} \]
  5. Taylor expanded in theta around inf 93.5%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}}{\cos delta - \sin \phi_1 \cdot \left(\sin delta \cdot \cos \phi_1 + \cos delta \cdot \sin \phi_1\right)} \]
  6. Final simplification93.5%

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

Alternative 5?

\[\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + \left(\frac{\cos \left(\phi_1 + \phi_1\right)}{2} - 0.5\right)} \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    3. sub-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    4. +-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
    5. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
    6. distribute-rgt-neg-in99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
    7. fma-def99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
  4. Taylor expanded in theta around 0 93.5%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + -1 \cdot \left(\sin \phi_1 \cdot \left(\sin delta \cdot \cos \phi_1 + \cos delta \cdot \sin \phi_1\right)\right)}} \]
  5. Taylor expanded in delta around 0 91.1%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + -1 \cdot \color{blue}{{\sin \phi_1}^{2}}} \]
  6. Step-by-step derivation
    1. unpow291.1%

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + -1 \cdot \color{blue}{\frac{\cos \left(\phi_1 - \phi_1\right) - \cos \left(\phi_1 + \phi_1\right)}{2}}} \]
  7. Applied egg-rr91.1%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + -1 \cdot \color{blue}{\frac{\cos \left(\phi_1 - \phi_1\right) - \cos \left(\phi_1 + \phi_1\right)}{2}}} \]
  8. Step-by-step derivation
    1. div-sub91.1%

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + -1 \cdot \left(\frac{\cos \color{blue}{0}}{2} - \frac{\cos \left(\phi_1 + \phi_1\right)}{2}\right)} \]
    3. cos-091.1%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + -1 \cdot \left(\frac{\color{blue}{1}}{2} - \frac{\cos \left(\phi_1 + \phi_1\right)}{2}\right)} \]
    4. metadata-eval91.1%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + -1 \cdot \left(\color{blue}{0.5} - \frac{\cos \left(\phi_1 + \phi_1\right)}{2}\right)} \]
  9. Simplified91.1%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\cos delta + -1 \cdot \color{blue}{\left(0.5 - \frac{\cos \left(\phi_1 + \phi_1\right)}{2}\right)}} \]
  10. Final simplification91.1%

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

Alternative 6?

\[\begin{array}{l} \mathbf{if}\;delta \leq -5.5 \cdot 10^{-5} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{{\cos \phi_1}^{2}}\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if delta < -5.5000000000000002e-5 or 2.15e15 < delta

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
      5. *-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.7%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in delta around inf 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}}{\cos delta} \]
    6. Step-by-step derivation
      1. associate-*r*83.2%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\cos \phi_1 \cdot \sin delta\right)} \cdot \sin theta}{\cos delta} \]
      3. associate-*l*83.2%

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

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

    if -5.5000000000000002e-5 < delta < 2.15e15

    1. Initial program 99.5%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.5%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.5%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in theta around 0 98.4%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + -1 \cdot \left(\sin \phi_1 \cdot \left(\sin delta \cdot \cos \phi_1 + \cos delta \cdot \sin \phi_1\right)\right)}} \]
    5. Taylor expanded in delta around 0 98.0%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{1 + -1 \cdot {\sin \phi_1}^{2}}} \]
    6. Step-by-step derivation
      1. mul-1-neg98.0%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{1 + \color{blue}{\left(-{\sin \phi_1}^{2}\right)}} \]
      2. unsub-neg98.0%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{1 - {\sin \phi_1}^{2}}} \]
      3. unpow298.0%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{1 - \color{blue}{\sin \phi_1 \cdot \sin \phi_1}} \]
      4. 1-sub-sin98.2%

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

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{{\cos \phi_1}^{2}}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification90.8%

    \[\leadsto \begin{array}{l} \mathbf{if}\;delta \leq -5.5 \cdot 10^{-5} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{{\cos \phi_1}^{2}}\\ \end{array} \]

Alternative 7?

\[\begin{array}{l} \mathbf{if}\;delta \leq -4.3 \cdot 10^{-7} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\frac{\cos \left(\phi_1 + \phi_1\right) + 1}{2}}\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if delta < -4.3000000000000001e-7 or 2.15e15 < delta

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
      5. *-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.7%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in delta around inf 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}}{\cos delta} \]
    6. Step-by-step derivation
      1. associate-*r*83.2%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\cos \phi_1 \cdot \sin delta\right)} \cdot \sin theta}{\cos delta} \]
      3. associate-*l*83.2%

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

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

    if -4.3000000000000001e-7 < delta < 2.15e15

    1. Initial program 99.5%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. associate-*l*99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. cancel-sign-sub-inv99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
      3. cancel-sign-sub99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(-\left(-\sin \phi_1\right)\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
      4. remove-double-neg99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1} \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      5. fma-def99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      6. associate-*l*99.6%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)\right)}} \]
    4. Step-by-step derivation
      1. sin-asin99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
      2. add-sqr-sqrt45.5%

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

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sqrt{\color{blue}{\left(-\sin \phi_1\right) \cdot \left(-\sin \phi_1\right)}} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
      5. sqrt-unprod47.8%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\left(\sqrt{-\sin \phi_1} \cdot \sqrt{-\sin \phi_1}\right)} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
      6. add-sqr-sqrt89.7%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \cos delta + \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
      8. associate-*r*89.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \color{blue}{\left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta}\right)} \]
      9. expm1-log1p-u89.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)\right)}} \]
    5. Applied egg-rr99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \phi_1 \cdot \mathsf{fma}\left(\cos delta, \sin \phi_1, \cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)\right)\right)\right)}} \]
    6. Taylor expanded in delta around 0 98.0%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{1 - {\sin \phi_1}^{2}}} \]
    7. Step-by-step derivation
      1. unpow298.0%

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

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

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{{\cos \phi_1}^{2}}} \]
    9. Step-by-step derivation
      1. unpow298.2%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\frac{\cos \left(\phi_1 + \phi_1\right) + \cos \left(\phi_1 - \phi_1\right)}{2}}} \]
    10. Applied egg-rr98.1%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\frac{\cos \left(\phi_1 + \phi_1\right) + \cos \left(\phi_1 - \phi_1\right)}{2}}} \]
    11. Step-by-step derivation
      1. +-commutative98.1%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\frac{\cos \color{blue}{0} + \cos \left(\phi_1 + \phi_1\right)}{2}} \]
      3. cos-098.1%

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\frac{1 + \cos \left(\phi_1 + \phi_1\right)}{2}}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification90.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;delta \leq -4.3 \cdot 10^{-7} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\frac{\cos \left(\phi_1 + \phi_1\right) + 1}{2}}\\ \end{array} \]

Alternative 8?

\[\begin{array}{l} \mathbf{if}\;delta \leq -0.000125 \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot delta\right)}{{\cos \phi_1}^{2}}\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if delta < -1.25e-4 or 2.15e15 < delta

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
      5. *-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.7%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in delta around inf 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}}{\cos delta} \]
    6. Step-by-step derivation
      1. associate-*r*83.2%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\cos \phi_1 \cdot \sin delta\right)} \cdot \sin theta}{\cos delta} \]
      3. associate-*l*83.2%

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

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

    if -1.25e-4 < delta < 2.15e15

    1. Initial program 99.5%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. associate-*l*99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. cancel-sign-sub-inv99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
      3. cancel-sign-sub99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(-\left(-\sin \phi_1\right)\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
      4. remove-double-neg99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1} \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      5. fma-def99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      6. associate-*l*99.6%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)\right)}} \]
    4. Step-by-step derivation
      1. sin-asin99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
      2. add-sqr-sqrt45.5%

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

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sqrt{\color{blue}{\left(-\sin \phi_1\right) \cdot \left(-\sin \phi_1\right)}} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
      5. sqrt-unprod47.8%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\left(\sqrt{-\sin \phi_1} \cdot \sqrt{-\sin \phi_1}\right)} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
      6. add-sqr-sqrt89.7%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \cos delta + \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
      8. associate-*r*89.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \color{blue}{\left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta}\right)} \]
      9. expm1-log1p-u89.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)\right)}} \]
    5. Applied egg-rr99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \phi_1 \cdot \mathsf{fma}\left(\cos delta, \sin \phi_1, \cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)\right)\right)\right)}} \]
    6. Taylor expanded in delta around 0 98.0%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{1 - {\sin \phi_1}^{2}}} \]
    7. Step-by-step derivation
      1. unpow298.0%

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

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

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{{\cos \phi_1}^{2}}} \]
    9. Taylor expanded in delta around 0 97.9%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\cos \phi_1 \cdot \left(delta \cdot \sin theta\right)}}{{\cos \phi_1}^{2}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification90.6%

    \[\leadsto \begin{array}{l} \mathbf{if}\;delta \leq -0.000125 \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot delta\right)}{{\cos \phi_1}^{2}}\\ \end{array} \]

Alternative 9?

\[\begin{array}{l} \mathbf{if}\;delta \leq -1.48 \cdot 10^{-5} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(delta \cdot \cos \phi_1\right)}{{\cos \phi_1}^{2}}\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if delta < -1.4800000000000001e-5 or 2.15e15 < delta

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
      5. *-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.7%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in delta around inf 83.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}}{\cos delta} \]
    6. Step-by-step derivation
      1. associate-*r*83.2%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\cos \phi_1 \cdot \sin delta\right)} \cdot \sin theta}{\cos delta} \]
      3. associate-*l*83.2%

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

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

    if -1.4800000000000001e-5 < delta < 2.15e15

    1. Initial program 99.5%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. associate-*l*99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. cancel-sign-sub-inv99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
      3. cancel-sign-sub99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta - \left(-\left(-\sin \phi_1\right)\right) \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)}} \]
      4. remove-double-neg99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\sin \phi_1} \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      5. fma-def99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \color{blue}{\left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      6. associate-*l*99.6%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)\right)}} \]
    4. Step-by-step derivation
      1. sin-asin99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sin \phi_1 \cdot \color{blue}{\mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
      2. add-sqr-sqrt45.5%

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

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \sqrt{\color{blue}{\left(-\sin \phi_1\right) \cdot \left(-\sin \phi_1\right)}} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
      5. sqrt-unprod47.8%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\left(\sqrt{-\sin \phi_1} \cdot \sqrt{-\sin \phi_1}\right)} \cdot \mathsf{fma}\left(\sin \phi_1, \cos delta, \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)} \]
      6. add-sqr-sqrt89.7%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \color{blue}{\left(\sin \phi_1 \cdot \cos delta + \cos \phi_1 \cdot \left(\sin delta \cdot \cos theta\right)\right)}} \]
      8. associate-*r*89.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \color{blue}{\left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta}\right)} \]
      9. expm1-log1p-u89.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\left(-\sin \phi_1\right) \cdot \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)\right)}} \]
    5. Applied egg-rr99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\cos delta - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sin \phi_1 \cdot \mathsf{fma}\left(\cos delta, \sin \phi_1, \cos theta \cdot \left(\sin delta \cdot \cos \phi_1\right)\right)\right)\right)}} \]
    6. Taylor expanded in delta around 0 98.0%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{1 - {\sin \phi_1}^{2}}} \]
    7. Step-by-step derivation
      1. unpow298.0%

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

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

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(\sin delta \cdot \cos \phi_1\right)}{\color{blue}{{\cos \phi_1}^{2}}} \]
    9. Taylor expanded in delta around 0 97.9%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\cos \phi_1 \cdot \left(delta \cdot \sin theta\right)}}{{\cos \phi_1}^{2}} \]
    10. Step-by-step derivation
      1. associate-*r*98.0%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\cos \phi_1 \cdot delta\right) \cdot \sin theta}}{{\cos \phi_1}^{2}} \]
    11. Simplified98.0%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\cos \phi_1 \cdot delta\right) \cdot \sin theta}}{{\cos \phi_1}^{2}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification90.6%

    \[\leadsto \begin{array}{l} \mathbf{if}\;delta \leq -1.48 \cdot 10^{-5} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \left(delta \cdot \cos \phi_1\right)}{{\cos \phi_1}^{2}}\\ \end{array} \]

Alternative 10?

\[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_1 \cdot \left(\sin theta \cdot \sin delta\right)}{\cos delta} \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    3. sub-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    4. +-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
    5. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
    6. distribute-rgt-neg-in99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
    7. fma-def99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
  4. Taylor expanded in phi1 around 0 86.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
  5. Taylor expanded in delta around inf 86.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\cos \phi_1 \cdot \sin theta\right)}}{\cos delta} \]
  6. Step-by-step derivation
    1. associate-*r*86.6%

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

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\cos \phi_1 \cdot \sin delta\right)} \cdot \sin theta}{\cos delta} \]
    3. associate-*l*86.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\cos \phi_1 \cdot \left(\sin delta \cdot \sin theta\right)}}{\cos delta} \]
  7. Simplified86.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\cos \phi_1 \cdot \left(\sin delta \cdot \sin theta\right)}}{\cos delta} \]
  8. Final simplification86.6%

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

Alternative 11?

\[\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \sin delta}{\cos delta} \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    3. sub-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    4. +-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
    5. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
    6. distribute-rgt-neg-in99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
    7. fma-def99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
  4. Taylor expanded in phi1 around 0 86.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
  5. Taylor expanded in phi1 around 0 83.8%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \color{blue}{\sin theta}}{\cos delta} \]
  6. Final simplification83.8%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot \sin delta}{\cos delta} \]

Alternative 12?

\[\begin{array}{l} \mathbf{if}\;delta \leq -2.3 \cdot 10^{-11} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{theta \cdot \sin delta}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if delta < -2.30000000000000014e-11 or 2.15e15 < delta

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
      5. *-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.6%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 83.3%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in phi1 around 0 79.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \color{blue}{\sin theta}}{\cos delta} \]
    6. Taylor expanded in theta around 0 68.9%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot theta}}{\cos delta} \]

    if -2.30000000000000014e-11 < delta < 2.15e15

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.5%

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

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.5%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.5%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 89.8%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in lambda1 around inf 82.7%

      \[\leadsto \color{blue}{\lambda_1} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification75.8%

    \[\leadsto \begin{array}{l} \mathbf{if}\;delta \leq -2.3 \cdot 10^{-11} \lor \neg \left(delta \leq 2.15 \cdot 10^{+15}\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{theta \cdot \sin delta}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1\\ \end{array} \]

Alternative 13?

\[\begin{array}{l} \mathbf{if}\;delta \leq -1.12 \cdot 10^{+60} \lor \neg \left(delta \leq 270000000000\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{theta \cdot \sin delta}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot delta}{\cos delta}\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if delta < -1.1199999999999999e60 or 2.7e11 < delta

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
      5. *-commutative99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.7%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.6%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 81.8%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in phi1 around 0 78.1%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \color{blue}{\sin theta}}{\cos delta} \]
    6. Taylor expanded in theta around 0 69.2%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot theta}}{\cos delta} \]

    if -1.1199999999999999e60 < delta < 2.7e11

    1. Initial program 99.6%

      \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      2. associate-*l*99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
      3. sub-neg99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
      4. +-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
      5. *-commutative99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
      6. distribute-rgt-neg-in99.6%

        \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
      7. fma-def99.5%

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

      \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
    4. Taylor expanded in phi1 around 0 90.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
    5. Taylor expanded in phi1 around 0 88.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \color{blue}{\sin theta}}{\cos delta} \]
    6. Taylor expanded in delta around 0 87.5%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin theta \cdot delta}}{\cos delta} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification79.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;delta \leq -1.12 \cdot 10^{+60} \lor \neg \left(delta \leq 270000000000\right):\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{theta \cdot \sin delta}{\cos delta}\\ \mathbf{else}:\\ \;\;\;\;\lambda_1 + \tan^{-1}_* \frac{\sin theta \cdot delta}{\cos delta}\\ \end{array} \]

Alternative 14?

\[\lambda_1 \]
Derivation
  1. Initial program 99.6%

    \[\lambda_1 + \tan^{-1}_* \frac{\left(\sin theta \cdot \sin delta\right) \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
  2. Step-by-step derivation
    1. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\left(\sin delta \cdot \sin theta\right)} \cdot \cos \phi_1}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    2. associate-*l*99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\color{blue}{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}}{\cos delta - \sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)} \]
    3. sub-neg99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta + \left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right)}} \]
    4. +-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\left(-\sin \phi_1 \cdot \sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right)\right) + \cos delta}} \]
    5. *-commutative99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\left(-\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \sin \phi_1}\right) + \cos delta} \]
    6. distribute-rgt-neg-in99.6%

      \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\sin \sin^{-1} \left(\sin \phi_1 \cdot \cos delta + \left(\cos \phi_1 \cdot \sin delta\right) \cdot \cos theta\right) \cdot \left(-\sin \phi_1\right)} + \cos delta} \]
    7. fma-def99.6%

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

    \[\leadsto \color{blue}{\lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\mathsf{fma}\left(\sin \sin^{-1} \left(\mathsf{fma}\left(\sin delta, \cos \phi_1 \cdot \cos theta, \cos delta \cdot \sin \phi_1\right)\right), -\sin \phi_1, \cos delta\right)}} \]
  4. Taylor expanded in phi1 around 0 86.6%

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\sin delta \cdot \left(\sin theta \cdot \cos \phi_1\right)}{\color{blue}{\cos delta}} \]
  5. Taylor expanded in lambda1 around inf 70.3%

    \[\leadsto \color{blue}{\lambda_1} \]
  6. Final simplification70.3%

    \[\leadsto \lambda_1 \]

Reproduce

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