VandenBroeck and Keller, Equation (20)

Average Error: 61.6 → 2.2

Time: 18.8s

Precision: binary64

Cost: 52416

Math

\[-\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) \]

↓

\[\mathsf{fma}\left(0.5, f \cdot \left(f \cdot \left(0.5 \cdot \left({\pi}^{2} \cdot 0.08333333333333333\right)\right)\right), \log \left(\sqrt[3]{\frac{4}{\pi}}\right) \cdot 3 - \log f\right) \cdot \frac{-4}{\pi} \]

FPCore

(FPCore (f)
 :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)))))))))

↓

(FPCore (f)
 :precision binary64
 (*
  (fma
   0.5
   (* f (* f (* 0.5 (* (pow PI 2.0) 0.08333333333333333))))
   (- (* (log (cbrt (/ 4.0 PI))) 3.0) (log f)))
  (/ -4.0 PI)))

C

double code(double f) {
	return -((1.0 / (((double) M_PI) / 4.0)) * log(((exp(((((double) M_PI) / 4.0) * f)) + exp(-((((double) M_PI) / 4.0) * f))) / (exp(((((double) M_PI) / 4.0) * f)) - exp(-((((double) M_PI) / 4.0) * f))))));
}

↓

double code(double f) {
	return fma(0.5, (f * (f * (0.5 * (pow(((double) M_PI), 2.0) * 0.08333333333333333)))), ((log(cbrt((4.0 / ((double) M_PI)))) * 3.0) - log(f))) * (-4.0 / ((double) M_PI));
}

Julia

function code(f)
	return Float64(-Float64(Float64(1.0 / Float64(pi / 4.0)) * log(Float64(Float64(exp(Float64(Float64(pi / 4.0) * f)) + exp(Float64(-Float64(Float64(pi / 4.0) * f)))) / Float64(exp(Float64(Float64(pi / 4.0) * f)) - exp(Float64(-Float64(Float64(pi / 4.0) * f))))))))
end

↓

function code(f)
	return Float64(fma(0.5, Float64(f * Float64(f * Float64(0.5 * Float64((pi ^ 2.0) * 0.08333333333333333)))), Float64(Float64(log(cbrt(Float64(4.0 / pi))) * 3.0) - log(f))) * Float64(-4.0 / pi))
end

Wolfram

