Initial program 41.2
\[\sqrt{\frac{e^{2 \cdot x} - 1}{e^{x} - 1}}
\]
Simplified0.0
\[\leadsto \color{blue}{\sqrt{1 + e^{x}}}
\]
Proof
(sqrt.f64 (+.f64 1 (exp.f64 x))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (exp.f64 x) 1))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (+.f64 (exp.f64 x) 1) 1))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (/.f64 (+.f64 (exp.f64 x) 1) (Rewrite<= *-inverses_binary64 (/.f64 (-.f64 (exp.f64 x) 1) (-.f64 (exp.f64 x) 1))))): 139 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (exp.f64 x) 1) (-.f64 (exp.f64 x) 1)) (-.f64 (exp.f64 x) 1)))): 1 points increase in error, 0 points decrease in error
(sqrt.f64 (/.f64 (Rewrite<= difference-of-sqr-1_binary64 (-.f64 (*.f64 (exp.f64 x) (exp.f64 x)) 1)) (-.f64 (exp.f64 x) 1))): 13 points increase in error, 1 points decrease in error
(sqrt.f64 (/.f64 (-.f64 (Rewrite<= exp-lft-sqr_binary64 (exp.f64 (*.f64 x 2))) 1) (-.f64 (exp.f64 x) 1))): 12 points increase in error, 0 points decrease in error
(sqrt.f64 (/.f64 (-.f64 (exp.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 x))) 1) (-.f64 (exp.f64 x) 1))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \sqrt{1 + e^{x}}
\]