Simplified11.8
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{e^{\frac{\log x}{n}}}{x \cdot x}, \frac{0.5}{n \cdot n} + \frac{-0.5}{n}, \frac{e^{\frac{\log x}{n}}}{x \cdot n}\right)}
\]
Proof
(fma.f64 (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x x)) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (log.f64 x)))) n)) (*.f64 x x)) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (/.f64 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (log.f64 x)))) n)) (*.f64 x x)) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (*.f64 -1 (log.f64 x)) n)))) (*.f64 x x)) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (neg.f64 (/.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (log.f64 x))) n))) (*.f64 x x)) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (neg.f64 (/.f64 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 x))) n))) (*.f64 x x)) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n)))) (*.f64 x x)) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (Rewrite<= unpow2_binary64 (pow.f64 x 2))) (+.f64 (/.f64 1/2 (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (+.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1/2 1)) (*.f64 n n)) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (+.f64 (/.f64 (*.f64 1/2 1) (Rewrite<= unpow2_binary64 (pow.f64 n 2))) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2)))) (/.f64 -1/2 n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (+.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (/.f64 (Rewrite<= metadata-eval (neg.f64 1/2)) n)) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (+.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1/2 n)))) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (+.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1/2 1)) n))) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (+.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (neg.f64 (Rewrite<= associate-*r/_binary64 (*.f64 1/2 (/.f64 1 n))))) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n)))) (/.f64 (exp.f64 (/.f64 (log.f64 x) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n))) (/.f64 (exp.f64 (/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (log.f64 x)))) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n))) (/.f64 (exp.f64 (/.f64 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (log.f64 x)))) n)) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n))) (/.f64 (exp.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (*.f64 -1 (log.f64 x)) n)))) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n))) (/.f64 (exp.f64 (neg.f64 (/.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (log.f64 x))) n))) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n))) (/.f64 (exp.f64 (neg.f64 (/.f64 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 x))) n))) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n))) (/.f64 (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n)))) (*.f64 x n))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n))) (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (Rewrite<= *-commutative_binary64 (*.f64 n x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (pow.f64 x 2)) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n)))) (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (*.f64 n x)))): 1 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (-.f64 (*.f64 1/2 (/.f64 1 (pow.f64 n 2))) (*.f64 1/2 (/.f64 1 n)))) (pow.f64 x 2))) (/.f64 (exp.f64 (*.f64 -1 (/.f64 (log.f64 (/.f64 1 x)) n))) (*.f64 n x))): 6 points increase in error, 7 points decrease in error