code[f_] := (-N[(N[(1.0 / N[(Pi / 4.0), $MachinePrecision]), $MachinePrecision] * N[Log[N[(N[(N[Exp[N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision]], $MachinePrecision] + N[Exp[(-N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision])], $MachinePrecision]), $MachinePrecision] / N[(N[Exp[N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision]], $MachinePrecision] - N[Exp[(-N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision])], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision])

↓

code[f_] := N[(N[(0.5 * N[(f * N[(f * N[(0.5 * N[(N[Power[Pi, 2.0], $MachinePrecision] * 0.08333333333333333), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(N[Log[N[Power[N[(4.0 / Pi), $MachinePrecision], 1/3], $MachinePrecision]], $MachinePrecision] * 3.0), $MachinePrecision] - N[Log[f], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(-4.0 / Pi), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 61.6

   \[-\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. Simplified 61.6

   \[\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

3. Taylor expanded in f around inf 61.6

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

4. Simplified 61.7

   \[\leadsto \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{\color{blue}{{\left(e^{0.25}\right)}^{\left(\pi \cdot f\right)}} - e^{-0.25 \cdot \left(\pi \cdot f\right)}}\right) \cdot \frac{-4}{\pi} \]
   Proof
   (pow.f64 (exp.f64 1/4) (*.f64 (PI.f64) f)): 0 points increase in error, 0 points decrease in error
   (pow.f64 (exp.f64 1/4) (Rewrite=> *-commutative_binary64 (*.f64 f (PI.f64)))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 1/4 (*.f64 f (PI.f64))))): 4 points increase in error, 0 points decrease in error

5. Taylor expanded in f around 0 2.1

   \[\leadsto \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot 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} \]

6. Simplified 2.1

   \[\leadsto \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{\color{blue}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, {\pi}^{3} \cdot \left(0.005208333333333333 \cdot {f}^{3}\right)\right)\right)}}\right) \cdot \frac{-4}{\pi} \]
   Proof
   (fma.f64 (pow.f64 f 5) (*.f64 (pow.f64 (PI.f64) 5) 1/61440) (fma.f64 (*.f64 (PI.f64) 1/2) f (*.f64 (pow.f64 (PI.f64) 3) (*.f64 1/192 (pow.f64 f 3))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (*.f64 (pow.f64 (PI.f64) 5) (Rewrite<= metadata-eval (-.f64 1/122880 -1/122880))) (fma.f64 (*.f64 (PI.f64) 1/2) f (*.f64 (pow.f64 (PI.f64) 3) (*.f64 1/192 (pow.f64 f 3))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5)))) (fma.f64 (*.f64 (PI.f64) 1/2) f (*.f64 (pow.f64 (PI.f64) 3) (*.f64 1/192 (pow.f64 f 3))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))) (fma.f64 (*.f64 (PI.f64) (Rewrite<= metadata-eval (-.f64 1/4 -1/4))) f (*.f64 (pow.f64 (PI.f64) 3) (*.f64 1/192 (pow.f64 f 3))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))) (fma.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64)))) f (*.f64 (pow.f64 (PI.f64) 3) (*.f64 1/192 (pow.f64 f 3))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))) (fma.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f (*.f64 (pow.f64 (PI.f64) 3) (*.f64 (Rewrite<= metadata-eval (-.f64 1/384 -1/384)) (pow.f64 f 3))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))) (fma.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (PI.f64) 3) (-.f64 1/384 -1/384)) (pow.f64 f 3))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))) (fma.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f (*.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)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))) (fma.f64 (-.f64 (*.f64 1/4 (PI.f64)) (*.f64 -1/4 (PI.f64))) f (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))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 f 5) (-.f64 (*.f64 1/122880 (pow.f64 (PI.f64) 5)) (*.f64 -1/122880 (pow.f64 (PI.f64) 5))) (Rewrite<= fma-def_binary64 (+.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))))))): 0 points increase in error, 2 points decrease in error
   (Rewrite<= fma-def_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

7. Taylor expanded in f around 0 2.2

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

8. Simplified 2.2

   \[\leadsto \color{blue}{\mathsf{fma}\left(0.5, f \cdot \left(f \cdot \left(0.5 \cdot \left({\pi}^{2} \cdot 0.08333333333333333\right)\right)\right), \log \left(\frac{4}{\pi}\right) - \log f\right)} \cdot \frac{-4}{\pi} \]
   Proof
   (fma.f64 1/2 (*.f64 f (*.f64 f (*.f64 1/2 (*.f64 (pow.f64 (PI.f64) 2) 1/12)))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 f (*.f64 f (*.f64 1/2 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 (PI.f64) (PI.f64))) 1/12)))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 f (*.f64 f (*.f64 1/2 (*.f64 (*.f64 (PI.f64) (PI.f64)) (Rewrite<= metadata-eval (-.f64 1/8 1/24)))))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 6 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 f (*.f64 f (*.f64 1/2 (Rewrite<= associate-*r*_binary64 (*.f64 (PI.f64) (*.f64 (PI.f64) (-.f64 1/8 1/24))))))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 6 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 f (*.f64 f (*.f64 1/2 (*.f64 (PI.f64) (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64)))))))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 f (*.f64 f (*.f64 1/2 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 f f) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 1 points increase in error, 1 points decrease in error
   (fma.f64 1/2 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 f 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (Rewrite<= +-rgt-identity_binary64 (+.f64 (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))) 0))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))) (Rewrite<= metadata-eval (*.f64 -1/4 0)))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))) (*.f64 -1/4 (Rewrite<= metadata-eval (pow.f64 0 2))))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))) (*.f64 -1/4 (pow.f64 (Rewrite<= mul0-rgt_binary64 (*.f64 (PI.f64) 0)) 2)))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))) (*.f64 -1/4 (pow.f64 (*.f64 (PI.f64) (Rewrite<= metadata-eval (+.f64 -1/4 1/4))) 2)))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))) (*.f64 -1/4 (pow.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))) 2)))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (-.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 f))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (Rewrite<= unsub-neg_binary64 (+.f64 (log.f64 (/.f64 4 (PI.f64))) (neg.f64 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 f))))): 2 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (log.f64 (/.f64 4 (PI.f64))) 0)) (log.f64 (/.f64 1 f)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (+.f64 (log.f64 (/.f64 4 (PI.f64))) (Rewrite<= mul0-lft_binary64 (*.f64 0 f))) (log.f64 (/.f64 1 f)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 (Rewrite<= mul0-rgt_binary64 (*.f64 (PI.f64) 0)) f)) (log.f64 (/.f64 1 f)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 (*.f64 (PI.f64) (Rewrite<= metadata-eval (+.f64 -1/4 1/4))) f)) (log.f64 (/.f64 1 f)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))) f)) (log.f64 (/.f64 1 f)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) f) (log.f64 (/.f64 4 (PI.f64))))) (log.f64 (/.f64 1 f)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (Rewrite=> associate-+l+_binary64 (+.f64 (*.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f)))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 (Rewrite=> distribute-rgt-out_binary64 (*.f64 (PI.f64) (+.f64 -1/4 1/4))) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 (*.f64 (PI.f64) (Rewrite=> metadata-eval 0)) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 (Rewrite=> mul0-rgt_binary64 0) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (Rewrite=> mul0-lft_binary64 0) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (Rewrite<= mul0-rgt_binary64 (*.f64 (*.f64 1/2 f) 0)) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 (*.f64 1/2 f) (Rewrite<= mul0-rgt_binary64 (*.f64 (PI.f64) 0))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 (*.f64 1/2 f) (*.f64 (PI.f64) (Rewrite<= metadata-eval (+.f64 -1/4 1/4)))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 (*.f64 1/2 f) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 1/2 (*.f64 f (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (log.f64 (/.f64 1 f))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 1/2 (*.f64 f (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (Rewrite=> log-rec_binary64 (neg.f64 (log.f64 f)))))): 0 points increase in error, 2 points decrease in error
   (fma.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64))))) (+.f64 (*.f64 1/2 (*.f64 f (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (log.f64 f)))))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 1/2 (*.f64 f (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))))): 0 points increase in error, 0 points decrease in error
   (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (*.f64 1/2 (*.f64 f (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 1/2 f) (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (*.f64 (*.f64 1/2 f) (Rewrite=> distribute-rgt-out_binary64 (*.f64 (PI.f64) (+.f64 -1/4 1/4))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (*.f64 (*.f64 1/2 f) (*.f64 (PI.f64) (Rewrite=> metadata-eval 0)))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (*.f64 (*.f64 1/2 f) (Rewrite=> mul0-rgt_binary64 0))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (Rewrite=> mul0-rgt_binary64 0)) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (Rewrite<= mul0-lft_binary64 (*.f64 0 f))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (*.f64 (Rewrite<= mul0-rgt_binary64 (*.f64 (PI.f64) 0)) f)) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (*.f64 (*.f64 (PI.f64) (Rewrite<= metadata-eval (+.f64 -1/4 1/4))) f)) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (*.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))) f)) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))): 0 points increase in error, 0 points decrease in error
   (Rewrite=> associate-+l+_binary64 (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 (Rewrite=> distribute-rgt-out_binary64 (*.f64 (PI.f64) (+.f64 -1/4 1/4))) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 (*.f64 (PI.f64) (Rewrite=> metadata-eval 0)) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 (Rewrite=> mul0-rgt_binary64 0) f) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (Rewrite=> mul0-lft_binary64 0) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (Rewrite<= mul0-rgt_binary64 (*.f64 (*.f64 1/2 f) 0)) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 (*.f64 1/2 f) (Rewrite<= mul0-rgt_binary64 (*.f64 (PI.f64) 0))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 (*.f64 1/2 f) (*.f64 (PI.f64) (Rewrite<= metadata-eval (+.f64 -1/4 1/4)))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 (*.f64 1/2 f) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 1/2 (*.f64 f (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 1/2 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) f))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 1/2 (*.f64 (pow.f64 f 2) (+.f64 (*.f64 -1/4 (pow.f64 (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64))) 2)) (*.f64 1/2 (*.f64 (-.f64 (*.f64 1/8 (PI.f64)) (*.f64 1/24 (PI.f64))) (PI.f64)))))) (+.f64 (*.f64 1/2 (Rewrite=> *-commutative_binary64 (*.f64 f (+.f64 (*.f64 -1/4 (PI.f64)) (*.f64 1/4 (PI.f64)))))) (+.f64 (log.f64 (/.f64 4 (PI.f64))) (*.f64 -1 (log.f64 f))))): 0 points increase in error, 0 points decrease in error

