Error

Try it out

Derivation

1. Initial program 58.5

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

3. Applied add-exp-log58.5

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

4. Applied add-exp-log58.5

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

5. Applied div-exp58.5

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

6. Applied simplify58.5

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

8. Applied flip--58.5

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

9. Applied log-div58.5

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

10. Applied associate--r-58.5

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

11. Applied exp-sum58.5

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

12. Applied log-prod58.5

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

13. Applied simplify50.4

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

14. Applied simplify0.6

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

16. Applied log1p-expm1-u0.6

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

17. Applied simplify0.0

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

Runtime

Time bar (total: 3.1m)Debug logProfile

herbie shell --seed '#(1072936661 1621281212 3440817831 3219514234 460296804 1258167384)' +o rules:numerics
(FPCore (x)
  :name "Hyperbolic arc-(co)tangent"
  (* (/ 1 2) (log (/ (+ 1 x) (- 1 x)))))