Initial program 0.0
\[\left(\left(x \cdot y + z \cdot t\right) + a \cdot b\right) + c \cdot i\]
Initial simplification0.0
\[\leadsto (b \cdot a + \left(z \cdot t\right))_* + (i \cdot c + \left(x \cdot y\right))_*\]
- Using strategy
rm Applied add-cbrt-cube27.6
\[\leadsto \color{blue}{\sqrt[3]{\left((b \cdot a + \left(z \cdot t\right))_* \cdot (b \cdot a + \left(z \cdot t\right))_*\right) \cdot (b \cdot a + \left(z \cdot t\right))_*}} + (i \cdot c + \left(x \cdot y\right))_*\]
- Using strategy
rm Applied *-un-lft-identity27.6
\[\leadsto \sqrt[3]{\left((b \cdot a + \left(z \cdot t\right))_* \cdot (b \cdot a + \left(z \cdot t\right))_*\right) \cdot (b \cdot a + \left(z \cdot t\right))_*} + \color{blue}{1 \cdot (i \cdot c + \left(x \cdot y\right))_*}\]
Applied *-un-lft-identity27.6
\[\leadsto \color{blue}{1 \cdot \sqrt[3]{\left((b \cdot a + \left(z \cdot t\right))_* \cdot (b \cdot a + \left(z \cdot t\right))_*\right) \cdot (b \cdot a + \left(z \cdot t\right))_*}} + 1 \cdot (i \cdot c + \left(x \cdot y\right))_*\]
Applied distribute-lft-out27.6
\[\leadsto \color{blue}{1 \cdot \left(\sqrt[3]{\left((b \cdot a + \left(z \cdot t\right))_* \cdot (b \cdot a + \left(z \cdot t\right))_*\right) \cdot (b \cdot a + \left(z \cdot t\right))_*} + (i \cdot c + \left(x \cdot y\right))_*\right)}\]
Simplified0.0
\[\leadsto 1 \cdot \color{blue}{\left((t \cdot z + \left(b \cdot a\right))_* + (c \cdot i + \left(x \cdot y\right))_*\right)}\]
Final simplification0.0
\[\leadsto (c \cdot i + \left(x \cdot y\right))_* + (t \cdot z + \left(b \cdot a\right))_*\]