Simplified43.7
\[\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))))): 4 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, 20 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))))): 7 points increase in error, 4 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))))): 2 points increase in error, 0 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))))): 2 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)))): 1 points increase in error, 1 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))): 10 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
Simplified7.2
\[\leadsto \mathsf{fma}\left(j, k \cdot -27, \color{blue}{\mathsf{fma}\left(x, \mathsf{fma}\left(-4, i, z \cdot \left(y \cdot \left(18 \cdot t\right)\right)\right), c \cdot b\right)}\right)
\]
Proof
(fma.f64 x (fma.f64 -4 i (*.f64 z (*.f64 y (*.f64 18 t)))) (*.f64 c b)): 0 points increase in error, 0 points decrease in error
(fma.f64 x (fma.f64 -4 i (*.f64 z (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y 18) t)))) (*.f64 c b)): 4 points increase in error, 9 points decrease in error
(fma.f64 x (fma.f64 -4 i (*.f64 z (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 18 y)) t))) (*.f64 c b)): 0 points increase in error, 0 points decrease in error
(fma.f64 x (fma.f64 -4 i (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (*.f64 18 y) t) z))) (*.f64 c b)): 0 points increase in error, 0 points decrease in error
(fma.f64 x (fma.f64 -4 i (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 18 y) (*.f64 t z)))) (*.f64 c b)): 24 points increase in error, 13 points decrease in error
(fma.f64 x (fma.f64 -4 i (Rewrite<= associate-*r*_binary64 (*.f64 18 (*.f64 y (*.f64 t z))))) (*.f64 c b)): 9 points increase in error, 9 points decrease in error
(fma.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -4 i) (*.f64 18 (*.f64 y (*.f64 t z))))) (*.f64 c b)): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i))) (*.f64 c b)): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (+.f64 (*.f64 18 (*.f64 y (*.f64 t z))) (*.f64 -4 i))) (*.f64 c b))): 3 points increase in error, 1 points decrease in error
(+.f64 (*.f64 x (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -4 i) (*.f64 18 (*.f64 y (*.f64 t z)))))) (*.f64 c b)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 (*.f64 -4 i) x) (*.f64 (*.f64 18 (*.f64 y (*.f64 t z))) x))) (*.f64 c b)): 1 points increase in error, 1 points decrease in error
(+.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -4 (*.f64 i x))) (*.f64 (*.f64 18 (*.f64 y (*.f64 t z))) x)) (*.f64 c b)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -4 (*.f64 i x)) (Rewrite=> associate-*l*_binary64 (*.f64 18 (*.f64 (*.f64 y (*.f64 t z)) x)))) (*.f64 c b)): 11 points increase in error, 12 points decrease in error
(+.f64 (+.f64 (*.f64 -4 (*.f64 i x)) (*.f64 18 (Rewrite<= associate-*r*_binary64 (*.f64 y (*.f64 (*.f64 t z) x))))) (*.f64 c b)): 19 points increase in error, 18 points decrease in error
(+.f64 (+.f64 (*.f64 -4 (*.f64 i x)) (*.f64 18 (*.f64 y (Rewrite<= associate-*r*_binary64 (*.f64 t (*.f64 z x)))))) (*.f64 c b)): 16 points increase in error, 15 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 c b) (+.f64 (*.f64 -4 (*.f64 i x)) (*.f64 18 (*.f64 y (*.f64 t (*.f64 z x))))))): 0 points increase in error, 0 points decrease in error