Simplified57.4
\[\leadsto \color{blue}{0.5 \cdot \sqrt{2 \cdot \left(re + \mathsf{hypot}\left(re, im\right)\right)}}
\]
Proof
(*.f64 1/2 (sqrt.f64 (*.f64 2 (+.f64 re (hypot.f64 re im))))): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (sqrt.f64 (*.f64 2 (+.f64 re (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 re re) (*.f64 im im)))))))): 121 points increase in error, 0 points decrease in error
(*.f64 1/2 (sqrt.f64 (*.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (sqrt.f64 (+.f64 (*.f64 re re) (*.f64 im im))) re))))): 0 points increase in error, 0 points decrease in error
Simplified30.9
\[\leadsto 0.5 \cdot \sqrt{2 \cdot \color{blue}{\frac{\left(-0.5 \cdot im\right) \cdot im}{re}}}
\]
Proof
(/.f64 (*.f64 (*.f64 -1/2 im) im) re): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1/2 (*.f64 im im))) re): 1 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1/2 (Rewrite<= unpow2_binary64 (pow.f64 im 2))) re): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 (pow.f64 im 2) re))): 0 points increase in error, 1 points decrease in error
Simplified31.4
\[\leadsto \color{blue}{\sqrt{\frac{-0.25}{\frac{re}{im \cdot im}}}}
\]
Proof
(sqrt.f64 (/.f64 -1/4 (/.f64 re (*.f64 im im)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 -1 1/4)) (/.f64 re (*.f64 im im)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 -1 (/.f64 re (*.f64 im im))) 1/4))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/4)): 3 points increase in error, 6 points decrease in error
(sqrt.f64 (*.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)))) 1/4)): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re))) (Rewrite<= metadata-eval (*.f64 1/2 1/2)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2) (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)))): 0 points increase in error, 1 points decrease in error
(Rewrite=> rem-sqrt-square_binary64 (fabs.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2))): 0 points increase in error, 1 points decrease in error
(fabs.f64 (Rewrite<= rem-cube-cbrt_binary64 (pow.f64 (cbrt.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)) 3))): 35 points increase in error, 5 points decrease in error
(fabs.f64 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 (cbrt.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)) (/.f64 3 2)) (pow.f64 (cbrt.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)) (/.f64 3 2))))): 8 points increase in error, 11 points decrease in error
(Rewrite=> fabs-sqr_binary64 (*.f64 (pow.f64 (cbrt.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)) (/.f64 3 2)) (pow.f64 (cbrt.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)) (/.f64 3 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sqr-pow_binary64 (pow.f64 (cbrt.f64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)) 3)): 11 points increase in error, 8 points decrease in error
(Rewrite=> rem-cube-cbrt_binary64 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2)): 5 points increase in error, 35 points decrease in error
(Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 (sqrt.f64 (/.f64 (*.f64 -1 (*.f64 im im)) re)) 1/2))): 0 points increase in error, 0 points decrease in error