Initial program 0.1
\[\left(\left(x \cdot \log y - y\right) - z\right) + \log t\]
- Using strategy
rm Applied add-cube-cbrt0.1
\[\leadsto \left(\left(x \cdot \log \color{blue}{\left(\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}\right)} - y\right) - z\right) + \log t\]
Applied log-prod0.1
\[\leadsto \left(\left(x \cdot \color{blue}{\left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \log \left(\sqrt[3]{y}\right)\right)} - y\right) - z\right) + \log t\]
Applied distribute-rgt-in0.1
\[\leadsto \left(\left(\color{blue}{\left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot x + \log \left(\sqrt[3]{y}\right) \cdot x\right)} - y\right) - z\right) + \log t\]
Applied associate--l+0.1
\[\leadsto \left(\color{blue}{\left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot x + \left(\log \left(\sqrt[3]{y}\right) \cdot x - y\right)\right)} - z\right) + \log t\]
- Using strategy
rm Applied *-un-lft-identity0.1
\[\leadsto \left(\left(\log \left(\sqrt[3]{\color{blue}{1 \cdot y}} \cdot \sqrt[3]{y}\right) \cdot x + \left(\log \left(\sqrt[3]{y}\right) \cdot x - y\right)\right) - z\right) + \log t\]
Applied cbrt-prod0.1
\[\leadsto \left(\left(\log \left(\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{y}\right)} \cdot \sqrt[3]{y}\right) \cdot x + \left(\log \left(\sqrt[3]{y}\right) \cdot x - y\right)\right) - z\right) + \log t\]
Applied associate-*l*0.1
\[\leadsto \left(\left(\log \color{blue}{\left(\sqrt[3]{1} \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right)} \cdot x + \left(\log \left(\sqrt[3]{y}\right) \cdot x - y\right)\right) - z\right) + \log t\]
Simplified0.1
\[\leadsto \left(\left(\log \left(\sqrt[3]{1} \cdot \color{blue}{{y}^{\frac{2}{3}}}\right) \cdot x + \left(\log \left(\sqrt[3]{y}\right) \cdot x - y\right)\right) - z\right) + \log t\]
Taylor expanded around 0 0.1
\[\leadsto \left(\left(\color{blue}{x \cdot \log \left({y}^{\frac{2}{3}}\right)} + \left(\log \left(\sqrt[3]{y}\right) \cdot x - y\right)\right) - z\right) + \log t\]
Final simplification0.1
\[\leadsto \left(\left(x \cdot \log \left({y}^{\frac{2}{3}}\right) + \left(\log \left(\sqrt[3]{y}\right) \cdot x - y\right)\right) - z\right) + \log t\]