Initial program 14.6
\[\frac{1}{x + 1} - \frac{1}{x - 1}
\]
Applied egg-rr14.0
\[\leadsto \color{blue}{\frac{\left(\left(-x\right) + 1\right) - \left(1 + x\right) \cdot -1}{\left(1 + x\right) \cdot \left(\left(-x\right) + 1\right)}}
\]
Taylor expanded in x around 0 0.4
\[\leadsto \frac{\color{blue}{2}}{\left(1 + x\right) \cdot \left(\left(-x\right) + 1\right)}
\]
Taylor expanded in x around 0 0.4
\[\leadsto \frac{2}{\color{blue}{1 + -1 \cdot {x}^{2}}}
\]
Simplified0.4
\[\leadsto \frac{2}{\color{blue}{1 - x \cdot x}}
\]
Proof
(-.f64 1 (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= unpow2_binary64 (pow.f64 x 2))): 0 points increase in error, 1 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
Final simplification0.4
\[\leadsto \frac{2}{1 - x \cdot x}
\]