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