Initial program 100.0%
\[\log \left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{x}\right)
\]
Step-by-step derivation
expm1-log1p-u100.0%
\[\leadsto \log \color{blue}{\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{x}\right)\right)\right)}
\]
expm1-udef100.0%
\[\leadsto \log \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{1}{x} + \frac{\sqrt{1 - x \cdot x}}{x}\right)} - 1\right)}
\]
+-commutative100.0%
\[\leadsto \log \left(e^{\mathsf{log1p}\left(\color{blue}{\frac{\sqrt{1 - x \cdot x}}{x} + \frac{1}{x}}\right)} - 1\right)
\]
div-inv100.0%
\[\leadsto \log \left(e^{\mathsf{log1p}\left(\color{blue}{\sqrt{1 - x \cdot x} \cdot \frac{1}{x}} + \frac{1}{x}\right)} - 1\right)
\]
*-un-lft-identity100.0%
\[\leadsto \log \left(e^{\mathsf{log1p}\left(\sqrt{1 - x \cdot x} \cdot \frac{1}{x} + \color{blue}{1 \cdot \frac{1}{x}}\right)} - 1\right)
\]
distribute-rgt-out100.0%
\[\leadsto \log \left(e^{\mathsf{log1p}\left(\color{blue}{\frac{1}{x} \cdot \left(\sqrt{1 - x \cdot x} + 1\right)}\right)} - 1\right)
\]
Applied egg-rr100.0%
\[\leadsto \log \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{1}{x} \cdot \left(\sqrt{1 - x \cdot x} + 1\right)\right)} - 1\right)}
\]
Step-by-step derivation
expm1-def100.0%
\[\leadsto \log \color{blue}{\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{x} \cdot \left(\sqrt{1 - x \cdot x} + 1\right)\right)\right)\right)}
\]
expm1-log1p100.0%
\[\leadsto \log \color{blue}{\left(\frac{1}{x} \cdot \left(\sqrt{1 - x \cdot x} + 1\right)\right)}
\]
associate-*l/100.0%
\[\leadsto \log \color{blue}{\left(\frac{1 \cdot \left(\sqrt{1 - x \cdot x} + 1\right)}{x}\right)}
\]
*-lft-identity100.0%
\[\leadsto \log \left(\frac{\color{blue}{\sqrt{1 - x \cdot x} + 1}}{x}\right)
\]
+-commutative100.0%
\[\leadsto \log \left(\frac{\color{blue}{1 + \sqrt{1 - x \cdot x}}}{x}\right)
\]
Simplified100.0%
\[\leadsto \log \color{blue}{\left(\frac{1 + \sqrt{1 - x \cdot x}}{x}\right)}
\]
Final simplification100.0%
\[\leadsto \log \left(\frac{1 + \sqrt{1 - x \cdot x}}{x}\right)
\]