Simplified3.7
\[\leadsto \left(\left(\sqrt{\pi \cdot 2} \cdot {\left(\left(\left(z - 1\right) + 7\right) + 0.5\right)}^{\left(\left(z - 1\right) + 0.5\right)}\right) \cdot e^{-\left(\left(\left(z - 1\right) + 7\right) + 0.5\right)}\right) \cdot \left(\left(\left(\left(\left(\left(\frac{\color{blue}{\left(-1258.1392167221638 - \frac{-394153.5179299711}{z}\right) + \mathsf{fma}\left(z, 0.9999999999996197, \frac{-457679.80848377093}{z \cdot z}\right)}}{\left(0.9999999999998099 - \frac{676.5203681218851}{z}\right) \cdot \left(z - -1\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 (-.f64 -125813921672216381783490107119158199/100000000000000000000000000000000 (/.f64 -39415351792997107601807255991627/100000000000000000000000000 z)) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (Rewrite<= metadata-eval (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000)) (/.f64 -39415351792997107601807255991627/100000000000000000000000000 z)) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000) (/.f64 (Rewrite<= metadata-eval (*.f64 -39415351792997107601807255991627/100000000000000000000000000 1)) z)) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000) (/.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 39415351792997107601807255991627/100000000000000000000000000)) 1) z)) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000) (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 39415351792997107601807255991627/100000000000000000000000000) (/.f64 1 z)))) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 31 points increase in error, 37 points decrease in error
(+.f64 (-.f64 (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000) (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z))))) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> sub-neg_binary64 (+.f64 (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000) (neg.f64 (neg.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)))))) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000) (Rewrite=> remove-double-neg_binary64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)))) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) (neg.f64 125813921672216381783490107119158199/100000000000000000000000000000000))) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000)) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 -45767980848377092942628957760201/100000000000000000000000000 (Rewrite<= unpow2_binary64 (pow.f64 z 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (/.f64 (Rewrite<= metadata-eval (neg.f64 45767980848377092942628957760201/100000000000000000000000000)) (pow.f64 z 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 45767980848377092942628957760201/100000000000000000000000000 (pow.f64 z 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 45767980848377092942628957760201/100000000000000000000000000 1)) (pow.f64 z 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (fma.f64 z 99999999999961980000000003613801/100000000000000000000000000000000 (neg.f64 (Rewrite<= associate-*r/_binary64 (*.f64 45767980848377092942628957760201/100000000000000000000000000 (/.f64 1 (pow.f64 z 2))))))): 16 points increase in error, 15 points decrease in error
(+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 z 99999999999961980000000003613801/100000000000000000000000000000000) (*.f64 45767980848377092942628957760201/100000000000000000000000000 (/.f64 1 (pow.f64 z 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 99999999999961980000000003613801/100000000000000000000000000000000 z)) (*.f64 45767980848377092942628957760201/100000000000000000000000000 (/.f64 1 (pow.f64 z 2))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000) (*.f64 99999999999961980000000003613801/100000000000000000000000000000000 z)) (*.f64 45767980848377092942628957760201/100000000000000000000000000 (/.f64 1 (pow.f64 z 2))))): 30 points increase in error, 37 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 99999999999961980000000003613801/100000000000000000000000000000000 z) (-.f64 (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z)) 125813921672216381783490107119158199/100000000000000000000000000000000))) (*.f64 45767980848377092942628957760201/100000000000000000000000000 (/.f64 1 (pow.f64 z 2)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 99999999999961980000000003613801/100000000000000000000000000000000 z) (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z))) 125813921672216381783490107119158199/100000000000000000000000000000000)) (*.f64 45767980848377092942628957760201/100000000000000000000000000 (/.f64 1 (pow.f64 z 2)))): 10 points increase in error, 11 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 (+.f64 (*.f64 99999999999961980000000003613801/100000000000000000000000000000000 z) (*.f64 39415351792997107601807255991627/100000000000000000000000000 (/.f64 1 z))) (+.f64 125813921672216381783490107119158199/100000000000000000000000000000000 (*.f64 45767980848377092942628957760201/100000000000000000000000000 (/.f64 1 (pow.f64 z 2)))))): 19 points increase in error, 17 points decrease in error
Simplified3.5
\[\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(\frac{\left(-1258.1392167221638 - \frac{-394153.5179299711}{z}\right) + \mathsf{fma}\left(z, 0.9999999999996197, \frac{-457679.80848377093}{z \cdot z}\right)}{\left(0.9999999999998099 - \frac{676.5203681218851}{z}\right) \cdot \left(z - -1\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))))))): 95 points increase in error, 103 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))))))): 79 points increase in error, 71 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)))))))): 74 points increase in error, 70 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)))))): 31 points increase in error, 33 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))))): 47 points increase in error, 38 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)))): 103 points increase in error, 98 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)))): 47 points increase in error, 40 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, 41 points decrease in error