Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(z, \frac{t}{16}, \mathsf{fma}\left(b, -0.25 \cdot a, \mathsf{fma}\left(x, y, c\right)\right)\right)}
\]
Proof
(fma.f64 z (/.f64 t 16) (fma.f64 b (*.f64 -1/4 a) (fma.f64 x y c))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (fma.f64 b (*.f64 (Rewrite<= metadata-eval (/.f64 -1 4)) a) (fma.f64 x y c))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (fma.f64 b (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 a))) (fma.f64 x y c))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (fma.f64 b (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 a) 4)) (fma.f64 x y c))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (fma.f64 b (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 a 4))) (fma.f64 x y c))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (fma.f64 b (*.f64 -1 (/.f64 a 4)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x y) c)))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (fma.f64 b (*.f64 -1 (/.f64 a 4)) (Rewrite<= +-commutative_binary64 (+.f64 c (*.f64 x y))))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 b (*.f64 -1 (/.f64 a 4))) (+.f64 c (*.f64 x y))))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 -1 (/.f64 a 4)) b)) (+.f64 c (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (/.f64 a 4) b))) (+.f64 c (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (+.f64 (*.f64 -1 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 a b) 4))) (+.f64 c (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (+.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (*.f64 a b) 4))) (+.f64 c (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 c (*.f64 x y)) (neg.f64 (/.f64 (*.f64 a b) 4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 c (*.f64 x y)) (/.f64 (*.f64 a b) 4)))): 0 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (Rewrite<= associate-+r-_binary64 (+.f64 c (-.f64 (*.f64 x y) (/.f64 (*.f64 a b) 4))))): 1 points increase in error, 0 points decrease in error
(fma.f64 z (/.f64 t 16) (Rewrite<= +-commutative_binary64 (+.f64 (-.f64 (*.f64 x y) (/.f64 (*.f64 a b) 4)) c))): 0 points increase in error, 1 points decrease in error
(fma.f64 z (/.f64 t 16) (Rewrite<= associate--r-_binary64 (-.f64 (*.f64 x y) (-.f64 (/.f64 (*.f64 a b) 4) c)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 z (/.f64 t 16)) (-.f64 (*.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 t 16) z)) (-.f64 (*.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 z (/.f64 t 16))) (-.f64 (*.f64 x y) (-.f64 (/.f64 (*.f64 a b) 4) c))): 1 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 z t) 16)) (-.f64 (*.f64 x y) (-.f64 (/.f64 (*.f64 a b) 4) c))): 0 points increase in error, 1 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