Initial program 29.5
\[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}
\]
Simplified43.9
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{\varepsilon + -1}\right)}^{x}, \frac{1 - \frac{1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}}
\]
Proof
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (+.f64 eps -1)) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (Rewrite<= +-commutative_binary64 (+.f64 -1 eps))) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) eps)) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 eps)))) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 1 eps)))) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 (neg.f64 (-.f64 1 eps)) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 1 points increase in error, 54 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 (-.f64 1 eps) x)))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)))))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 eps x) (*.f64 1 x)))))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 x (+.f64 eps 1)))))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 1 eps)))))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 1 eps) x))))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 (/.f64 1 eps)))) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 1 eps)) 1)) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 1 eps))) 1) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (/.f64 1 eps) 1))) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (/.f64 1 eps) 1))) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) 1)) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) (/.f64 1 (exp.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 1 points increase in error, 1 points decrease in error
(/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) (Rewrite<= exp-neg_binary64 (exp.f64 (neg.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 2 points increase in error, 1 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x)))) (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) (exp.f64 (neg.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 2 points increase in error, 7 points decrease in error
(/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x)))) (*.f64 (-.f64 (/.f64 1 eps) 1) (exp.f64 (neg.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 0 points increase in error, 0 points decrease in error
Applied egg-rr43.9
\[\leadsto \frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{\varepsilon + -1}\right)}^{x}, \frac{1 - \frac{1}{\varepsilon}}{\color{blue}{{\left(\sqrt[3]{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}^{3}}}\right)}{2}
\]
Taylor expanded in eps around 0 30.1
\[\leadsto \frac{\color{blue}{\left(\frac{e^{-1 \cdot x}}{\varepsilon} + \left(e^{-1 \cdot x} \cdot x + \left(\frac{1}{e^{x}} + e^{-1 \cdot x}\right)\right)\right) - \left(\frac{1}{\varepsilon \cdot e^{x}} + -1 \cdot \frac{x}{e^{x}}\right)}}{2}
\]
Simplified0.6
\[\leadsto \frac{\color{blue}{\left(2 \cdot e^{-x} + \frac{x}{e^{x}}\right) + \frac{x}{e^{x}}}}{2}
\]
Proof
(+.f64 (+.f64 (*.f64 2 (exp.f64 (neg.f64 x))) (/.f64 x (exp.f64 x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 2 (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x)))) (/.f64 x (exp.f64 x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= count-2_binary64 (+.f64 (exp.f64 (*.f64 -1 x)) (exp.f64 (*.f64 -1 x)))) (/.f64 x (exp.f64 x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-+l+_binary64 (+.f64 (exp.f64 (*.f64 -1 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 x (exp.f64 x))))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (exp.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 x))) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 x (exp.f64 x)))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 x (exp.f64 x)))) (/.f64 x (exp.f64 x))): 1 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)) (exp.f64 x)))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (exp.f64 x)) x)))) (/.f64 x (exp.f64 x))): 1 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (*.f64 (Rewrite=> rec-exp_binary64 (exp.f64 (neg.f64 x))) x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (*.f64 (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))) x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x))))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 x (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (*.f64 -1 (/.f64 x (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) 0)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (Rewrite<= +-inverses_binary64 (-.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (/.f64 (exp.f64 (*.f64 -1 x)) eps)))) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (/.f64 (exp.f64 (*.f64 -1 x)) eps))) (*.f64 -1 (/.f64 x (exp.f64 x)))): 127 points increase in error, 1 points decrease in error
(-.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x))) (/.f64 1 (exp.f64 x))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 x)))) (/.f64 1 (exp.f64 x)))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x)))) (/.f64 1 (exp.f64 x)))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (/.f64 1 (exp.f64 x))) (Rewrite=> rec-exp_binary64 (exp.f64 (neg.f64 x))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (/.f64 1 (exp.f64 x))) (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x)))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (/.f64 (exp.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 x))) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (/.f64 (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 1 points increase in error, 1 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (Rewrite=> associate-/l/_binary64 (/.f64 1 (*.f64 eps (exp.f64 x))))) (*.f64 -1 (/.f64 x (exp.f64 x)))): 2 points increase in error, 0 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (+.f64 (/.f64 1 (*.f64 eps (exp.f64 x))) (*.f64 -1 (/.f64 x (exp.f64 x)))))): 63 points increase in error, 62 points decrease in error
Taylor expanded in x around inf 0.6
\[\leadsto \frac{\color{blue}{\left(\frac{x}{e^{x}} + 2 \cdot e^{-x}\right)} + \frac{x}{e^{x}}}{2}
\]
Simplified0.6
\[\leadsto \frac{\color{blue}{\left(\frac{x}{e^{x}} + \frac{2}{e^{x}}\right)} + \frac{x}{e^{x}}}{2}
\]
Proof
(+.f64 (/.f64 x (exp.f64 x)) (/.f64 2 (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x (exp.f64 x)) (/.f64 (Rewrite<= metadata-eval (*.f64 2 1)) (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x (exp.f64 x)) (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 1 (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 x (exp.f64 x)) (*.f64 2 (Rewrite<= exp-neg_binary64 (exp.f64 (neg.f64 x))))): 1 points increase in error, 1 points decrease in error
Taylor expanded in x around inf 0.6
\[\leadsto \frac{\color{blue}{\left(2 \cdot \frac{1}{e^{x}} + \frac{x}{e^{x}}\right)} + \frac{x}{e^{x}}}{2}
\]
Simplified0.6
\[\leadsto \frac{\color{blue}{\frac{2 + x}{e^{x}}} + \frac{x}{e^{x}}}{2}
\]
Proof
(/.f64 (+.f64 2 x) (exp.f64 x)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 2 x))) (exp.f64 x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (exp.f64 x)) (+.f64 2 x))): 2 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> rec-exp_binary64 (exp.f64 (neg.f64 x))) (+.f64 2 x)): 1 points increase in error, 1 points decrease in error
(Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 2 (exp.f64 (neg.f64 x))) (*.f64 x (exp.f64 (neg.f64 x))))): 1 points increase in error, 1 points decrease in error
(Rewrite=> fma-def_binary64 (fma.f64 2 (exp.f64 (neg.f64 x)) (*.f64 x (exp.f64 (neg.f64 x))))): 0 points increase in error, 0 points decrease in error
(fma.f64 2 (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))) (*.f64 x (exp.f64 (neg.f64 x)))): 1 points increase in error, 1 points decrease in error
(fma.f64 2 (/.f64 1 (exp.f64 x)) (*.f64 x (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
(fma.f64 2 (/.f64 1 (exp.f64 x)) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 x 1) (exp.f64 x)))): 1 points increase in error, 0 points decrease in error
(fma.f64 2 (/.f64 1 (exp.f64 x)) (/.f64 (Rewrite=> *-rgt-identity_binary64 x) (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 (/.f64 1 (exp.f64 x))) (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
Final simplification0.6
\[\leadsto \frac{\frac{2 + x}{e^{x}} + \frac{x}{e^{x}}}{2}
\]