Simplified5.3
\[\leadsto \color{blue}{x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)}
\]
Proof
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 t a)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (-.f64 t a))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 -1 (-.f64 t a))))) y)): 9 points increase in error, 1 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (-.f64 t a)) -1))) y)): 1 points increase in error, 9 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 t) a)) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 t)) a) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 a (neg.f64 t))) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y))): 3 points increase in error, 1 points decrease in error
(+.f64 x (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (/.f64 (-.f64 z t) (-.f64 a t))))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) y))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))) y)): 57 points increase in error, 7 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)))): 14 points increase in error, 1 points decrease in error