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

↓

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

double f(double x) {
        double r9296632 = 1.0;
        double r9296633 = x;
        double r9296634 = r9296632 / r9296633;
        double r9296635 = r9296633 * r9296633;
        double r9296636 = r9296632 - r9296635;
        double r9296637 = sqrt(r9296636);
        double r9296638 = r9296637 / r9296633;
        double r9296639 = r9296634 + r9296638;
        double r9296640 = log(r9296639);
        return r9296640;
}

↓

double f(double x) {
        double r9296641 = 1.0;
        double r9296642 = x;
        double r9296643 = r9296642 * r9296642;
        double r9296644 = r9296641 - r9296643;
        double r9296645 = sqrt(r9296644);
        double r9296646 = r9296645 + r9296641;
        double r9296647 = r9296641 / r9296642;
        double r9296648 = r9296646 * r9296647;
        double r9296649 = log(r9296648);
        return r9296649;
}

\log \left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{x}\right)

↓

\log \left(\left(\sqrt{1 - x \cdot x} + 1\right) \cdot \frac{1}{x}\right)

Derivation

Initial program 0.0
\[\log \left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{x}\right)\]
Using strategy rm
Applied div-inv0.0
\[\leadsto \log \left(\frac{1}{x} + \color{blue}{\sqrt{1 - x \cdot x} \cdot \frac{1}{x}}\right)\]
Applied *-un-lft-identity0.0
\[\leadsto \log \left(\color{blue}{1 \cdot \frac{1}{x}} + \sqrt{1 - x \cdot x} \cdot \frac{1}{x}\right)\]
Applied distribute-rgt-out0.0
\[\leadsto \log \color{blue}{\left(\frac{1}{x} \cdot \left(1 + \sqrt{1 - x \cdot x}\right)\right)}\]
Final simplification0.0
\[\leadsto \log \left(\left(\sqrt{1 - x \cdot x} + 1\right) \cdot \frac{1}{x}\right)\]

Reproduce

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

Error

Derivation

Reproduce