Simplified4.4
\[\leadsto \color{blue}{y + \frac{\left(x - y\right) \cdot \left(z - a\right)}{t}}
\]
Proof
(+.f64 y (/.f64 (*.f64 (-.f64 x y) (-.f64 z a)) t)): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (*.f64 (Rewrite<= unsub-neg_binary64 (+.f64 x (neg.f64 y))) (-.f64 z a)) t)): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 y) x)) (-.f64 z a)) t)): 0 points increase in error, 17 points decrease in error
(+.f64 y (/.f64 (*.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 y)) x) (-.f64 z a)) t)): 17 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (*.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 y x))) (-.f64 z a)) t)): 0 points increase in error, 17 points decrease in error
(+.f64 y (/.f64 (*.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 y x))) (-.f64 z a)) t)): 17 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (*.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (-.f64 y x))) (-.f64 z a)) t)): 0 points increase in error, 17 points decrease in error
(+.f64 y (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (-.f64 y x) (-.f64 z a)))) t)): 17 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (*.f64 -1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 z (-.f64 y x)) (*.f64 a (-.f64 y x))))) t)): 0 points increase in error, 17 points decrease in error
(+.f64 y (/.f64 (*.f64 -1 (-.f64 (Rewrite=> *-commutative_binary64 (*.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)): 17 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 (*.f64 -1 (*.f64 a (-.f64 y x))) t)))): 0 points increase in error, 17 points decrease in error
(+.f64 y (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 y x) z) t))) (/.f64 (*.f64 -1 (*.f64 a (-.f64 y x))) t))): 17 points increase in error, 0 points decrease in error
(+.f64 y (-.f64 (*.f64 -1 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 z (-.f64 y x))) t)) (/.f64 (*.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, 17 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)))): 17 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, 17 points decrease in error