Simplified64.0
\[\leadsto \color{blue}{\mathsf{fma}\left(x, \mathsf{fma}\left(y, z, a \cdot \left(-t\right)\right), \mathsf{fma}\left(b, \mathsf{fma}\left(z, -c, t \cdot i\right), j \cdot \left(a \cdot c - y \cdot i\right)\right)\right)}
\]
Proof
(fma.f64 x (fma.f64 y z (*.f64 a (neg.f64 t))) (fma.f64 b (fma.f64 z (neg.f64 c) (*.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 (fma.f64 y z (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a t)))) (fma.f64 b (fma.f64 z (neg.f64 c) (*.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 (fma.f64 y z (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 t a)))) (fma.f64 b (fma.f64 z (neg.f64 c) (*.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 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 y z) (*.f64 t a))) (fma.f64 b (fma.f64 z (neg.f64 c) (*.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=> fma-udef_binary64 (+.f64 (*.f64 z (neg.f64 c)) (*.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<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 z c))) (*.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 (neg.f64 (Rewrite<= *-commutative_binary64 (*.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)))))): 0 points increase in error, 1 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)))))): 2 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
Simplified22.0
\[\leadsto \color{blue}{c \cdot \left(a \cdot j - b \cdot z\right) + y \cdot \left(z \cdot x - i \cdot j\right)}
\]
Proof
(+.f64 (*.f64 c (-.f64 (*.f64 a j) (*.f64 b z))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c (-.f64 (*.f64 a j) (Rewrite<= *-commutative_binary64 (*.f64 z b)))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 a j) (neg.f64 (*.f64 z b))))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 a j)))) (neg.f64 (*.f64 z b)))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c (+.f64 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 a j)))) (neg.f64 (*.f64 z b)))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 -1 (*.f64 a j)) (*.f64 z b))))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 c (neg.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j)))))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j)))))) (*.f64 y (-.f64 (*.f64 z x) (*.f64 i j)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (*.f64 y (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 z x) (neg.f64 (*.f64 i j)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (*.f64 y (+.f64 (*.f64 z x) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 i j)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (*.f64 y (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 i j)) (*.f64 z x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (*.f64 y (+.f64 (*.f64 -1 (*.f64 i j)) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 z x))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (*.f64 y (+.f64 (*.f64 -1 (*.f64 i j)) (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 z x))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (*.f64 y (+.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 i j))) (neg.f64 (*.f64 -1 (*.f64 z x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (*.f64 y (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j))))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 c (+.f64 (*.f64 z b) (*.f64 -1 (*.f64 a j)))) (*.f64 y (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x))))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (+.f64 (*.f64 c (+.f64 (*.f64 z b) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 a j))))) (*.f64 y (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x)))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (+.f64 (*.f64 c (Rewrite=> unsub-neg_binary64 (-.f64 (*.f64 z b) (*.f64 a j)))) (*.f64 y (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x)))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (+.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 c (*.f64 z b)) (*.f64 c (*.f64 a j)))) (*.f64 y (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x)))))): 1 points increase in error, 0 points decrease in error
(neg.f64 (+.f64 (-.f64 (*.f64 c (Rewrite=> *-commutative_binary64 (*.f64 b z))) (*.f64 c (*.f64 a j))) (*.f64 y (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x)))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (Rewrite<= associate--r-_binary64 (-.f64 (*.f64 c (*.f64 b z)) (-.f64 (*.f64 c (*.f64 a j)) (*.f64 y (+.f64 (*.f64 i j) (*.f64 -1 (*.f64 z x)))))))): 1 points increase in error, 0 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (-.f64 (*.f64 c (*.f64 a j)) (*.f64 y (+.f64 (*.f64 i j) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 z x)))))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (-.f64 (*.f64 c (*.f64 a j)) (*.f64 y (Rewrite=> unsub-neg_binary64 (-.f64 (*.f64 i j) (*.f64 z x))))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (-.f64 (*.f64 c (*.f64 a j)) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 y (*.f64 i j)) (*.f64 y (*.f64 z x))))))): 0 points increase in error, 1 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (*.f64 c (*.f64 a j)) (*.f64 y (*.f64 i j))) (*.f64 y (*.f64 z x)))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (+.f64 (-.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 c a) j)) (*.f64 y (*.f64 i j))) (*.f64 y (*.f64 z x))))): 16 points increase in error, 18 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (+.f64 (-.f64 (*.f64 (*.f64 c a) j) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 y i) j))) (*.f64 y (*.f64 z x))))): 16 points increase in error, 12 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (+.f64 (Rewrite=> distribute-rgt-out--_binary64 (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))) (*.f64 y (*.f64 z x))))): 1 points increase in error, 1 points decrease in error
(neg.f64 (-.f64 (*.f64 c (*.f64 b z)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y (*.f64 z x)) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (*.f64 c (*.f64 b z)) (+.f64 (*.f64 y (*.f64 z x)) (*.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 0 (*.f64 c (*.f64 b z))) (+.f64 (*.f64 y (*.f64 z x)) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (*.f64 c (*.f64 b z)))) (+.f64 (*.f64 y (*.f64 z x)) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 c (*.f64 b z)))) (+.f64 (*.f64 y (*.f64 z x)) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i))))): 0 points increase in error, 0 points decrease in error