Simplified16.4
\[\leadsto 0.5 \cdot \color{blue}{\frac{im}{\sqrt{re}}}
\]
Proof
(/.f64 im (sqrt.f64 re)): 0 points increase in error, 0 points decrease in error
(/.f64 im (Rewrite<= unpow1/2_binary64 (pow.f64 re 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 im (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 re) 1/2)))): 62 points increase in error, 43 points decrease in error
(/.f64 (Rewrite<= rem-exp-log_binary64 (exp.f64 (log.f64 im))) (exp.f64 (*.f64 (log.f64 re) 1/2))): 52 points increase in error, 53 points decrease in error
(Rewrite=> div-exp_binary64 (exp.f64 (-.f64 (log.f64 im) (*.f64 (log.f64 re) 1/2)))): 43 points increase in error, 38 points decrease in error
(exp.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (log.f64 im) (neg.f64 (*.f64 (log.f64 re) 1/2))))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 im) (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 (log.f64 re) (neg.f64 1/2))))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 im) (*.f64 (log.f64 re) (Rewrite=> metadata-eval -1/2)))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 im) (Rewrite=> *-commutative_binary64 (*.f64 -1/2 (log.f64 re))))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 im) (Rewrite<= log-pow_binary64 (log.f64 (pow.f64 re -1/2))))): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite<= +-commutative_binary64 (+.f64 (log.f64 (pow.f64 re -1/2)) (log.f64 im)))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (Rewrite=> log-pow_binary64 (*.f64 -1/2 (log.f64 re))) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 1/2)) (log.f64 re)) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 1/2 (log.f64 re)))) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 1/2 (neg.f64 (log.f64 re)))) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite=> fma-def_binary64 (fma.f64 1/2 (neg.f64 (log.f64 re)) (log.f64 im)))): 0 points increase in error, 0 points decrease in error
(exp.f64 (fma.f64 1/2 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 re))) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (fma.f64 1/2 (log.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1/2 2)) re)) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (fma.f64 1/2 (log.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1/2 re) 2))) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (log.f64 (*.f64 (/.f64 1/2 re) 2))) (log.f64 im)))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (Rewrite<= log-pow_binary64 (log.f64 (pow.f64 (*.f64 (/.f64 1/2 re) 2) 1/2))) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 (pow.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1/2 2) re)) 1/2)) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 (pow.f64 (/.f64 (Rewrite=> metadata-eval 1) re) 1/2)) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 (pow.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 2 1/2)) re) 1/2)) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (log.f64 (pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 1/2 re))) 1/2)) (log.f64 im))): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite<= log-prod_binary64 (log.f64 (*.f64 (pow.f64 (*.f64 2 (/.f64 1/2 re)) 1/2) im)))): 23 points increase in error, 26 points decrease in error
(Rewrite=> rem-exp-log_binary64 (*.f64 (pow.f64 (*.f64 2 (/.f64 1/2 re)) 1/2) im)): 52 points increase in error, 52 points decrease in error
(Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 (pow.f64 (*.f64 2 (/.f64 1/2 re)) 1/2) im))): 0 points increase in error, 0 points decrease in error