Simplified64.0
\[\leadsto \color{blue}{\mathsf{fma}\left(b, \mathsf{fma}\left(z, -c, a \cdot i\right), \mathsf{fma}\left(x, \mathsf{fma}\left(y, z, a \cdot \left(-t\right)\right), j \cdot \mathsf{fma}\left(i, -y, t \cdot c\right)\right)\right)}
\]
Proof
(fma.f64 b (fma.f64 z (neg.f64 c) (*.f64 a i)) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (fma.f64 z (neg.f64 c) (Rewrite<= *-commutative_binary64 (*.f64 i a))) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 z (neg.f64 c)) (*.f64 i a))) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 z c))) (*.f64 i a)) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 c z))) (*.f64 i a)) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 c z))) (*.f64 i a)) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (*.f64 c z) (*.f64 i a)))) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a)))) (fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (fma.f64 y z (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a t)))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (fma.f64 y z (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 t a)))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 j (fma.f64 i (neg.f64 y) (*.f64 t c))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (*.f64 j (fma.f64 i (neg.f64 y) (Rewrite<= *-commutative_binary64 (*.f64 c t)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (*.f64 j (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i (neg.f64 y)) (*.f64 c t)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (*.f64 j (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 i y))) (*.f64 c t))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (*.f64 j (+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 i) y)) (*.f64 c t))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (*.f64 j (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 c t) (*.f64 (neg.f64 i) y)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (*.f64 j (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 c t) (*.f64 i y)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 b (neg.f64 (-.f64 (*.f64 c z) (*.f64 i a)))) (+.f64 (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))))): 1 points increase in error, 1 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a))))) (+.f64 (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 b) (-.f64 (*.f64 c z) (*.f64 i a)))) (+.f64 (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (neg.f64 b) (-.f64 (*.f64 c z) (*.f64 i a))) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 (neg.f64 b) (-.f64 (*.f64 c z) (*.f64 i a))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 (neg.f64 b) (-.f64 (*.f64 c z) (*.f64 i a))))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a))))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))): 0 points increase in error, 0 points decrease in error