Simplified21.5
\[\leadsto \color{blue}{\frac{b}{d} - \frac{c}{d \cdot d} \cdot \left(\frac{b \cdot c}{d} - a\right)}
\]
Proof
(-.f64 (/.f64 b d) (*.f64 (/.f64 c (*.f64 d d)) (-.f64 (/.f64 (*.f64 b c) d) a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (*.f64 (/.f64 c (Rewrite<= unpow2_binary64 (pow.f64 d 2))) (-.f64 (/.f64 (*.f64 b c) d) a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 c (pow.f64 d 2)) (/.f64 (*.f64 b c) d)) (*.f64 (/.f64 c (pow.f64 d 2)) a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (-.f64 (*.f64 (/.f64 c (pow.f64 d 2)) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 c b)) d)) (*.f64 (/.f64 c (pow.f64 d 2)) a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c (*.f64 c b)) (*.f64 (pow.f64 d 2) d))) (*.f64 (/.f64 c (pow.f64 d 2)) a))): 18 points increase in error, 5 points decrease in error
(-.f64 (/.f64 b d) (-.f64 (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c c) b)) (*.f64 (pow.f64 d 2) d)) (*.f64 (/.f64 c (pow.f64 d 2)) a))): 13 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (-.f64 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) b) (*.f64 (pow.f64 d 2) d)) (*.f64 (/.f64 c (pow.f64 d 2)) a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (-.f64 (/.f64 (*.f64 (pow.f64 c 2) b) (*.f64 (Rewrite=> unpow2_binary64 (*.f64 d d)) d)) (*.f64 (/.f64 c (pow.f64 d 2)) a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (-.f64 (/.f64 (*.f64 (pow.f64 c 2) b) (Rewrite<= unpow3_binary64 (pow.f64 d 3))) (*.f64 (/.f64 c (pow.f64 d 2)) a))): 2 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b d) (-.f64 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 3)) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 c a) (pow.f64 d 2))))): 9 points increase in error, 6 points decrease in error
(Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (/.f64 b d) (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 3))) (/.f64 (*.f64 c a) (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 b d) (neg.f64 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 3))))) (/.f64 (*.f64 c a) (pow.f64 d 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 b d) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 3))))) (/.f64 (*.f64 c a) (pow.f64 d 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 3))) (/.f64 b d))) (/.f64 (*.f64 c a) (pow.f64 d 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (pow.f64 c 2) b) (pow.f64 d 3))) (+.f64 (/.f64 b d) (/.f64 (*.f64 c a) (pow.f64 d 2))))): 0 points increase in error, 0 points decrease in error
Simplified11.7
\[\leadsto \frac{b}{d} - \color{blue}{\frac{a}{d} \cdot \frac{-c}{d}}
\]
Proof
(*.f64 (/.f64 a d) (/.f64 (neg.f64 c) d)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 a d) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 c d)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> *-commutative_binary64 (*.f64 (neg.f64 (/.f64 c d)) (/.f64 a d))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 c d))) (/.f64 a d)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (/.f64 c d) (/.f64 a d)))): 0 points increase in error, 0 points decrease in error
(*.f64 -1 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c a) (*.f64 d d)))): 67 points increase in error, 38 points decrease in error
(*.f64 -1 (/.f64 (*.f64 c a) (Rewrite<= unpow2_binary64 (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error