VandenBroeck and Keller, Equation (20)

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]
6. Step-by-step derivation

   1. cosh-def97.4%

      \[\leadsto -\frac{\log \left(\frac{\color{blue}{\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{2}}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   2. cosh-undef97.4%

      \[\leadsto -\frac{\log \left(\frac{\frac{\color{blue}{2 \cdot \cosh \left(\frac{\pi}{4} \cdot f\right)}}{2}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   3. associate-*l/97.4%

      \[\leadsto -\frac{\log \left(\frac{\frac{2 \cdot \cosh \color{blue}{\left(\frac{\pi \cdot f}{4}\right)}}{2}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   4. associate-*l/97.4%

      \[\leadsto -\frac{\log \left(\frac{\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2}}{\sinh \color{blue}{\left(\frac{\pi \cdot f}{4}\right)}}\right)}{0.25 \cdot \pi} \]

   5. associate-/r*97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{0.25 \cdot \pi} \]

   6. *-commutative97.4%

      \[\leadsto -\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\color{blue}{\pi \cdot 0.25}} \]

   7. expm1-log1p-u96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   8. expm1-udef96.1%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]

7. Applied egg-rr97.5%

   \[\leadsto -\color{blue}{\left(\left(1 + \frac{\log \left(\frac{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)}{\pi \cdot 0.25}\right) - 1\right)} \]

8. Final simplification97.5%

   \[\leadsto 1 - \left(1 + \frac{\log \left(\frac{\cosh \left(f \cdot \left(\pi \cdot 0.25\right)\right)}{\sinh \left(f \cdot \left(\pi \cdot 0.25\right)\right)}\right)}{\pi \cdot 0.25}\right) \]

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]
6. Step-by-step derivation

   1. clear-num97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{1}{\frac{\sinh \left(\frac{\pi}{4} \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}}\right)}}{0.25 \cdot \pi} \]

   2. log-rec97.5%

      \[\leadsto -\frac{\color{blue}{-\log \left(\frac{\sinh \left(\frac{\pi}{4} \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}\right)}}{0.25 \cdot \pi} \]

   3. div-inv97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\color{blue}{\left(\pi \cdot \frac{1}{4}\right)} \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   4. metadata-eval97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\left(\pi \cdot \color{blue}{0.25}\right) \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   5. div-inv97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\color{blue}{\left(\pi \cdot \frac{1}{4}\right)} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   6. metadata-eval97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot \color{blue}{0.25}\right) \cdot f\right)}\right)}{0.25 \cdot \pi} \]

7. Applied egg-rr97.5%

   \[\leadsto -\frac{\color{blue}{-\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)}}{0.25 \cdot \pi} \]
8. Step-by-step derivation

   1. distribute-frac-neg97.5%

      \[\leadsto -\color{blue}{\left(-\frac{\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)}{0.25 \cdot \pi}\right)} \]

   2. neg-sub097.5%

      \[\leadsto -\color{blue}{\left(0 - \frac{\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)}{0.25 \cdot \pi}\right)} \]

   3. add-sqr-sqrt0.0%

      \[\leadsto -\left(0 - \frac{\color{blue}{\sqrt{\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)} \cdot \sqrt{\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)}}}{0.25 \cdot \pi}\right) \]

9. Applied egg-rr79.2%

   \[\leadsto -\color{blue}{\left(0 - \log \left({\left(\frac{\sinh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}{\cosh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}\right)}^{\left(\frac{4}{\pi}\right)}\right)\right)} \]
