Simplified5.2
\[\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
(Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 (/.f64 im (sqrt.f64 re))) (sqrt.f64 (/.f64 im (sqrt.f64 re))))): 30 points increase in error, 23 points decrease in error
(Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (sqrt.f64 (/.f64 im (sqrt.f64 re))) (sqrt.f64 (/.f64 im (sqrt.f64 re)))))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (Rewrite=> rem-square-sqrt_binary64 (/.f64 im (sqrt.f64 re)))): 23 points increase in error, 30 points decrease in error
(Rewrite<= rem-sqrt-square_binary64 (sqrt.f64 (*.f64 (/.f64 im (sqrt.f64 re)) (/.f64 im (sqrt.f64 re))))): 53 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 im im) (*.f64 (sqrt.f64 re) (sqrt.f64 re))))): 18 points increase in error, 5 points decrease in error
(sqrt.f64 (/.f64 (*.f64 im im) (Rewrite=> rem-square-sqrt_binary64 re))): 6 points increase in error, 48 points decrease in error
(sqrt.f64 (Rewrite=> associate-/l*_binary64 (/.f64 im (/.f64 re im)))): 12 points increase in error, 15 points decrease in error
(Rewrite<= unpow1/2_binary64 (pow.f64 (/.f64 im (/.f64 re im)) 1/2)): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-rgt-identity_binary64 (+.f64 (pow.f64 (/.f64 im (/.f64 re im)) 1/2) 0)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> unpow1/2_binary64 (sqrt.f64 (/.f64 im (/.f64 re im)))) 0): 0 points increase in error, 0 points decrease in error
(+.f64 (sqrt.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 im im) re))) 0): 15 points increase in error, 12 points decrease in error
(+.f64 (sqrt.f64 (/.f64 (*.f64 im im) (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 re) (sqrt.f64 re))))) 0): 48 points increase in error, 6 points decrease in error
(+.f64 (sqrt.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 im (sqrt.f64 re)) (/.f64 im (sqrt.f64 re))))) 0): 5 points increase in error, 18 points decrease in error
(+.f64 (Rewrite=> rem-sqrt-square_binary64 (fabs.f64 (/.f64 im (sqrt.f64 re)))) 0): 0 points increase in error, 53 points decrease in error
(+.f64 (fabs.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 (/.f64 im (sqrt.f64 re))) (sqrt.f64 (/.f64 im (sqrt.f64 re)))))) 0): 30 points increase in error, 23 points decrease in error
(+.f64 (Rewrite=> fabs-sqr_binary64 (*.f64 (sqrt.f64 (/.f64 im (sqrt.f64 re))) (sqrt.f64 (/.f64 im (sqrt.f64 re))))) 0): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> rem-square-sqrt_binary64 (/.f64 im (sqrt.f64 re))) 0): 23 points increase in error, 30 points decrease in error
(+.f64 (/.f64 im (sqrt.f64 re)) (Rewrite<= metadata-eval (-.f64 1 1))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 im (sqrt.f64 re)) 1) 1)): 58 points increase in error, 6 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (/.f64 im (sqrt.f64 re)))) 1): 0 points increase in error, 0 points decrease in error