Initial program 0.0
\[\frac{2}{e^{x} + e^{-x}}
\]
Taylor expanded in x around inf 0.0
\[\leadsto \color{blue}{\frac{2}{e^{-x} + e^{x}}}
\]
Simplified0.0
\[\leadsto \color{blue}{\frac{1}{\cosh x}}
\]
Proof
(/.f64 1 (cosh.f64 x)): 0 points increase in error, 0 points decrease in error
(/.f64 1 (Rewrite=> cosh-def_binary64 (/.f64 (+.f64 (exp.f64 x) (exp.f64 (neg.f64 x))) 2))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 1 (+.f64 (exp.f64 x) (exp.f64 (neg.f64 x)))) 2)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 2) (+.f64 (exp.f64 x) (exp.f64 (neg.f64 x))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> metadata-eval 2) (+.f64 (exp.f64 x) (exp.f64 (neg.f64 x)))): 0 points increase in error, 0 points decrease in error
(/.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (exp.f64 (neg.f64 x)) (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \frac{1}{\cosh x}
\]