Simplified59.4
\[\leadsto \color{blue}{\mathsf{fma}\left(j, a \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right)}
\]
Proof
(fma.f64 j (-.f64 (*.f64 a c) (*.f64 y i)) (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 z c) (*.f64 t i))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c a)) (*.f64 y i)) (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 z c) (*.f64 t i))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (-.f64 (*.f64 c a) (*.f64 y i)) (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c z)) (*.f64 t i))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i))) (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))))): 1 points increase in error, 1 points decrease in error
(Rewrite<= +-commutative_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
Simplified36.1
\[\leadsto \color{blue}{\mathsf{fma}\left(y, x \cdot z - j \cdot i, \left(t \cdot x\right) \cdot \left(-a\right)\right)}
\]
Proof
(fma.f64 y (-.f64 (*.f64 x z) (*.f64 j i)) (*.f64 (*.f64 t x) (neg.f64 a))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 z x)) (*.f64 j i)) (*.f64 (*.f64 t x) (neg.f64 a))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (-.f64 (*.f64 z x) (Rewrite<= *-commutative_binary64 (*.f64 i j))) (*.f64 (*.f64 t x) (neg.f64 a))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 z x) (neg.f64 (*.f64 i j)))) (*.f64 (*.f64 t x) (neg.f64 a))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (*.f64 z x) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 i j)))) (*.f64 (*.f64 t x) (neg.f64 a))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (*.f64 z x) (*.f64 -1 (*.f64 i j))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 t x) a)))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (*.f64 z x) (*.f64 -1 (*.f64 i j))) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 a (*.f64 t x))))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (*.f64 z x) (*.f64 -1 (*.f64 i j))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 a (*.f64 t x))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (+.f64 (*.f64 z x) (*.f64 -1 (*.f64 i j)))) (*.f64 -1 (*.f64 a (*.f64 t x))))): 2 points increase in error, 1 points decrease in error
(+.f64 (*.f64 y (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 i j)) (*.f64 z x)))) (*.f64 -1 (*.f64 a (*.f64 t x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 (*.f64 -1 (*.f64 i j)) y) (*.f64 (*.f64 z x) y))) (*.f64 -1 (*.f64 a (*.f64 t x)))): 2 points increase in error, 2 points decrease in error
(+.f64 (+.f64 (*.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 -1 i) j)) y) (*.f64 (*.f64 z x) y)) (*.f64 -1 (*.f64 a (*.f64 t x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 -1 i) (*.f64 j y))) (*.f64 (*.f64 z x) y)) (*.f64 -1 (*.f64 a (*.f64 t x)))): 19 points increase in error, 22 points decrease in error
(+.f64 (+.f64 (*.f64 (*.f64 -1 i) (Rewrite<= *-commutative_binary64 (*.f64 y j))) (*.f64 (*.f64 z x) y)) (*.f64 -1 (*.f64 a (*.f64 t x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 i (*.f64 y j)))) (*.f64 (*.f64 z x) y)) (*.f64 -1 (*.f64 a (*.f64 t x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (Rewrite<= *-commutative_binary64 (*.f64 y (*.f64 z x)))) (*.f64 -1 (*.f64 a (*.f64 t x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (+.f64 (*.f64 y (*.f64 z x)) (*.f64 -1 (*.f64 a (*.f64 t x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 a (*.f64 t x))) (*.f64 y (*.f64 z x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 y (*.f64 z x)) (*.f64 -1 (*.f64 a (*.f64 t x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (+.f64 (*.f64 y (*.f64 z x)) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 a (*.f64 t x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (Rewrite=> unsub-neg_binary64 (-.f64 (*.f64 y (*.f64 z x)) (*.f64 a (*.f64 t x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (-.f64 (*.f64 y (*.f64 z x)) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 a t) x)))): 30 points increase in error, 18 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y z) x)) (*.f64 (*.f64 a t) x))): 11 points increase in error, 24 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (Rewrite=> distribute-rgt-out--_binary64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 a t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 i (*.f64 y j))) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 y z) (*.f64 a t)) x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (-.f64 (*.f64 y z) (*.f64 a t)) x) (*.f64 -1 (*.f64 i (*.f64 y j))))): 0 points increase in error, 0 points decrease in error