Initial program 0.1
\[\left(\left(\left(x + y\right) + z\right) - z \cdot \log t\right) + \left(a - 0.5\right) \cdot b\]
- Using strategy
rm Applied add-cube-cbrt_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - z \cdot \log \color{blue}{\left(\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}\right)}\right) + \left(a - 0.5\right) \cdot b\]
Applied log-prod_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - z \cdot \color{blue}{\left(\log \left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) + \log \left(\sqrt[3]{t}\right)\right)}\right) + \left(a - 0.5\right) \cdot b\]
Applied distribute-rgt-in_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \color{blue}{\left(\log \left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot z + \log \left(\sqrt[3]{t}\right) \cdot z\right)}\right) + \left(a - 0.5\right) \cdot b\]
Simplified0.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(\color{blue}{z \cdot \left(2 \cdot \log \left(\sqrt[3]{t}\right)\right)} + \log \left(\sqrt[3]{t}\right) \cdot z\right)\right) + \left(a - 0.5\right) \cdot b\]
Simplified0.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(z \cdot \left(2 \cdot \log \left(\sqrt[3]{t}\right)\right) + \color{blue}{z \cdot \log \left(\sqrt[3]{t}\right)}\right)\right) + \left(a - 0.5\right) \cdot b\]
- Using strategy
rm Applied *-un-lft-identity_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(z \cdot \left(2 \cdot \log \left(\sqrt[3]{\color{blue}{1 \cdot t}}\right)\right) + z \cdot \log \left(\sqrt[3]{t}\right)\right)\right) + \left(a - 0.5\right) \cdot b\]
Applied cbrt-prod_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(z \cdot \left(2 \cdot \log \color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{t}\right)}\right) + z \cdot \log \left(\sqrt[3]{t}\right)\right)\right) + \left(a - 0.5\right) \cdot b\]
Applied log-prod_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(z \cdot \left(2 \cdot \color{blue}{\left(\log \left(\sqrt[3]{1}\right) + \log \left(\sqrt[3]{t}\right)\right)}\right) + z \cdot \log \left(\sqrt[3]{t}\right)\right)\right) + \left(a - 0.5\right) \cdot b\]
Applied distribute-lft-in_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(z \cdot \color{blue}{\left(2 \cdot \log \left(\sqrt[3]{1}\right) + 2 \cdot \log \left(\sqrt[3]{t}\right)\right)} + z \cdot \log \left(\sqrt[3]{t}\right)\right)\right) + \left(a - 0.5\right) \cdot b\]
Applied distribute-lft-in_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(\color{blue}{\left(z \cdot \left(2 \cdot \log \left(\sqrt[3]{1}\right)\right) + z \cdot \left(2 \cdot \log \left(\sqrt[3]{t}\right)\right)\right)} + z \cdot \log \left(\sqrt[3]{t}\right)\right)\right) + \left(a - 0.5\right) \cdot b\]
Applied associate-+l+_binary640.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \color{blue}{\left(z \cdot \left(2 \cdot \log \left(\sqrt[3]{1}\right)\right) + \left(z \cdot \left(2 \cdot \log \left(\sqrt[3]{t}\right)\right) + z \cdot \log \left(\sqrt[3]{t}\right)\right)\right)}\right) + \left(a - 0.5\right) \cdot b\]
Simplified0.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(z \cdot \left(2 \cdot \log \left(\sqrt[3]{1}\right)\right) + \color{blue}{z \cdot \log t}\right)\right) + \left(a - 0.5\right) \cdot b\]
Final simplification0.1
\[\leadsto \left(\left(\left(x + y\right) + z\right) - \left(z \cdot \left(2 \cdot \log \left(\sqrt[3]{1}\right)\right) + z \cdot \log t\right)\right) + \left(a - 0.5\right) \cdot b\]