Initial program 8.4
\[\frac{x0}{1 - x1} - x0\]
- Using strategy
rm Applied clear-num7.5
\[\leadsto \color{blue}{\frac{1}{\frac{1 - x1}{x0}}} - x0\]
- Using strategy
rm Applied flip3--7.6
\[\leadsto \color{blue}{\frac{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}{\frac{1}{\frac{1 - x1}{x0}} \cdot \frac{1}{\frac{1 - x1}{x0}} + \left(x0 \cdot x0 + \frac{1}{\frac{1 - x1}{x0}} \cdot x0\right)}}\]
- Using strategy
rm Applied *-un-lft-identity7.6
\[\leadsto \frac{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}{\color{blue}{1 \cdot \left(\frac{1}{\frac{1 - x1}{x0}} \cdot \frac{1}{\frac{1 - x1}{x0}} + \left(x0 \cdot x0 + \frac{1}{\frac{1 - x1}{x0}} \cdot x0\right)\right)}}\]
Applied add-cube-cbrt7.5
\[\leadsto \frac{\color{blue}{\left(\sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}} \cdot \sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}\right) \cdot \sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}}}{1 \cdot \left(\frac{1}{\frac{1 - x1}{x0}} \cdot \frac{1}{\frac{1 - x1}{x0}} + \left(x0 \cdot x0 + \frac{1}{\frac{1 - x1}{x0}} \cdot x0\right)\right)}\]
Applied times-frac7.5
\[\leadsto \color{blue}{\frac{\sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}} \cdot \sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}}{1} \cdot \frac{\sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}}{\frac{1}{\frac{1 - x1}{x0}} \cdot \frac{1}{\frac{1 - x1}{x0}} + \left(x0 \cdot x0 + \frac{1}{\frac{1 - x1}{x0}} \cdot x0\right)}}\]
Simplified5.1
\[\leadsto \frac{\sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}} \cdot \sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}}{1} \cdot \color{blue}{\frac{\sqrt[3]{{\left(\frac{x0}{1 - x1}\right)}^{3} + \left(-x0\right) \cdot \left(x0 \cdot x0\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + x0 \cdot \left(x0 + \frac{x0}{1 - x1}\right)}}\]
Final simplification5.1
\[\leadsto \frac{\sqrt[3]{{\left(\frac{x0}{1 - x1}\right)}^{3} + \left(-x0\right) \cdot \left(x0 \cdot x0\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 + \frac{x0}{1 - x1}\right) \cdot x0} \cdot \left(\sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}} \cdot \sqrt[3]{{\left(\frac{1}{\frac{1 - x1}{x0}}\right)}^{3} - {x0}^{3}}\right)\]