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