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