Simplified6.1
\[\leadsto \color{blue}{t - \frac{t - x}{z} \cdot \left(y - a\right)}
\]
Proof
(-.f64 t (*.f64 (/.f64 (-.f64 t x) z) (-.f64 y a))): 0 points increase in error, 0 points decrease in error
(-.f64 t (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 t x) (/.f64 z (-.f64 y a))))): 22 points increase in error, 31 points decrease in error
(-.f64 t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 t x) (-.f64 y a)) z))): 45 points increase in error, 20 points decrease in error
(-.f64 t (/.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 y (-.f64 t x)) (*.f64 a (-.f64 t x)))) z)): 1 points increase in error, 1 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 (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 y (-.f64 t x)) z) (/.f64 (*.f64 a (-.f64 t x)) z))))): 1 points increase in error, 1 points decrease in error
(+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.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
(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, 2 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
Simplified0.4
\[\leadsto t - \color{blue}{\frac{x - t}{\frac{z}{a - y}}}
\]
Proof
(/.f64 (-.f64 x t) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (-.f64 x t)))) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 x t)))) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 x) t))) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 x)) t)) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 t (neg.f64 x)))) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 t x))) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (-.f64 t x))) (/.f64 z (-.f64 a y))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (Rewrite<= unsub-neg_binary64 (+.f64 a (neg.f64 y))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (+.f64 a (Rewrite=> neg-mul-1_binary64 (*.f64 -1 y))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 y) a)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (+.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 y)) a))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 y)) a))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 y a))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 y a))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 t x)) (/.f64 z (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (-.f64 y a))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 -1 (-.f64 t x)) (*.f64 -1 (-.f64 y a))) z)): 61 points increase in error, 32 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (*.f64 -1 (-.f64 t x)) (/.f64 (*.f64 -1 (-.f64 y a)) z))): 27 points increase in error, 56 points decrease in error
(*.f64 (*.f64 -1 (-.f64 t x)) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 y a) z)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 -1 (-.f64 t x)) (Rewrite=> mul-1-neg_binary64 (neg.f64 (/.f64 (-.f64 y a) z)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (*.f64 -1 (-.f64 t x)) (/.f64 (-.f64 y a) z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (*.f64 -1 (-.f64 t x))) (/.f64 (-.f64 y a) z))): 0 points increase in error, 0 points decrease in error
(*.f64 (neg.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (-.f64 t x)))) (/.f64 (-.f64 y a) z)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> remove-double-neg_binary64 (-.f64 t x)) (/.f64 (-.f64 y a) z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 y a) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 t (/.f64 (-.f64 y a) z)) (*.f64 x (/.f64 (-.f64 y a) z)))): 2 points increase in error, 1 points decrease in error
(-.f64 (*.f64 t (Rewrite=> div-sub_binary64 (-.f64 (/.f64 y z) (/.f64 a z)))) (*.f64 x (/.f64 (-.f64 y a) z))): 3 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t (-.f64 (/.f64 y z) (/.f64 a z))) (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 y a) z) x))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t (-.f64 (/.f64 y z) (/.f64 a z))) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 y a) x) z))): 29 points increase in error, 12 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 t (-.f64 (/.f64 y z) (/.f64 a z))) (neg.f64 (/.f64 (*.f64 (-.f64 y a) x) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 t (-.f64 (/.f64 y z) (/.f64 a z))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 y a) x) z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (-.f64 y a) x) z)) (*.f64 t (-.f64 (/.f64 y z) (/.f64 a z))))): 0 points increase in error, 0 points decrease in error