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
(/.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))): 127 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, 1 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))))))): 1 points increase in error, 0 points decrease in error
Applied egg-rr16.7
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt[3]{1 + x}\right)\right)} + \sqrt[3]{x}, {\left(\sqrt[3]{1 + x}\right)}^{2}\right)}
\]
Applied egg-rr0.5
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \color{blue}{\frac{{\left(1 + \sqrt[3]{1 + x}\right)}^{3} - 1}{\left(1 + \sqrt[3]{1 + x}\right) \cdot \left(1 + \sqrt[3]{1 + x}\right) + \left(1 + \left(1 + \sqrt[3]{1 + x}\right) \cdot 1\right)}} + \sqrt[3]{x}, {\left(\sqrt[3]{1 + x}\right)}^{2}\right)}
\]
Simplified0.5
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \color{blue}{\frac{-1 + {\left(1 + \sqrt[3]{1 + x}\right)}^{3}}{1 + \left(1 + \sqrt[3]{1 + x}\right) \cdot \left(2 + \sqrt[3]{1 + x}\right)}} + \sqrt[3]{x}, {\left(\sqrt[3]{1 + x}\right)}^{2}\right)}
\]
Proof
(/.f64 (+.f64 -1 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3)) (+.f64 1 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 2 (cbrt.f64 (+.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) -1)) (+.f64 1 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 2 (cbrt.f64 (+.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) (Rewrite<= metadata-eval (neg.f64 1))) (+.f64 1 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 2 (cbrt.f64 (+.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1)) (+.f64 1 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 2 (cbrt.f64 (+.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (+.f64 1 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 (Rewrite<= metadata-eval (+.f64 1 1)) (cbrt.f64 (+.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (+.f64 1 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (Rewrite<= associate-+r+_binary64 (+.f64 1 (+.f64 1 (cbrt.f64 (+.f64 1 x)))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (+.f64 1 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 1) (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 1 (cbrt.f64 (+.f64 1 x)))))))): 1 points increase in error, 5 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (+.f64 1 (+.f64 (Rewrite=> *-rgt-identity_binary64 (+.f64 1 (cbrt.f64 (+.f64 1 x)))) (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 1 (cbrt.f64 (+.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (+.f64 1 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 1 (cbrt.f64 (+.f64 1 x)))) (+.f64 1 (cbrt.f64 (+.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 1 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 1 (cbrt.f64 (+.f64 1 x))))) (+.f64 1 (cbrt.f64 (+.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 1 (cbrt.f64 (+.f64 1 x)))) 1)) (+.f64 1 (cbrt.f64 (+.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 1 (cbrt.f64 (+.f64 1 x)))) (+.f64 1 (+.f64 1 (cbrt.f64 (+.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 3) 1) (+.f64 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) (+.f64 1 (cbrt.f64 (+.f64 1 x)))) (+.f64 1 (Rewrite<= *-rgt-identity_binary64 (*.f64 (+.f64 1 (cbrt.f64 (+.f64 1 x))) 1))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr21.5
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \frac{-1 + \color{blue}{\frac{{\left(1 + \left(1 + x\right)\right)}^{3}}{{\left(1 + \left({\left(\sqrt[3]{1 + x}\right)}^{2} - \sqrt[3]{1 + x}\right)\right)}^{3}}}}{1 + \left(1 + \sqrt[3]{1 + x}\right) \cdot \left(2 + \sqrt[3]{1 + x}\right)} + \sqrt[3]{x}, {\left(\sqrt[3]{1 + x}\right)}^{2}\right)}
\]
Simplified0.4
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \frac{-1 + \color{blue}{{\left(\frac{x + 2}{{\left(\sqrt[3]{x + 1}\right)}^{2} + \left(1 - \sqrt[3]{x + 1}\right)}\right)}^{3}}}{1 + \left(1 + \sqrt[3]{1 + x}\right) \cdot \left(2 + \sqrt[3]{1 + x}\right)} + \sqrt[3]{x}, {\left(\sqrt[3]{1 + x}\right)}^{2}\right)}
\]
Proof
(pow.f64 (/.f64 (+.f64 x 2) (+.f64 (pow.f64 (cbrt.f64 (+.f64 x 1)) 2) (-.f64 1 (cbrt.f64 (+.f64 x 1))))) 3): 0 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 2 x)) (+.f64 (pow.f64 (cbrt.f64 (+.f64 x 1)) 2) (-.f64 1 (cbrt.f64 (+.f64 x 1))))) 3): 0 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (+.f64 (Rewrite<= metadata-eval (+.f64 1 1)) x) (+.f64 (pow.f64 (cbrt.f64 (+.f64 x 1)) 2) (-.f64 1 (cbrt.f64 (+.f64 x 1))))) 3): 0 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (Rewrite<= associate-+r+_binary64 (+.f64 1 (+.f64 1 x))) (+.f64 (pow.f64 (cbrt.f64 (+.f64 x 1)) 2) (-.f64 1 (cbrt.f64 (+.f64 x 1))))) 3): 2 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (+.f64 (pow.f64 (cbrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 x))) 2) (-.f64 1 (cbrt.f64 (+.f64 x 1))))) 3): 0 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (+.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (-.f64 1 (cbrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 x)))))) 3): 0 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) 1) (cbrt.f64 (+.f64 1 x))))) 3): 0 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2))) (cbrt.f64 (+.f64 1 x)))) 3): 0 points increase in error, 0 points decrease in error
(pow.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (Rewrite<= associate-+r-_binary64 (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))))) 3): 0 points increase in error, 0 points decrease in error
(Rewrite<= cube-unmult_binary64 (*.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x))))) (*.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x))))) (/.f64 (+.f64 1 (+.f64 1 x)) (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))))))): 13 points increase in error, 21 points decrease in error
(*.f64 (/.f64 (+.f64 1 (+.f64 1 x)) (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x))))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 1 (+.f64 1 x)) (+.f64 1 (+.f64 1 x))) (*.f64 (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))) (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))))))): 87 points increase in error, 13 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 1 (+.f64 1 x)) (*.f64 (+.f64 1 (+.f64 1 x)) (+.f64 1 (+.f64 1 x)))) (*.f64 (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))) (*.f64 (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))) (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))))))): 26 points increase in error, 13 points decrease in error
(/.f64 (Rewrite<= cube-mult_binary64 (pow.f64 (+.f64 1 (+.f64 1 x)) 3)) (*.f64 (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))) (*.f64 (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))) (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x))))))): 5 points increase in error, 6 points decrease in error
(/.f64 (pow.f64 (+.f64 1 (+.f64 1 x)) 3) (Rewrite<= cube-mult_binary64 (pow.f64 (+.f64 1 (-.f64 (pow.f64 (cbrt.f64 (+.f64 1 x)) 2) (cbrt.f64 (+.f64 1 x)))) 3))): 2 points increase in error, 6 points decrease in error
Final simplification0.4
\[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x}, \sqrt[3]{x} + \frac{-1 + {\left(\frac{x + 2}{{\left(\sqrt[3]{1 + x}\right)}^{2} + \left(1 - \sqrt[3]{1 + x}\right)}\right)}^{3}}{1 + \left(1 + \sqrt[3]{1 + x}\right) \cdot \left(2 + \sqrt[3]{1 + x}\right)}, {\left(\sqrt[3]{1 + x}\right)}^{2}\right)}
\]