10. Step-by-step derivation

    1. neg-sub079.2%

       \[\leadsto -\color{blue}{\left(-\log \left({\left(\frac{\sinh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}{\cosh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}\right)}^{\left(\frac{4}{\pi}\right)}\right)\right)} \]

    2. log-pow97.4%

       \[\leadsto -\left(-\color{blue}{\frac{4}{\pi} \cdot \log \left(\frac{\sinh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}{\cosh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}\right)}\right) \]

    3. *-commutative97.4%

       \[\leadsto -\left(-\color{blue}{\log \left(\frac{\sinh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}{\cosh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}\right) \cdot \frac{4}{\pi}}\right) \]

    4. distribute-rgt-neg-in97.4%

       \[\leadsto -\color{blue}{\log \left(\frac{\sinh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}{\cosh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}\right) \cdot \left(-\frac{4}{\pi}\right)} \]

    5. *-commutative97.4%

       \[\leadsto -\log \left(\frac{\sinh \color{blue}{\left(\left(0.25 \cdot f\right) \cdot \pi\right)}}{\cosh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}\right) \cdot \left(-\frac{4}{\pi}\right) \]

    6. associate-*r*97.4%

       \[\leadsto -\log \left(\frac{\sinh \color{blue}{\left(0.25 \cdot \left(f \cdot \pi\right)\right)}}{\cosh \left(\pi \cdot \left(0.25 \cdot f\right)\right)}\right) \cdot \left(-\frac{4}{\pi}\right) \]

    7. *-commutative97.4%

       \[\leadsto -\log \left(\frac{\sinh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}{\cosh \color{blue}{\left(\left(0.25 \cdot f\right) \cdot \pi\right)}}\right) \cdot \left(-\frac{4}{\pi}\right) \]

    8. associate-*r*97.4%

       \[\leadsto -\log \left(\frac{\sinh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}{\cosh \color{blue}{\left(0.25 \cdot \left(f \cdot \pi\right)\right)}}\right) \cdot \left(-\frac{4}{\pi}\right) \]

    9. distribute-neg-frac97.4%

       \[\leadsto -\log \left(\frac{\sinh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}{\cosh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}\right) \cdot \color{blue}{\frac{-4}{\pi}} \]

    10. metadata-eval97.4%

        \[\leadsto -\log \left(\frac{\sinh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}{\cosh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}\right) \cdot \frac{\color{blue}{-4}}{\pi} \]

11. Simplified97.4%

    \[\leadsto -\color{blue}{\log \left(\frac{\sinh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}{\cosh \left(0.25 \cdot \left(f \cdot \pi\right)\right)}\right) \cdot \frac{-4}{\pi}} \]

12. Final simplification97.4%

    \[\leadsto \log \left(\frac{\sinh \left(0.25 \cdot \left(\pi \cdot f\right)\right)}{\cosh \left(0.25 \cdot \left(\pi \cdot f\right)\right)}\right) \cdot \frac{--4}{\pi} \]

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]

6. Final simplification97.4%

   \[\leadsto \frac{-\log \left(\frac{\cosh \left(f \cdot \frac{\pi}{4}\right)}{\sinh \left(f \cdot \frac{\pi}{4}\right)}\right)}{\pi \cdot 0.25} \]

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]
6. Step-by-step derivation

   1. clear-num97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{1}{\frac{\sinh \left(\frac{\pi}{4} \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}}\right)}}{0.25 \cdot \pi} \]

   2. log-rec97.5%

      \[\leadsto -\frac{\color{blue}{-\log \left(\frac{\sinh \left(\frac{\pi}{4} \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}\right)}}{0.25 \cdot \pi} \]

   3. div-inv97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\color{blue}{\left(\pi \cdot \frac{1}{4}\right)} \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   4. metadata-eval97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\left(\pi \cdot \color{blue}{0.25}\right) \cdot f\right)}{\cosh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   5. div-inv97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\color{blue}{\left(\pi \cdot \frac{1}{4}\right)} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   6. metadata-eval97.5%

      \[\leadsto -\frac{-\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot \color{blue}{0.25}\right) \cdot f\right)}\right)}{0.25 \cdot \pi} \]

7. Applied egg-rr97.5%

   \[\leadsto -\frac{\color{blue}{-\log \left(\frac{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)}}{0.25 \cdot \pi} \]

8. Final simplification97.5%

   \[\leadsto \frac{\log \left(\frac{\sinh \left(f \cdot \left(\pi \cdot 0.25\right)\right)}{\cosh \left(f \cdot \left(\pi \cdot 0.25\right)\right)}\right)}{\pi \cdot 0.25} \]

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]

6. Taylor expanded in f around 0 96.1%

   \[\leadsto -\frac{\log \color{blue}{\left(\frac{4}{f \cdot \pi}\right)}}{0.25 \cdot \pi} \]
7. Step-by-step derivation

   1. add-sqr-sqrt95.6%

      \[\leadsto -\frac{\color{blue}{\sqrt{\log \left(\frac{4}{f \cdot \pi}\right)} \cdot \sqrt{\log \left(\frac{4}{f \cdot \pi}\right)}}}{0.25 \cdot \pi} \]

   2. sqrt-unprod96.2%

      \[\leadsto -\frac{\color{blue}{\sqrt{\log \left(\frac{4}{f \cdot \pi}\right) \cdot \log \left(\frac{4}{f \cdot \pi}\right)}}}{0.25 \cdot \pi} \]

   3. pow296.2%

      \[\leadsto -\frac{\sqrt{\color{blue}{{\log \left(\frac{4}{f \cdot \pi}\right)}^{2}}}}{0.25 \cdot \pi} \]

   4. *-commutative96.2%

      \[\leadsto -\frac{\sqrt{{\log \left(\frac{4}{\color{blue}{\pi \cdot f}}\right)}^{2}}}{0.25 \cdot \pi} \]

