Migdal et al, Equation (51)

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. div-sub99.5%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\color{blue}{\left(\frac{1}{2} - \frac{k}{2}\right)}} \]

   2. metadata-eval99.5%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\color{blue}{0.5} - \frac{k}{2}\right)} \]

   3. pow-sub99.7%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{\frac{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{0.5}}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{k}{2}\right)}}} \]

   4. pow1/299.7%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \frac{\color{blue}{\sqrt{\left(2 \cdot \pi\right) \cdot n}}}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{k}{2}\right)}} \]

   5. associate-*l*99.7%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \frac{\sqrt{\color{blue}{2 \cdot \left(\pi \cdot n\right)}}}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{k}{2}\right)}} \]

   6. associate-*l*99.7%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{{\color{blue}{\left(2 \cdot \left(\pi \cdot n\right)\right)}}^{\left(\frac{k}{2}\right)}} \]

   7. div-inv99.7%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\color{blue}{\left(k \cdot \frac{1}{2}\right)}}} \]

   8. metadata-eval99.7%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(k \cdot \color{blue}{0.5}\right)}} \]

3. Applied egg-rr99.7%

   \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{\frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(k \cdot 0.5\right)}}} \]

4. Final simplification99.7%

   \[\leadsto \frac{1}{\sqrt{k}} \cdot \frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(k \cdot 0.5\right)}} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. expm1-log1p-u96.1%

      \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{\sqrt{k}}\right)\right)} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   2. expm1-udef77.0%

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

   3. inv-pow77.0%

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

   4. sqrt-pow277.0%

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

   5. metadata-eval77.0%

      \[\leadsto \left(e^{\mathsf{log1p}\left({k}^{\color{blue}{-0.5}}\right)} - 1\right) \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

3. Applied egg-rr77.0%

   \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left({k}^{-0.5}\right)} - 1\right)} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left({k}^{-0.5}\right)\right)} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   2. expm1-log1p99.5%

      \[\leadsto \color{blue}{{k}^{-0.5}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

5. Simplified99.5%

   \[\leadsto \color{blue}{{k}^{-0.5}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

6. Final simplification99.5%

   \[\leadsto {k}^{-0.5} \cdot {\left(n \cdot \left(2 \cdot \pi\right)\right)}^{\left(\frac{1 - k}{2}\right)} \]

1. Split input into 2 regimes

2. if k < 7.0000000000000001e-67

   1. Initial program 99.3%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Step-by-step derivation

      1. *-commutative99.3%

         \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

      2. *-commutative99.3%

         \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      3. associate-*r*99.3%

         \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      4. div-inv99.4%

         \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

      5. add-sqr-sqrt99.0%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      6. sqrt-unprod63.2%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      7. frac-times63.1%

         \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

   3. Applied egg-rr63.3%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

   4. Taylor expanded in k around 0 63.3%

      \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
   5. Step-by-step derivation

      1. associate-*r*63.3%

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

      2. *-commutative63.3%

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

      3. *-commutative63.3%

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

   6. Simplified63.3%

      \[\leadsto \sqrt{\frac{\color{blue}{\pi \cdot \left(n \cdot 2\right)}}{k}} \]
   7. Step-by-step derivation

      1. sqrt-div99.4%

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

      2. pow1/299.4%

         \[\leadsto \frac{\color{blue}{{\left(\pi \cdot \left(n \cdot 2\right)\right)}^{0.5}}}{\sqrt{k}} \]

      3. associate-*r*99.4%

         \[\leadsto \frac{{\color{blue}{\left(\left(\pi \cdot n\right) \cdot 2\right)}}^{0.5}}{\sqrt{k}} \]

      4. *-commutative99.4%

         \[\leadsto \frac{{\left(\color{blue}{\left(n \cdot \pi\right)} \cdot 2\right)}^{0.5}}{\sqrt{k}} \]

      5. pow-prod-down99.2%

         \[\leadsto \frac{\color{blue}{{\left(n \cdot \pi\right)}^{0.5} \cdot {2}^{0.5}}}{\sqrt{k}} \]

      6. pow1/299.2%

         \[\leadsto \frac{\color{blue}{\sqrt{n \cdot \pi}} \cdot {2}^{0.5}}{\sqrt{k}} \]

      7. pow1/299.2%

         \[\leadsto \frac{\sqrt{n \cdot \pi} \cdot \color{blue}{\sqrt{2}}}{\sqrt{k}} \]

      8. *-commutative99.2%

         \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{n \cdot \pi}}}{\sqrt{k}} \]

      9. sqrt-unprod99.4%

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

      10. *-commutative99.4%

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

   8. Applied egg-rr99.4%

      \[\leadsto \color{blue}{\frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{\sqrt{k}}} \]
   9. Step-by-step derivation

      1. *-commutative99.4%

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

      2. associate-*r*99.4%

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

   10. Simplified99.4%

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

   if 7.0000000000000001e-67 < k

   1. Initial program 99.5%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Step-by-step derivation

      1. *-commutative99.5%

         \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

      2. *-commutative99.5%

         \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      3. associate-*r*99.5%

         \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      4. div-inv99.5%

         \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

      5. add-sqr-sqrt99.5%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      6. sqrt-unprod99.5%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      7. frac-times99.5%

         \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

   3. Applied egg-rr99.6%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification99.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;k \leq 7 \cdot 10^{-67}:\\ \;\;\;\;\frac{\sqrt{\pi \cdot \left(2 \cdot n\right)}}{\sqrt{k}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}\\ \end{array} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. associate-*l/99.5%

      \[\leadsto \color{blue}{\frac{1 \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

   2. *-lft-identity99.5%

      \[\leadsto \frac{\color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)}}}{\sqrt{k}} \]

   3. *-commutative99.5%

      \[\leadsto \frac{{\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \]

   4. associate-*l*99.5%

      \[\leadsto \frac{{\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \]

3. Simplified99.5%

   \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

4. Final simplification99.5%

   \[\leadsto \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \]

1. Split input into 2 regimes

2. if k < 5.1e271

   1. Initial program 99.4%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Step-by-step derivation

      1. *-commutative99.4%

         \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

      2. *-commutative99.4%

         \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      3. associate-*r*99.4%

         \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      4. div-inv99.4%

         \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

      5. add-sqr-sqrt99.2%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      6. sqrt-unprod84.7%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      7. frac-times84.7%

         \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

   3. Applied egg-rr84.8%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

   4. Taylor expanded in k around 0 37.9%

      \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
   5. Step-by-step derivation

      1. associate-*r*37.9%

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

      2. *-commutative37.9%

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

      3. *-commutative37.9%

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

   6. Simplified37.9%

      \[\leadsto \sqrt{\frac{\color{blue}{\pi \cdot \left(n \cdot 2\right)}}{k}} \]
   7. Step-by-step derivation

      1. sqrt-div52.6%

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

      2. pow1/252.6%

         \[\leadsto \frac{\color{blue}{{\left(\pi \cdot \left(n \cdot 2\right)\right)}^{0.5}}}{\sqrt{k}} \]

      3. associate-*r*52.6%

         \[\leadsto \frac{{\color{blue}{\left(\left(\pi \cdot n\right) \cdot 2\right)}}^{0.5}}{\sqrt{k}} \]

      4. *-commutative52.6%

         \[\leadsto \frac{{\left(\color{blue}{\left(n \cdot \pi\right)} \cdot 2\right)}^{0.5}}{\sqrt{k}} \]

      5. pow-prod-down52.5%

         \[\leadsto \frac{\color{blue}{{\left(n \cdot \pi\right)}^{0.5} \cdot {2}^{0.5}}}{\sqrt{k}} \]

      6. pow1/252.5%

         \[\leadsto \frac{\color{blue}{\sqrt{n \cdot \pi}} \cdot {2}^{0.5}}{\sqrt{k}} \]

      7. pow1/252.5%

         \[\leadsto \frac{\sqrt{n \cdot \pi} \cdot \color{blue}{\sqrt{2}}}{\sqrt{k}} \]

      8. *-commutative52.5%

         \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{n \cdot \pi}}}{\sqrt{k}} \]

      9. sqrt-unprod52.6%

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

      10. *-commutative52.6%

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

   8. Applied egg-rr52.6%

      \[\leadsto \color{blue}{\frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{\sqrt{k}}} \]
   9. Step-by-step derivation

      1. *-commutative52.6%

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

      2. associate-*r*52.6%

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

   10. Simplified52.6%

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

   if 5.1e271 < k

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Step-by-step derivation

      1. *-commutative100.0%

         \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

      2. *-commutative100.0%

         \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      3. associate-*r*100.0%

         \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      4. div-inv100.0%

         \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

      5. add-sqr-sqrt100.0%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      6. sqrt-unprod100.0%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      7. frac-times100.0%

         \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

   3. Applied egg-rr100.0%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

   4. Taylor expanded in k around 0 3.2%

      \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
   5. Step-by-step derivation

      1. associate-*r*3.2%

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

      2. *-commutative3.2%

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

      3. *-commutative3.2%

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

   6. Simplified3.2%

      \[\leadsto \sqrt{\frac{\color{blue}{\pi \cdot \left(n \cdot 2\right)}}{k}} \]
   7. Step-by-step derivation

      1. add-cbrt-cube35.1%

         \[\leadsto \color{blue}{\sqrt[3]{\left(\sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right) \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}}} \]

      2. pow1/335.1%

         \[\leadsto \color{blue}{{\left(\left(\sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right) \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right)}^{0.3333333333333333}} \]

      3. add-sqr-sqrt35.1%

         \[\leadsto {\left(\color{blue}{\frac{\pi \cdot \left(n \cdot 2\right)}{k}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right)}^{0.3333333333333333} \]

      4. pow135.1%

         \[\leadsto {\left(\color{blue}{{\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{1}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right)}^{0.3333333333333333} \]

      5. pow1/235.1%

         \[\leadsto {\left({\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{1} \cdot \color{blue}{{\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{0.5}}\right)}^{0.3333333333333333} \]

      6. pow-prod-up35.1%

         \[\leadsto {\color{blue}{\left({\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{\left(1 + 0.5\right)}\right)}}^{0.3333333333333333} \]

      7. associate-/l*35.1%

         \[\leadsto {\left({\color{blue}{\left(\frac{\pi}{\frac{k}{n \cdot 2}}\right)}}^{\left(1 + 0.5\right)}\right)}^{0.3333333333333333} \]

      8. *-commutative35.1%

         \[\leadsto {\left({\left(\frac{\pi}{\frac{k}{\color{blue}{2 \cdot n}}}\right)}^{\left(1 + 0.5\right)}\right)}^{0.3333333333333333} \]

      9. metadata-eval35.1%

         \[\leadsto {\left({\left(\frac{\pi}{\frac{k}{2 \cdot n}}\right)}^{\color{blue}{1.5}}\right)}^{0.3333333333333333} \]

   8. Applied egg-rr35.1%

      \[\leadsto \color{blue}{{\left({\left(\frac{\pi}{\frac{k}{2 \cdot n}}\right)}^{1.5}\right)}^{0.3333333333333333}} \]
   9. Step-by-step derivation

      1. unpow1/335.1%

         \[\leadsto \color{blue}{\sqrt[3]{{\left(\frac{\pi}{\frac{k}{2 \cdot n}}\right)}^{1.5}}} \]

      2. associate-/r*35.1%

         \[\leadsto \sqrt[3]{{\left(\frac{\pi}{\color{blue}{\frac{\frac{k}{2}}{n}}}\right)}^{1.5}} \]

   10. Simplified35.1%

       \[\leadsto \color{blue}{\sqrt[3]{{\left(\frac{\pi}{\frac{\frac{k}{2}}{n}}\right)}^{1.5}}} \]

   11. Taylor expanded in k around 0 35.1%

       \[\leadsto \sqrt[3]{\color{blue}{e^{1.5 \cdot \left(-1 \cdot \log k + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}}} \]
   12. Step-by-step derivation

       1. exp-prod35.1%

          \[\leadsto \sqrt[3]{\color{blue}{{\left(e^{1.5}\right)}^{\left(-1 \cdot \log k + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}}} \]

       2. neg-mul-135.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\color{blue}{\left(-\log k\right)} + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}} \]

       3. log-rec35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\color{blue}{\log \left(\frac{1}{k}\right)} + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}} \]

       4. +-commutative35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\color{blue}{\left(\log \left(2 \cdot \left(n \cdot \pi\right)\right) + \log \left(\frac{1}{k}\right)\right)}}} \]

       5. associate-*r*35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\log \color{blue}{\left(\left(2 \cdot n\right) \cdot \pi\right)} + \log \left(\frac{1}{k}\right)\right)}} \]

       6. *-commutative35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\log \color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)} + \log \left(\frac{1}{k}\right)\right)}} \]

       7. log-rec35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\log \left(\pi \cdot \left(2 \cdot n\right)\right) + \color{blue}{\left(-\log k\right)}\right)}} \]

       8. unsub-neg35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\color{blue}{\left(\log \left(\pi \cdot \left(2 \cdot n\right)\right) - \log k\right)}}} \]

       9. log-div35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\color{blue}{\log \left(\frac{\pi \cdot \left(2 \cdot n\right)}{k}\right)}}} \]

       10. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{\color{blue}{\left(2 \cdot n\right) \cdot \pi}}{k}\right)}} \]

       11. associate-*r*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}\right)}} \]

       12. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{2 \cdot \color{blue}{\left(\pi \cdot n\right)}}{k}\right)}} \]

       13. associate-/l*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \color{blue}{\left(\frac{2}{\frac{k}{\pi \cdot n}}\right)}}} \]

       14. associate-/r/35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \color{blue}{\left(\frac{2}{k} \cdot \left(\pi \cdot n\right)\right)}}} \]

       15. metadata-eval35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{\color{blue}{\frac{1}{0.5}}}{k} \cdot \left(\pi \cdot n\right)\right)}} \]

       16. associate-/r*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\color{blue}{\frac{1}{0.5 \cdot k}} \cdot \left(\pi \cdot n\right)\right)}} \]

       17. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{1}{\color{blue}{k \cdot 0.5}} \cdot \left(\pi \cdot n\right)\right)}} \]

       18. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{1}{k \cdot 0.5} \cdot \color{blue}{\left(n \cdot \pi\right)}\right)}} \]

       19. associate-*l*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \color{blue}{\left(\left(\frac{1}{k \cdot 0.5} \cdot n\right) \cdot \pi\right)}}} \]

   13. Simplified35.1%

       \[\leadsto \sqrt[3]{\color{blue}{{\left(\pi \cdot \left(n \cdot \frac{2}{k}\right)\right)}^{1.5}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification51.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;k \leq 5.1 \cdot 10^{+271}:\\ \;\;\;\;\frac{\sqrt{\pi \cdot \left(2 \cdot n\right)}}{\sqrt{k}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{{\left(\pi \cdot \left(n \cdot \frac{2}{k}\right)\right)}^{1.5}}\\ \end{array} \]

1. Split input into 2 regimes

2. if k < 4.4000000000000002e274

   1. Initial program 99.4%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Step-by-step derivation

      1. *-commutative99.4%

         \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

      2. *-commutative99.4%

         \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      3. associate-*r*99.4%

         \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      4. div-inv99.4%

         \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

      5. add-sqr-sqrt99.2%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      6. sqrt-unprod84.7%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      7. frac-times84.7%

         \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

   3. Applied egg-rr84.8%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

   4. Taylor expanded in k around 0 37.9%

      \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
   5. Step-by-step derivation

      1. associate-*r*37.9%

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

      2. *-commutative37.9%

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

      3. *-commutative37.9%

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

   6. Simplified37.9%

      \[\leadsto \sqrt{\frac{\color{blue}{\pi \cdot \left(n \cdot 2\right)}}{k}} \]
   7. Step-by-step derivation

      1. sqrt-div52.6%

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

      2. pow1/252.6%

         \[\leadsto \frac{\color{blue}{{\left(\pi \cdot \left(n \cdot 2\right)\right)}^{0.5}}}{\sqrt{k}} \]

      3. associate-*r*52.6%

         \[\leadsto \frac{{\color{blue}{\left(\left(\pi \cdot n\right) \cdot 2\right)}}^{0.5}}{\sqrt{k}} \]

      4. *-commutative52.6%

         \[\leadsto \frac{{\left(\color{blue}{\left(n \cdot \pi\right)} \cdot 2\right)}^{0.5}}{\sqrt{k}} \]

      5. pow-prod-down52.5%

         \[\leadsto \frac{\color{blue}{{\left(n \cdot \pi\right)}^{0.5} \cdot {2}^{0.5}}}{\sqrt{k}} \]

      6. pow1/252.5%

         \[\leadsto \frac{\color{blue}{\sqrt{n \cdot \pi}} \cdot {2}^{0.5}}{\sqrt{k}} \]

      7. pow1/252.5%

         \[\leadsto \frac{\sqrt{n \cdot \pi} \cdot \color{blue}{\sqrt{2}}}{\sqrt{k}} \]

      8. *-commutative52.5%

         \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{n \cdot \pi}}}{\sqrt{k}} \]

      9. *-un-lft-identity52.5%

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

      10. associate-*l/52.5%

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

      11. pow1/252.5%

          \[\leadsto \frac{1}{\color{blue}{{k}^{0.5}}} \cdot \left(\sqrt{2} \cdot \sqrt{n \cdot \pi}\right) \]

      12. pow-flip52.5%

          \[\leadsto \color{blue}{{k}^{\left(-0.5\right)}} \cdot \left(\sqrt{2} \cdot \sqrt{n \cdot \pi}\right) \]

      13. metadata-eval52.5%

          \[\leadsto {k}^{\color{blue}{-0.5}} \cdot \left(\sqrt{2} \cdot \sqrt{n \cdot \pi}\right) \]

      14. sqrt-unprod52.6%

          \[\leadsto {k}^{-0.5} \cdot \color{blue}{\sqrt{2 \cdot \left(n \cdot \pi\right)}} \]

      15. *-commutative52.6%

          \[\leadsto {k}^{-0.5} \cdot \sqrt{2 \cdot \color{blue}{\left(\pi \cdot n\right)}} \]

   8. Applied egg-rr52.6%

      \[\leadsto \color{blue}{{k}^{-0.5} \cdot \sqrt{2 \cdot \left(\pi \cdot n\right)}} \]
   9. Step-by-step derivation

      1. *-commutative52.6%

         \[\leadsto {k}^{-0.5} \cdot \sqrt{2 \cdot \color{blue}{\left(n \cdot \pi\right)}} \]

      2. associate-*r*52.6%

         \[\leadsto {k}^{-0.5} \cdot \sqrt{\color{blue}{\left(2 \cdot n\right) \cdot \pi}} \]

   10. Simplified52.6%

       \[\leadsto \color{blue}{{k}^{-0.5} \cdot \sqrt{\left(2 \cdot n\right) \cdot \pi}} \]

   if 4.4000000000000002e274 < k

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Step-by-step derivation

      1. *-commutative100.0%

         \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

      2. *-commutative100.0%

         \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      3. associate-*r*100.0%

         \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

      4. div-inv100.0%

         \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

      5. add-sqr-sqrt100.0%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      6. sqrt-unprod100.0%

         \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

      7. frac-times100.0%

         \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

   3. Applied egg-rr100.0%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

   4. Taylor expanded in k around 0 3.2%

      \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
   5. Step-by-step derivation

      1. associate-*r*3.2%

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

      2. *-commutative3.2%

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

      3. *-commutative3.2%

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

   6. Simplified3.2%

      \[\leadsto \sqrt{\frac{\color{blue}{\pi \cdot \left(n \cdot 2\right)}}{k}} \]
   7. Step-by-step derivation

      1. add-cbrt-cube35.1%

         \[\leadsto \color{blue}{\sqrt[3]{\left(\sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right) \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}}} \]

      2. pow1/335.1%

         \[\leadsto \color{blue}{{\left(\left(\sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right) \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right)}^{0.3333333333333333}} \]

      3. add-sqr-sqrt35.1%

         \[\leadsto {\left(\color{blue}{\frac{\pi \cdot \left(n \cdot 2\right)}{k}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right)}^{0.3333333333333333} \]

      4. pow135.1%

         \[\leadsto {\left(\color{blue}{{\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{1}} \cdot \sqrt{\frac{\pi \cdot \left(n \cdot 2\right)}{k}}\right)}^{0.3333333333333333} \]

      5. pow1/235.1%

         \[\leadsto {\left({\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{1} \cdot \color{blue}{{\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{0.5}}\right)}^{0.3333333333333333} \]

      6. pow-prod-up35.1%

         \[\leadsto {\color{blue}{\left({\left(\frac{\pi \cdot \left(n \cdot 2\right)}{k}\right)}^{\left(1 + 0.5\right)}\right)}}^{0.3333333333333333} \]

      7. associate-/l*35.1%

         \[\leadsto {\left({\color{blue}{\left(\frac{\pi}{\frac{k}{n \cdot 2}}\right)}}^{\left(1 + 0.5\right)}\right)}^{0.3333333333333333} \]

      8. *-commutative35.1%

         \[\leadsto {\left({\left(\frac{\pi}{\frac{k}{\color{blue}{2 \cdot n}}}\right)}^{\left(1 + 0.5\right)}\right)}^{0.3333333333333333} \]

      9. metadata-eval35.1%

         \[\leadsto {\left({\left(\frac{\pi}{\frac{k}{2 \cdot n}}\right)}^{\color{blue}{1.5}}\right)}^{0.3333333333333333} \]

   8. Applied egg-rr35.1%

      \[\leadsto \color{blue}{{\left({\left(\frac{\pi}{\frac{k}{2 \cdot n}}\right)}^{1.5}\right)}^{0.3333333333333333}} \]
   9. Step-by-step derivation

      1. unpow1/335.1%

         \[\leadsto \color{blue}{\sqrt[3]{{\left(\frac{\pi}{\frac{k}{2 \cdot n}}\right)}^{1.5}}} \]

      2. associate-/r*35.1%

         \[\leadsto \sqrt[3]{{\left(\frac{\pi}{\color{blue}{\frac{\frac{k}{2}}{n}}}\right)}^{1.5}} \]

   10. Simplified35.1%

       \[\leadsto \color{blue}{\sqrt[3]{{\left(\frac{\pi}{\frac{\frac{k}{2}}{n}}\right)}^{1.5}}} \]

   11. Taylor expanded in k around 0 35.1%

       \[\leadsto \sqrt[3]{\color{blue}{e^{1.5 \cdot \left(-1 \cdot \log k + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}}} \]
   12. Step-by-step derivation

       1. exp-prod35.1%

          \[\leadsto \sqrt[3]{\color{blue}{{\left(e^{1.5}\right)}^{\left(-1 \cdot \log k + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}}} \]

       2. neg-mul-135.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\color{blue}{\left(-\log k\right)} + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}} \]

       3. log-rec35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\color{blue}{\log \left(\frac{1}{k}\right)} + \log \left(2 \cdot \left(n \cdot \pi\right)\right)\right)}} \]

       4. +-commutative35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\color{blue}{\left(\log \left(2 \cdot \left(n \cdot \pi\right)\right) + \log \left(\frac{1}{k}\right)\right)}}} \]

       5. associate-*r*35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\log \color{blue}{\left(\left(2 \cdot n\right) \cdot \pi\right)} + \log \left(\frac{1}{k}\right)\right)}} \]

       6. *-commutative35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\log \color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)} + \log \left(\frac{1}{k}\right)\right)}} \]

       7. log-rec35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\left(\log \left(\pi \cdot \left(2 \cdot n\right)\right) + \color{blue}{\left(-\log k\right)}\right)}} \]

       8. unsub-neg35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\color{blue}{\left(\log \left(\pi \cdot \left(2 \cdot n\right)\right) - \log k\right)}}} \]

       9. log-div35.1%

          \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\color{blue}{\log \left(\frac{\pi \cdot \left(2 \cdot n\right)}{k}\right)}}} \]

       10. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{\color{blue}{\left(2 \cdot n\right) \cdot \pi}}{k}\right)}} \]

       11. associate-*r*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}\right)}} \]

       12. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{2 \cdot \color{blue}{\left(\pi \cdot n\right)}}{k}\right)}} \]

       13. associate-/l*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \color{blue}{\left(\frac{2}{\frac{k}{\pi \cdot n}}\right)}}} \]

       14. associate-/r/35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \color{blue}{\left(\frac{2}{k} \cdot \left(\pi \cdot n\right)\right)}}} \]

       15. metadata-eval35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{\color{blue}{\frac{1}{0.5}}}{k} \cdot \left(\pi \cdot n\right)\right)}} \]

       16. associate-/r*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\color{blue}{\frac{1}{0.5 \cdot k}} \cdot \left(\pi \cdot n\right)\right)}} \]

       17. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{1}{\color{blue}{k \cdot 0.5}} \cdot \left(\pi \cdot n\right)\right)}} \]

       18. *-commutative35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \left(\frac{1}{k \cdot 0.5} \cdot \color{blue}{\left(n \cdot \pi\right)}\right)}} \]

       19. associate-*l*35.1%

           \[\leadsto \sqrt[3]{{\left(e^{1.5}\right)}^{\log \color{blue}{\left(\left(\frac{1}{k \cdot 0.5} \cdot n\right) \cdot \pi\right)}}} \]

   13. Simplified35.1%

       \[\leadsto \sqrt[3]{\color{blue}{{\left(\pi \cdot \left(n \cdot \frac{2}{k}\right)\right)}^{1.5}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification51.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;k \leq 4.4 \cdot 10^{+274}:\\ \;\;\;\;{k}^{-0.5} \cdot \sqrt{\pi \cdot \left(2 \cdot n\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{{\left(\pi \cdot \left(n \cdot \frac{2}{k}\right)\right)}^{1.5}}\\ \end{array} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. *-commutative99.5%

      \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

   2. *-commutative99.5%

      \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   3. associate-*r*99.5%

      \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   4. div-inv99.5%

      \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

   5. add-sqr-sqrt99.3%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   6. sqrt-unprod85.6%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   7. frac-times85.6%

      \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

3. Applied egg-rr85.7%

   \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

4. Taylor expanded in k around 0 35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
5. Step-by-step derivation

   1. associate-*r*35.9%

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

   2. *-commutative35.9%

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

   3. *-commutative35.9%

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

6. Simplified35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{\pi \cdot \left(n \cdot 2\right)}}{k}} \]
7. Step-by-step derivation

   1. sqrt-div49.7%

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

   2. pow1/249.7%

      \[\leadsto \frac{\color{blue}{{\left(\pi \cdot \left(n \cdot 2\right)\right)}^{0.5}}}{\sqrt{k}} \]

   3. associate-*r*49.7%

      \[\leadsto \frac{{\color{blue}{\left(\left(\pi \cdot n\right) \cdot 2\right)}}^{0.5}}{\sqrt{k}} \]

   4. *-commutative49.7%

      \[\leadsto \frac{{\left(\color{blue}{\left(n \cdot \pi\right)} \cdot 2\right)}^{0.5}}{\sqrt{k}} \]

   5. pow-prod-down49.6%

      \[\leadsto \frac{\color{blue}{{\left(n \cdot \pi\right)}^{0.5} \cdot {2}^{0.5}}}{\sqrt{k}} \]

   6. pow1/249.6%

      \[\leadsto \frac{\color{blue}{\sqrt{n \cdot \pi}} \cdot {2}^{0.5}}{\sqrt{k}} \]

   7. pow1/249.6%

      \[\leadsto \frac{\sqrt{n \cdot \pi} \cdot \color{blue}{\sqrt{2}}}{\sqrt{k}} \]

   8. *-commutative49.6%

      \[\leadsto \frac{\color{blue}{\sqrt{2} \cdot \sqrt{n \cdot \pi}}}{\sqrt{k}} \]

   9. sqrt-unprod49.7%

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

   10. *-commutative49.7%

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

8. Applied egg-rr49.7%

   \[\leadsto \color{blue}{\frac{\sqrt{2 \cdot \left(\pi \cdot n\right)}}{\sqrt{k}}} \]
9. Step-by-step derivation

   1. *-commutative49.7%

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

   2. associate-*r*49.7%

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

10. Simplified49.7%

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

11. Final simplification49.7%

    \[\leadsto \frac{\sqrt{\pi \cdot \left(2 \cdot n\right)}}{\sqrt{k}} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. *-commutative99.5%

      \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

   2. *-commutative99.5%

      \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   3. associate-*r*99.5%

      \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   4. div-inv99.5%

      \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

   5. add-sqr-sqrt99.3%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   6. sqrt-unprod85.6%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   7. frac-times85.6%

      \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

3. Applied egg-rr85.7%

   \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

4. Taylor expanded in k around 0 35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
5. Step-by-step derivation

   1. associate-*r*35.9%

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

   2. *-commutative35.9%

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

   3. *-commutative35.9%

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

6. Simplified35.9%

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

7. Taylor expanded in n around 0 35.9%

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

   1. associate-/l*35.9%

      \[\leadsto \sqrt{2 \cdot \color{blue}{\frac{n}{\frac{k}{\pi}}}} \]

9. Simplified35.9%

   \[\leadsto \sqrt{\color{blue}{2 \cdot \frac{n}{\frac{k}{\pi}}}} \]
10. Step-by-step derivation

    1. div-inv35.8%

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

    2. clear-num35.9%

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

11. Applied egg-rr35.9%

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

12. Final simplification35.9%

    \[\leadsto \sqrt{2 \cdot \left(n \cdot \frac{\pi}{k}\right)} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. *-commutative99.5%

      \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

   2. *-commutative99.5%

      \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   3. associate-*r*99.5%

      \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   4. div-inv99.5%

      \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

   5. add-sqr-sqrt99.3%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   6. sqrt-unprod85.6%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   7. frac-times85.6%

      \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

3. Applied egg-rr85.7%

   \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

4. Taylor expanded in k around 0 35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
5. Step-by-step derivation

   1. associate-*r*35.9%

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

   2. *-commutative35.9%

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

   3. *-commutative35.9%

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

6. Simplified35.9%

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

7. Taylor expanded in n around 0 35.9%

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

   1. associate-/l*35.9%

      \[\leadsto \sqrt{2 \cdot \color{blue}{\frac{n}{\frac{k}{\pi}}}} \]

9. Simplified35.9%

   \[\leadsto \sqrt{\color{blue}{2 \cdot \frac{n}{\frac{k}{\pi}}}} \]
10. Step-by-step derivation

    1. associate-/r/35.9%

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

11. Applied egg-rr35.9%

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

12. Final simplification35.9%

    \[\leadsto \sqrt{2 \cdot \left(\pi \cdot \frac{n}{k}\right)} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. *-commutative99.5%

      \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

   2. *-commutative99.5%

      \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   3. associate-*r*99.5%

      \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   4. div-inv99.5%

      \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

   5. add-sqr-sqrt99.3%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   6. sqrt-unprod85.6%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   7. frac-times85.6%

      \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

3. Applied egg-rr85.7%

   \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

4. Taylor expanded in k around 0 35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
5. Step-by-step derivation

   1. associate-*r*35.9%

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

   2. *-commutative35.9%

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

   3. *-commutative35.9%

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

6. Simplified35.9%

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

7. Taylor expanded in n around 0 35.9%

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

   1. associate-/l*35.9%

      \[\leadsto \sqrt{2 \cdot \color{blue}{\frac{n}{\frac{k}{\pi}}}} \]

9. Simplified35.9%

   \[\leadsto \sqrt{\color{blue}{2 \cdot \frac{n}{\frac{k}{\pi}}}} \]

10. Final simplification35.9%

    \[\leadsto \sqrt{2 \cdot \frac{n}{\frac{k}{\pi}}} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. *-commutative99.5%

      \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

   2. *-commutative99.5%

      \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   3. associate-*r*99.5%

      \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   4. div-inv99.5%

      \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

   5. add-sqr-sqrt99.3%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   6. sqrt-unprod85.6%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   7. frac-times85.6%

      \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

3. Applied egg-rr85.7%

   \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

4. Taylor expanded in k around 0 35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
5. Step-by-step derivation

   1. associate-*r*35.9%

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

   2. *-commutative35.9%

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

   3. *-commutative35.9%

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

6. Simplified35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{\pi \cdot \left(n \cdot 2\right)}}{k}} \]
7. Step-by-step derivation

   1. expm1-log1p-u34.4%

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

   2. expm1-udef36.9%

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

   3. associate-/l*36.9%

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

   4. *-commutative36.9%

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

8. Applied egg-rr36.9%

   \[\leadsto \color{blue}{e^{\mathsf{log1p}\left(\sqrt{\frac{\pi}{\frac{k}{2 \cdot n}}}\right)} - 1} \]
9. Step-by-step derivation

   1. expm1-def34.4%

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

   2. expm1-log1p35.9%

      \[\leadsto \color{blue}{\sqrt{\frac{\pi}{\frac{k}{2 \cdot n}}}} \]

   3. associate-/r*35.9%

      \[\leadsto \sqrt{\frac{\pi}{\color{blue}{\frac{\frac{k}{2}}{n}}}} \]

10. Simplified35.9%

    \[\leadsto \color{blue}{\sqrt{\frac{\pi}{\frac{\frac{k}{2}}{n}}}} \]

11. Final simplification35.9%

    \[\leadsto \sqrt{\frac{\pi}{\frac{\frac{k}{2}}{n}}} \]

1. Initial program 99.5%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Step-by-step derivation

   1. *-commutative99.5%

      \[\leadsto \color{blue}{{\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}}} \]

   2. *-commutative99.5%

      \[\leadsto {\left(\color{blue}{\left(\pi \cdot 2\right)} \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   3. associate-*r*99.5%

      \[\leadsto {\color{blue}{\left(\pi \cdot \left(2 \cdot n\right)\right)}}^{\left(\frac{1 - k}{2}\right)} \cdot \frac{1}{\sqrt{k}} \]

   4. div-inv99.5%

      \[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \]

   5. add-sqr-sqrt99.3%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}} \cdot \sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   6. sqrt-unprod85.6%

      \[\leadsto \color{blue}{\sqrt{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}} \cdot \frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k}}}} \]

   7. frac-times85.6%

      \[\leadsto \sqrt{\color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(\frac{1 - k}{2}\right)}}{\sqrt{k} \cdot \sqrt{k}}}} \]

3. Applied egg-rr85.7%

   \[\leadsto \color{blue}{\sqrt{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(1 - k\right)}}{k}}} \]

4. Taylor expanded in k around 0 35.9%

   \[\leadsto \sqrt{\frac{\color{blue}{2 \cdot \left(n \cdot \pi\right)}}{k}} \]
5. Step-by-step derivation

   1. associate-*r*35.9%

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

   2. *-commutative35.9%

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

   3. *-commutative35.9%

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

6. Simplified35.9%

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

7. Final simplification35.9%

   \[\leadsto \sqrt{\frac{\pi \cdot \left(2 \cdot n\right)}{k}} \]

herbie shell --seed 2023166 
(FPCore (k n)
  :name "Migdal et al, Equation (51)"
  :precision binary64
  (* (/ 1.0 (sqrt k)) (pow (* (* 2.0 PI) n) (/ (- 1.0 k) 2.0))))