Initial program 30.0
\[\sqrt[3]{x + 1} - \sqrt[3]{x}
\]
Applied egg-rr29.3
\[\leadsto \color{blue}{\left(\left(x + 1\right) - x\right) \cdot \frac{1}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}}
\]
Simplified0.5
\[\leadsto \color{blue}{\frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\left(\sqrt[3]{1 + x}\right)}^{2}\right)}}
\]
Proof
[Start]29.3 | \[ \left(\left(x + 1\right) - x\right) \cdot \frac{1}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}
\] |
|---|
associate-*r/ [=>]29.3 | \[ \color{blue}{\frac{\left(\left(x + 1\right) - x\right) \cdot 1}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}}
\] |
|---|
*-rgt-identity [=>]29.3 | \[ \frac{\color{blue}{\left(x + 1\right) - x}}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}
\] |
|---|
+-commutative [=>]29.3 | \[ \frac{\color{blue}{\left(1 + x\right)} - x}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}
\] |
|---|
associate--l+ [=>]0.5 | \[ \frac{\color{blue}{1 + \left(x - x\right)}}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}
\] |
|---|
+-inverses [=>]0.5 | \[ \frac{1 + \color{blue}{0}}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}
\] |
|---|
metadata-eval [=>]0.5 | \[ \frac{\color{blue}{1}}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right)}
\] |
|---|
+-commutative [=>]0.5 | \[ \frac{1}{\color{blue}{\sqrt[3]{x} \cdot \left(\sqrt[3]{x + 1} + \sqrt[3]{x}\right) + {\left(\sqrt[3]{x + 1}\right)}^{2}}}
\] |
|---|
fma-def [=>]0.5 | \[ \frac{1}{\color{blue}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{x + 1} + \sqrt[3]{x}, {\left(\sqrt[3]{x + 1}\right)}^{2}\right)}}
\] |
|---|
+-commutative [=>]0.5 | \[ \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{\color{blue}{1 + x}} + \sqrt[3]{x}, {\left(\sqrt[3]{x + 1}\right)}^{2}\right)}
\] |
|---|
+-commutative [=>]0.5 | \[ \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\left(\sqrt[3]{\color{blue}{1 + x}}\right)}^{2}\right)}
\] |
|---|
Applied egg-rr0.5
\[\leadsto \frac{1}{\color{blue}{{\left(\sqrt[3]{x}\right)}^{2} + \sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} + \sqrt[3]{x}\right)}}
\]
Applied egg-rr0.5
\[\leadsto \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \color{blue}{\frac{\sqrt[3]{x + 1}}{\frac{1}{\sqrt[3]{x} + \sqrt[3]{x + 1}}}}}
\]
Applied egg-rr0.3
\[\leadsto \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\color{blue}{\frac{1}{1 + \left(x + x\right)} \cdot {\left(\sqrt[3]{x}\right)}^{2} + \frac{1}{1 + \left(x + x\right)} \cdot \left(\sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right)\right)}}}
\]
Simplified0.3
\[\leadsto \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\color{blue}{\frac{\mathsf{fma}\left(\sqrt[3]{1 + x} - \sqrt[3]{x}, \sqrt[3]{1 + x}, {\left(\sqrt[3]{x}\right)}^{2}\right)}{\mathsf{fma}\left(x, 2, 1\right)}}}}
\]
Proof
[Start]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{1}{1 + \left(x + x\right)} \cdot {\left(\sqrt[3]{x}\right)}^{2} + \frac{1}{1 + \left(x + x\right)} \cdot \left(\sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right)\right)}}
\] |
|---|
distribute-lft-out [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\color{blue}{\frac{1}{1 + \left(x + x\right)} \cdot \left({\left(\sqrt[3]{x}\right)}^{2} + \sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right)\right)}}}
\] |
|---|
+-commutative [<=]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{1}{1 + \left(x + x\right)} \cdot \color{blue}{\left(\sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right) + {\left(\sqrt[3]{x}\right)}^{2}\right)}}}
\] |
|---|
associate-*l/ [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\color{blue}{\frac{1 \cdot \left(\sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right) + {\left(\sqrt[3]{x}\right)}^{2}\right)}{1 + \left(x + x\right)}}}}
\] |
|---|
*-lft-identity [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{\color{blue}{\sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right) + {\left(\sqrt[3]{x}\right)}^{2}}}{1 + \left(x + x\right)}}}
\] |
|---|
*-commutative [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{\color{blue}{\left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right) \cdot \sqrt[3]{1 + x}} + {\left(\sqrt[3]{x}\right)}^{2}}{1 + \left(x + x\right)}}}
\] |
|---|
fma-def [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{\color{blue}{\mathsf{fma}\left(\sqrt[3]{1 + x} - \sqrt[3]{x}, \sqrt[3]{1 + x}, {\left(\sqrt[3]{x}\right)}^{2}\right)}}{1 + \left(x + x\right)}}}
\] |
|---|
+-commutative [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{\mathsf{fma}\left(\sqrt[3]{1 + x} - \sqrt[3]{x}, \sqrt[3]{1 + x}, {\left(\sqrt[3]{x}\right)}^{2}\right)}{\color{blue}{\left(x + x\right) + 1}}}}
\] |
|---|
count-2 [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{\mathsf{fma}\left(\sqrt[3]{1 + x} - \sqrt[3]{x}, \sqrt[3]{1 + x}, {\left(\sqrt[3]{x}\right)}^{2}\right)}{\color{blue}{2 \cdot x} + 1}}}
\] |
|---|
*-commutative [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{\mathsf{fma}\left(\sqrt[3]{1 + x} - \sqrt[3]{x}, \sqrt[3]{1 + x}, {\left(\sqrt[3]{x}\right)}^{2}\right)}{\color{blue}{x \cdot 2} + 1}}}
\] |
|---|
fma-def [=>]0.3 | \[ \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{x + 1}}{\frac{\mathsf{fma}\left(\sqrt[3]{1 + x} - \sqrt[3]{x}, \sqrt[3]{1 + x}, {\left(\sqrt[3]{x}\right)}^{2}\right)}{\color{blue}{\mathsf{fma}\left(x, 2, 1\right)}}}}
\] |
|---|
Final simplification0.3
\[\leadsto \frac{1}{{\left(\sqrt[3]{x}\right)}^{2} + \frac{\sqrt[3]{1 + x}}{\frac{\mathsf{fma}\left(\sqrt[3]{1 + x} - \sqrt[3]{x}, \sqrt[3]{1 + x}, {\left(\sqrt[3]{x}\right)}^{2}\right)}{\mathsf{fma}\left(x, 2, 1\right)}}}
\]