Initial program 0.5
\[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)}
\]
Simplified0.5
\[\leadsto \color{blue}{\frac{{\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(0.5 - \frac{k}{2}\right)}}{\sqrt{k}}}
\]
Proof
(/.f64 (pow.f64 (*.f64 (PI.f64) (*.f64 2 n)) (-.f64 1/2 (/.f64 k 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (PI.f64) 2) n)) (-.f64 1/2 (/.f64 k 2))) (sqrt.f64 k)): 8 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 (PI.f64))) n) (-.f64 1/2 (/.f64 k 2))) (sqrt.f64 k)): 1 points increase in error, 8 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (-.f64 (Rewrite<= metadata-eval (/.f64 1 2)) (/.f64 k 2))) (sqrt.f64 k)): 9 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 1 k) 2))) (sqrt.f64 k)): 0 points increase in error, 9 points decrease in error
(/.f64 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (/.f64 (-.f64 1 k) 2) 2)) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (/.f64 (-.f64 1 k) 2) 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2))) (sqrt.f64 k)): 9 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2)))) (sqrt.f64 k)): 0 points increase in error, 1 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2)))): 1 points increase in error, 8 points decrease in error
Applied egg-rr0.4
\[\leadsto \frac{\color{blue}{\sqrt{\pi \cdot \left(2 \cdot n\right)} \cdot {\left(\pi \cdot \left(2 \cdot n\right)\right)}^{\left(k \cdot -0.5\right)}}}{\sqrt{k}}
\]
Simplified0.4
\[\leadsto \frac{\color{blue}{\sqrt{\left(2 \cdot \pi\right) \cdot n} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(k \cdot -0.5\right)}}}{\sqrt{k}}
\]
Proof
(/.f64 (*.f64 (sqrt.f64 (*.f64 (*.f64 2 (PI.f64)) n)) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (*.f64 k -1/2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sqrt.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (PI.f64) 2)) n)) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (*.f64 k -1/2))) (sqrt.f64 k)): 5 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (PI.f64) (*.f64 2 n)))) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (*.f64 k -1/2))) (sqrt.f64 k)): 0 points increase in error, 5 points decrease in error
(/.f64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) (*.f64 2 n))) (pow.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (PI.f64) 2)) n) (*.f64 k -1/2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) (*.f64 2 n))) (pow.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (PI.f64) (*.f64 2 n))) (*.f64 k -1/2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
Final simplification0.4
\[\leadsto \frac{\sqrt{\left(2 \cdot \pi\right) \cdot n} \cdot {\left(\left(2 \cdot \pi\right) \cdot n\right)}^{\left(k \cdot -0.5\right)}}{\sqrt{k}}
\]