Initial program 46.23
\[\sqrt[3]{x + 1} - \sqrt[3]{x}
\]
Applied egg-rr45.18
\[\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.82
\[\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]45.18 | \[ \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/ [=>]45.18 | \[ \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 [=>]45.18 | \[ \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 [=>]45.18 | \[ \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.83 | \[ \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.83 | \[ \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.83 | \[ \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.83 | \[ \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.82 | \[ \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.82 | \[ \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.82 | \[ \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-rr26.72
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\color{blue}{\left(e^{\mathsf{log1p}\left(x\right) \cdot 0.3333333333333333}\right)}}^{2}\right)}
\]
Simplified26.49
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\color{blue}{\left(\sqrt[3]{e^{\mathsf{log1p}\left(x\right)}}\right)}}^{2}\right)}
\]
Proof
[Start]26.72 | \[ \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\left(e^{\mathsf{log1p}\left(x\right) \cdot 0.3333333333333333}\right)}^{2}\right)}
\] |
|---|
exp-prod [=>]26.66 | \[ \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\color{blue}{\left({\left(e^{\mathsf{log1p}\left(x\right)}\right)}^{0.3333333333333333}\right)}}^{2}\right)}
\] |
|---|
unpow1/3 [=>]26.49 | \[ \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\color{blue}{\left(\sqrt[3]{e^{\mathsf{log1p}\left(x\right)}}\right)}}^{2}\right)}
\] |
|---|
Applied egg-rr0.86
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, {\left(\sqrt[3]{\color{blue}{{\left(\sqrt[3]{x + 1}\right)}^{3}}}\right)}^{2}\right)}
\]
Final simplification0.86
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{x} + \sqrt[3]{1 + x}, {\left(\sqrt[3]{{\left(\sqrt[3]{1 + x}\right)}^{3}}\right)}^{2}\right)}
\]