Initial program 9.7
\[\left(\frac{1}{x + 1} - \frac{2}{x}\right) + \frac{1}{x - 1}
\]
Simplified9.7
\[\leadsto \color{blue}{\frac{1}{1 + x} + \left(\frac{1}{x + -1} + \frac{-2}{x}\right)}
\]
Proof
(+.f64 (/.f64 1 (+.f64 1 x)) (+.f64 (/.f64 1 (+.f64 x -1)) (/.f64 -2 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 (Rewrite<= +-commutative_binary64 (+.f64 x 1))) (+.f64 (/.f64 1 (+.f64 x -1)) (/.f64 -2 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 (+.f64 x 1)) (+.f64 (/.f64 1 (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (/.f64 -2 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 (+.f64 x 1)) (+.f64 (/.f64 1 (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (/.f64 -2 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 (+.f64 x 1)) (+.f64 (/.f64 1 (-.f64 x 1)) (/.f64 (Rewrite<= metadata-eval (neg.f64 2)) x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 (+.f64 x 1)) (+.f64 (/.f64 1 (-.f64 x 1)) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 2 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 (+.f64 x 1)) (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 2 x)) (/.f64 1 (-.f64 x 1))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (/.f64 1 (+.f64 x 1)) (neg.f64 (/.f64 2 x))) (/.f64 1 (-.f64 x 1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 1 (+.f64 x 1)) (/.f64 2 x))) (/.f64 1 (-.f64 x 1))): 0 points increase in error, 0 points decrease in error
Applied egg-rr25.9
\[\leadsto \frac{1}{1 + x} + \color{blue}{\frac{\left(1 - x\right) + \left(x \cdot -0.5\right) \cdot -1}{\left(x \cdot -0.5\right) \cdot \left(1 - x\right)}}
\]
Applied egg-rr9.7
\[\leadsto \color{blue}{\frac{\left(1 - x\right) + \left(1 + x\right) \cdot \frac{\mathsf{fma}\left(x, 0.5, 1 - x\right)}{x \cdot -0.5}}{\left(1 + x\right) \cdot \left(1 - x\right)}}
\]
Taylor expanded in x around 0 0.1
\[\leadsto \frac{\color{blue}{\frac{-2}{x}}}{\left(1 + x\right) \cdot \left(1 - x\right)}
\]
Final simplification0.1
\[\leadsto \frac{\frac{-2}{x}}{\left(x + 1\right) \cdot \left(1 - x\right)}
\]