Simplified40.2
\[\leadsto \color{blue}{\mathsf{fma}\left(t, \mathsf{fma}\left(x \cdot 18, y \cdot z, a \cdot -4\right), \mathsf{fma}\left(b, c, i \cdot \left(x \cdot -4\right)\right)\right) + k \cdot \left(j \cdot -27\right)}
\]
Proof
(+.f64 (fma.f64 t (fma.f64 (*.f64 x 18) (*.f64 y z) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 t (fma.f64 (*.f64 x 18) (*.f64 y z) (*.f64 a (Rewrite<= metadata-eval (neg.f64 4)))) (fma.f64 b c (*.f64 i (*.f64 x -4)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 t (fma.f64 (*.f64 x 18) (*.f64 y z) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4)))) (fma.f64 b c (*.f64 i (*.f64 x -4)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 t (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (*.f64 x 18) (*.f64 y z)) (*.f64 a 4))) (fma.f64 b c (*.f64 i (*.f64 x -4)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 t (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 x 18) y) z)) (*.f64 a 4)) (fma.f64 b c (*.f64 i (*.f64 x -4)))) (*.f64 k (*.f64 j -27))): 14 points increase in error, 23 points decrease in error
(+.f64 (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)))))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (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)))))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (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)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (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))))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (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)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (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)))) (*.f64 k (*.f64 j -27))): 2 points increase in error, 0 points decrease in error
(+.f64 (+.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))) (*.f64 k (*.f64 j -27))): 3 points increase in error, 1 points decrease in error
(+.f64 (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))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.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 k (*.f64 j (Rewrite<= metadata-eval (neg.f64 27))))): 0 points increase in error, 0 points decrease in error
(+.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 k (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 j 27))))): 0 points increase in error, 0 points decrease in error
(+.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)) (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 j 27)) k))): 0 points increase in error, 0 points decrease in error
(+.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)) (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (*.f64 j 27) k)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_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