8. Applied egg-rr96.2%

   \[\leadsto -\frac{\color{blue}{\sqrt{{\log \left(\frac{4}{\pi \cdot f}\right)}^{2}}}}{0.25 \cdot \pi} \]
9. Step-by-step derivation

   1. unpow296.2%

      \[\leadsto -\frac{\sqrt{\color{blue}{\log \left(\frac{4}{\pi \cdot f}\right) \cdot \log \left(\frac{4}{\pi \cdot f}\right)}}}{0.25 \cdot \pi} \]

   2. rem-sqrt-square96.2%

      \[\leadsto -\frac{\color{blue}{\left|\log \left(\frac{4}{\pi \cdot f}\right)\right|}}{0.25 \cdot \pi} \]

   3. *-commutative96.2%

      \[\leadsto -\frac{\left|\log \left(\frac{4}{\color{blue}{f \cdot \pi}}\right)\right|}{0.25 \cdot \pi} \]

10. Simplified96.2%

    \[\leadsto -\frac{\color{blue}{\left|\log \left(\frac{4}{f \cdot \pi}\right)\right|}}{0.25 \cdot \pi} \]

11. Final simplification96.2%

    \[\leadsto \frac{-\left|\log \left(\frac{4}{\pi \cdot f}\right)\right|}{\pi \cdot 0.25} \]

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]
6. Step-by-step derivation

   1. cosh-def97.4%

      \[\leadsto -\frac{\log \left(\frac{\color{blue}{\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{2}}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   2. cosh-undef97.4%

      \[\leadsto -\frac{\log \left(\frac{\frac{\color{blue}{2 \cdot \cosh \left(\frac{\pi}{4} \cdot f\right)}}{2}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   3. associate-*l/97.4%

      \[\leadsto -\frac{\log \left(\frac{\frac{2 \cdot \cosh \color{blue}{\left(\frac{\pi \cdot f}{4}\right)}}{2}}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi} \]

   4. associate-*l/97.4%

      \[\leadsto -\frac{\log \left(\frac{\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2}}{\sinh \color{blue}{\left(\frac{\pi \cdot f}{4}\right)}}\right)}{0.25 \cdot \pi} \]

   5. associate-/r*97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{0.25 \cdot \pi} \]

   6. *-commutative97.4%

      \[\leadsto -\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\color{blue}{\pi \cdot 0.25}} \]

   7. expm1-log1p-u96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   8. expm1-udef96.1%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]

7. Applied egg-rr97.5%

   \[\leadsto -\color{blue}{\left(\left(1 + \frac{\log \left(\frac{\cosh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}{\sinh \left(\left(\pi \cdot 0.25\right) \cdot f\right)}\right)}{\pi \cdot 0.25}\right) - 1\right)} \]

8. Taylor expanded in f around 0 96.1%

   \[\leadsto -\left(\left(1 + \frac{\log \color{blue}{\left(\frac{4}{f \cdot \pi}\right)}}{\pi \cdot 0.25}\right) - 1\right) \]

9. Final simplification96.1%

   \[\leadsto 1 + \left(-1 - \frac{\log \left(\frac{4}{\pi \cdot f}\right)}{\pi \cdot 0.25}\right) \]

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]

6. Taylor expanded in f around 0 96.1%

   \[\leadsto -\frac{\log \color{blue}{\left(\frac{4}{f \cdot \pi}\right)}}{0.25 \cdot \pi} \]
7. Step-by-step derivation

   1. div-inv96.0%

      \[\leadsto -\color{blue}{\log \left(\frac{4}{f \cdot \pi}\right) \cdot \frac{1}{0.25 \cdot \pi}} \]

   2. *-commutative96.0%

      \[\leadsto -\log \left(\frac{4}{\color{blue}{\pi \cdot f}}\right) \cdot \frac{1}{0.25 \cdot \pi} \]

   3. *-commutative96.0%

      \[\leadsto -\log \left(\frac{4}{\pi \cdot f}\right) \cdot \frac{1}{\color{blue}{\pi \cdot 0.25}} \]

   4. inv-pow96.0%

      \[\leadsto -\log \left(\frac{4}{\pi \cdot f}\right) \cdot \color{blue}{{\left(\pi \cdot 0.25\right)}^{-1}} \]

   5. *-commutative96.0%

      \[\leadsto -\log \left(\frac{4}{\pi \cdot f}\right) \cdot {\color{blue}{\left(0.25 \cdot \pi\right)}}^{-1} \]

   6. unpow-prod-down96.0%

      \[\leadsto -\log \left(\frac{4}{\pi \cdot f}\right) \cdot \color{blue}{\left({0.25}^{-1} \cdot {\pi}^{-1}\right)} \]

   7. metadata-eval96.0%

      \[\leadsto -\log \left(\frac{4}{\pi \cdot f}\right) \cdot \left(\color{blue}{4} \cdot {\pi}^{-1}\right) \]

   8. inv-pow96.0%

      \[\leadsto -\log \left(\frac{4}{\pi \cdot f}\right) \cdot \left(4 \cdot \color{blue}{\frac{1}{\pi}}\right) \]

8. Applied egg-rr96.0%

   \[\leadsto -\color{blue}{\log \left(\frac{4}{\pi \cdot f}\right) \cdot \left(4 \cdot \frac{1}{\pi}\right)} \]
9. Step-by-step derivation

   1. *-commutative96.0%

      \[\leadsto -\color{blue}{\left(4 \cdot \frac{1}{\pi}\right) \cdot \log \left(\frac{4}{\pi \cdot f}\right)} \]

   2. associate-*r/96.0%

      \[\leadsto -\color{blue}{\frac{4 \cdot 1}{\pi}} \cdot \log \left(\frac{4}{\pi \cdot f}\right) \]

   3. metadata-eval96.0%

      \[\leadsto -\frac{\color{blue}{4}}{\pi} \cdot \log \left(\frac{4}{\pi \cdot f}\right) \]

   4. *-commutative96.0%

      \[\leadsto -\frac{4}{\pi} \cdot \log \left(\frac{4}{\color{blue}{f \cdot \pi}}\right) \]

10. Simplified96.0%

    \[\leadsto -\color{blue}{\frac{4}{\pi} \cdot \log \left(\frac{4}{f \cdot \pi}\right)} \]

11. Final simplification96.0%

    \[\leadsto \log \left(\frac{4}{\pi \cdot f}\right) \cdot \frac{-4}{\pi} \]

1. Initial program 7.9%

   \[-\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) \]
2. Step-by-step derivation

   1. expm1-log1p-u7.9%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\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)\right)\right)} \]

   2. expm1-udef7.9%

      \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\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)\right)} - 1\right)} \]

