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