Initial program 0.4
\[\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 flip3--0.4
\[\leadsto \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 \color{blue}{\frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}}\]
Applied flip--0.4
\[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \color{blue}{\frac{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]
Applied associate-*r/0.4
\[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{\color{blue}{\frac{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]
Applied sqrt-div0.4
\[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \color{blue}{\frac{\sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]
Applied associate-*r/0.4
\[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}} \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]
Applied frac-times0.4
\[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)}}}\]
Applied associate-/r/0.4
\[\leadsto \color{blue}{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)}\]
Simplified0.3
\[\leadsto \color{blue}{\frac{\frac{\frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{\pi}}{t}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)}}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)}} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
- Using strategy
rm Applied *-un-lft-identity0.3
\[\leadsto \frac{\frac{\frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{\pi}}{\color{blue}{1 \cdot t}}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)}}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
Applied div-inv0.3
\[\leadsto \frac{\frac{\frac{\color{blue}{\left(1 - \left(5 \cdot v\right) \cdot v\right) \cdot \frac{1}{\pi}}}{1 \cdot t}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)}}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
Applied times-frac0.3
\[\leadsto \frac{\frac{\color{blue}{\frac{1 - \left(5 \cdot v\right) \cdot v}{1} \cdot \frac{\frac{1}{\pi}}{t}}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)}}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
Applied associate-/l*0.4
\[\leadsto \frac{\color{blue}{\frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{1}}{\frac{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)}}{\frac{\frac{1}{\pi}}{t}}}}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
Simplified0.4
\[\leadsto \frac{\frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{1}}{\color{blue}{\left(\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)} \cdot \pi\right) \cdot t}}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
- Using strategy
rm Applied associate-/r*0.1
\[\leadsto \frac{\color{blue}{\frac{\frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{1}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)} \cdot \pi}}{t}}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
Simplified0.1
\[\leadsto \frac{\frac{\color{blue}{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\sqrt{\left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right) \cdot 2}}}{\pi}}}{t}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
Final simplification0.1
\[\leadsto \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(\left(\left(v \cdot v\right) \cdot 1 + \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right) + 1 \cdot 1\right)\right) \cdot \frac{\frac{\frac{\frac{1 - \left(v \cdot v\right) \cdot 5}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}}{\pi}}{t}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)}\]