Simplified6.7
\[\leadsto \color{blue}{x + \mathsf{fma}\left(z - t, \frac{y}{t - a}, y\right)}
\]
Proof
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 y (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 y 1)) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (/.f64 y (Rewrite<= metadata-eval (neg.f64 -1))) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 y))) (neg.f64 -1)) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (neg.f64 y))) (neg.f64 -1)) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (neg.f64 y) -1)) (neg.f64 -1)) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (Rewrite=> associate-/l*_binary64 (/.f64 (neg.f64 y) (/.f64 (neg.f64 -1) -1))) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (/.f64 (neg.f64 y) (/.f64 (Rewrite=> metadata-eval 1) -1)) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (/.f64 (neg.f64 y) (Rewrite=> metadata-eval -1)) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (Rewrite<= associate-/r*_binary64 (/.f64 (neg.f64 y) (*.f64 -1 (-.f64 t a)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (neg.f64 y) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 t a)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (neg.f64 y) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 t a)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (neg.f64 y) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 t) a))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (neg.f64 y) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 t)) a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (neg.f64 y) (Rewrite<= +-commutative_binary64 (+.f64 a (neg.f64 t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (/.f64 (neg.f64 y) (Rewrite<= sub-neg_binary64 (-.f64 a t))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (-.f64 z t) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 y (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 z t) (neg.f64 (/.f64 y (-.f64 a t)))) y))): 17 points increase in error, 29 points decrease in error
(+.f64 x (+.f64 (*.f64 (-.f64 z t) (Rewrite=> distribute-neg-frac_binary64 (/.f64 (neg.f64 y) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (-.f64 z t) (neg.f64 y)) (-.f64 a t))) y)): 48 points increase in error, 13 points decrease in error
(+.f64 x (+.f64 (/.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (-.f64 z t) y))) (-.f64 a t)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= sub-neg_binary64 (-.f64 y (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))): 15 points increase in error, 8 points decrease in error