Simplified2.3
\[\leadsto \color{blue}{\mathsf{fma}\left(t - z, \frac{y}{t - a}, x\right)}
\]
Proof
(fma.f64 (-.f64 t z) (/.f64 y (-.f64 t a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 y (-.f64 t a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (/.f64 y (-.f64 t a))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 y) (*.f64 -1 (-.f64 t a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (/.f64 (*.f64 -1 y) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 t a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (/.f64 (*.f64 -1 y) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 t a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (/.f64 (*.f64 -1 y) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 t) a))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (/.f64 (*.f64 -1 y) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 t)) a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (/.f64 (*.f64 -1 y) (Rewrite<= +-commutative_binary64 (+.f64 a (neg.f64 t)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (/.f64 (*.f64 -1 y) (Rewrite<= sub-neg_binary64 (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 t z) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 y (-.f64 a t)))) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 t z) (*.f64 -1 (/.f64 y (-.f64 a t)))) x)): 2 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 t z) -1) (/.f64 y (-.f64 a t)))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (-.f64 t z))) (/.f64 y (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 t z))) (/.f64 y (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 t z))) (/.f64 y (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 t) z)) (/.f64 y (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 t)) z) (/.f64 y (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 z (neg.f64 t))) (/.f64 y (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 z t)) (/.f64 y (-.f64 a t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))) x): 54 points increase in error, 20 points decrease in error
(+.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y (-.f64 z t))) (-.f64 a t)) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 x (/.f64 (*.f64 y (-.f64 z t)) (-.f64 a t)))): 0 points increase in error, 0 points decrease in error