9. Applied egg-rr 2.2

   \[\leadsto \mathsf{fma}\left(0.5, f \cdot \left(f \cdot \left(0.5 \cdot \left({\pi}^{2} \cdot 0.08333333333333333\right)\right)\right), \color{blue}{\left(2 \cdot \log \left(\sqrt[3]{\frac{4}{\pi}}\right) + \log \left(\sqrt[3]{\frac{4}{\pi}}\right)\right)} - \log f\right) \cdot \frac{-4}{\pi} \]

10. Simplified 2.2

    \[\leadsto \mathsf{fma}\left(0.5, f \cdot \left(f \cdot \left(0.5 \cdot \left({\pi}^{2} \cdot 0.08333333333333333\right)\right)\right), \color{blue}{\log \left(\sqrt[3]{\frac{4}{\pi}}\right) \cdot 3} - \log f\right) \cdot \frac{-4}{\pi} \]
    Proof
    (*.f64 (log.f64 (cbrt.f64 (/.f64 4 (PI.f64)))) 3): 0 points increase in error, 0 points decrease in error
    (Rewrite<= *-commutative_binary64 (*.f64 3 (log.f64 (cbrt.f64 (/.f64 4 (PI.f64)))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite<= metadata-eval (+.f64 2 1)) (log.f64 (cbrt.f64 (/.f64 4 (PI.f64))))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 2 (log.f64 (cbrt.f64 (/.f64 4 (PI.f64))))) (log.f64 (cbrt.f64 (/.f64 4 (PI.f64)))))): 0 points increase in error, 0 points decrease in error

