Simplified25.3
\[\leadsto \color{blue}{\mathsf{fma}\left(j, k \cdot -27, \mathsf{fma}\left(t, \mathsf{fma}\left(x, y \cdot \left(18 \cdot z\right), a \cdot -4\right), \mathsf{fma}\left(b, c, i \cdot \left(x \cdot -4\right)\right)\right)\right)}
\]
Proof
(fma.f64 j (*.f64 k -27) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (*.f64 k (Rewrite<= metadata-eval (neg.f64 27))) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 k 27))) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 27 k))) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y 18) z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 1 points increase in error, 2 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 18 y)) z) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (*.f64 (*.f64 18 y) z) (*.f64 a (Rewrite<= metadata-eval (neg.f64 4)))) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (*.f64 (*.f64 18 y) z) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4)))) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x (*.f64 (*.f64 18 y) z)) (*.f64 a 4))) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x (*.f64 18 y)) z)) (*.f64 a 4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 7 points increase in error, 9 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 18) y)) z) (*.f64 a 4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 1 points increase in error, 2 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (*.f64 i (*.f64 x (Rewrite<= metadata-eval (neg.f64 4))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (*.f64 i (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 x 4))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 x 4)) i))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (*.f64 x 4) i)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b c) (*.f64 (*.f64 x 4) i))))): 0 points increase in error, 1 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4))) (-.f64 (*.f64 b c) (*.f64 (*.f64 x 4) i))))): 1 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (+.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t))) (-.f64 (*.f64 b c) (*.f64 (*.f64 x 4) i)))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 j (neg.f64 (*.f64 27 k))) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 j (*.f64 27 k)))) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 j 27) k))) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i))): 12 points increase in error, 10 points decrease in error
(+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (*.f64 j 27)) k)) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)) (*.f64 (neg.f64 (*.f64 j 27)) k))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)) (*.f64 (*.f64 j 27) k))): 0 points increase in error, 0 points decrease in error
Simplified16.0
\[\leadsto \color{blue}{\mathsf{fma}\left(c, b, \mathsf{fma}\left(x, \mathsf{fma}\left(y, z \cdot \left(18 \cdot t\right), -4 \cdot i\right), k \cdot \left(-27 \cdot j\right)\right)\right)}
\]
Proof
(fma.f64 c b (fma.f64 x (fma.f64 y (*.f64 z (*.f64 18 t)) (*.f64 -4 i)) (*.f64 k (*.f64 -27 j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c b (fma.f64 x (fma.f64 y (*.f64 z (Rewrite<= *-commutative_binary64 (*.f64 t 18))) (*.f64 -4 i)) (*.f64 k (*.f64 -27 j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c b (fma.f64 x (fma.f64 y (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z t) 18)) (*.f64 -4 i)) (*.f64 k (*.f64 -27 j)))): 3 points increase in error, 4 points decrease in error
(fma.f64 c b (fma.f64 x (fma.f64 y (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 t z)) 18) (*.f64 -4 i)) (*.f64 k (*.f64 -27 j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c b (fma.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (*.f64 (*.f64 t z) 18)) (*.f64 -4 i))) (*.f64 k (*.f64 -27 j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c b (fma.f64 x (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y (*.f64 t z)) 18)) (*.f64 -4 i)) (*.f64 k (*.f64 -27 j)))): 3 points increase in error, 4 points decrease in error
(fma.f64 c b (fma.f64 x (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 18 (*.f64 y (*.f64 t z)))) (*.f64 -4 i)) (*.f64 k (*.f64 -27 j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c b (fma.f64 x (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 k -27) j)))): 14 points increase in error, 13 points decrease in error
(fma.f64 c b (fma.f64 x (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i)) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -27 k)) j))): 0 points increase in error, 0 points decrease in error
(fma.f64 c b (fma.f64 x (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i)) (Rewrite<= associate-*r*_binary64 (*.f64 -27 (*.f64 k j))))): 18 points increase in error, 9 points decrease in error
(fma.f64 c b (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i))) (*.f64 -27 (*.f64 k j))))): 1 points increase in error, 1 points decrease in error
(fma.f64 c b (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i)) x)) (*.f64 -27 (*.f64 k j)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> fma-udef_binary64 (+.f64 (*.f64 c b) (+.f64 (*.f64 (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i)) x) (*.f64 -27 (*.f64 k j))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c b) (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 x (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i)))) (*.f64 -27 (*.f64 k j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c b) (+.f64 (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 (*.f64 18 (*.f64 y (*.f64 t z))) x) (*.f64 (*.f64 -4 i) x))) (*.f64 -27 (*.f64 k j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c b) (+.f64 (+.f64 (Rewrite=> associate-*l*_binary64 (*.f64 18 (*.f64 (*.f64 y (*.f64 t z)) x))) (*.f64 (*.f64 -4 i) x)) (*.f64 -27 (*.f64 k j)))): 6 points increase in error, 5 points decrease in error
(+.f64 (*.f64 c b) (+.f64 (+.f64 (*.f64 18 (Rewrite<= associate-*r*_binary64 (*.f64 y (*.f64 (*.f64 t z) x)))) (*.f64 (*.f64 -4 i) x)) (*.f64 -27 (*.f64 k j)))): 9 points increase in error, 11 points decrease in error
(+.f64 (*.f64 c b) (+.f64 (+.f64 (*.f64 18 (*.f64 y (Rewrite<= associate-*r*_binary64 (*.f64 t (*.f64 z x))))) (*.f64 (*.f64 -4 i) x)) (*.f64 -27 (*.f64 k j)))): 18 points increase in error, 12 points decrease in error
(+.f64 (*.f64 c b) (+.f64 (+.f64 (*.f64 18 (*.f64 y (*.f64 t (*.f64 z x)))) (Rewrite<= associate-*r*_binary64 (*.f64 -4 (*.f64 i x)))) (*.f64 -27 (*.f64 k j)))): 0 points increase in error, 1 points decrease in error
(+.f64 (*.f64 c b) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 18 (*.f64 y (*.f64 t (*.f64 z x)))) (+.f64 (*.f64 -4 (*.f64 i x)) (*.f64 -27 (*.f64 k j)))))): 0 points increase in error, 0 points decrease in error