Simplified61.3
\[\leadsto \color{blue}{\log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{e^{\frac{\pi \cdot f}{4}} - e^{-0.25 \cdot \left(\pi \cdot f\right)}}\right) \cdot \frac{-4}{\pi}}
\]
Proof
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 4)) (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 (*.f64 (PI.f64) f)))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 (PI.f64) f)) 4)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (PI.f64) f) 4))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 -1 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 4)) (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 (*.f64 (PI.f64) f)))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 (PI.f64) f)) 4)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (PI.f64) f) 4))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 -1 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (/.f64 (Rewrite<= metadata-eval (neg.f64 4)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 4 (PI.f64))))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1 4)) (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (PI.f64)) 4)))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 (PI.f64) 4))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (/.f64 1 (/.f64 (PI.f64) 4))) (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 (/.f64 1 (/.f64 (PI.f64) 4)) (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))))))): 0 points increase in error, 0 points decrease in error