Initial program 47.6
\[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}
\]
Applied egg-rr47.6
\[\leadsto \color{blue}{\left({\left(x + 1\right)}^{\left(\frac{3}{n}\right)} - {x}^{\left(\frac{3}{n}\right)}\right) \cdot \frac{1}{{\left(x + x \cdot x\right)}^{\left({n}^{-1}\right)} + \left({\left(x + 1\right)}^{\left(\frac{2}{n}\right)} + {x}^{\left(\frac{2}{n}\right)}\right)}}
\]
Simplified47.6
\[\leadsto \color{blue}{\frac{\left({\left(1 + x\right)}^{\left(\frac{3}{n}\right)} - {x}^{\left(\frac{3}{n}\right)}\right) \cdot 1}{{\left(\left(1 + x\right) \cdot x\right)}^{\left(\frac{1}{n}\right)} + \left({x}^{\left(\frac{2}{n}\right)} + {\left(1 + x\right)}^{\left(\frac{2}{n}\right)}\right)}}
\]
Proof
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 1 x) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 8 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 8 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 x (*.f64 x x))) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 8 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (Rewrite<= unpow-1_binary64 (pow.f64 n -1))) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 8 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (pow.f64 n -1)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)) (/.f64 2 n))))): 0 points increase in error, 8 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (pow.f64 n -1)) (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (+.f64 x 1) (/.f64 2 n)) (pow.f64 x (/.f64 2 n)))))): 8 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) (/.f64 1 (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (pow.f64 n -1)) (+.f64 (pow.f64 (+.f64 x 1) (/.f64 2 n)) (pow.f64 x (/.f64 2 n))))))): 0 points increase in error, 8 points decrease in error
Taylor expanded in x around 0 47.6
\[\leadsto \frac{\color{blue}{\left(1 - e^{3 \cdot \frac{\log x}{n}}\right)} \cdot 1}{{\left(\left(1 + x\right) \cdot x\right)}^{\left(\frac{1}{n}\right)} + \left({x}^{\left(\frac{2}{n}\right)} + {\left(1 + x\right)}^{\left(\frac{2}{n}\right)}\right)}
\]
Applied egg-rr47.6
\[\leadsto \frac{\color{blue}{\frac{-\left(1 - e^{\frac{\log x}{n} \cdot 6}\right)}{-\left(1 + {\left({x}^{\left(\frac{1}{n}\right)}\right)}^{3}\right)}} \cdot 1}{{\left(\left(1 + x\right) \cdot x\right)}^{\left(\frac{1}{n}\right)} + \left({x}^{\left(\frac{2}{n}\right)} + {\left(1 + x\right)}^{\left(\frac{2}{n}\right)}\right)}
\]
Simplified1.9
\[\leadsto \frac{\color{blue}{\frac{\mathsf{expm1}\left(\frac{\log x}{n} \cdot 6\right)}{-1 - {\left({x}^{\left(\frac{1}{n}\right)}\right)}^{3}}} \cdot 1}{{\left(\left(1 + x\right) \cdot x\right)}^{\left(\frac{1}{n}\right)} + \left({x}^{\left(\frac{2}{n}\right)} + {\left(1 + x\right)}^{\left(\frac{2}{n}\right)}\right)}
\]
Proof
(/.f64 (*.f64 (/.f64 (expm1.f64 (*.f64 (/.f64 (log.f64 x) n) 6)) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6)) 1)) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 11 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (Rewrite=> sub-neg_binary64 (+.f64 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6)) (neg.f64 1))) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 11 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6)) (Rewrite=> metadata-eval -1)) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 11 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 -1 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6)))) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 10 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6))) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 1 points increase in error, 10 points decrease in error
(/.f64 (*.f64 (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6))))) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 10 points increase in error, 1 points decrease in error
(/.f64 (*.f64 (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 1 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6))))) (-.f64 -1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 1 points increase in error, 10 points decrease in error
(/.f64 (*.f64 (/.f64 (neg.f64 (-.f64 1 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6)))) (Rewrite<= unsub-neg_binary64 (+.f64 -1 (neg.f64 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 11 points decrease in error
(/.f64 (*.f64 (/.f64 (neg.f64 (-.f64 1 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6)))) (+.f64 (Rewrite<= metadata-eval (neg.f64 1)) (neg.f64 (pow.f64 (pow.f64 x (/.f64 1 n)) 3)))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (neg.f64 (-.f64 1 (exp.f64 (*.f64 (/.f64 (log.f64 x) n) 6)))) (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 1 (pow.f64 (pow.f64 x (/.f64 1 n)) 3))))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 11 points increase in error, 0 points decrease in error
Initial program 20.9
\[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}
\]
Taylor expanded in x around inf 2.0
\[\leadsto \color{blue}{\frac{e^{-1 \cdot \frac{\log \left(\frac{1}{x}\right)}{n}}}{n \cdot x}}
\]
Simplified2.0
\[\leadsto \color{blue}{\frac{e^{\frac{\log x}{n}}}{x \cdot n}}
\]
Proof
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 1 x) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (*.f64 (+.f64 1 x) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 8 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)) x) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 0 points increase in error, 8 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 x (*.f64 x x))) (/.f64 1 n)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 8 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (Rewrite<= unpow-1_binary64 (pow.f64 n -1))) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (+.f64 1 x) (/.f64 2 n))))): 8 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (pow.f64 n -1)) (+.f64 (pow.f64 x (/.f64 2 n)) (pow.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 1)) (/.f64 2 n))))): 0 points increase in error, 8 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) 1) (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (pow.f64 n -1)) (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (+.f64 x 1) (/.f64 2 n)) (pow.f64 x (/.f64 2 n)))))): 8 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 (pow.f64 (+.f64 x 1) (/.f64 3 n)) (pow.f64 x (/.f64 3 n))) (/.f64 1 (+.f64 (pow.f64 (+.f64 x (*.f64 x x)) (pow.f64 n -1)) (+.f64 (pow.f64 (+.f64 x 1) (/.f64 2 n)) (pow.f64 x (/.f64 2 n))))))): 0 points increase in error, 8 points decrease in error