Initial program 0.2
\[\left(x \cdot 3\right) \cdot x\]
- Using strategy
rm Applied add-sqr-sqrt_binary640.4
\[\leadsto \color{blue}{\sqrt{\left(x \cdot 3\right) \cdot x} \cdot \sqrt{\left(x \cdot 3\right) \cdot x}}\]
Simplified0.4
\[\leadsto \color{blue}{\sqrt{x \cdot \left(x \cdot 3\right)}} \cdot \sqrt{\left(x \cdot 3\right) \cdot x}\]
Simplified0.4
\[\leadsto \sqrt{x \cdot \left(x \cdot 3\right)} \cdot \color{blue}{\sqrt{x \cdot \left(x \cdot 3\right)}}\]
- Using strategy
rm Applied *-un-lft-identity_binary640.4
\[\leadsto \sqrt{x \cdot \left(x \cdot 3\right)} \cdot \color{blue}{\left(1 \cdot \sqrt{x \cdot \left(x \cdot 3\right)}\right)}\]
Applied associate-*r*_binary640.4
\[\leadsto \color{blue}{\left(\sqrt{x \cdot \left(x \cdot 3\right)} \cdot 1\right) \cdot \sqrt{x \cdot \left(x \cdot 3\right)}}\]
Simplified0.3
\[\leadsto \color{blue}{\left|x \cdot \sqrt{3}\right|} \cdot \sqrt{x \cdot \left(x \cdot 3\right)}\]
- Using strategy
rm Applied associate-*r*_binary640.3
\[\leadsto \left|x \cdot \sqrt{3}\right| \cdot \sqrt{\color{blue}{\left(x \cdot x\right) \cdot 3}}\]
- Using strategy
rm Applied pow1_binary640.3
\[\leadsto \left|x \cdot \sqrt{3}\right| \cdot \color{blue}{{\left(\sqrt{\left(x \cdot x\right) \cdot 3}\right)}^{1}}\]
Applied pow1_binary640.3
\[\leadsto \color{blue}{{\left(\left|x \cdot \sqrt{3}\right|\right)}^{1}} \cdot {\left(\sqrt{\left(x \cdot x\right) \cdot 3}\right)}^{1}\]
Applied pow-prod-down_binary640.3
\[\leadsto \color{blue}{{\left(\left|x \cdot \sqrt{3}\right| \cdot \sqrt{\left(x \cdot x\right) \cdot 3}\right)}^{1}}\]
Simplified0.2
\[\leadsto {\color{blue}{\left(\left(x \cdot x\right) \cdot 3\right)}}^{1}\]
Final simplification0.2
\[\leadsto \left(x \cdot x\right) \cdot 3\]