Initial program 0.0
\[\log \left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{x}\right)\]
- Using strategy
rm Applied add-sqr-sqrt0.0
\[\leadsto \log \left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}\right)\]
Applied *-un-lft-identity0.0
\[\leadsto \log \left(\frac{1}{x} + \frac{\color{blue}{1 \cdot \sqrt{1 - x \cdot x}}}{\sqrt{x} \cdot \sqrt{x}}\right)\]
Applied times-frac0.0
\[\leadsto \log \left(\frac{1}{x} + \color{blue}{\frac{1}{\sqrt{x}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{x}}}\right)\]
Applied add-sqr-sqrt0.0
\[\leadsto \log \left(\frac{1}{\color{blue}{\sqrt{x} \cdot \sqrt{x}}} + \frac{1}{\sqrt{x}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{x}}\right)\]
Applied *-un-lft-identity0.0
\[\leadsto \log \left(\frac{\color{blue}{1 \cdot 1}}{\sqrt{x} \cdot \sqrt{x}} + \frac{1}{\sqrt{x}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{x}}\right)\]
Applied times-frac0.0
\[\leadsto \log \left(\color{blue}{\frac{1}{\sqrt{x}} \cdot \frac{1}{\sqrt{x}}} + \frac{1}{\sqrt{x}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{x}}\right)\]
Applied distribute-lft-out0.0
\[\leadsto \log \color{blue}{\left(\frac{1}{\sqrt{x}} \cdot \left(\frac{1}{\sqrt{x}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{x}}\right)\right)}\]
Applied log-prod0.2
\[\leadsto \color{blue}{\log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\sqrt{x}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{x}}\right)}\]
- Using strategy
rm Applied add-cube-cbrt0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\sqrt{x}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{\color{blue}{\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \sqrt[3]{x}}}}\right)\]
Applied sqrt-prod0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\sqrt{x}} + \frac{\sqrt{1 - x \cdot x}}{\color{blue}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}} \cdot \sqrt{\sqrt[3]{x}}}}\right)\]
Applied *-un-lft-identity0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\sqrt{x}} + \frac{\color{blue}{1 \cdot \sqrt{1 - x \cdot x}}}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}} \cdot \sqrt{\sqrt[3]{x}}}\right)\]
Applied times-frac0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\sqrt{x}} + \color{blue}{\frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}}\right)\]
Applied add-cube-cbrt0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\sqrt{\color{blue}{\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \sqrt[3]{x}}}} + \frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\]
Applied sqrt-prod0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\color{blue}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}} \cdot \sqrt{\sqrt[3]{x}}}} + \frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\]
Applied *-un-lft-identity0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{\color{blue}{1 \cdot 1}}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}} \cdot \sqrt{\sqrt[3]{x}}} + \frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\]
Applied times-frac0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\color{blue}{\frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}} \cdot \frac{1}{\sqrt{\sqrt[3]{x}}}} + \frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}} \cdot \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\]
Applied distribute-lft-out0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \log \color{blue}{\left(\frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}} \cdot \left(\frac{1}{\sqrt{\sqrt[3]{x}}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\right)}\]
Applied log-prod0.2
\[\leadsto \log \left(\frac{1}{\sqrt{x}}\right) + \color{blue}{\left(\log \left(\frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}}\right) + \log \left(\frac{1}{\sqrt{\sqrt[3]{x}}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\right)}\]
Applied associate-+r+0.3
\[\leadsto \color{blue}{\left(\log \left(\frac{1}{\sqrt{x}}\right) + \log \left(\frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}}\right)\right) + \log \left(\frac{1}{\sqrt{\sqrt[3]{x}}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)}\]
Simplified0.3
\[\leadsto \color{blue}{\left(-\left(\log \left(\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}\right) + \log \left(\sqrt{x}\right)\right)\right)} + \log \left(\frac{1}{\sqrt{\sqrt[3]{x}}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\]
Final simplification0.3
\[\leadsto \left(-\left(\log \left(\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}\right) + \log \left(\sqrt{x}\right)\right)\right) + \log \left(\frac{1}{\sqrt{\sqrt[3]{x}}} + \frac{\sqrt{1 - x \cdot x}}{\sqrt{\sqrt[3]{x}}}\right)\]