Initial program 0.5
\[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
- Using strategy
rm Applied add-sqr-sqrt_binary640.5
\[\leadsto \frac{\color{blue}{\sqrt{1 - 5 \cdot \left(v \cdot v\right)} \cdot \sqrt{1 - 5 \cdot \left(v \cdot v\right)}}}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
Applied times-frac_binary640.5
\[\leadsto \color{blue}{\frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}} \cdot \frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{1 - v \cdot v}}\]
Simplified0.5
\[\leadsto \color{blue}{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}} \cdot \frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{1 - v \cdot v}\]
Simplified0.5
\[\leadsto \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}} \cdot \color{blue}{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}}\]
- Using strategy
rm Applied associate-/r*_binary640.5
\[\leadsto \color{blue}{\frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\pi \cdot t}}{\sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
- Using strategy
rm Applied sqrt-prod_binary640.5
\[\leadsto \frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\pi \cdot t}}{\color{blue}{\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}}} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
Applied *-un-lft-identity_binary640.5
\[\leadsto \frac{\frac{\sqrt{\color{blue}{1 \cdot \left(1 - \left(v \cdot v\right) \cdot 5\right)}}}{\pi \cdot t}}{\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
Applied sqrt-prod_binary640.5
\[\leadsto \frac{\frac{\color{blue}{\sqrt{1} \cdot \sqrt{1 - \left(v \cdot v\right) \cdot 5}}}{\pi \cdot t}}{\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
Applied times-frac_binary640.4
\[\leadsto \frac{\color{blue}{\frac{\sqrt{1}}{\pi} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{t}}}{\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
Applied times-frac_binary640.3
\[\leadsto \color{blue}{\left(\frac{\frac{\sqrt{1}}{\pi}}{\sqrt{2}} \cdot \frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{t}}{\sqrt{1 - 3 \cdot \left(v \cdot v\right)}}\right)} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
Simplified0.3
\[\leadsto \left(\color{blue}{\frac{\frac{1}{\pi}}{\sqrt{2}}} \cdot \frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{t}}{\sqrt{1 - 3 \cdot \left(v \cdot v\right)}}\right) \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
Simplified0.3
\[\leadsto \left(\frac{\frac{1}{\pi}}{\sqrt{2}} \cdot \color{blue}{\frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{t}}{\sqrt{1 - \left(v \cdot v\right) \cdot 3}}}\right) \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
Final simplification0.3
\[\leadsto \left(\frac{\frac{1}{\pi}}{\sqrt{2}} \cdot \frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{t}}{\sqrt{1 - \left(v \cdot v\right) \cdot 3}}\right) \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]