Migdal et al, Equation (64)

1. Initial program 99.5%

   \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
2. Step-by-step derivation

   1. distribute-lft-out99.5%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   2. associate-*l/99.6%

      \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

   3. associate-*r/99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

   4. fma-def99.6%

      \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

3. Simplified99.6%

   \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
4. Step-by-step derivation

   1. div-inv99.5%

      \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

   2. add-sqr-sqrt99.5%

      \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

   3. pow299.5%

      \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

   4. fma-def99.5%

      \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

   5. hypot-def99.5%

      \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

   6. pow1/299.5%

      \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

   7. pow-flip99.6%

      \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

   8. metadata-eval99.6%

      \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

5. Applied egg-rr99.6%

   \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

6. Final simplification99.6%

   \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right) \]

1. Split input into 3 regimes

2. if a1 < -6.1999999999999996e247

   1. Initial program 100.0%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out100.0%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/100.0%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/100.0%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def100.0%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified100.0%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv100.0%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt100.0%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow2100.0%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def100.0%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def100.0%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/2100.0%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip100.0%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval100.0%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr100.0%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around inf 100.0%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left({a1}^{2} \cdot \cos th\right)} \]
   7. Step-by-step derivation

      1. unpow2100.0%

         \[\leadsto \sqrt{0.5} \cdot \left(\color{blue}{\left(a1 \cdot a1\right)} \cdot \cos th\right) \]

   8. Simplified100.0%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left(\left(a1 \cdot a1\right) \cdot \cos th\right)} \]

   9. Taylor expanded in th around 0 100.0%

      \[\leadsto \sqrt{0.5} \cdot \left(\left(a1 \cdot a1\right) \cdot \color{blue}{\left(1 + -0.5 \cdot {th}^{2}\right)}\right) \]
   10. Step-by-step derivation

       1. unpow2100.0%

          \[\leadsto \sqrt{0.5} \cdot \left(\left(a1 \cdot a1\right) \cdot \left(1 + -0.5 \cdot \color{blue}{\left(th \cdot th\right)}\right)\right) \]

   11. Simplified100.0%

       \[\leadsto \sqrt{0.5} \cdot \left(\left(a1 \cdot a1\right) \cdot \color{blue}{\left(1 + -0.5 \cdot \left(th \cdot th\right)\right)}\right) \]

   if -6.1999999999999996e247 < a1 < -5.3e-135

   1. Initial program 99.5%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.5%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 72.3%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]
   5. Step-by-step derivation

      1. expm1-log1p-u72.3%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{\sqrt{2}}\right)\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      2. expm1-udef72.3%

         \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{1}{\sqrt{2}}\right)} - 1\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      3. add-sqr-sqrt72.3%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{\sqrt{\frac{1}{\sqrt{2}}} \cdot \sqrt{\frac{1}{\sqrt{2}}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      4. sqrt-unprod72.3%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{\sqrt{\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      5. frac-times72.3%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{\frac{1 \cdot 1}{\sqrt{2} \cdot \sqrt{2}}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      6. metadata-eval72.3%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\frac{\color{blue}{1}}{\sqrt{2} \cdot \sqrt{2}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      7. add-sqr-sqrt72.0%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\frac{1}{\color{blue}{2}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      8. metadata-eval72.0%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{0.5}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   6. Applied egg-rr72.0%

      \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\sqrt{0.5}\right)} - 1\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]
   7. Step-by-step derivation

      1. expm1-def72.0%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{0.5}\right)\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      2. expm1-log1p72.4%

         \[\leadsto \color{blue}{\sqrt{0.5}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   8. Simplified72.4%

      \[\leadsto \color{blue}{\sqrt{0.5}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   if -5.3e-135 < a1

   1. Initial program 99.5%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.5%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.6%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.6%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]

   4. Taylor expanded in a1 around 0 64.1%

      \[\leadsto \color{blue}{\frac{{a2}^{2} \cdot \cos th}{\sqrt{2}}} \]
   5. Step-by-step derivation

      1. unpow264.1%

         \[\leadsto \frac{\color{blue}{\left(a2 \cdot a2\right)} \cdot \cos th}{\sqrt{2}} \]

      2. associate-*l*64.1%

         \[\leadsto \frac{\color{blue}{a2 \cdot \left(a2 \cdot \cos th\right)}}{\sqrt{2}} \]

      3. associate-*r/64.1%

         \[\leadsto \color{blue}{a2 \cdot \frac{a2 \cdot \cos th}{\sqrt{2}}} \]

   6. Simplified64.1%

      \[\leadsto \color{blue}{a2 \cdot \frac{a2 \cdot \cos th}{\sqrt{2}}} \]
3. Recombined 3 regimes into one program.

4. Final simplification68.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a1 \leq -6.2 \cdot 10^{+247}:\\ \;\;\;\;\sqrt{0.5} \cdot \left(\left(a1 \cdot a1\right) \cdot \left(1 + -0.5 \cdot \left(th \cdot th\right)\right)\right)\\ \mathbf{elif}\;a1 \leq -5.3 \cdot 10^{-135}:\\ \;\;\;\;\sqrt{0.5} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)\\ \mathbf{else}:\\ \;\;\;\;a2 \cdot \frac{\cos th \cdot a2}{\sqrt{2}}\\ \end{array} \]

1. Initial program 99.5%

   \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
2. Step-by-step derivation

   1. distribute-lft-out99.5%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

3. Simplified99.5%

   \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]
4. Step-by-step derivation

   1. clear-num99.5%

      \[\leadsto \color{blue}{\frac{1}{\frac{\sqrt{2}}{\cos th}}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   2. associate-/r/99.5%

      \[\leadsto \color{blue}{\left(\frac{1}{\sqrt{2}} \cdot \cos th\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   3. pow1/299.5%

      \[\leadsto \left(\frac{1}{\color{blue}{{2}^{0.5}}} \cdot \cos th\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   4. pow-flip99.6%

      \[\leadsto \left(\color{blue}{{2}^{\left(-0.5\right)}} \cdot \cos th\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. metadata-eval99.6%

      \[\leadsto \left({2}^{\color{blue}{-0.5}} \cdot \cos th\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

5. Applied egg-rr99.6%

   \[\leadsto \color{blue}{\left({2}^{-0.5} \cdot \cos th\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

6. Taylor expanded in th around inf 99.6%

   \[\leadsto \color{blue}{\left(\sqrt{0.5} \cdot \cos th\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

7. Final simplification99.6%

   \[\leadsto \left(\cos th \cdot \sqrt{0.5}\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

1. Split input into 2 regimes

2. if a2 < 5.20000000000000005e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.7%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.6%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.6%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.6%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.6%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around inf 70.7%

      \[\leadsto \cos th \cdot \color{blue}{\left(\sqrt{0.5} \cdot {a1}^{2}\right)} \]
   7. Step-by-step derivation

      1. unpow270.7%

         \[\leadsto \cos th \cdot \left(\sqrt{0.5} \cdot \color{blue}{\left(a1 \cdot a1\right)}\right) \]

   8. Simplified70.7%

      \[\leadsto \cos th \cdot \color{blue}{\left(\sqrt{0.5} \cdot \left(a1 \cdot a1\right)\right)} \]

   if 5.20000000000000005e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.5%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.5%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.5%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.5%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]

   4. Taylor expanded in a1 around 0 71.2%

      \[\leadsto \color{blue}{\frac{{a2}^{2} \cdot \cos th}{\sqrt{2}}} \]
   5. Step-by-step derivation

      1. unpow271.2%

         \[\leadsto \frac{\color{blue}{\left(a2 \cdot a2\right)} \cdot \cos th}{\sqrt{2}} \]

      2. associate-*l*71.3%

         \[\leadsto \frac{\color{blue}{a2 \cdot \left(a2 \cdot \cos th\right)}}{\sqrt{2}} \]

      3. associate-*r/71.3%

         \[\leadsto \color{blue}{a2 \cdot \frac{a2 \cdot \cos th}{\sqrt{2}}} \]

   6. Simplified71.3%

      \[\leadsto \color{blue}{a2 \cdot \frac{a2 \cdot \cos th}{\sqrt{2}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 5.2 \cdot 10^{-104}:\\ \;\;\;\;\cos th \cdot \left(\sqrt{0.5} \cdot \left(a1 \cdot a1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;a2 \cdot \frac{\cos th \cdot a2}{\sqrt{2}}\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 5.20000000000000005e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.7%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.6%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.6%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.6%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.6%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around inf 70.7%

      \[\leadsto \cos th \cdot \color{blue}{\left(\sqrt{0.5} \cdot {a1}^{2}\right)} \]
   7. Step-by-step derivation

      1. unpow270.7%

         \[\leadsto \cos th \cdot \left(\sqrt{0.5} \cdot \color{blue}{\left(a1 \cdot a1\right)}\right) \]

   8. Simplified70.7%

      \[\leadsto \cos th \cdot \color{blue}{\left(\sqrt{0.5} \cdot \left(a1 \cdot a1\right)\right)} \]

   if 5.20000000000000005e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.5%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.5%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.5%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.5%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]

   4. Taylor expanded in a1 around 0 71.3%

      \[\leadsto \cos th \cdot \color{blue}{\frac{{a2}^{2}}{\sqrt{2}}} \]
   5. Step-by-step derivation

      1. unpow271.3%

         \[\leadsto \cos th \cdot \frac{\color{blue}{a2 \cdot a2}}{\sqrt{2}} \]

      2. associate-/l*71.3%

         \[\leadsto \cos th \cdot \color{blue}{\frac{a2}{\frac{\sqrt{2}}{a2}}} \]

   6. Simplified71.3%

      \[\leadsto \cos th \cdot \color{blue}{\frac{a2}{\frac{\sqrt{2}}{a2}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 5.2 \cdot 10^{-104}:\\ \;\;\;\;\cos th \cdot \left(\sqrt{0.5} \cdot \left(a1 \cdot a1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\cos th \cdot \frac{a2}{\frac{\sqrt{2}}{a2}}\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 4.3000000000000001e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.7%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.6%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.6%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.6%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.6%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around inf 70.7%

      \[\leadsto \cos th \cdot \color{blue}{\left(\sqrt{0.5} \cdot {a1}^{2}\right)} \]
   7. Step-by-step derivation

      1. unpow270.7%

         \[\leadsto \cos th \cdot \left(\sqrt{0.5} \cdot \color{blue}{\left(a1 \cdot a1\right)}\right) \]

   8. Simplified70.7%

      \[\leadsto \cos th \cdot \color{blue}{\left(\sqrt{0.5} \cdot \left(a1 \cdot a1\right)\right)} \]

   if 4.3000000000000001e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.5%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.5%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.5%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.5%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.4%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.4%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.4%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.4%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.7%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around 0 71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left({a2}^{2} \cdot \cos th\right)} \]
   7. Step-by-step derivation

      1. unpow271.4%

         \[\leadsto \sqrt{0.5} \cdot \left(\color{blue}{\left(a2 \cdot a2\right)} \cdot \cos th\right) \]

   8. Simplified71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left(\left(a2 \cdot a2\right) \cdot \cos th\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 4.3 \cdot 10^{-104}:\\ \;\;\;\;\cos th \cdot \left(\sqrt{0.5} \cdot \left(a1 \cdot a1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5} \cdot \left(\cos th \cdot \left(a2 \cdot a2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 4.8000000000000001e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]
   4. Step-by-step derivation

      1. clear-num99.6%

         \[\leadsto \color{blue}{\frac{1}{\frac{\sqrt{2}}{\cos th}}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      2. associate-/r/99.6%

         \[\leadsto \color{blue}{\left(\frac{1}{\sqrt{2}} \cdot \cos th\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      3. pow1/299.6%

         \[\leadsto \left(\frac{1}{\color{blue}{{2}^{0.5}}} \cdot \cos th\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      4. pow-flip99.6%

         \[\leadsto \left(\color{blue}{{2}^{\left(-0.5\right)}} \cdot \cos th\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

      5. metadata-eval99.6%

         \[\leadsto \left({2}^{\color{blue}{-0.5}} \cdot \cos th\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Applied egg-rr99.6%

      \[\leadsto \color{blue}{\left({2}^{-0.5} \cdot \cos th\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   6. Taylor expanded in th around inf 99.6%

      \[\leadsto \color{blue}{\left(\sqrt{0.5} \cdot \cos th\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   7. Taylor expanded in a1 around inf 70.7%

      \[\leadsto \left(\sqrt{0.5} \cdot \cos th\right) \cdot \color{blue}{{a1}^{2}} \]
   8. Step-by-step derivation

      1. unpow253.0%

         \[\leadsto \frac{1}{\sqrt{2}} \cdot \color{blue}{\left(a1 \cdot a1\right)} \]

   9. Simplified70.7%

      \[\leadsto \left(\sqrt{0.5} \cdot \cos th\right) \cdot \color{blue}{\left(a1 \cdot a1\right)} \]

   if 4.8000000000000001e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.5%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.5%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.5%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.5%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.4%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.4%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.4%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.4%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.7%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around 0 71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left({a2}^{2} \cdot \cos th\right)} \]
   7. Step-by-step derivation

      1. unpow271.4%

         \[\leadsto \sqrt{0.5} \cdot \left(\color{blue}{\left(a2 \cdot a2\right)} \cdot \cos th\right) \]

   8. Simplified71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left(\left(a2 \cdot a2\right) \cdot \cos th\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 4.8 \cdot 10^{-104}:\\ \;\;\;\;\left(\cos th \cdot \sqrt{0.5}\right) \cdot \left(a1 \cdot a1\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5} \cdot \left(\cos th \cdot \left(a2 \cdot a2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 8.59999999999999928e-105

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.7%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.6%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]

   4. Taylor expanded in a1 around inf 70.7%

      \[\leadsto \color{blue}{\frac{{a1}^{2} \cdot \cos th}{\sqrt{2}}} \]
   5. Step-by-step derivation

      1. unpow270.7%

         \[\leadsto \frac{\color{blue}{\left(a1 \cdot a1\right)} \cdot \cos th}{\sqrt{2}} \]

      2. *-commutative70.7%

         \[\leadsto \frac{\color{blue}{\cos th \cdot \left(a1 \cdot a1\right)}}{\sqrt{2}} \]

      3. associate-*l/70.7%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right)} \]

   6. Simplified70.7%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right)} \]

   if 8.59999999999999928e-105 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.5%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.5%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.5%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.5%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.4%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.4%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.4%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.4%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.7%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around 0 71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left({a2}^{2} \cdot \cos th\right)} \]
   7. Step-by-step derivation

      1. unpow271.4%

         \[\leadsto \sqrt{0.5} \cdot \left(\color{blue}{\left(a2 \cdot a2\right)} \cdot \cos th\right) \]

   8. Simplified71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left(\left(a2 \cdot a2\right) \cdot \cos th\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 8.6 \cdot 10^{-105}:\\ \;\;\;\;\left(a1 \cdot a1\right) \cdot \frac{\cos th}{\sqrt{2}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5} \cdot \left(\cos th \cdot \left(a2 \cdot a2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 5.20000000000000005e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.7%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.6%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]

   4. Taylor expanded in a1 around inf 70.7%

      \[\leadsto \color{blue}{\frac{{a1}^{2} \cdot \cos th}{\sqrt{2}}} \]
   5. Step-by-step derivation

      1. unpow270.7%

         \[\leadsto \frac{\color{blue}{\left(a1 \cdot a1\right)} \cdot \cos th}{\sqrt{2}} \]

      2. *-commutative70.7%

         \[\leadsto \frac{\color{blue}{\cos th \cdot \left(a1 \cdot a1\right)}}{\sqrt{2}} \]

   6. Simplified70.7%

      \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1\right)}{\sqrt{2}}} \]

   if 5.20000000000000005e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.5%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.5%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.5%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.5%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.4%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.4%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.4%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.4%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.4%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.7%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.7%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around 0 71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left({a2}^{2} \cdot \cos th\right)} \]
   7. Step-by-step derivation

      1. unpow271.4%

         \[\leadsto \sqrt{0.5} \cdot \left(\color{blue}{\left(a2 \cdot a2\right)} \cdot \cos th\right) \]

   8. Simplified71.4%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left(\left(a2 \cdot a2\right) \cdot \cos th\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 5.2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\cos th \cdot \left(a1 \cdot a1\right)}{\sqrt{2}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5} \cdot \left(\cos th \cdot \left(a2 \cdot a2\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 3.19999999999999989e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 73.4%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Taylor expanded in a1 around inf 53.0%

      \[\leadsto \frac{1}{\sqrt{2}} \cdot \color{blue}{{a1}^{2}} \]
   6. Step-by-step derivation

      1. unpow253.0%

         \[\leadsto \frac{1}{\sqrt{2}} \cdot \color{blue}{\left(a1 \cdot a1\right)} \]

   7. Simplified53.0%

      \[\leadsto \frac{1}{\sqrt{2}} \cdot \color{blue}{\left(a1 \cdot a1\right)} \]

   8. Taylor expanded in a1 around 0 53.1%

      \[\leadsto \color{blue}{\frac{{a1}^{2}}{\sqrt{2}}} \]
   9. Step-by-step derivation

      1. unpow253.1%

         \[\leadsto \frac{\color{blue}{a1 \cdot a1}}{\sqrt{2}} \]

   10. Simplified53.1%

       \[\leadsto \color{blue}{\frac{a1 \cdot a1}{\sqrt{2}}} \]

   if 3.19999999999999989e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 65.4%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Taylor expanded in a1 around 0 47.7%

      \[\leadsto \color{blue}{\frac{{a2}^{2}}{\sqrt{2}}} \]
   6. Step-by-step derivation

      1. unpow247.7%

         \[\leadsto \frac{\color{blue}{a2 \cdot a2}}{\sqrt{2}} \]

      2. associate-*r/47.8%

         \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]

   7. Simplified47.8%

      \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]
   8. Step-by-step derivation

      1. add-sqr-sqrt47.7%

         \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{\frac{a2}{\sqrt{2}}} \cdot \sqrt{\frac{a2}{\sqrt{2}}}\right)} \]

      2. sqrt-unprod47.8%

         \[\leadsto a2 \cdot \color{blue}{\sqrt{\frac{a2}{\sqrt{2}} \cdot \frac{a2}{\sqrt{2}}}} \]

      3. div-inv47.8%

         \[\leadsto a2 \cdot \sqrt{\color{blue}{\left(a2 \cdot \frac{1}{\sqrt{2}}\right)} \cdot \frac{a2}{\sqrt{2}}} \]

      4. div-inv47.7%

         \[\leadsto a2 \cdot \sqrt{\left(a2 \cdot \frac{1}{\sqrt{2}}\right) \cdot \color{blue}{\left(a2 \cdot \frac{1}{\sqrt{2}}\right)}} \]

      5. swap-sqr47.7%

         \[\leadsto a2 \cdot \sqrt{\color{blue}{\left(a2 \cdot a2\right) \cdot \left(\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}}\right)}} \]

      6. frac-times47.7%

         \[\leadsto a2 \cdot \sqrt{\left(a2 \cdot a2\right) \cdot \color{blue}{\frac{1 \cdot 1}{\sqrt{2} \cdot \sqrt{2}}}} \]

      7. metadata-eval47.7%

         \[\leadsto a2 \cdot \sqrt{\left(a2 \cdot a2\right) \cdot \frac{\color{blue}{1}}{\sqrt{2} \cdot \sqrt{2}}} \]

      8. add-sqr-sqrt48.0%

         \[\leadsto a2 \cdot \sqrt{\left(a2 \cdot a2\right) \cdot \frac{1}{\color{blue}{2}}} \]

      9. metadata-eval48.0%

         \[\leadsto a2 \cdot \sqrt{\left(a2 \cdot a2\right) \cdot \color{blue}{0.5}} \]

   9. Applied egg-rr48.0%

      \[\leadsto a2 \cdot \color{blue}{\sqrt{\left(a2 \cdot a2\right) \cdot 0.5}} \]
3. Recombined 2 regimes into one program.

4. Final simplification51.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 3.2 \cdot 10^{-104}:\\ \;\;\;\;\frac{a1 \cdot a1}{\sqrt{2}}\\ \mathbf{else}:\\ \;\;\;\;a2 \cdot \sqrt{0.5 \cdot \left(a2 \cdot a2\right)}\\ \end{array} \]

1. Initial program 99.5%

   \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
2. Step-by-step derivation

   1. distribute-lft-out99.5%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

3. Simplified99.5%

   \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

4. Taylor expanded in th around 0 70.8%

   \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]
5. Step-by-step derivation

   1. expm1-log1p-u70.8%

      \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{\sqrt{2}}\right)\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   2. expm1-udef70.8%

      \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{1}{\sqrt{2}}\right)} - 1\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   3. add-sqr-sqrt70.8%

      \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{\sqrt{\frac{1}{\sqrt{2}}} \cdot \sqrt{\frac{1}{\sqrt{2}}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   4. sqrt-unprod70.8%

      \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{\sqrt{\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. frac-times70.8%

      \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{\frac{1 \cdot 1}{\sqrt{2} \cdot \sqrt{2}}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   6. metadata-eval70.8%

      \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\frac{\color{blue}{1}}{\sqrt{2} \cdot \sqrt{2}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   7. add-sqr-sqrt70.5%

      \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\frac{1}{\color{blue}{2}}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   8. metadata-eval70.5%

      \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{0.5}}\right)} - 1\right) \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

6. Applied egg-rr70.5%

   \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\sqrt{0.5}\right)} - 1\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]
7. Step-by-step derivation

   1. expm1-def70.5%

      \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{0.5}\right)\right)} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   2. expm1-log1p70.8%

      \[\leadsto \color{blue}{\sqrt{0.5}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

8. Simplified70.8%

   \[\leadsto \color{blue}{\sqrt{0.5}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

9. Final simplification70.8%

   \[\leadsto \sqrt{0.5} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

1. Split input into 2 regimes

2. if a2 < 4.9000000000000003e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

      2. associate-*l/99.7%

         \[\leadsto \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}} \]

      3. associate-*r/99.6%

         \[\leadsto \color{blue}{\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}} \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \frac{\color{blue}{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}}{\sqrt{2}} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\cos th \cdot \frac{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}{\sqrt{2}}} \]
   4. Step-by-step derivation

      1. div-inv99.6%

         \[\leadsto \cos th \cdot \color{blue}{\left(\mathsf{fma}\left(a1, a1, a2 \cdot a2\right) \cdot \frac{1}{\sqrt{2}}\right)} \]

      2. add-sqr-sqrt99.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)} \cdot \sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)} \cdot \frac{1}{\sqrt{2}}\right) \]

      3. pow299.6%

         \[\leadsto \cos th \cdot \left(\color{blue}{{\left(\sqrt{\mathsf{fma}\left(a1, a1, a2 \cdot a2\right)}\right)}^{2}} \cdot \frac{1}{\sqrt{2}}\right) \]

      4. fma-def99.6%

         \[\leadsto \cos th \cdot \left({\left(\sqrt{\color{blue}{a1 \cdot a1 + a2 \cdot a2}}\right)}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      5. hypot-def99.6%

         \[\leadsto \cos th \cdot \left({\color{blue}{\left(\mathsf{hypot}\left(a1, a2\right)\right)}}^{2} \cdot \frac{1}{\sqrt{2}}\right) \]

      6. pow1/299.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \frac{1}{\color{blue}{{2}^{0.5}}}\right) \]

      7. pow-flip99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot \color{blue}{{2}^{\left(-0.5\right)}}\right) \]

      8. metadata-eval99.6%

         \[\leadsto \cos th \cdot \left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{\color{blue}{-0.5}}\right) \]

   5. Applied egg-rr99.6%

      \[\leadsto \cos th \cdot \color{blue}{\left({\left(\mathsf{hypot}\left(a1, a2\right)\right)}^{2} \cdot {2}^{-0.5}\right)} \]

   6. Taylor expanded in a1 around inf 70.7%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left({a1}^{2} \cdot \cos th\right)} \]
   7. Step-by-step derivation

      1. unpow270.7%

         \[\leadsto \sqrt{0.5} \cdot \left(\color{blue}{\left(a1 \cdot a1\right)} \cdot \cos th\right) \]

   8. Simplified70.7%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left(\left(a1 \cdot a1\right) \cdot \cos th\right)} \]

   9. Taylor expanded in th around 0 53.0%

      \[\leadsto \color{blue}{\sqrt{0.5} \cdot {a1}^{2}} \]
   10. Step-by-step derivation

       1. unpow253.0%

          \[\leadsto \sqrt{0.5} \cdot \color{blue}{\left(a1 \cdot a1\right)} \]

   11. Simplified53.0%

       \[\leadsto \color{blue}{\sqrt{0.5} \cdot \left(a1 \cdot a1\right)} \]

   if 4.9000000000000003e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 65.4%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Taylor expanded in a1 around 0 47.7%

      \[\leadsto \color{blue}{\frac{{a2}^{2}}{\sqrt{2}}} \]
   6. Step-by-step derivation

      1. unpow247.7%

         \[\leadsto \frac{\color{blue}{a2 \cdot a2}}{\sqrt{2}} \]

      2. associate-*r/47.8%

         \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]

   7. Simplified47.8%

      \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]
   8. Step-by-step derivation

      1. expm1-log1p-u46.7%

         \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)\right)} \]

      2. expm1-udef39.8%

         \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)} - 1\right)} \]

      3. div-inv39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(\color{blue}{a2 \cdot \frac{1}{\sqrt{2}}}\right)} - 1\right) \]

      4. add-sqr-sqrt39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\left(\sqrt{\frac{1}{\sqrt{2}}} \cdot \sqrt{\frac{1}{\sqrt{2}}}\right)}\right)} - 1\right) \]

      5. sqrt-unprod39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\sqrt{\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}}}}\right)} - 1\right) \]

      6. frac-times39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{\frac{1 \cdot 1}{\sqrt{2} \cdot \sqrt{2}}}}\right)} - 1\right) \]

      7. metadata-eval39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{\color{blue}{1}}{\sqrt{2} \cdot \sqrt{2}}}\right)} - 1\right) \]

      8. add-sqr-sqrt39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{1}{\color{blue}{2}}}\right)} - 1\right) \]

      9. metadata-eval39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{0.5}}\right)} - 1\right) \]

   9. Applied egg-rr39.8%

      \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)} - 1\right)} \]
   10. Step-by-step derivation

       1. expm1-def46.7%

          \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)\right)} \]

       2. expm1-log1p47.9%

          \[\leadsto a2 \cdot \color{blue}{\left(a2 \cdot \sqrt{0.5}\right)} \]

       3. *-commutative47.9%

          \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]

   11. Simplified47.9%

       \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification51.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 4.9 \cdot 10^{-104}:\\ \;\;\;\;\sqrt{0.5} \cdot \left(a1 \cdot a1\right)\\ \mathbf{else}:\\ \;\;\;\;a2 \cdot \left(a2 \cdot \sqrt{0.5}\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 5.20000000000000005e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 73.4%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Taylor expanded in a1 around inf 53.1%

      \[\leadsto \color{blue}{\frac{{a1}^{2}}{\sqrt{2}}} \]
   6. Step-by-step derivation

      1. unpow253.1%

         \[\leadsto \frac{\color{blue}{a1 \cdot a1}}{\sqrt{2}} \]

      2. associate-/l*53.0%

         \[\leadsto \color{blue}{\frac{a1}{\frac{\sqrt{2}}{a1}}} \]

   7. Simplified53.0%

      \[\leadsto \color{blue}{\frac{a1}{\frac{\sqrt{2}}{a1}}} \]

   if 5.20000000000000005e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 65.4%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Taylor expanded in a1 around 0 47.7%

      \[\leadsto \color{blue}{\frac{{a2}^{2}}{\sqrt{2}}} \]
   6. Step-by-step derivation

      1. unpow247.7%

         \[\leadsto \frac{\color{blue}{a2 \cdot a2}}{\sqrt{2}} \]

      2. associate-*r/47.8%

         \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]

   7. Simplified47.8%

      \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]
   8. Step-by-step derivation

      1. expm1-log1p-u46.7%

         \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)\right)} \]

      2. expm1-udef39.8%

         \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)} - 1\right)} \]

      3. div-inv39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(\color{blue}{a2 \cdot \frac{1}{\sqrt{2}}}\right)} - 1\right) \]

      4. add-sqr-sqrt39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\left(\sqrt{\frac{1}{\sqrt{2}}} \cdot \sqrt{\frac{1}{\sqrt{2}}}\right)}\right)} - 1\right) \]

      5. sqrt-unprod39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\sqrt{\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}}}}\right)} - 1\right) \]

      6. frac-times39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{\frac{1 \cdot 1}{\sqrt{2} \cdot \sqrt{2}}}}\right)} - 1\right) \]

      7. metadata-eval39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{\color{blue}{1}}{\sqrt{2} \cdot \sqrt{2}}}\right)} - 1\right) \]

      8. add-sqr-sqrt39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{1}{\color{blue}{2}}}\right)} - 1\right) \]

      9. metadata-eval39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{0.5}}\right)} - 1\right) \]

   9. Applied egg-rr39.8%

      \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)} - 1\right)} \]
   10. Step-by-step derivation

       1. expm1-def46.7%

          \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)\right)} \]

       2. expm1-log1p47.9%

          \[\leadsto a2 \cdot \color{blue}{\left(a2 \cdot \sqrt{0.5}\right)} \]

       3. *-commutative47.9%

          \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]

   11. Simplified47.9%

       \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification51.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 5.2 \cdot 10^{-104}:\\ \;\;\;\;\frac{a1}{\frac{\sqrt{2}}{a1}}\\ \mathbf{else}:\\ \;\;\;\;a2 \cdot \left(a2 \cdot \sqrt{0.5}\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if a2 < 5.20000000000000005e-104

   1. Initial program 99.6%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.6%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 73.4%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Taylor expanded in a1 around inf 53.0%

      \[\leadsto \frac{1}{\sqrt{2}} \cdot \color{blue}{{a1}^{2}} \]
   6. Step-by-step derivation

      1. unpow253.0%

         \[\leadsto \frac{1}{\sqrt{2}} \cdot \color{blue}{\left(a1 \cdot a1\right)} \]

   7. Simplified53.0%

      \[\leadsto \frac{1}{\sqrt{2}} \cdot \color{blue}{\left(a1 \cdot a1\right)} \]

   8. Taylor expanded in a1 around 0 53.1%

      \[\leadsto \color{blue}{\frac{{a1}^{2}}{\sqrt{2}}} \]
   9. Step-by-step derivation

      1. unpow253.1%

         \[\leadsto \frac{\color{blue}{a1 \cdot a1}}{\sqrt{2}} \]

   10. Simplified53.1%

       \[\leadsto \color{blue}{\frac{a1 \cdot a1}{\sqrt{2}}} \]

   if 5.20000000000000005e-104 < a2

   1. Initial program 99.4%

      \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
   2. Step-by-step derivation

      1. distribute-lft-out99.4%

         \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

   4. Taylor expanded in th around 0 65.4%

      \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

   5. Taylor expanded in a1 around 0 47.7%

      \[\leadsto \color{blue}{\frac{{a2}^{2}}{\sqrt{2}}} \]
   6. Step-by-step derivation

      1. unpow247.7%

         \[\leadsto \frac{\color{blue}{a2 \cdot a2}}{\sqrt{2}} \]

      2. associate-*r/47.8%

         \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]

   7. Simplified47.8%

      \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]
   8. Step-by-step derivation

      1. expm1-log1p-u46.7%

         \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)\right)} \]

      2. expm1-udef39.8%

         \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)} - 1\right)} \]

      3. div-inv39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(\color{blue}{a2 \cdot \frac{1}{\sqrt{2}}}\right)} - 1\right) \]

      4. add-sqr-sqrt39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\left(\sqrt{\frac{1}{\sqrt{2}}} \cdot \sqrt{\frac{1}{\sqrt{2}}}\right)}\right)} - 1\right) \]

      5. sqrt-unprod39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\sqrt{\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}}}}\right)} - 1\right) \]

      6. frac-times39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{\frac{1 \cdot 1}{\sqrt{2} \cdot \sqrt{2}}}}\right)} - 1\right) \]

      7. metadata-eval39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{\color{blue}{1}}{\sqrt{2} \cdot \sqrt{2}}}\right)} - 1\right) \]

      8. add-sqr-sqrt39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{1}{\color{blue}{2}}}\right)} - 1\right) \]

      9. metadata-eval39.8%

         \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{0.5}}\right)} - 1\right) \]

   9. Applied egg-rr39.8%

      \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)} - 1\right)} \]
   10. Step-by-step derivation

       1. expm1-def46.7%

          \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)\right)} \]

       2. expm1-log1p47.9%

          \[\leadsto a2 \cdot \color{blue}{\left(a2 \cdot \sqrt{0.5}\right)} \]

       3. *-commutative47.9%

          \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]

   11. Simplified47.9%

       \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification51.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a2 \leq 5.2 \cdot 10^{-104}:\\ \;\;\;\;\frac{a1 \cdot a1}{\sqrt{2}}\\ \mathbf{else}:\\ \;\;\;\;a2 \cdot \left(a2 \cdot \sqrt{0.5}\right)\\ \end{array} \]

