Simplified21.1
\[\leadsto \color{blue}{y - \frac{y - x}{\frac{t}{z - a}}}
\]
Proof
(-.f64 y (/.f64 (-.f64 y x) (/.f64 t (-.f64 z a)))): 0 points increase in error, 0 points decrease in error
(-.f64 y (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 y x) (-.f64 z a)) t))): 37 points increase in error, 32 points decrease in error
(-.f64 y (/.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 z (-.f64 y x)) (*.f64 a (-.f64 y x)))) t)): 0 points increase in error, 1 points decrease in error
(-.f64 y (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 z (-.f64 y x)) t) (/.f64 (*.f64 a (-.f64 y x)) t)))): 1 points increase in error, 0 points decrease in error
(-.f64 y (-.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (-.f64 y x) z)) t) (/.f64 (*.f64 a (-.f64 y x)) t))): 0 points increase in error, 0 points decrease in error
(-.f64 y (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (*.f64 (-.f64 y x) z) (*.f64 a (-.f64 y x))) t))): 0 points increase in error, 1 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 y (neg.f64 (/.f64 (-.f64 (*.f64 (-.f64 y x) z) (*.f64 a (-.f64 y x))) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 (-.f64 y x) z) (*.f64 a (-.f64 y x))) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 (*.f64 (-.f64 y x) z) (*.f64 a (-.f64 y x)))) t))): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (*.f64 (-.f64 y x) z)) (*.f64 -1 (*.f64 a (-.f64 y x))))) t)): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (-.f64 (*.f64 -1 (*.f64 (-.f64 y x) z)) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 a (-.f64 y x))))) t)): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 -1 (*.f64 (-.f64 y x) z)) t) (/.f64 (neg.f64 (*.f64 a (-.f64 y x))) t)))): 1 points increase in error, 0 points decrease in error
(+.f64 y (-.f64 (/.f64 (*.f64 -1 (Rewrite<= *-commutative_binary64 (*.f64 z (-.f64 y x)))) t) (/.f64 (neg.f64 (*.f64 a (-.f64 y x))) t))): 0 points increase in error, 0 points decrease in error
(+.f64 y (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t))) (/.f64 (neg.f64 (*.f64 a (-.f64 y x))) t))): 0 points increase in error, 0 points decrease in error
(+.f64 y (-.f64 (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t)) (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 a (-.f64 y x)))) t))): 0 points increase in error, 0 points decrease in error
(+.f64 y (-.f64 (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t)) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 a (-.f64 y x)) t))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 y (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t))) (*.f64 -1 (/.f64 (*.f64 a (-.f64 y x)) t)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t)) y)) (*.f64 -1 (/.f64 (*.f64 a (-.f64 y x)) t))): 0 points increase in error, 0 points decrease in error