Simplified0.6
\[\leadsto \color{blue}{\left(z - y\right) \cdot \frac{x}{z - t}}
\]
Proof
(*.f64 (-.f64 z y) (/.f64 x (-.f64 z t))): 0 points increase in error, 0 points decrease in error
(Rewrite=> *-commutative_binary64 (*.f64 (/.f64 x (-.f64 z t)) (-.f64 z y))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 x (/.f64 (-.f64 z t) (-.f64 z y)))): 28 points increase in error, 66 points decrease in error
(/.f64 x (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 z t) (-.f64 z y))))): 0 points increase in error, 0 points decrease in error
(/.f64 x (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (/.f64 (-.f64 z t) (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (-.f64 z t)) (*.f64 -1 (-.f64 z y))))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 z t))) (*.f64 -1 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 z t))) (*.f64 -1 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 z) t)) (*.f64 -1 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 z)) t) (*.f64 -1 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 t (neg.f64 z))) (*.f64 -1 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 t z)) (*.f64 -1 (-.f64 z y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (-.f64 t z) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 z y))))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (-.f64 t z) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 z y))))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (-.f64 t z) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 z) y)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (-.f64 t z) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 z)) y))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (-.f64 t z) (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 z))))): 0 points increase in error, 0 points decrease in error
(/.f64 x (/.f64 (-.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 (*.f64 x (-.f64 y z)) (-.f64 t z))): 66 points increase in error, 30 points decrease in error