3. Applied egg-rr96.1%

   \[\leadsto -\color{blue}{\left(e^{\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)} - 1\right)} \]
4. Step-by-step derivation

   1. expm1-def96.1%

      \[\leadsto -\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}\right)\right)} \]

   2. expm1-log1p97.4%

      \[\leadsto -\color{blue}{\frac{\log \left(\frac{2 \cdot \cosh \left(\frac{\pi \cdot f}{4}\right)}{2 \cdot \sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25}} \]

   3. times-frac97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{2}{2} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   4. metadata-eval97.4%

      \[\leadsto -\frac{\log \left(\color{blue}{1} \cdot \frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   5. *-lft-identity97.4%

      \[\leadsto -\frac{\log \color{blue}{\left(\frac{\cosh \left(\frac{\pi \cdot f}{4}\right)}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}}{\pi \cdot 0.25} \]

   6. associate-/l*97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   7. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}{\sinh \left(\frac{\pi \cdot f}{4}\right)}\right)}{\pi \cdot 0.25} \]

   8. associate-/l*97.1%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{\frac{4}{f}}\right)}}\right)}{\pi \cdot 0.25} \]

   9. associate-/r/97.4%

      \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \color{blue}{\left(\frac{\pi}{4} \cdot f\right)}}\right)}{\pi \cdot 0.25} \]

   10. *-commutative97.4%

       \[\leadsto -\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{\color{blue}{0.25 \cdot \pi}} \]

5. Simplified97.4%

   \[\leadsto -\color{blue}{\frac{\log \left(\frac{\cosh \left(\frac{\pi}{4} \cdot f\right)}{\sinh \left(\frac{\pi}{4} \cdot f\right)}\right)}{0.25 \cdot \pi}} \]

6. Taylor expanded in f around 0 96.1%

   \[\leadsto -\frac{\log \color{blue}{\left(\frac{4}{f \cdot \pi}\right)}}{0.25 \cdot \pi} \]

7. Final simplification96.1%

   \[\leadsto \frac{-\log \left(\frac{4}{\pi \cdot f}\right)}{\pi \cdot 0.25} \]

herbie shell --seed 2023166 
(FPCore (f)
  :name "VandenBroeck and Keller, Equation (20)"
  :precision binary64
  (- (* (/ 1.0 (/ PI 4.0)) (log (/ (+ (exp (* (/ PI 4.0) f)) (exp (- (* (/ PI 4.0) f)))) (- (exp (* (/ PI 4.0) f)) (exp (- (* (/ PI 4.0) f)))))))))