Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(t, \frac{z}{16}, \mathsf{fma}\left(x, y, c - b \cdot \frac{a}{4}\right)\right)}
\]
Proof
(fma.f64 t (/.f64 z 16) (fma.f64 x y (-.f64 c (*.f64 b (/.f64 a 4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (fma.f64 x y (-.f64 c (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 a 4) b))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (fma.f64 x y (-.f64 c (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 a b) 4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (fma.f64 x y (Rewrite<= unsub-neg_binary64 (+.f64 c (neg.f64 (/.f64 (*.f64 a b) 4)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (fma.f64 x y (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 (*.f64 a b) 4)) c)))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (fma.f64 x y (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 (*.f64 a b) 4))) c))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (fma.f64 x y (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 (/.f64 (*.f64 a b) 4) c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (fma.f64 x y (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (/.f64 (*.f64 a b) 4) c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (/.f64 z 16) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x y) (-.f64 (/.f64 (*.f64 a b) 4) c)))): 2 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (/.f64 z 16)) (-.f64 (*.f64 x y) (-.f64 (/.f64 (*.f64 a b) 4) c)))): 1 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 z 16) t)) (-.f64 (*.f64 x y) (-.f64 (/.f64 (*.f64 a b) 4) c))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 z t) 16)) (-.f64 (*.f64 x y) (-.f64 (/.f64 (*.f64 a b) 4) c))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (*.f64 z t) 16) (*.f64 x y)) (-.f64 (/.f64 (*.f64 a b) 4) c))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x y) (/.f64 (*.f64 z t) 16))) (-.f64 (/.f64 (*.f64 a b) 4) c)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (+.f64 (*.f64 x y) (/.f64 (*.f64 z t) 16)) (/.f64 (*.f64 a b) 4)) c)): 0 points increase in error, 0 points decrease in error