Initial program 14.6
\[\frac{1}{x + 1} - \frac{1}{x}
\]
Simplified14.6
\[\leadsto \color{blue}{\frac{-1}{x} - \frac{-1}{1 + x}}
\]
Proof
(-.f64 (/.f64 -1 x) (/.f64 -1 (+.f64 1 x))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) x) (/.f64 -1 (+.f64 1 x))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 x))) (/.f64 -1 (+.f64 1 x))): 0 points increase in error, 0 points decrease in error
(-.f64 (neg.f64 (/.f64 1 x)) (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) (+.f64 1 x))): 0 points increase in error, 0 points decrease in error
(-.f64 (neg.f64 (/.f64 1 x)) (/.f64 (neg.f64 1) (Rewrite<= +-commutative_binary64 (+.f64 x 1)))): 0 points increase in error, 0 points decrease in error
(-.f64 (neg.f64 (/.f64 1 x)) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 (+.f64 x 1))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 (/.f64 1 x)) (neg.f64 (neg.f64 (/.f64 1 (+.f64 x 1)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 x)) (Rewrite=> remove-double-neg_binary64 (/.f64 1 (+.f64 x 1)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (/.f64 1 (+.f64 x 1)) (neg.f64 (/.f64 1 x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_binary64 (-.f64 (/.f64 1 (+.f64 x 1)) (/.f64 1 x))): 0 points increase in error, 0 points decrease in error
Applied egg-rr14.0
\[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left(-1, x, -1\right) - \left(-x\right)}{x}}{x + 1}}
\]
Taylor expanded in x around 0 0.1
\[\leadsto \frac{\frac{\color{blue}{-1}}{x}}{x + 1}
\]
Final simplification0.1
\[\leadsto \frac{\frac{-1}{x}}{x + 1}
\]