Simplified25.8
\[\leadsto e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \color{blue}{\left(\left(\left(\left(-0.5 \cdot y.im\right) \cdot y.im\right) \cdot {\log \left(\mathsf{hypot}\left(x.im, x.re\right)\right)}^{2} + 1\right) \cdot \cos \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) - y.im \cdot \left(\log \left(\mathsf{hypot}\left(x.im, x.re\right)\right) \cdot \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right)}
\]
Proof
(-.f64 (*.f64 (+.f64 (*.f64 (*.f64 (*.f64 -1/2 y.im) y.im) (pow.f64 (log.f64 (hypot.f64 x.im x.re)) 2)) 1) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (+.f64 (*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1/2 (*.f64 y.im y.im))) (pow.f64 (log.f64 (hypot.f64 x.im x.re)) 2)) 1) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (+.f64 (*.f64 (*.f64 -1/2 (Rewrite<= unpow2_binary64 (pow.f64 y.im 2))) (pow.f64 (log.f64 (hypot.f64 x.im x.re)) 2)) 1) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (+.f64 (*.f64 (*.f64 -1/2 (pow.f64 y.im 2)) (pow.f64 (log.f64 (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 x.im x.im) (*.f64 x.re x.re))))) 2)) 1) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 111 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (+.f64 (*.f64 (*.f64 -1/2 (pow.f64 y.im 2)) (pow.f64 (log.f64 (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 x.im 2)) (*.f64 x.re x.re)))) 2)) 1) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (+.f64 (*.f64 (*.f64 -1/2 (pow.f64 y.im 2)) (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (Rewrite<= unpow2_binary64 (pow.f64 x.re 2))))) 2)) 1) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 (*.f64 (*.f64 -1/2 (pow.f64 y.im 2)) (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2)) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 -1/2 (pow.f64 y.im 2)) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 3 points decrease in error
(-.f64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (Rewrite<= associate-*r*_binary64 (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))))) (*.f64 y.im (*.f64 (log.f64 (hypot.f64 x.im x.re)) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))))) (*.f64 y.im (*.f64 (log.f64 (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 x.im x.im) (*.f64 x.re x.re))))) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))))) (*.f64 y.im (*.f64 (log.f64 (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 x.im 2)) (*.f64 x.re x.re)))) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))))) (*.f64 y.im (*.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (Rewrite<= unpow2_binary64 (pow.f64 x.re 2))))) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y.im (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2))))) (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))))) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 y.im (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r-_binary64 (+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (-.f64 (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))) (*.f64 (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 y.im (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))) (neg.f64 (*.f64 (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 y.im (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (+.f64 (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 y.im (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))) (*.f64 -1 (*.f64 (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 y.im (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))))))) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1/2 (*.f64 (pow.f64 y.im 2) (*.f64 (pow.f64 (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2)))) 2) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))) (+.f64 (*.f64 -1 (*.f64 (sin.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (*.f64 y.im (log.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2))))))) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re)))))): 1 points increase in error, 1 points decrease in error
Simplified17.1
\[\leadsto \color{blue}{\cos \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot {\left(\mathsf{hypot}\left(x.im, x.re\right)\right)}^{y.re}}
\]
Proof
(*.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (pow.f64 (hypot.f64 x.im x.re) y.re)): 0 points increase in error, 0 points decrease in error
(*.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (pow.f64 (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 x.im x.im) (*.f64 x.re x.re)))) y.re)): 81 points increase in error, 12 points decrease in error
(*.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (pow.f64 (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 x.im 2)) (*.f64 x.re x.re))) y.re)): 0 points increase in error, 0 points decrease in error
(*.f64 (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))) (pow.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (Rewrite<= unpow2_binary64 (pow.f64 x.re 2)))) y.re)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 (sqrt.f64 (+.f64 (pow.f64 x.im 2) (pow.f64 x.re 2))) y.re) (cos.f64 (*.f64 y.re (atan2.f64 x.im x.re))))): 0 points increase in error, 0 points decrease in error