Initial program 0.0
\[\frac{x}{1 + \sqrt{x + 1}}
\]
Applied egg-rr58.9
\[\leadsto \color{blue}{\frac{x}{-x} \cdot 1 + \frac{x}{-x} \cdot \left(-\sqrt{x + 1}\right)}
\]
Simplified58.9
\[\leadsto \color{blue}{\sqrt{x + 1} + -1}
\]
Proof
(+.f64 (sqrt.f64 (+.f64 x 1)) -1): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 -1 (sqrt.f64 (+.f64 x 1)))): 14 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) (sqrt.f64 (+.f64 x 1))): 0 points increase in error, 14 points decrease in error
(Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 (sqrt.f64 (+.f64 x 1))))): 14 points increase in error, 0 points decrease in error
(Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 1 (sqrt.f64 (+.f64 x 1))))): 14 points increase in error, 0 points decrease in error
(Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 1 (sqrt.f64 (+.f64 x 1))))): 14 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (neg.f64 (Rewrite<= *-inverses_binary64 (/.f64 (neg.f64 x) (neg.f64 x)))) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 14 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= distribute-frac-neg_binary64 (/.f64 (neg.f64 (neg.f64 x)) (neg.f64 x))) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 (Rewrite=> remove-double-neg_binary64 x) (neg.f64 x)) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 x (neg.f64 x)) 1)) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (Rewrite=> *-rgt-identity_binary64 (/.f64 x (neg.f64 x))) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 14 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x (neg.f64 x)) (Rewrite=> sub-neg_binary64 (+.f64 1 (neg.f64 (sqrt.f64 (+.f64 x 1)))))): 14 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 x (neg.f64 x)) 1) (*.f64 (/.f64 x (neg.f64 x)) (neg.f64 (sqrt.f64 (+.f64 x 1)))))): 0 points increase in error, 14 points decrease in error
Taylor expanded in x around 0 0.3
\[\leadsto \color{blue}{-0.125 \cdot {x}^{2} + \left(0.5 \cdot x + 0.0625 \cdot {x}^{3}\right)}
\]
Simplified0.3
\[\leadsto \color{blue}{x \cdot \left(0.5 + x \cdot \left(-0.125 + x \cdot 0.0625\right)\right)}
\]
Proof
(*.f64 x (+.f64 1/2 (*.f64 x (+.f64 -1/8 (*.f64 x 1/16))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 1/2 (*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x 1/16) -1/8))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 1/2 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 x 1/16) x) (*.f64 -1/8 x))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 1/2 (+.f64 (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 1/16 x)) x) (*.f64 -1/8 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 1/2 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 1/16 (*.f64 x x))) (*.f64 -1/8 x)))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 1/2 (+.f64 (*.f64 1/16 (Rewrite<= unpow2_binary64 (pow.f64 x 2))) (*.f64 -1/8 x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 x 1/2) (*.f64 x (+.f64 (*.f64 1/16 (pow.f64 x 2)) (*.f64 -1/8 x))))): 16 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/2 x)) (*.f64 x (+.f64 (*.f64 1/16 (pow.f64 x 2)) (*.f64 -1/8 x)))): 0 points increase in error, 16 points decrease in error
(+.f64 (*.f64 1/2 x) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 1/16 (pow.f64 x 2)) x) (*.f64 (*.f64 -1/8 x) x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 x) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 1/16 (*.f64 (pow.f64 x 2) x))) (*.f64 (*.f64 -1/8 x) x))): 6 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 x) (+.f64 (*.f64 1/16 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 x x)) x)) (*.f64 (*.f64 -1/8 x) x))): 16 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 x) (+.f64 (*.f64 1/16 (Rewrite<= unpow3_binary64 (pow.f64 x 3))) (*.f64 (*.f64 -1/8 x) x))): 0 points increase in error, 16 points decrease in error
(+.f64 (*.f64 1/2 x) (+.f64 (*.f64 1/16 (pow.f64 x 3)) (Rewrite<= associate-*r*_binary64 (*.f64 -1/8 (*.f64 x x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 x) (+.f64 (*.f64 1/16 (pow.f64 x 3)) (*.f64 -1/8 (Rewrite<= unpow2_binary64 (pow.f64 x 2))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 1/2 x) (*.f64 1/16 (pow.f64 x 3))) (*.f64 -1/8 (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/8 (pow.f64 x 2)) (+.f64 (*.f64 1/2 x) (*.f64 1/16 (pow.f64 x 3))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.3
\[\leadsto \color{blue}{x \cdot \left(0.5 + x \cdot -0.125\right) + x \cdot \left(x \cdot \left(x \cdot 0.0625\right)\right)}
\]
Initial program 0.5
\[\frac{x}{1 + \sqrt{x + 1}}
\]
Applied egg-rr0.1
\[\leadsto \color{blue}{\frac{x}{-x} \cdot 1 + \frac{x}{-x} \cdot \left(-\sqrt{x + 1}\right)}
\]
Simplified0.1
\[\leadsto \color{blue}{\sqrt{x + 1} + -1}
\]
Proof
(+.f64 (sqrt.f64 (+.f64 x 1)) -1): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 -1 (sqrt.f64 (+.f64 x 1)))): 14 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) (sqrt.f64 (+.f64 x 1))): 0 points increase in error, 14 points decrease in error
(Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 (sqrt.f64 (+.f64 x 1))))): 14 points increase in error, 0 points decrease in error
(Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 1 (sqrt.f64 (+.f64 x 1))))): 14 points increase in error, 0 points decrease in error
(Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 1 (sqrt.f64 (+.f64 x 1))))): 14 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (neg.f64 (Rewrite<= *-inverses_binary64 (/.f64 (neg.f64 x) (neg.f64 x)))) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 14 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= distribute-frac-neg_binary64 (/.f64 (neg.f64 (neg.f64 x)) (neg.f64 x))) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 (Rewrite=> remove-double-neg_binary64 x) (neg.f64 x)) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 x (neg.f64 x)) 1)) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 0 points increase in error, 14 points decrease in error
(*.f64 (Rewrite=> *-rgt-identity_binary64 (/.f64 x (neg.f64 x))) (-.f64 1 (sqrt.f64 (+.f64 x 1)))): 14 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x (neg.f64 x)) (Rewrite=> sub-neg_binary64 (+.f64 1 (neg.f64 (sqrt.f64 (+.f64 x 1)))))): 14 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 x (neg.f64 x)) 1) (*.f64 (/.f64 x (neg.f64 x)) (neg.f64 (sqrt.f64 (+.f64 x 1)))))): 0 points increase in error, 14 points decrease in error