Simplified2.2
\[\leadsto \color{blue}{\left(\sqrt{2} \cdot \left(\sqrt{\pi} \cdot \frac{e^{-6.5 - z}}{{\left(z - -6.5\right)}^{\left(0.5 - z\right)}}\right)\right)} \cdot \left(\left(\left(\left(\left(\left(\left(\left(0.9999999999998099 + \frac{676.5203681218851}{\left(z - 1\right) + 1}\right) + \frac{-1259.1392167224028}{\left(z - 1\right) + 2}\right) + \frac{771.3234287776531}{\left(z - 1\right) + 3}\right) + \frac{-176.6150291621406}{\left(z - 1\right) + 4}\right) + \frac{12.507343278686905}{\left(z - 1\right) + 5}\right) + \frac{-0.13857109526572012}{\left(z - 1\right) + 6}\right) + \frac{9.984369578019572 \cdot 10^{-6}}{\left(z - 1\right) + 7}\right) + \frac{1.5056327351493116 \cdot 10^{-7}}{\left(z - 1\right) + 8}\right)
\]
Proof
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 -13/2 z)) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (Rewrite<= unsub-neg_binary64 (+.f64 -13/2 (neg.f64 z)))) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (+.f64 (Rewrite<= metadata-eval (neg.f64 13/2)) (neg.f64 z))) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 13/2 z)))) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (neg.f64 (Rewrite=> +-commutative_binary64 (+.f64 z 13/2)))) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 z) (neg.f64 13/2)))) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 z)) (neg.f64 13/2))) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 -1 z) 13/2))) (pow.f64 (-.f64 z -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (-.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 z)) -13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (Rewrite=> fma-neg_binary64 (fma.f64 1 z (neg.f64 -13/2))) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (fma.f64 1 z (Rewrite=> metadata-eval 13/2)) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1 z) 13/2)) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (+.f64 (Rewrite=> *-lft-identity_binary64 z) 13/2) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (Rewrite<= +-commutative_binary64 (+.f64 13/2 z)) (-.f64 1/2 z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (+.f64 13/2 z) (Rewrite<= unsub-neg_binary64 (+.f64 1/2 (neg.f64 z))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (+.f64 13/2 z) (+.f64 1/2 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 z))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (pow.f64 (+.f64 13/2 z) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 z) 1/2)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 (+.f64 13/2 z)) (+.f64 (*.f64 -1 z) 1/2))))))): 89 points increase in error, 104 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (exp.f64 (*.f64 (log.f64 (+.f64 13/2 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 z))))) (+.f64 (*.f64 -1 z) 1/2)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (exp.f64 (*.f64 (log.f64 (+.f64 13/2 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 z))))) (+.f64 (*.f64 -1 z) 1/2)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (/.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (exp.f64 (*.f64 (log.f64 (Rewrite<= sub-neg_binary64 (-.f64 13/2 (*.f64 -1 z)))) (+.f64 (*.f64 -1 z) 1/2)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (Rewrite=> div-exp_binary64 (exp.f64 (-.f64 (-.f64 (*.f64 -1 z) 13/2) (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2))))))): 68 points increase in error, 81 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (exp.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (-.f64 (*.f64 -1 z) 13/2) (neg.f64 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (exp.f64 (+.f64 (-.f64 (*.f64 -1 z) 13/2) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))))))): 87 points increase in error, 63 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (sqrt.f64 (PI.f64)) (Rewrite<= *-commutative_binary64 (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (exp.f64 (-.f64 (*.f64 -1 z) 13/2)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (exp.f64 (-.f64 (*.f64 -1 z) 13/2))) (sqrt.f64 (PI.f64))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (Rewrite=> associate-*l*_binary64 (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (*.f64 (exp.f64 (-.f64 (*.f64 -1 z) 13/2)) (sqrt.f64 (PI.f64)))))): 34 points increase in error, 34 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (*.f64 (exp.f64 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 -1 z) (neg.f64 13/2)))) (sqrt.f64 (PI.f64))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (*.f64 (exp.f64 (+.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 z)) (neg.f64 13/2))) (sqrt.f64 (PI.f64))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (*.f64 (exp.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 z 13/2)))) (sqrt.f64 (PI.f64))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 2) (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (*.f64 (exp.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 13/2 z)))) (sqrt.f64 (PI.f64))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sqrt.f64 2) (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2))))) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64))))): 44 points increase in error, 49 points decrease in error
(*.f64 (Rewrite=> *-commutative_binary64 (*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2)))) (sqrt.f64 2))) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (exp.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (+.f64 (*.f64 -1 z) 1/2))))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (exp.f64 (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 (log.f64 (-.f64 13/2 (*.f64 -1 z))) (neg.f64 (+.f64 (*.f64 -1 z) 1/2))))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (exp.f64 (*.f64 (log.f64 (Rewrite=> sub-neg_binary64 (+.f64 13/2 (neg.f64 (*.f64 -1 z))))) (neg.f64 (+.f64 (*.f64 -1 z) 1/2)))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (exp.f64 (*.f64 (log.f64 (+.f64 13/2 (neg.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 z))))) (neg.f64 (+.f64 (*.f64 -1 z) 1/2)))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (exp.f64 (*.f64 (log.f64 (+.f64 13/2 (Rewrite=> remove-double-neg_binary64 z))) (neg.f64 (+.f64 (*.f64 -1 z) 1/2)))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (Rewrite=> exp-to-pow_binary64 (pow.f64 (+.f64 13/2 z) (neg.f64 (+.f64 (*.f64 -1 z) 1/2)))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 110 points increase in error, 86 points decrease in error
(*.f64 (*.f64 (pow.f64 (+.f64 13/2 z) (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (*.f64 -1 z)) (neg.f64 1/2)))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (+.f64 13/2 z) (+.f64 (neg.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 z))) (neg.f64 1/2))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (+.f64 13/2 z) (+.f64 (Rewrite=> remove-double-neg_binary64 z) (neg.f64 1/2))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (+.f64 13/2 z) (Rewrite<= sub-neg_binary64 (-.f64 z 1/2))) (sqrt.f64 2)) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 2) (pow.f64 (+.f64 13/2 z) (-.f64 z 1/2)))) (*.f64 (exp.f64 (neg.f64 (+.f64 13/2 z))) (sqrt.f64 (PI.f64)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (pow.f64 (+.f64 13/2 z) (-.f64 z 1/2))) (exp.f64 (neg.f64 (+.f64 13/2 z)))) (sqrt.f64 (PI.f64)))): 43 points increase in error, 41 points decrease in error
(*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (sqrt.f64 2) (*.f64 (pow.f64 (+.f64 13/2 z) (-.f64 z 1/2)) (exp.f64 (neg.f64 (+.f64 13/2 z)))))) (sqrt.f64 (PI.f64))): 34 points increase in error, 39 points decrease in error