Initial program 0.0
\[-\log \left(\frac{1}{x} - 1\right)\]
- Using strategy
rm Applied add-sqr-sqrt_binary640.0
\[\leadsto -\log \left(\frac{1}{\color{blue}{\sqrt{x} \cdot \sqrt{x}}} - 1\right)\]
Applied add-sqr-sqrt_binary640.0
\[\leadsto -\log \left(\frac{\color{blue}{\sqrt{1} \cdot \sqrt{1}}}{\sqrt{x} \cdot \sqrt{x}} - 1\right)\]
Applied times-frac_binary640.0
\[\leadsto -\log \left(\color{blue}{\frac{\sqrt{1}}{\sqrt{x}} \cdot \frac{\sqrt{1}}{\sqrt{x}}} - 1\right)\]
Applied difference-of-sqr-1_binary640.0
\[\leadsto -\log \color{blue}{\left(\left(\frac{\sqrt{1}}{\sqrt{x}} + 1\right) \cdot \left(\frac{\sqrt{1}}{\sqrt{x}} - 1\right)\right)}\]
Applied log-prod_binary640.0
\[\leadsto -\color{blue}{\left(\log \left(\frac{\sqrt{1}}{\sqrt{x}} + 1\right) + \log \left(\frac{\sqrt{1}}{\sqrt{x}} - 1\right)\right)}\]
Simplified0.0
\[\leadsto -\left(\color{blue}{\log \left(1 + \frac{1}{\sqrt{x}}\right)} + \log \left(\frac{\sqrt{1}}{\sqrt{x}} - 1\right)\right)\]
Simplified0.0
\[\leadsto -\left(\log \left(1 + \frac{1}{\sqrt{x}}\right) + \color{blue}{\log \left(\frac{1}{\sqrt{x}} - 1\right)}\right)\]
- Using strategy
rm Applied add-exp-log_binary640.0
\[\leadsto -\left(\log \left(1 + \frac{1}{\color{blue}{e^{\log \left(\sqrt{x}\right)}}}\right) + \log \left(\frac{1}{\sqrt{x}} - 1\right)\right)\]
Applied 1-exp_binary640.0
\[\leadsto -\left(\log \left(1 + \frac{\color{blue}{e^{0}}}{e^{\log \left(\sqrt{x}\right)}}\right) + \log \left(\frac{1}{\sqrt{x}} - 1\right)\right)\]
Applied div-exp_binary640.0
\[\leadsto -\left(\log \left(1 + \color{blue}{e^{0 - \log \left(\sqrt{x}\right)}}\right) + \log \left(\frac{1}{\sqrt{x}} - 1\right)\right)\]
Simplified0.0
\[\leadsto -\left(\log \left(1 + e^{\color{blue}{-\log \left(\sqrt{x}\right)}}\right) + \log \left(\frac{1}{\sqrt{x}} - 1\right)\right)\]
- Using strategy
rm Applied add-sqr-sqrt_binary640.0
\[\leadsto -\left(\log \left(1 + e^{-\log \left(\sqrt{x}\right)}\right) + \log \color{blue}{\left(\sqrt{\frac{1}{\sqrt{x}} - 1} \cdot \sqrt{\frac{1}{\sqrt{x}} - 1}\right)}\right)\]
Applied log-prod_binary640.0
\[\leadsto -\left(\log \left(1 + e^{-\log \left(\sqrt{x}\right)}\right) + \color{blue}{\left(\log \left(\sqrt{\frac{1}{\sqrt{x}} - 1}\right) + \log \left(\sqrt{\frac{1}{\sqrt{x}} - 1}\right)\right)}\right)\]
Simplified0.0
\[\leadsto -\left(\log \left(1 + e^{-\log \left(\sqrt{x}\right)}\right) + \left(\color{blue}{\log \left(\sqrt{-1 + \frac{1}{\sqrt{x}}}\right)} + \log \left(\sqrt{\frac{1}{\sqrt{x}} - 1}\right)\right)\right)\]
Simplified0.0
\[\leadsto -\left(\log \left(1 + e^{-\log \left(\sqrt{x}\right)}\right) + \left(\log \left(\sqrt{-1 + \frac{1}{\sqrt{x}}}\right) + \color{blue}{\log \left(\sqrt{-1 + \frac{1}{\sqrt{x}}}\right)}\right)\right)\]
- Using strategy
rm Applied add-exp-log_binary640.0
\[\leadsto -\left(\log \left(1 + e^{-\log \left(\sqrt{x}\right)}\right) + \left(\log \left(\sqrt{-1 + \frac{1}{\sqrt{x}}}\right) + \log \color{blue}{\left(e^{\log \left(\sqrt{-1 + \frac{1}{\sqrt{x}}}\right)}\right)}\right)\right)\]
Final simplification0.0
\[\leadsto -\left(\log \left(1 + e^{-\log \left(\sqrt{x}\right)}\right) + \left(\log \left(\sqrt{-1 + \frac{1}{\sqrt{x}}}\right) + \log \left(e^{\log \left(\sqrt{-1 + \frac{1}{\sqrt{x}}}\right)}\right)\right)\right)\]