Simplified0.6
\[\leadsto \color{blue}{\frac{\frac{y}{b - y} \cdot \left(x - \frac{t - a}{b - y}\right)}{z} + \frac{t - a}{b - y}}
\]
Proof
(+.f64 (/.f64 (*.f64 (/.f64 y (-.f64 b y)) (-.f64 x (/.f64 (-.f64 t a) (-.f64 b y)))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 y (-.f64 b y)) x) (*.f64 (/.f64 y (-.f64 b y)) (/.f64 (-.f64 t a) (-.f64 b y))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (-.f64 (Rewrite<= associate-/r/_binary64 (/.f64 y (/.f64 (-.f64 b y) x))) (*.f64 (/.f64 y (-.f64 b y)) (/.f64 (-.f64 t a) (-.f64 b y)))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 18 points increase in error, 13 points decrease in error
(+.f64 (/.f64 (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 (/.f64 y (-.f64 b y)) (/.f64 (-.f64 t a) (-.f64 b y)))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 28 points increase in error, 15 points decrease in error
(+.f64 (/.f64 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 y (-.f64 t a)) (*.f64 (-.f64 b y) (-.f64 b y))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 34 points increase in error, 2 points decrease in error
(+.f64 (/.f64 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 t a) y)) (*.f64 (-.f64 b y) (-.f64 b y)))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 b y) 2)))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (Rewrite<= metadata-eval (*.f64 -1 -1)) (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 -1 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z))) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 t (-.f64 b y)) (/.f64 a (-.f64 b y))))): 1 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)) (/.f64 t (-.f64 b y))) (/.f64 a (-.f64 b y)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 t (-.f64 b y)) (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2))))) z))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (/.f64 (*.f64 -1 (Rewrite=> distribute-lft-out--_binary64 (*.f64 -1 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))))) z)) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (/.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 -1 -1) (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2))))) z)) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (/.f64 (*.f64 (Rewrite=> metadata-eval 1) (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (/.f64 (Rewrite=> *-lft-identity_binary64 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (/.f64 (*.f64 y x) (-.f64 b y)) z) (/.f64 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)) z)))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (-.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 y x) (*.f64 (-.f64 b y) z))) (/.f64 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)) z))) (/.f64 a (-.f64 b y))): 15 points increase in error, 13 points decrease in error
(-.f64 (+.f64 (/.f64 t (-.f64 b y)) (-.f64 (/.f64 (*.f64 y x) (*.f64 (-.f64 b y) z)) (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 (-.f64 t a) y) (*.f64 (pow.f64 (-.f64 b y) 2) z))))) (/.f64 a (-.f64 b y))): 2 points increase in error, 2 points decrease in error
(-.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 t (-.f64 b y)) (/.f64 (*.f64 y x) (*.f64 (-.f64 b y) z))) (/.f64 (*.f64 (-.f64 t a) y) (*.f64 (pow.f64 (-.f64 b y) 2) z)))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 t (-.f64 b y)) (/.f64 (*.f64 y x) (Rewrite<= *-commutative_binary64 (*.f64 z (-.f64 b y))))) (/.f64 (*.f64 (-.f64 t a) y) (*.f64 (pow.f64 (-.f64 b y) 2) z))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 y x) (*.f64 z (-.f64 b y))) (/.f64 t (-.f64 b y)))) (/.f64 (*.f64 (-.f64 t a) y) (*.f64 (pow.f64 (-.f64 b y) 2) z))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (+.f64 (/.f64 (*.f64 y x) (*.f64 z (-.f64 b y))) (/.f64 t (-.f64 b y))) (/.f64 (*.f64 (-.f64 t a) y) (Rewrite<= *-commutative_binary64 (*.f64 z (pow.f64 (-.f64 b y) 2))))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 (+.f64 (/.f64 (*.f64 y x) (*.f64 z (-.f64 b y))) (/.f64 t (-.f64 b y))) (+.f64 (/.f64 (*.f64 (-.f64 t a) y) (*.f64 z (pow.f64 (-.f64 b y) 2))) (/.f64 a (-.f64 b y))))): 0 points increase in error, 0 points decrease in error