Simplified2.1
\[\leadsto \color{blue}{\frac{\frac{x}{z - t}}{z - y}}
\]
Proof
(/.f64 (/.f64 x (-.f64 z t)) (-.f64 z y)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (Rewrite=> sub-neg_binary64 (+.f64 z (neg.f64 t)))) (-.f64 z y)): 0 points increase in error, 15 points decrease in error
(/.f64 (/.f64 x (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 z))) (neg.f64 t))) (-.f64 z y)): 1 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 z) t)))) (-.f64 z y)): 0 points increase in error, 1 points decrease in error
(/.f64 (/.f64 x (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 t (neg.f64 z))))) (-.f64 z y)): 16 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 t z)))) (-.f64 z y)): 0 points increase in error, 16 points decrease in error
(/.f64 (/.f64 x (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (-.f64 t z)))) (-.f64 z y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 x (-.f64 t z)) -1)) (-.f64 z y)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (/.f64 x (-.f64 t z)) (*.f64 -1 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (-.f64 t z)) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (-.f64 t z)) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (-.f64 t z)) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 z) y))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (-.f64 t z)) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 z)) y)): 16 points increase in error, 0 points decrease in error
(/.f64 (/.f64 x (-.f64 t z)) (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 z)))): 0 points increase in error, 16 points decrease in error
(/.f64 (/.f64 x (-.f64 t z)) (Rewrite<= sub-neg_binary64 (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-/l/_binary64 (/.f64 x (*.f64 (-.f64 y z) (-.f64 t z)))): 0 points increase in error, 0 points decrease in error