Initial program 1.0
\[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}
\]
Simplified0.0
\[\leadsto \color{blue}{\frac{\frac{1.3333333333333333}{\pi \cdot \left(1 - v \cdot v\right)}}{\sqrt{2 + \left(v \cdot v\right) \cdot -6}}}
\]
Proof
(/.f64 (/.f64 4/3 (*.f64 (PI.f64) (-.f64 1 (*.f64 v v)))) (sqrt.f64 (+.f64 2 (*.f64 (*.f64 v v) -6)))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 4 3)) (*.f64 (PI.f64) (-.f64 1 (*.f64 v v)))) (sqrt.f64 (+.f64 2 (*.f64 (*.f64 v v) -6)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 4 (*.f64 3 (*.f64 (PI.f64) (-.f64 1 (*.f64 v v)))))) (sqrt.f64 (+.f64 2 (*.f64 (*.f64 v v) -6)))): 1 points increase in error, 3 points decrease in error
(/.f64 (/.f64 4 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 3 (PI.f64)) (-.f64 1 (*.f64 v v))))) (sqrt.f64 (+.f64 2 (*.f64 (*.f64 v v) -6)))): 0 points increase in error, 1 points decrease in error
(/.f64 (/.f64 4 (*.f64 (*.f64 3 (PI.f64)) (-.f64 1 (*.f64 v v)))) (sqrt.f64 (+.f64 2 (*.f64 (*.f64 v v) (Rewrite<= metadata-eval (neg.f64 6)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 4 (*.f64 (*.f64 3 (PI.f64)) (-.f64 1 (*.f64 v v)))) (sqrt.f64 (+.f64 2 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 v v) 6)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 4 (*.f64 (*.f64 3 (PI.f64)) (-.f64 1 (*.f64 v v)))) (sqrt.f64 (+.f64 2 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 6 (*.f64 v v))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 4 (*.f64 (*.f64 3 (PI.f64)) (-.f64 1 (*.f64 v v)))) (sqrt.f64 (Rewrite<= sub-neg_binary64 (-.f64 2 (*.f64 6 (*.f64 v v)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 4 (*.f64 (*.f64 (*.f64 3 (PI.f64)) (-.f64 1 (*.f64 v v))) (sqrt.f64 (-.f64 2 (*.f64 6 (*.f64 v v))))))): 249 points increase in error, 1 points decrease in error
Applied egg-rr0.0
\[\leadsto \frac{\color{blue}{\frac{1}{\pi \cdot \left(1 - v \cdot v\right)} \cdot 1.3333333333333333}}{\sqrt{2 + \left(v \cdot v\right) \cdot -6}}
\]
Final simplification0.0
\[\leadsto \frac{\frac{1}{\pi \cdot \left(1 - v \cdot v\right)} \cdot 1.3333333333333333}{\sqrt{2 + \left(v \cdot v\right) \cdot -6}}
\]