Initial program 61.1
\[-\frac{1}{\frac{\pi}{4}} \cdot \log \left(\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{e^{\frac{\pi}{4} \cdot f} - e^{-\frac{\pi}{4} \cdot f}}\right)
\]
Applied sinh-undef_binary641.7
\[\leadsto -\frac{1}{\frac{\pi}{4}} \cdot \log \left(\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{\color{blue}{2 \cdot \sinh \left(\frac{\pi}{4} \cdot f\right)}}\right)
\]
Applied add-sqr-sqrt_binary641.8
\[\leadsto -\frac{1}{\frac{\pi}{4}} \cdot \log \left(\frac{\color{blue}{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}} \cdot \sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}}{2 \cdot \sinh \left(\frac{\pi}{4} \cdot f\right)}\right)
\]
Applied times-frac_binary641.8
\[\leadsto -\frac{1}{\frac{\pi}{4}} \cdot \log \color{blue}{\left(\frac{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}{2} \cdot \frac{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}
\]
Applied log-prod_binary642.0
\[\leadsto -\frac{1}{\frac{\pi}{4}} \cdot \color{blue}{\left(\log \left(\frac{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}{2}\right) + \log \left(\frac{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)\right)}
\]
Applied distribute-rgt-in_binary641.7
\[\leadsto -\color{blue}{\left(\log \left(\frac{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}{2}\right) \cdot \frac{1}{\frac{\pi}{4}} + \log \left(\frac{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right) \cdot \frac{1}{\frac{\pi}{4}}\right)}
\]
Simplified1.7
\[\leadsto -\left(\color{blue}{\frac{4}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{2}\right)} + \log \left(\frac{\sqrt{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right) \cdot \frac{1}{\frac{\pi}{4}}\right)
\]
Simplified1.7
\[\leadsto -\left(\frac{4}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{2}\right) + \color{blue}{\frac{4}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{\sinh \left(f \cdot \frac{\pi}{4}\right)}\right)}\right)
\]
Applied div-inv_binary641.7
\[\leadsto -\left(\frac{4}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{2}\right) + \color{blue}{\left(4 \cdot \frac{1}{\pi}\right)} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{\sinh \left(f \cdot \frac{\pi}{4}\right)}\right)\right)
\]
Applied associate-*l*_binary641.7
\[\leadsto -\left(\frac{4}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{2}\right) + \color{blue}{4 \cdot \left(\frac{1}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{\sinh \left(f \cdot \frac{\pi}{4}\right)}\right)\right)}\right)
\]
Simplified1.7
\[\leadsto -\left(\frac{4}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{2}\right) + 4 \cdot \color{blue}{\frac{\log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{\sinh \left(f \cdot \frac{\pi}{4}\right)}\right)}{\pi}}\right)
\]
Final simplification1.7
\[\leadsto \frac{\log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{\sinh \left(f \cdot \frac{\pi}{4}\right)}\right)}{\pi} \cdot -4 - \frac{4}{\pi} \cdot \log \left(\frac{\sqrt{e^{f \cdot \frac{\pi}{4}} + e^{-f \cdot \frac{\pi}{4}}}}{2}\right)
\]