1. Initial program 99.5%

   \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right) \]
2. Step-by-step derivation

   1. distribute-lft-out99.5%

      \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

3. Simplified99.5%

   \[\leadsto \color{blue}{\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)} \]

4. Taylor expanded in th around 0 70.8%

   \[\leadsto \frac{\color{blue}{1}}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right) \]

5. Taylor expanded in a1 around 0 40.6%

   \[\leadsto \color{blue}{\frac{{a2}^{2}}{\sqrt{2}}} \]
6. Step-by-step derivation

   1. unpow240.6%

      \[\leadsto \frac{\color{blue}{a2 \cdot a2}}{\sqrt{2}} \]

   2. associate-*r/40.6%

      \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]

7. Simplified40.6%

   \[\leadsto \color{blue}{a2 \cdot \frac{a2}{\sqrt{2}}} \]
8. Step-by-step derivation

   1. expm1-log1p-u26.5%

      \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)\right)} \]

   2. expm1-udef22.0%

      \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{a2}{\sqrt{2}}\right)} - 1\right)} \]

   3. div-inv22.0%

      \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(\color{blue}{a2 \cdot \frac{1}{\sqrt{2}}}\right)} - 1\right) \]

   4. add-sqr-sqrt22.0%

      \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\left(\sqrt{\frac{1}{\sqrt{2}}} \cdot \sqrt{\frac{1}{\sqrt{2}}}\right)}\right)} - 1\right) \]

   5. sqrt-unprod22.0%

      \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \color{blue}{\sqrt{\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}}}}\right)} - 1\right) \]

   6. frac-times22.0%

      \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{\frac{1 \cdot 1}{\sqrt{2} \cdot \sqrt{2}}}}\right)} - 1\right) \]

   7. metadata-eval22.0%

      \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{\color{blue}{1}}{\sqrt{2} \cdot \sqrt{2}}}\right)} - 1\right) \]

   8. add-sqr-sqrt22.0%

      \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\frac{1}{\color{blue}{2}}}\right)} - 1\right) \]

   9. metadata-eval22.0%

      \[\leadsto a2 \cdot \left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{\color{blue}{0.5}}\right)} - 1\right) \]

9. Applied egg-rr22.0%

   \[\leadsto a2 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)} - 1\right)} \]
10. Step-by-step derivation

    1. expm1-def26.5%

       \[\leadsto a2 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(a2 \cdot \sqrt{0.5}\right)\right)} \]

    2. expm1-log1p40.6%

       \[\leadsto a2 \cdot \color{blue}{\left(a2 \cdot \sqrt{0.5}\right)} \]

    3. *-commutative40.6%

       \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]

11. Simplified40.6%

    \[\leadsto a2 \cdot \color{blue}{\left(\sqrt{0.5} \cdot a2\right)} \]

12. Final simplification40.6%

    \[\leadsto a2 \cdot \left(a2 \cdot \sqrt{0.5}\right) \]

herbie shell --seed 2023166 
(FPCore (a1 a2 th)
  :name "Migdal et al, Equation (64)"
  :precision binary64
  (+ (* (/ (cos th) (sqrt 2.0)) (* a1 a1)) (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))