Simplified0.6
\[\leadsto \color{blue}{\mathsf{fma}\left(a, 27 \cdot b, x \cdot 2 - y \cdot \left(9 \cdot \left(z \cdot t\right)\right)\right)}
\]
Proof
(fma.f64 a (*.f64 27 b) (-.f64 (*.f64 x 2) (*.f64 y (*.f64 9 (*.f64 z t))))): 0 points increase in error, 0 points decrease in error
(fma.f64 a (*.f64 27 b) (-.f64 (*.f64 x 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y 9) (*.f64 z t))))): 0 points increase in error, 0 points decrease in error
(fma.f64 a (*.f64 27 b) (-.f64 (*.f64 x 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 y 9) z) t)))): 2 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (*.f64 27 b)) (-.f64 (*.f64 x 2) (*.f64 (*.f64 (*.f64 y 9) z) t)))): 2 points increase in error, 2 points decrease in error
(+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a 27) b)) (-.f64 (*.f64 x 2) (*.f64 (*.f64 (*.f64 y 9) z) t))): 0 points increase in error, 3 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (-.f64 (*.f64 x 2) (*.f64 (*.f64 (*.f64 y 9) z) t)) (*.f64 (*.f64 a 27) b))): 5 points increase in error, 1 points decrease in error
Simplified0.5
\[\leadsto \color{blue}{\mathsf{fma}\left(y, z \cdot \left(t \cdot -9\right), \mathsf{fma}\left(2, x, 27 \cdot \left(a \cdot b\right)\right)\right)}
\]
Proof
(fma.f64 y (*.f64 z (*.f64 t -9)) (fma.f64 2 x (*.f64 27 (*.f64 a b)))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z t) -9)) (fma.f64 2 x (*.f64 27 (*.f64 a b)))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (*.f64 (*.f64 z t) -9) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 x) (*.f64 27 (*.f64 a b))))): 20 points increase in error, 0 points decrease in error
(fma.f64 y (*.f64 (*.f64 z t) -9) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 x 2)) (*.f64 27 (*.f64 a b)))): 0 points increase in error, 20 points decrease in error
(fma.f64 y (*.f64 (*.f64 z t) -9) (+.f64 (*.f64 x 2) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 a b) 27)))): 0 points increase in error, 5 points decrease in error
(fma.f64 y (*.f64 (*.f64 z t) -9) (+.f64 (*.f64 x 2) (Rewrite<= associate-*r*_binary64 (*.f64 a (*.f64 b 27))))): 19 points increase in error, 0 points decrease in error
(fma.f64 y (*.f64 (*.f64 z t) -9) (+.f64 (*.f64 x 2) (*.f64 a (Rewrite<= *-commutative_binary64 (*.f64 27 b))))): 0 points increase in error, 14 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (*.f64 (*.f64 z t) -9)) (+.f64 (*.f64 x 2) (*.f64 a (*.f64 27 b))))): 5 points increase in error, 5 points decrease in error
(Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 y (*.f64 (*.f64 z t) -9)) (*.f64 x 2)) (*.f64 a (*.f64 27 b)))): 10 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 y (*.f64 (*.f64 z t) -9)) (*.f64 x 2)) (*.f64 a (Rewrite=> *-commutative_binary64 (*.f64 b 27)))): 0 points increase in error, 15 points decrease in error
(+.f64 (+.f64 (*.f64 y (*.f64 (*.f64 z t) -9)) (*.f64 x 2)) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 a b) 27))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 y (*.f64 (*.f64 z t) -9)) (*.f64 x 2)) (Rewrite<= *-commutative_binary64 (*.f64 27 (*.f64 a b)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-+l+_binary64 (+.f64 (*.f64 y (*.f64 (*.f64 z t) -9)) (+.f64 (*.f64 x 2) (*.f64 27 (*.f64 a b))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 y (*.f64 (*.f64 z t) -9)) (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 2 x)) (*.f64 27 (*.f64 a b)))): 15 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 2 x) (*.f64 27 (*.f64 a b))) (*.f64 y (*.f64 (*.f64 z t) -9)))): 0 points increase in error, 15 points decrease in error
(+.f64 (+.f64 (*.f64 2 x) (*.f64 27 (*.f64 a b))) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 y (*.f64 z t)) -9))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 2 x) (*.f64 27 (*.f64 a b))) (*.f64 (*.f64 y (Rewrite=> *-commutative_binary64 (*.f64 t z))) -9)): 5 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 2 x) (*.f64 27 (*.f64 a b))) (Rewrite<= *-commutative_binary64 (*.f64 -9 (*.f64 y (*.f64 t z))))): 0 points increase in error, 5 points decrease in error
(+.f64 (+.f64 (*.f64 2 x) (*.f64 27 (*.f64 a b))) (*.f64 (Rewrite<= metadata-eval (neg.f64 9)) (*.f64 y (*.f64 t z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (+.f64 (*.f64 2 x) (*.f64 27 (*.f64 a b))) (*.f64 9 (*.f64 y (*.f64 t z))))): 0 points increase in error, 0 points decrease in error