Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(y + \left(t + -2\right), b, \mathsf{fma}\left(z, 1 - y, \mathsf{fma}\left(a, 1 - t, x\right)\right)\right)}
\]
Proof
(fma.f64 (+.f64 y (+.f64 t -2)) b (fma.f64 z (-.f64 1 y) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 y (+.f64 t (Rewrite<= metadata-eval (neg.f64 2)))) b (fma.f64 z (-.f64 1 y) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 y t) (neg.f64 2))) b (fma.f64 z (-.f64 1 y) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 y t) 2)) b (fma.f64 z (-.f64 1 y) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 y))) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 y) 1)) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 y)) 1) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 y 1))) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 y 1))) (fma.f64 a (-.f64 1 t) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (fma.f64 a (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 t))) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (fma.f64 a (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 t) 1)) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (fma.f64 a (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 t)) 1) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (fma.f64 a (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 t 1))) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (fma.f64 a (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 t 1))) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (neg.f64 (-.f64 t 1))) x)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (-.f64 t 1)) a)) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (fma.f64 z (neg.f64 (-.f64 y 1)) (Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 (neg.f64 (-.f64 t 1)) a))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z (neg.f64 (-.f64 y 1))) (+.f64 x (*.f64 (neg.f64 (-.f64 t 1)) a))))): 2 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (-.f64 y 1)) z)) (+.f64 x (*.f64 (neg.f64 (-.f64 t 1)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 (neg.f64 (-.f64 y 1)) z) x) (*.f64 (neg.f64 (-.f64 t 1)) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 (neg.f64 (-.f64 y 1)) z))) (*.f64 (neg.f64 (-.f64 t 1)) a))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (+.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 x (*.f64 (-.f64 y 1) z))) (*.f64 (neg.f64 (-.f64 t 1)) a))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 (+.f64 y t) 2) b (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (-.f64 x (*.f64 (-.f64 y 1) z)) (*.f64 (-.f64 t 1) a)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 (+.f64 y t) 2) b) (-.f64 (-.f64 x (*.f64 (-.f64 y 1) z)) (*.f64 (-.f64 t 1) a)))): 1 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (-.f64 (-.f64 x (*.f64 (-.f64 y 1) z)) (*.f64 (-.f64 t 1) a)) (*.f64 (-.f64 (+.f64 y t) 2) b))): 0 points increase in error, 0 points decrease in error