Simplified10.3
\[\leadsto \frac{\color{blue}{0.5 \cdot \mathsf{fma}\left({\left(\frac{c}{d}\right)}^{3}, a, b \cdot \left(\frac{c}{d} \cdot \frac{c}{d}\right)\right) - \mathsf{fma}\left(\frac{c}{d}, a, b\right)}}{\mathsf{hypot}\left(c, d\right)}
\]
Proof
(-.f64 (*.f64 1/2 (fma.f64 (pow.f64 (/.f64 c d) 3) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (Rewrite<= cube-unmult_binary64 (*.f64 (/.f64 c d) (*.f64 (/.f64 c d) (/.f64 c d)))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 1 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (*.f64 (/.f64 c d) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c c) (*.f64 d d)))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 20 points increase in error, 1 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (*.f64 (/.f64 c d) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 d d))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (*.f64 (/.f64 c d) (/.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 d 2)))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c (pow.f64 c 2)) (*.f64 d (pow.f64 d 2)))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 15 points increase in error, 1 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (*.f64 c (Rewrite=> unpow2_binary64 (*.f64 c c))) (*.f64 d (pow.f64 d 2))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (Rewrite<= cube-mult_binary64 (pow.f64 c 3)) (*.f64 d (pow.f64 d 2))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 1 points increase in error, 1 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (pow.f64 c 3) (*.f64 d (Rewrite=> unpow2_binary64 (*.f64 d d)))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (pow.f64 c 3) (Rewrite<= cube-mult_binary64 (pow.f64 d 3))) a (*.f64 b (*.f64 (/.f64 c d) (/.f64 c d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (pow.f64 c 3) (pow.f64 d 3)) a (*.f64 b (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c c) (*.f64 d d)))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 2 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (pow.f64 c 3) (pow.f64 d 3)) a (*.f64 b (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 d d))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (pow.f64 c 3) (pow.f64 d 3)) a (*.f64 b (/.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 d 2)))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (pow.f64 c 3) (pow.f64 d 3)) a (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 c 2) (pow.f64 d 2)) b)))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (fma.f64 (/.f64 (pow.f64 c 3) (pow.f64 d 3)) a (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2))))) (fma.f64 (/.f64 c d) a b)): 4 points increase in error, 1 points decrease in error
(-.f64 (*.f64 1/2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 d 3)) a) (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 1/2 (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2)))) (fma.f64 (/.f64 c d) a b)): 3 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2))))) (fma.f64 (/.f64 c d) a b)): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 c d) a) b))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2)))) (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 c a) d)) b)): 4 points increase in error, 4 points decrease in error
(-.f64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2)))) (Rewrite<= +-commutative_binary64 (+.f64 b (/.f64 (*.f64 c a) d)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2)))) (neg.f64 (+.f64 b (/.f64 (*.f64 c a) d))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2)))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 b (/.f64 (*.f64 c a) d))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2)))) (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 -1 b) (*.f64 -1 (/.f64 (*.f64 c a) d))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 3) a) (pow.f64 d 3))) (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 2))) (+.f64 (*.f64 -1 b) (*.f64 -1 (/.f64 (*.f64 c a) d)))))): 0 points increase in error, 0 points decrease in error