Initial program 58.6
\[\frac{1}{2} \cdot \log \left(\frac{1 + x}{1 - x}\right)\]
Initial simplification50.5
\[\leadsto (\left(\log \left(1 - x\right)\right) \cdot \left(\frac{-1}{2}\right) + \left(\frac{\log_* (1 + x)}{2}\right))_*\]
- Using strategy
rm Applied sub-neg50.5
\[\leadsto (\left(\log \color{blue}{\left(1 + \left(-x\right)\right)}\right) \cdot \left(\frac{-1}{2}\right) + \left(\frac{\log_* (1 + x)}{2}\right))_*\]
Applied log1p-def0.0
\[\leadsto (\color{blue}{\left(\log_* (1 + \left(-x\right))\right)} \cdot \left(\frac{-1}{2}\right) + \left(\frac{\log_* (1 + x)}{2}\right))_*\]
- Using strategy
rm Applied log1p-expm1-u0.0
\[\leadsto \color{blue}{\log_* (1 + (e^{(\left(\log_* (1 + \left(-x\right))\right) \cdot \left(\frac{-1}{2}\right) + \left(\frac{\log_* (1 + x)}{2}\right))_*} - 1)^*)}\]
Final simplification0.0
\[\leadsto \log_* (1 + (e^{(\left(\log_* (1 + \left(-x\right))\right) \cdot \left(\frac{-1}{2}\right) + \left(\frac{\log_* (1 + x)}{2}\right))_*} - 1)^*)\]