Simplified58.0
\[\leadsto \left(0.5 \cdot \cos re\right) \cdot \color{blue}{\frac{e^{im \cdot -3} - e^{3 \cdot im}}{1 + \left(e^{im \cdot -2} + {\left(e^{2}\right)}^{im}\right)}}
\]
Proof
(/.f64 (-.f64 (exp.f64 (*.f64 im -3)) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (*.f64 im (Rewrite<= metadata-eval (+.f64 -2 -1)))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (*.f64 im (+.f64 (Rewrite<= metadata-eval (+.f64 -1 -1)) -1))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 im (+.f64 -1 -1)) (*.f64 im -1)))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (+.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1 im) (*.f64 -1 im))) (*.f64 im -1))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (+.f64 (+.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 im)) (*.f64 -1 im)) (*.f64 im -1))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (+.f64 (+.f64 (neg.f64 im) (Rewrite<= neg-mul-1_binary64 (neg.f64 im))) (*.f64 im -1))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (+.f64 (+.f64 (neg.f64 im) (neg.f64 im)) (Rewrite<= *-commutative_binary64 (*.f64 -1 im)))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (exp.f64 (+.f64 (+.f64 (neg.f64 im) (neg.f64 im)) (Rewrite<= neg-mul-1_binary64 (neg.f64 im)))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 (+.f64 (neg.f64 im) (neg.f64 im))) (exp.f64 (neg.f64 im)))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 2 points increase in error, 1 points decrease in error
(/.f64 (-.f64 (*.f64 (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im)))) (exp.f64 (neg.f64 im))) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 2 points increase in error, 3 points decrease in error
(/.f64 (-.f64 (Rewrite<= unpow3_binary64 (pow.f64 (exp.f64 (neg.f64 im)) 3)) (exp.f64 (*.f64 3 im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 2 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (exp.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 2 1)) im))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (exp.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 im (*.f64 2 im))))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (exp.f64 (+.f64 im (Rewrite<= count-2_binary64 (+.f64 im im))))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 im) (exp.f64 (+.f64 im im))))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 1 points increase in error, 1 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (*.f64 (exp.f64 im) (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 im) (exp.f64 im))))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 3 points increase in error, 2 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (Rewrite<= cube-mult_binary64 (pow.f64 (exp.f64 im) 3))) (+.f64 1 (+.f64 (exp.f64 (*.f64 im -2)) (pow.f64 (exp.f64 2) im)))): 1 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (exp.f64 (*.f64 im (Rewrite<= metadata-eval (+.f64 -1 -1)))) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (exp.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1 im) (*.f64 -1 im)))) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (exp.f64 (+.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 im)) (*.f64 -1 im))) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (exp.f64 (+.f64 (neg.f64 im) (Rewrite<= neg-mul-1_binary64 (neg.f64 im)))) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im)))) (pow.f64 (exp.f64 2) im)))): 0 points increase in error, 1 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im))) (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 2 im)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im))) (exp.f64 (Rewrite<= count-2_binary64 (+.f64 im im)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 1 (+.f64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im))) (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 im) (exp.f64 im)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im))) (*.f64 (exp.f64 im) (exp.f64 im))) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 (+.f64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im))) (*.f64 (exp.f64 im) (exp.f64 im))) (Rewrite<= lft-mult-inverse_binary64 (*.f64 (/.f64 1 (exp.f64 im)) (exp.f64 im))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (+.f64 (+.f64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im))) (*.f64 (exp.f64 im) (exp.f64 im))) (*.f64 (Rewrite<= exp-neg_binary64 (exp.f64 (neg.f64 im))) (exp.f64 im)))): 2 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (exp.f64 (neg.f64 im)) 3) (pow.f64 (exp.f64 im) 3)) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 (neg.f64 im))) (+.f64 (*.f64 (exp.f64 im) (exp.f64 im)) (*.f64 (exp.f64 (neg.f64 im)) (exp.f64 im)))))): 0 points increase in error, 2 points decrease in error