Initial program 29.8
\[\sqrt[3]{x + 1} - \sqrt[3]{x}
\]
Applied egg-rr29.2
\[\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
(/.f64 1 (fma.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 1 x)) (cbrt.f64 x)) (pow.f64 (cbrt.f64 (+.f64 1 x)) 2))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= metadata-eval (+.f64 1 0)) (fma.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 1 x)) (cbrt.f64 x)) (pow.f64 (cbrt.f64 (+.f64 1 x)) 2))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 1 (Rewrite<= +-inverses_binary64 (-.f64 x x))) (fma.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 1 x)) (cbrt.f64 x)) (pow.f64 (cbrt.f64 (+.f64 1 x)) 2))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 1 x) x)) (fma.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 1 x)) (cbrt.f64 x)) (pow.f64 (cbrt.f64 (+.f64 1 x)) 2))): 114 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)) x) (fma.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 1 x)) (cbrt.f64 x)) (pow.f64 (cbrt.f64 (+.f64 1 x)) 2))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 x 1) x) (fma.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1))) (cbrt.f64 x)) (pow.f64 (cbrt.f64 (+.f64 1 x)) 2))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 x 1) x) (fma.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x)) (pow.f64 (cbrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1))) 2))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 x 1) x) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x))) (pow.f64 (cbrt.f64 (+.f64 x 1)) 2)))): 1 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 x 1) x) (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (cbrt.f64 (+.f64 x 1)) 2) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 (+.f64 x 1) x) 1)) (+.f64 (pow.f64 (cbrt.f64 (+.f64 x 1)) 2) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 (+.f64 x 1) x) (/.f64 1 (+.f64 (pow.f64 (cbrt.f64 (+.f64 x 1)) 2) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x))))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr17.3
\[\leadsto \frac{1}{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{1 + x} + \sqrt[3]{x}, e^{0.6666666666666666 \cdot \mathsf{log1p}\left(x\right)}\right)\right)\right)}}
\]
Applied egg-rr0.5
\[\leadsto \frac{1}{\color{blue}{\mathsf{fma}\left(\sqrt[3]{x + 1}, \sqrt[3]{x + 1}, \sqrt[3]{x} \cdot \left(\sqrt[3]{x} + \sqrt[3]{x + 1}\right)\right)}}
\]
Simplified0.5
\[\leadsto \frac{1}{\color{blue}{{\left(\sqrt[3]{1 + x}\right)}^{2} + \sqrt[3]{x} \cdot \left(\sqrt[3]{x} + \sqrt[3]{1 + x}\right)}}
\]
Proof
(+.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 x) (cbrt.f64 (+.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 (cbrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1))) 2) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 x) (cbrt.f64 (+.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> unpow2_binary64 (*.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 (+.f64 x 1)))) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 x) (cbrt.f64 (+.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 (+.f64 x 1))) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 x) (cbrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-udef_binary64 (fma.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 (+.f64 x 1)) (*.f64 (cbrt.f64 x) (+.f64 (cbrt.f64 x) (cbrt.f64 (+.f64 x 1)))))): 12 points increase in error, 8 points decrease in error
Applied egg-rr7.6
\[\leadsto \frac{1}{{\left(\sqrt[3]{1 + x}\right)}^{2} + \color{blue}{\frac{\left(x + \left(x + 1\right)\right) \cdot \sqrt[3]{x}}{{\left(\sqrt[3]{x}\right)}^{2} + \sqrt[3]{x + 1} \cdot \left(\sqrt[3]{x + 1} - \sqrt[3]{x}\right)}}}
\]
Simplified0.2
\[\leadsto \frac{1}{{\left(\sqrt[3]{1 + x}\right)}^{2} + \color{blue}{\frac{\sqrt[3]{x}}{\frac{{\left(\sqrt[3]{x}\right)}^{2} + \sqrt[3]{x + 1} \cdot \left(\sqrt[3]{x + 1} - \sqrt[3]{x}\right)}{x + \left(x + 1\right)}}}}
\]
Proof
(/.f64 (cbrt.f64 x) (/.f64 (+.f64 (pow.f64 (cbrt.f64 x) 2) (*.f64 (cbrt.f64 (+.f64 x 1)) (-.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x)))) (+.f64 x (+.f64 x 1)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (cbrt.f64 x) (+.f64 x (+.f64 x 1))) (+.f64 (pow.f64 (cbrt.f64 x) 2) (*.f64 (cbrt.f64 (+.f64 x 1)) (-.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x)))))): 47 points increase in error, 18 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 x (+.f64 x 1)) (cbrt.f64 x))) (+.f64 (pow.f64 (cbrt.f64 x) 2) (*.f64 (cbrt.f64 (+.f64 x 1)) (-.f64 (cbrt.f64 (+.f64 x 1)) (cbrt.f64 x))))): 0 points increase in error, 0 points decrease in error
Final simplification0.2
\[\leadsto \frac{1}{{\left(\sqrt[3]{1 + x}\right)}^{2} + \frac{\sqrt[3]{x}}{\frac{{\left(\sqrt[3]{x}\right)}^{2} + \sqrt[3]{1 + x} \cdot \left(\sqrt[3]{1 + x} - \sqrt[3]{x}\right)}{x + \left(1 + x\right)}}}
\]