Initial program 0.7
\[\frac{e^{a}}{e^{a} + e^{b}}
\]
Applied egg-rr0.7
\[\leadsto \color{blue}{{\left(\frac{e^{a} + e^{b}}{e^{a}}\right)}^{-1}}
\]
Taylor expanded in a around inf 0.7
\[\leadsto \color{blue}{\frac{e^{a}}{e^{a} + e^{b}}}
\]
Simplified0.0
\[\leadsto \color{blue}{\frac{1}{1 + e^{b - a}}}
\]
Proof
(/.f64 1 (+.f64 1 (exp.f64 (-.f64 b a)))): 0 points increase in error, 0 points decrease in error
(/.f64 1 (+.f64 1 (exp.f64 (Rewrite<= unsub-neg_binary64 (+.f64 b (neg.f64 a)))))): 0 points increase in error, 0 points decrease in error
(/.f64 1 (+.f64 1 (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 b) (exp.f64 (neg.f64 a)))))): 2 points increase in error, 0 points decrease in error
(/.f64 1 (+.f64 (Rewrite<= rgt-mult-inverse_binary64 (*.f64 (exp.f64 a) (/.f64 1 (exp.f64 a)))) (*.f64 (exp.f64 b) (exp.f64 (neg.f64 a))))): 71 points increase in error, 0 points decrease in error
(/.f64 1 (+.f64 (*.f64 (exp.f64 a) (Rewrite=> rec-exp_binary64 (exp.f64 (neg.f64 a)))) (*.f64 (exp.f64 b) (exp.f64 (neg.f64 a))))): 4 points increase in error, 0 points decrease in error
(/.f64 1 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (exp.f64 (neg.f64 a)) (+.f64 (exp.f64 a) (exp.f64 b))))): 0 points increase in error, 70 points decrease in error
(/.f64 1 (*.f64 (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 a))) (+.f64 (exp.f64 a) (exp.f64 b)))): 0 points increase in error, 4 points decrease in error
(/.f64 1 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (+.f64 (exp.f64 a) (exp.f64 b))) (exp.f64 a)))): 1 points increase in error, 1 points decrease in error
(/.f64 1 (/.f64 (Rewrite=> *-lft-identity_binary64 (+.f64 (exp.f64 a) (exp.f64 b))) (exp.f64 a))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 1 (exp.f64 a)) (+.f64 (exp.f64 a) (exp.f64 b)))): 1 points increase in error, 1 points decrease in error
(/.f64 (Rewrite=> *-lft-identity_binary64 (exp.f64 a)) (+.f64 (exp.f64 a) (exp.f64 b))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \frac{1}{1 + e^{b - a}}
\]