Simplified1.3
\[\leadsto \color{blue}{e^{\left(\left|n - m\right| - {\left(0.5 \cdot \left(n + m\right) - M\right)}^{2}\right) - \ell}}
\]
Proof
(exp.f64 (-.f64 (-.f64 (fabs.f64 (-.f64 n m)) (pow.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M) 2)) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (-.f64 (Rewrite<= fabs-sub_binary64 (fabs.f64 (-.f64 m n))) (pow.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M) 2)) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (-.f64 (fabs.f64 (-.f64 m n)) (Rewrite=> unpow2_binary64 (*.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M) (-.f64 (*.f64 1/2 (+.f64 n m)) M)))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 (fabs.f64 (-.f64 m n)) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M)))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (Rewrite=> fabs-sub_binary64 (fabs.f64 (-.f64 n m))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (Rewrite<= unsub-neg_binary64 (+.f64 n (neg.f64 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (+.f64 n (Rewrite<= mul-1-neg_binary64 (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (Rewrite<= fabs-neg_binary64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m))))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 n m) 1/2)) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 (+.f64 n (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 m)))) 1/2) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 (+.f64 n (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 m)))) 1/2) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 n (*.f64 -1 m))) 1/2) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/2 (-.f64 n (*.f64 -1 m)))) M)) (-.f64 (*.f64 1/2 (+.f64 n m)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M)) (-.f64 (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 n m) 1/2)) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M)) (-.f64 (*.f64 (+.f64 n (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 m)))) 1/2) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M)) (-.f64 (*.f64 (+.f64 n (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 m)))) 1/2) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M)) (-.f64 (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 n (*.f64 -1 m))) 1/2) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (+.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (neg.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M)) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/2 (-.f64 n (*.f64 -1 m)))) M))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (*.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M)))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (-.f64 (-.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2))) l)): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite<= associate--r+_binary64 (-.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m)))) (+.f64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2) l)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> exp-diff_binary64 (/.f64 (exp.f64 (fabs.f64 (neg.f64 (+.f64 n (*.f64 -1 m))))) (exp.f64 (+.f64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2) l)))): 200 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (Rewrite=> fabs-neg_binary64 (fabs.f64 (+.f64 n (*.f64 -1 m))))) (exp.f64 (+.f64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2) l))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (+.f64 n (Rewrite=> mul-1-neg_binary64 (neg.f64 m))))) (exp.f64 (+.f64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2) l))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (Rewrite=> unsub-neg_binary64 (-.f64 n m)))) (exp.f64 (+.f64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2) l))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (Rewrite<= fabs-sub_binary64 (fabs.f64 (-.f64 m n)))) (exp.f64 (+.f64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2) l))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (exp.f64 (Rewrite=> +-commutative_binary64 (+.f64 l (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2))))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (Rewrite=> exp-sum_binary64 (*.f64 (exp.f64 l) (exp.f64 (pow.f64 (-.f64 (*.f64 1/2 (-.f64 n (*.f64 -1 m))) M) 2))))): 5 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (*.f64 (exp.f64 l) (exp.f64 (pow.f64 (-.f64 (Rewrite=> *-commutative_binary64 (*.f64 (-.f64 n (*.f64 -1 m)) 1/2)) M) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (*.f64 (exp.f64 l) (exp.f64 (pow.f64 (-.f64 (*.f64 (Rewrite=> sub-neg_binary64 (+.f64 n (neg.f64 (*.f64 -1 m)))) 1/2) M) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (*.f64 (exp.f64 l) (exp.f64 (pow.f64 (-.f64 (*.f64 (+.f64 n (neg.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 m)))) 1/2) M) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (*.f64 (exp.f64 l) (exp.f64 (pow.f64 (-.f64 (*.f64 (+.f64 n (Rewrite=> remove-double-neg_binary64 m)) 1/2) M) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (*.f64 (exp.f64 l) (exp.f64 (pow.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/2 (+.f64 n m))) M) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (exp.f64 (fabs.f64 (-.f64 m n))) (Rewrite<= exp-sum_binary64 (exp.f64 (+.f64 l (pow.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M) 2))))): 0 points increase in error, 5 points decrease in error
(Rewrite<= exp-diff_binary64 (exp.f64 (-.f64 (fabs.f64 (-.f64 m n)) (+.f64 l (pow.f64 (-.f64 (*.f64 1/2 (+.f64 n m)) M) 2))))): 0 points increase in error, 200 points decrease in error