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(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(0.5 - \frac{k}{2}\right)}}{\sqrt{k}}}
\]
Proof
(/.f64 (pow.f64 (*.f64 2 (*.f64 (PI.f64) 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 2 (PI.f64)) n)) (-.f64 1/2 (/.f64 k 2))) (sqrt.f64 k)): 0 points increase in error, 0 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)): 0 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, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= /-rgt-identity_binary64 (/.f64 (/.f64 (-.f64 1 k) 2) 1))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (/.f64 (-.f64 1 k) 2) (Rewrite<= metadata-eval (/.f64 2 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 (-.f64 1 k) 2) 2) 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (/.f64 (-.f64 1 k) 2) 2) 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= *-commutative_binary64 (*.f64 2 (/.f64 (/.f64 (-.f64 1 k) 2) 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= pow-sqr_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)): 57 points increase in error, 16 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)): 16 points increase in error, 57 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, 0 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)))): 30 points increase in error, 15 points decrease in error
Applied egg-rr0.4
\[\leadsto \frac{\color{blue}{\frac{\sqrt{\pi \cdot \left(n \cdot 2\right)}}{{\left(\pi \cdot \left(n \cdot 2\right)\right)}^{\left(0.5 \cdot k\right)}}}}{\sqrt{k}}
\]
Applied egg-rr0.4
\[\leadsto \color{blue}{\sqrt{\pi \cdot \left(n + n\right)} \cdot \frac{1}{{\left(\sqrt{\pi \cdot \left(n + n\right)}\right)}^{k} \cdot \sqrt{k}}}
\]
Simplified0.4
\[\leadsto \color{blue}{\frac{\sqrt{2 \cdot \left(n \cdot \pi\right)}}{\sqrt{k} \cdot {\left(\sqrt{2 \cdot \left(n \cdot \pi\right)}\right)}^{k}}}
\]
Proof
(/.f64 (sqrt.f64 (*.f64 2 (*.f64 n (PI.f64)))) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (*.f64 2 (*.f64 n (PI.f64)))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 2 n) (PI.f64)))) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (*.f64 2 (*.f64 n (PI.f64)))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (Rewrite<= count-2_binary64 (+.f64 n n)) (PI.f64))) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (*.f64 2 (*.f64 n (PI.f64)))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 (PI.f64) (+.f64 n n)))) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (*.f64 2 (*.f64 n (PI.f64)))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 2 n) (PI.f64)))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (*.f64 (Rewrite<= count-2_binary64 (+.f64 n n)) (PI.f64))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 (PI.f64) (+.f64 n n)))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) 1)) (*.f64 (sqrt.f64 k) (pow.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) k))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) 1) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) k) (sqrt.f64 k)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) (/.f64 1 (*.f64 (pow.f64 (sqrt.f64 (*.f64 (PI.f64) (+.f64 n n))) k) (sqrt.f64 k))))): 33 points increase in error, 16 points decrease in error
Final simplification0.4
\[\leadsto \frac{\sqrt{2 \cdot \left(n \cdot \pi\right)}}{\sqrt{k} \cdot {\left(\sqrt{2 \cdot \left(n \cdot \pi\right)}\right)}^{k}}
\]