Initial program 29.2
\[\frac{x}{x + 1} - \frac{x + 1}{x - 1}
\]
Applied egg-rr29.0
\[\leadsto \color{blue}{\frac{\left(x + -1\right) - \frac{x + 1}{x} \cdot \left(x + 1\right)}{\frac{x + 1}{x} \cdot \left(x + -1\right)}}
\]
Taylor expanded in x around 0 0.0
\[\leadsto \frac{\color{blue}{-\left(3 + \frac{1}{x}\right)}}{\frac{x + 1}{x} \cdot \left(x + -1\right)}
\]
Simplified0.0
\[\leadsto \frac{\color{blue}{\frac{-1}{x} + -3}}{\frac{x + 1}{x} \cdot \left(x + -1\right)}
\]
Proof
(+.f64 (/.f64 -1 x) -3): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) x) -3): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 x))) -3): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 x)) (Rewrite<= metadata-eval (neg.f64 3))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 3) (neg.f64 (/.f64 1 x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 3 (/.f64 1 x)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in x around 0 0.0
\[\leadsto \frac{\frac{-1}{x} + -3}{\color{blue}{x - \frac{1}{x}}}
\]
Final simplification0.0
\[\leadsto \frac{\frac{-1}{x} + -3}{x + \frac{-1}{x}}
\]