Simplified15.8
\[\leadsto \color{blue}{\frac{z}{b} - \frac{\frac{t}{\frac{b}{1 + a} \cdot \frac{b}{z}} - \frac{t}{b} \cdot x}{y}}
\]
Proof
(-.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 t (*.f64 (/.f64 b (+.f64 1 a)) (/.f64 b z))) (*.f64 (/.f64 t b) x)) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 t (Rewrite<= times-frac_binary64 (/.f64 (*.f64 b b) (*.f64 (+.f64 1 a) z)))) (*.f64 (/.f64 t b) x)) y)): 17 points increase in error, 4 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 t (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2)) (*.f64 (+.f64 1 a) z))) (*.f64 (/.f64 t b) x)) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2))) (*.f64 (/.f64 t b) x)) y)): 17 points increase in error, 6 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) (Rewrite<= associate-/r/_binary64 (/.f64 t (/.f64 b x)))) y)): 7 points increase in error, 11 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 t x) b))) y)): 9 points increase in error, 4 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) (neg.f64 (/.f64 (*.f64 t x) b)))) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (+.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 t x) b)))) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 t x) b)) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)))) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 t x) b)) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2))))) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 t x) b)) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)))) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 z b) (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 -1 (/.f64 (*.f64 t x) b)) (*.f64 -1 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2))))) y)): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 z b) (neg.f64 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 t x) b)) (*.f64 -1 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)))) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (Rewrite=> distribute-neg-frac_binary64 (/.f64 (neg.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 t x) b)) (*.f64 -1 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2))))) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (neg.f64 (Rewrite=> distribute-lft-out--_binary64 (*.f64 -1 (-.f64 (/.f64 (*.f64 t x) b) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)))))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (neg.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (-.f64 (/.f64 (*.f64 t x) b) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)))))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (Rewrite=> remove-double-neg_binary64 (-.f64 (/.f64 (*.f64 t x) b) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (/.f64 (*.f64 t x) b) y) (/.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 t x) (*.f64 b y))) (/.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) y))): 10 points increase in error, 6 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (/.f64 (*.f64 t x) (Rewrite<= *-commutative_binary64 (*.f64 y b))) (/.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (/.f64 (*.f64 t x) (*.f64 y b)) (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (*.f64 (pow.f64 b 2) y))))): 7 points increase in error, 4 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (/.f64 (*.f64 t x) (*.f64 y b)) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (Rewrite<= *-commutative_binary64 (*.f64 y (pow.f64 b 2)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 z b) (/.f64 (*.f64 t x) (*.f64 y b))) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (*.f64 y (pow.f64 b 2))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 t x) (*.f64 y b)) (/.f64 z b))) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (*.f64 y (pow.f64 b 2)))): 0 points increase in error, 0 points decrease in error