Simplified62.3
\[\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, 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)))))): 1 points increase in error, 1 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
Simplified26.4
\[\leadsto \color{blue}{\mathsf{fma}\left(c, j \cdot a - b \cdot z, i \cdot \left(b \cdot t - j \cdot y\right)\right)}
\]
Proof
(fma.f64 c (-.f64 (*.f64 j a) (*.f64 b z)) (*.f64 i (-.f64 (*.f64 b t) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 a j)) (*.f64 b z)) (*.f64 i (-.f64 (*.f64 b t) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (-.f64 (*.f64 a j) (Rewrite=> *-commutative_binary64 (*.f64 z b))) (*.f64 i (-.f64 (*.f64 b t) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 a j) (neg.f64 (*.f64 z b)))) (*.f64 i (-.f64 (*.f64 b t) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 z b)))) (*.f64 i (-.f64 (*.f64 b t) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (*.f64 i (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 t b)) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (*.f64 i (-.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 t b)))) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (*.f64 i (-.f64 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 t b)))) (*.f64 j y)))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (*.f64 i (-.f64 (neg.f64 (*.f64 -1 (*.f64 t b))) (Rewrite<= *-commutative_binary64 (*.f64 y j))))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (*.f64 i (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 (*.f64 -1 (*.f64 t b))) (neg.f64 (*.f64 y j)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (*.f64 i (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 -1 (*.f64 t b)) (*.f64 y j)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (*.f64 i (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-neg_binary64 (-.f64 (*.f64 c (+.f64 (*.f64 a j) (*.f64 -1 (*.f64 z b)))) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b)))))): 2 points increase in error, 0 points decrease in error
(-.f64 (*.f64 c (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 z b)) (*.f64 a j)))) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 c (*.f64 -1 (*.f64 z b))) (*.f64 c (*.f64 a j)))) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))): 1 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 c (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 z b)))) (*.f64 c (*.f64 a j))) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 c (*.f64 z b)))) (*.f64 c (*.f64 a j))) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 c (*.f64 z b)))) (*.f64 c (*.f64 a j))) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1 (*.f64 c (Rewrite<= *-commutative_binary64 (*.f64 b z)))) (*.f64 c (*.f64 a j))) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate--l+_binary64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (-.f64 (*.f64 c (*.f64 a j)) (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 t b))))))): 0 points increase in error, 1 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (-.f64 (*.f64 c (*.f64 a j)) (*.f64 i (+.f64 (*.f64 y j) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 t b))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (-.f64 (*.f64 c (*.f64 a j)) (*.f64 i (Rewrite=> unsub-neg_binary64 (-.f64 (*.f64 y j) (*.f64 t b)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (-.f64 (*.f64 c (*.f64 a j)) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 i (*.f64 y j)) (*.f64 i (*.f64 t b)))))): 1 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (-.f64 (*.f64 c (*.f64 a j)) (-.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 i y) j)) (*.f64 i (*.f64 t b))))): 19 points increase in error, 12 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (-.f64 (*.f64 c (*.f64 a j)) (-.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 y i)) j) (*.f64 i (*.f64 t b))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (-.f64 (*.f64 c (*.f64 a j)) (-.f64 (Rewrite<= associate-*r*_binary64 (*.f64 y (*.f64 i j))) (*.f64 i (*.f64 t b))))): 13 points increase in error, 27 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (*.f64 c (*.f64 a j)) (*.f64 y (*.f64 i j))) (*.f64 i (*.f64 t b))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (+.f64 (-.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 c a) j)) (*.f64 y (*.f64 i j))) (*.f64 i (*.f64 t b)))): 20 points increase in error, 20 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (+.f64 (-.f64 (*.f64 (*.f64 c a) j) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 y i) j))) (*.f64 i (*.f64 t b)))): 26 points increase in error, 15 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (+.f64 (Rewrite=> distribute-rgt-out--_binary64 (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))) (*.f64 i (*.f64 t b)))): 2 points increase in error, 2 points decrease in error
(+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 i (*.f64 t b)) (*.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 -1 (*.f64 c (*.f64 b z))) (*.f64 i (*.f64 t b))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 i (*.f64 t b)) (*.f64 -1 (*.f64 c (*.f64 b z))))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 i (*.f64 t b)) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 c (*.f64 b z))))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> unsub-neg_binary64 (-.f64 (*.f64 i (*.f64 t b)) (*.f64 c (*.f64 b z)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 i (*.f64 t b)) (*.f64 c (Rewrite=> *-commutative_binary64 (*.f64 z b)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 i (*.f64 t b)) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 c z) b))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 15 points increase in error, 12 points decrease in error
(+.f64 (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 (*.f64 i (*.f64 t b)) (*.f64 (neg.f64 (*.f64 c z)) b))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 i t) b)) (*.f64 (neg.f64 (*.f64 c z)) b)) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 9 points increase in error, 17 points decrease in error
(+.f64 (+.f64 (*.f64 (*.f64 i t) b) (*.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 c z))) b)) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 b (+.f64 (*.f64 i t) (*.f64 -1 (*.f64 c z))))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 1 points increase in error, 1 points decrease in error
(+.f64 (*.f64 b (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 c z)) (*.f64 i t)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error