Initial program 0.2
\[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}
\]
Simplified0.2
\[\leadsto \color{blue}{\frac{1}{\left(s + \frac{s}{e^{\frac{\left|x\right|}{s}}}\right) \cdot \left(1 + e^{\frac{\left|x\right|}{s}}\right)}}
\]
Proof
[Start]0.2 | \[ \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}
\] |
|---|
associate-/l/ [<=]0.2 | \[ \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{1 + e^{\frac{-\left|x\right|}{s}}}}{s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}
\] |
|---|
*-lft-identity [<=]0.2 | \[ \frac{\color{blue}{1 \cdot \frac{e^{\frac{-\left|x\right|}{s}}}{1 + e^{\frac{-\left|x\right|}{s}}}}}{s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}
\] |
|---|
*-lft-identity [<=]0.2 | \[ \frac{1 \cdot \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{1 \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}}{s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}
\] |
|---|
*-commutative [<=]0.2 | \[ \frac{1 \cdot \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot 1}}}{s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}
\] |
|---|
associate-*r/ [=>]0.2 | \[ \frac{\color{blue}{\frac{1 \cdot e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot 1}}}{s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}
\] |
|---|
associate-/l* [=>]0.2 | \[ \frac{\color{blue}{\frac{1}{\frac{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot 1}{e^{\frac{-\left|x\right|}{s}}}}}}{s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}
\] |
|---|
associate-/l/ [=>]0.2 | \[ \color{blue}{\frac{1}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \frac{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot 1}{e^{\frac{-\left|x\right|}{s}}}}}
\] |
|---|
Applied egg-rr11.7
\[\leadsto \frac{1}{\color{blue}{\frac{s}{e^{\frac{x}{s}}} + \left(s + e^{\frac{x}{s}} \cdot \left(s + \frac{s}{e^{\frac{x}{s}}}\right)\right)}}
\]
Taylor expanded in s around 0 11.7
\[\leadsto \frac{1}{\frac{s}{e^{\frac{x}{s}}} + \color{blue}{\left(1 + e^{\frac{x}{s}} \cdot \left(1 + \frac{1}{e^{\frac{x}{s}}}\right)\right) \cdot s}}
\]
Simplified0.1
\[\leadsto \frac{1}{\frac{s}{e^{\frac{x}{s}}} + \color{blue}{s \cdot \left(e^{\frac{x}{s}} + 2\right)}}
\]
Proof
[Start]11.7 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + \left(1 + e^{\frac{x}{s}} \cdot \left(1 + \frac{1}{e^{\frac{x}{s}}}\right)\right) \cdot s}
\] |
|---|
*-commutative [=>]11.7 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + \color{blue}{s \cdot \left(1 + e^{\frac{x}{s}} \cdot \left(1 + \frac{1}{e^{\frac{x}{s}}}\right)\right)}}
\] |
|---|
+-commutative [=>]11.7 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + s \cdot \color{blue}{\left(e^{\frac{x}{s}} \cdot \left(1 + \frac{1}{e^{\frac{x}{s}}}\right) + 1\right)}}
\] |
|---|
distribute-lft-in [=>]23.2 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + s \cdot \left(\color{blue}{\left(e^{\frac{x}{s}} \cdot 1 + e^{\frac{x}{s}} \cdot \frac{1}{e^{\frac{x}{s}}}\right)} + 1\right)}
\] |
|---|
associate-+l+ [=>]23.2 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + s \cdot \color{blue}{\left(e^{\frac{x}{s}} \cdot 1 + \left(e^{\frac{x}{s}} \cdot \frac{1}{e^{\frac{x}{s}}} + 1\right)\right)}}
\] |
|---|
*-rgt-identity [=>]23.2 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + s \cdot \left(\color{blue}{e^{\frac{x}{s}}} + \left(e^{\frac{x}{s}} \cdot \frac{1}{e^{\frac{x}{s}}} + 1\right)\right)}
\] |
|---|
rgt-mult-inverse [=>]0.1 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + s \cdot \left(e^{\frac{x}{s}} + \left(\color{blue}{1} + 1\right)\right)}
\] |
|---|
metadata-eval [=>]0.1 | \[ \frac{1}{\frac{s}{e^{\frac{x}{s}}} + s \cdot \left(e^{\frac{x}{s}} + \color{blue}{2}\right)}
\] |
|---|
Taylor expanded in s around 0 0.1
\[\leadsto \color{blue}{\frac{1}{s \cdot \left(e^{\frac{x}{s}} + \left(2 + \frac{1}{e^{\frac{x}{s}}}\right)\right)}}
\]
Simplified0.2
\[\leadsto \color{blue}{\frac{\frac{1}{s}}{\left(2 + e^{\frac{x}{s}}\right) + e^{\frac{-x}{s}}}}
\]
Proof
[Start]0.1 | \[ \frac{1}{s \cdot \left(e^{\frac{x}{s}} + \left(2 + \frac{1}{e^{\frac{x}{s}}}\right)\right)}
\] |
|---|
associate-/r* [=>]0.2 | \[ \color{blue}{\frac{\frac{1}{s}}{e^{\frac{x}{s}} + \left(2 + \frac{1}{e^{\frac{x}{s}}}\right)}}
\] |
|---|
associate-+r+ [=>]0.2 | \[ \frac{\frac{1}{s}}{\color{blue}{\left(e^{\frac{x}{s}} + 2\right) + \frac{1}{e^{\frac{x}{s}}}}}
\] |
|---|
+-commutative [=>]0.2 | \[ \frac{\frac{1}{s}}{\color{blue}{\left(2 + e^{\frac{x}{s}}\right)} + \frac{1}{e^{\frac{x}{s}}}}
\] |
|---|
exp-neg [<=]0.2 | \[ \frac{\frac{1}{s}}{\left(2 + e^{\frac{x}{s}}\right) + \color{blue}{e^{-\frac{x}{s}}}}
\] |
|---|
distribute-neg-frac [=>]0.2 | \[ \frac{\frac{1}{s}}{\left(2 + e^{\frac{x}{s}}\right) + e^{\color{blue}{\frac{-x}{s}}}}
\] |
|---|
Applied egg-rr0.2
\[\leadsto \color{blue}{-\frac{\frac{1}{s}}{-2 - 2 \cdot \cosh \left(\frac{x}{s}\right)}}
\]
Final simplification0.2
\[\leadsto \frac{\frac{-1}{s}}{-2 + -2 \cdot \cosh \left(\frac{x}{s}\right)}
\]