11. Final simplification 2.2

    \[\leadsto \mathsf{fma}\left(0.5, f \cdot \left(f \cdot \left(0.5 \cdot \left({\pi}^{2} \cdot 0.08333333333333333\right)\right)\right), \log \left(\sqrt[3]{\frac{4}{\pi}}\right) \cdot 3 - \log f\right) \cdot \frac{-4}{\pi} \]

Alternatives

Alternative 1
Error	2.2
Cost	45888

\[\frac{-4}{\pi} \cdot \mathsf{fma}\left(0.5, f \cdot \left(f \cdot \left(0.5 \cdot \left({\pi}^{2} \cdot 0.08333333333333333\right)\right)\right), \log \left(\frac{4}{\pi}\right) - \log f\right) \]

Alternative 2
Error	2.2
Cost	32768

\[\mathsf{fma}\left(-4, \frac{\log \left(\frac{4}{f \cdot \pi}\right)}{\pi}, \pi \cdot \left(-0.08333333333333333 \cdot \left(f \cdot f\right)\right)\right) \]

Alternative 3
Error	2.5
Cost	26048

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

Alternative 4
Error	2.6
Cost	19648

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

Alternative 5
Error	2.5
Cost	19648

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

Alternative 6
Error	45.4
Cost	19520

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

Alternative 7
Error	45.4
Cost	19520

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

Alternative 8
Error	54.1
Cost	6528

\[\frac{-64}{\pi} \]

Reproduce

herbie shell --seed 2022329 
(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)))))))))