Simplified0.2
\[\leadsto \color{blue}{\mathsf{fma}\left(a, \frac{z - y}{t - \left(z + -1\right)}, x\right)}
\]
Proof
(fma.f64 a (/.f64 (-.f64 z y) (-.f64 t (+.f64 z -1))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (/.f64 (-.f64 z y) (-.f64 t (+.f64 z (Rewrite<= metadata-eval (neg.f64 1))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (/.f64 (-.f64 z y) (-.f64 t (Rewrite<= sub-neg_binary64 (-.f64 z 1)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (/.f64 (-.f64 z y) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 t z) 1))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (Rewrite=> div-sub_binary64 (-.f64 (/.f64 z (+.f64 (-.f64 t z) 1)) (/.f64 y (+.f64 (-.f64 t z) 1)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 z (+.f64 (-.f64 t z) 1)) (neg.f64 (/.f64 y (+.f64 (-.f64 t z) 1))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 z (+.f64 (-.f64 t z) 1))))) (neg.f64 (/.f64 y (+.f64 (-.f64 t z) 1)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 (/.f64 z (+.f64 (-.f64 t z) 1))) (/.f64 y (+.f64 (-.f64 t z) 1))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 y (+.f64 (-.f64 t z) 1)) (neg.f64 (/.f64 z (+.f64 (-.f64 t z) 1)))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 y (+.f64 (-.f64 t z) 1)) (/.f64 z (+.f64 (-.f64 t z) 1))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 a (neg.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 y z) (+.f64 (-.f64 t z) 1)))) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (neg.f64 (/.f64 (-.f64 y z) (+.f64 (-.f64 t z) 1)))) x)): 1 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a (/.f64 (-.f64 y z) (+.f64 (-.f64 t z) 1))))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 y z) (+.f64 (-.f64 t z) 1)) a))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 y z) (/.f64 (+.f64 (-.f64 t z) 1) a)))) x): 27 points increase in error, 5 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 x (neg.f64 (/.f64 (-.f64 y z) (/.f64 (+.f64 (-.f64 t z) 1) a))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_binary64 (-.f64 x (/.f64 (-.f64 y z) (/.f64 (+.f64 (-.f64 t z) 1) a)))): 0 points increase in error, 0 points decrease in error