Average Error: 0.0 → 0.0
Time: 4.5m
Precision: 64
Internal Precision: 128
\[\log \left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{x}\right)\]
↓
\[\log \left(\sqrt{1 + x \cdot x} \cdot \left(\left(\sqrt{1 - x \cdot x} \cdot \sqrt{1 - x \cdot x} + \sqrt{1 - x \cdot x}\right) + 1\right)\right) + \left(\log \left((\left(1 - x \cdot x\right) \cdot \left(\sqrt{1 - x \cdot x}\right) + 1)_*\right) - \log \left(\left(\left(\sqrt{1 - \left(x \cdot x\right) \cdot \left(x \cdot x\right)} \cdot \sqrt{1 - x \cdot x}\right) \cdot \left(\left(\sqrt{1 - x \cdot x} \cdot \sqrt{1 - x \cdot x} + \sqrt{1 - x \cdot x}\right) + 1\right) + \left(1 - {\left(\sqrt{1 - x \cdot x}\right)}^{3}\right) \cdot \sqrt{1 + x \cdot x}\right) \cdot x\right)\right)\]

Error

Bits error versus x

Derivation

  1. Initial program 0.0

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

  3. Applied div-inv0.1

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

  4. Applied distribute-rgt1-in0.1

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

  6. Applied flip3-+0.1

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

  7. Applied frac-times0.1

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

  8. Applied log-div0.2

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

  9. Simplified0.2

    \[\leadsto \color{blue}{\log \left((\left(1 - x \cdot x\right) \cdot \left(\sqrt{1 - x \cdot x}\right) + 1)_*\right)} - \log \left(\left(\sqrt{1 - x \cdot x} \cdot \sqrt{1 - x \cdot x} + \left(1 \cdot 1 - \sqrt{1 - x \cdot x} \cdot 1\right)\right) \cdot x\right)\]
  10. Using strategy rm

  11. Applied flip3--0.2

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

  12. Applied flip--0.2

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

  13. Applied sqrt-div0.2

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

  14. Applied associate-*r/0.2

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

  15. Applied frac-add0.2

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

  16. Applied associate-*l/0.2

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

  17. Applied log-div0.0

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

  18. Applied associate--r-0.0

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

  19. Final simplification0.0

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

Reproduce

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