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