Initial program 61.5
\[-\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)
\]
Simplified61.5
\[\leadsto \color{blue}{\log \left(\frac{{\left(e^{\frac{\pi}{4}}\right)}^{f} + {\left(e^{\frac{\pi}{4}}\right)}^{\left(-f\right)}}{{\left(e^{\frac{\pi}{4}}\right)}^{f} - {\left(e^{\frac{\pi}{4}}\right)}^{\left(-f\right)}}\right) \cdot \frac{-4}{\pi}}
\]
Proof
(*.f64 (log.f64 (/.f64 (+.f64 (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) f) (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) (neg.f64 f))) (-.f64 (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) f) (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) (neg.f64 f))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f))) (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) (neg.f64 f))) (-.f64 (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) f) (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) (neg.f64 f))))) (/.f64 -4 (PI.f64))): 1 points increase in error, 0 points decrease in error
(*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) (neg.f64 f))))) (-.f64 (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) f) (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) (neg.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<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))) (-.f64 (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) f) (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) (neg.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 (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f))) (pow.f64 (exp.f64 (/.f64 (PI.f64) 4)) (neg.f64 f))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 1 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)) (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) (neg.f64 f))))))) (/.f64 -4 (PI.f64))): 1 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<= distribute-rgt-neg-in_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
Taylor expanded in f around 0 2.3
\[\leadsto \log \left(\frac{{\left(e^{\frac{\pi}{4}}\right)}^{f} + {\left(e^{\frac{\pi}{4}}\right)}^{\left(-f\right)}}{\color{blue}{{f}^{5} \cdot \left(8.138020833333333 \cdot 10^{-6} \cdot {\pi}^{5} - -8.138020833333333 \cdot 10^{-6} \cdot {\pi}^{5}\right) + \left(\left(0.25 \cdot \pi - -0.25 \cdot \pi\right) \cdot f + {f}^{3} \cdot \left(0.0026041666666666665 \cdot {\pi}^{3} - -0.0026041666666666665 \cdot {\pi}^{3}\right)\right)}}\right) \cdot \frac{-4}{\pi}
\]
Simplified2.3
\[\leadsto \log \left(\frac{{\left(e^{\frac{\pi}{4}}\right)}^{f} + {\left(e^{\frac{\pi}{4}}\right)}^{\left(-f\right)}}{\color{blue}{\mathsf{fma}\left({\pi}^{3}, {f}^{3} \cdot 0.005208333333333333, \mathsf{fma}\left(\pi, f \cdot 0.5, {\pi}^{5} \cdot \left({f}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}\right)\right)\right)}}\right) \cdot \frac{-4}{\pi}
\]
Proof
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (pow.f64 f 3) 1/192) (fma.f64 (PI.f64) (*.f64 f 1/2) (*.f64 (pow.f64 (PI.f64) 5) (*.f64 (pow.f64 f 5) 1/61440)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (pow.f64 f 3) (Rewrite<= metadata-eval (-.f64 1/384 -1/384))) (fma.f64 (PI.f64) (*.f64 f 1/2) (*.f64 (pow.f64 (PI.f64) 5) (*.f64 (pow.f64 f 5) 1/61440)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3))) (fma.f64 (PI.f64) (*.f64 f 1/2) (*.f64 (pow.f64 (PI.f64) 5) (*.f64 (pow.f64 f 5) 1/61440)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (fma.f64 (PI.f64) (*.f64 f (Rewrite<= metadata-eval (/.f64 1 2))) (*.f64 (pow.f64 (PI.f64) 5) (*.f64 (pow.f64 f 5) 1/61440)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (fma.f64 (PI.f64) (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 2) f)) (*.f64 (pow.f64 (PI.f64) 5) (*.f64 (pow.f64 f 5) 1/61440)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (fma.f64 (PI.f64) (*.f64 (/.f64 1 2) f) (*.f64 (pow.f64 (PI.f64) 5) (*.f64 (pow.f64 f 5) (Rewrite<= metadata-eval (-.f64 1/122880 -1/122880)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (fma.f64 (PI.f64) (*.f64 (/.f64 1 2) f) (*.f64 (pow.f64 (PI.f64) 5) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 1/122880 -1/122880) (pow.f64 f 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (fma.f64 (PI.f64) (*.f64 (/.f64 1 2) f) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (PI.f64) 5) (-.f64 1/122880 -1/122880)) (pow.f64 f 5))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (fma.f64 (PI.f64) (*.f64 (/.f64 1 2) f) (*.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (pow.f64 f 5)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (fma.f64 (PI.f64) (*.f64 (/.f64 1 2) f) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (PI.f64) (*.f64 (/.f64 1 2) f)) (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))))))): 1 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (PI.f64) (/.f64 1 2)) f)) (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (+.f64 (*.f64 (*.f64 (PI.f64) (Rewrite=> metadata-eval 1/2)) f) (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (+.f64 (*.f64 (*.f64 (PI.f64) (Rewrite<= metadata-eval (-.f64 1/4 -1/4))) f) (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (+.f64 (*.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64)))) f) (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (*.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (pow.f64 (PI.f64) 3) (*.f64 (-.f64 1/384 -1/384) (pow.f64 f 3))) (+.f64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (*.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (PI.f64) 3) (-.f64 1/384 -1/384)) (pow.f64 f 3))) (+.f64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (*.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 1/384 (pow.f64 (PI.f64) 3)) (*.f64 -1/384 (pow.f64 (PI.f64) 3)))) (pow.f64 f 3)) (+.f64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (*.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 f 3) (-.f64 (*.f64 1/384 (pow.f64 (PI.f64) 3)) (*.f64 -1/384 (pow.f64 (PI.f64) 3))))) (+.f64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (*.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (*.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f)) (*.f64 (pow.f64 f 3) (-.f64 (*.f64 1/384 (pow.f64 (PI.f64) 3)) (*.f64 -1/384 (pow.f64 (PI.f64) 3)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (+.f64 (*.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f) (*.f64 (pow.f64 f 3) (-.f64 (*.f64 1/384 (pow.f64 (PI.f64) 3)) (*.f64 -1/384 (pow.f64 (PI.f64) 3))))))): 1 points increase in error, 0 points decrease in error
Final simplification2.3
\[\leadsto \log \left(\frac{{\left(e^{\frac{\pi}{4}}\right)}^{f} + {\left(e^{\frac{\pi}{4}}\right)}^{\left(-f\right)}}{\mathsf{fma}\left({\pi}^{3}, {f}^{3} \cdot 0.005208333333333333, \mathsf{fma}\left(\pi, f \cdot 0.5, {\pi}^{5} \cdot \left({f}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}\right)\right)\right)}\right) \cdot \frac{-4}{\pi}
\]