Average Error: 58.5 → 0.2
Time: 22.0s
Precision: 64
Internal Precision: 128
\[\frac{1}{2} \cdot \log \left(\frac{1 + x}{1 - x}\right)\]
↓
\[\frac{1}{2} \cdot \left(\log_* (1 + (x \cdot x + x)_*) + \left(\log_* (1 + x) + \log \left(\frac{1}{1 - {x}^{3}}\right)\right)\right)\]

Error

Bits error versus x

Derivation

  1. Initial program 58.5

    \[\frac{1}{2} \cdot \log \left(\frac{1 + x}{1 - x}\right)\]

  2. Simplified58.5

    \[\leadsto \color{blue}{\log \left(\frac{x + 1}{1 - x}\right) \cdot \frac{1}{2}}\]
  3. Using strategy rm

  4. Applied div-inv58.5

    \[\leadsto \log \color{blue}{\left(\left(x + 1\right) \cdot \frac{1}{1 - x}\right)} \cdot \frac{1}{2}\]

  5. Applied log-prod58.5

    \[\leadsto \color{blue}{\left(\log \left(x + 1\right) + \log \left(\frac{1}{1 - x}\right)\right)} \cdot \frac{1}{2}\]

  6. Simplified50.5

    \[\leadsto \left(\color{blue}{\log_* (1 + x)} + \log \left(\frac{1}{1 - x}\right)\right) \cdot \frac{1}{2}\]
  7. Using strategy rm

  8. Applied flip3--50.5

    \[\leadsto \left(\log_* (1 + x) + \log \left(\frac{1}{\color{blue}{\frac{{1}^{3} - {x}^{3}}{1 \cdot 1 + \left(x \cdot x + 1 \cdot x\right)}}}\right)\right) \cdot \frac{1}{2}\]

  9. Applied associate-/r/50.4

    \[\leadsto \left(\log_* (1 + x) + \log \color{blue}{\left(\frac{1}{{1}^{3} - {x}^{3}} \cdot \left(1 \cdot 1 + \left(x \cdot x + 1 \cdot x\right)\right)\right)}\right) \cdot \frac{1}{2}\]

  10. Applied log-prod50.4

    \[\leadsto \left(\log_* (1 + x) + \color{blue}{\left(\log \left(\frac{1}{{1}^{3} - {x}^{3}}\right) + \log \left(1 \cdot 1 + \left(x \cdot x + 1 \cdot x\right)\right)\right)}\right) \cdot \frac{1}{2}\]

  11. Applied associate-+r+50.4

    \[\leadsto \color{blue}{\left(\left(\log_* (1 + x) + \log \left(\frac{1}{{1}^{3} - {x}^{3}}\right)\right) + \log \left(1 \cdot 1 + \left(x \cdot x + 1 \cdot x\right)\right)\right)} \cdot \frac{1}{2}\]

  12. Simplified0.2

    \[\leadsto \left(\left(\log_* (1 + x) + \log \left(\frac{1}{{1}^{3} - {x}^{3}}\right)\right) + \color{blue}{\log_* (1 + (x \cdot x + x)_*)}\right) \cdot \frac{1}{2}\]

  13. Final simplification0.2

    \[\leadsto \frac{1}{2} \cdot \left(\log_* (1 + (x \cdot x + x)_*) + \left(\log_* (1 + x) + \log \left(\frac{1}{1 - {x}^{3}}\right)\right)\right)\]

Reproduce

herbie shell --seed 2019053 +o rules:numerics
(FPCore (x)
  :name "Hyperbolic arc-(co)tangent"
  (* (/ 1 2) (log (/ (+ 1 x) (- 1 x)))))