Initial program 62.7
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
Simplified62.7
\[\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 (Rewrite<= *-commutative_binary64 (*.f64 i a)) (*.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 i a) (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 (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 (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.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)) (neg.f64 (neg.f64 (*.f64 i a))))) (*.f64 j (-.f64 (*.f64 t c) (*.f64 y i))))): 21 points increase in error, 0 points decrease in error
(fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (fma.f64 b (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 c z) (neg.f64 (*.f64 i a))))) (*.f64 j (-.f64 (*.f64 t c) (*.f64 y i))))): 21 points increase in error, 0 points decrease in error
(fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (fma.f64 b (neg.f64 (Rewrite<= sub-neg_binary64 (-.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 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 c t)))) (*.f64 y i))))): 0 points increase in error, 21 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 (neg.f64 (neg.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))) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 j (neg.f64 (neg.f64 (*.f64 c t)))) (*.f64 j (*.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 (*.f64 j (Rewrite=> remove-double-neg_binary64 (*.f64 c t))) (*.f64 j (*.f64 i y))))): 21 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))) (Rewrite=> distribute-lft-out--_binary64 (*.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<= 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, 21 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))))))): 21 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)))))): 0 points increase in error, 21 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
Taylor expanded in i around -inf 26.0
\[\leadsto \color{blue}{-1 \cdot \left(c \cdot \left(b \cdot z\right)\right) + \left(-1 \cdot \left(i \cdot \left(y \cdot j + -1 \cdot \left(a \cdot b\right)\right)\right) + \left(\left(y \cdot z - a \cdot t\right) \cdot x + c \cdot \left(t \cdot j\right)\right)\right)}
\]
Simplified26.0
\[\leadsto \color{blue}{\left(c \cdot \left(t \cdot j - z \cdot b\right) - i \cdot \left(y \cdot j - a \cdot b\right)\right) + x \cdot \left(y \cdot z - t \cdot a\right)}
\]
Proof
(+.f64 (-.f64 (*.f64 c (-.f64 (*.f64 t j) (*.f64 z b))) (*.f64 i (-.f64 (*.f64 y j) (*.f64 a b)))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 c (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 t j) (neg.f64 (*.f64 z b))))) (*.f64 i (-.f64 (*.f64 y j) (*.f64 a b)))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 23 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 c (+.f64 (*.f64 t j) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 z b))))) (*.f64 i (-.f64 (*.f64 y j) (*.f64 a b)))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 23 points decrease in error
(+.f64 (-.f64 (*.f64 c (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 z b)) (*.f64 t j)))) (*.f64 i (-.f64 (*.f64 y j) (*.f64 a b)))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 c (+.f64 (*.f64 -1 (*.f64 z b)) (*.f64 t j))) (*.f64 i (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 y j) (neg.f64 (*.f64 a b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 23 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 c (+.f64 (*.f64 -1 (*.f64 z b)) (*.f64 t j))) (*.f64 i (+.f64 (*.f64 y j) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 a b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 23 points decrease in error
(+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 c (+.f64 (*.f64 -1 (*.f64 z b)) (*.f64 t j))) (neg.f64 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 23 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 c (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 t j) (*.f64 -1 (*.f64 z b))))) (neg.f64 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 (*.f64 t j) c) (*.f64 (*.f64 -1 (*.f64 z b)) c))) (neg.f64 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 c (*.f64 t j))) (*.f64 (*.f64 -1 (*.f64 z b)) c)) (neg.f64 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 23 points decrease in error
(+.f64 (+.f64 (+.f64 (*.f64 c (*.f64 t j)) (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (*.f64 z b) c)))) (neg.f64 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (+.f64 (*.f64 c (*.f64 t j)) (*.f64 -1 (Rewrite<= *-commutative_binary64 (*.f64 c (*.f64 z b))))) (neg.f64 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (+.f64 (*.f64 c (*.f64 t j)) (*.f64 -1 (*.f64 c (*.f64 z b)))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 23 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))) (+.f64 (*.f64 c (*.f64 t j)) (*.f64 -1 (*.f64 c (*.f64 z b)))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 23 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 z b))) (*.f64 c (*.f64 t j))))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 23 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))) (+.f64 (*.f64 -1 (*.f64 c (Rewrite<= *-commutative_binary64 (*.f64 b z)))) (*.f64 c (*.f64 t j)))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))) (*.f64 -1 (*.f64 c (*.f64 b z)))) (*.f64 c (*.f64 t j)))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 23 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))))) (*.f64 c (*.f64 t j))) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))): 0 points increase in error, 23 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (+.f64 (*.f64 c (*.f64 t j)) (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a)))))): 23 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (+.f64 (*.f64 c (*.f64 t j)) (*.f64 x (-.f64 (*.f64 y z) (Rewrite<= *-commutative_binary64 (*.f64 a t)))))): 0 points increase in error, 23 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (+.f64 (*.f64 c (*.f64 t j)) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 y z) (*.f64 a t)) x)))): 23 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b)))))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (-.f64 (*.f64 y z) (*.f64 a t)) x) (*.f64 c (*.f64 t j))))): 0 points increase in error, 23 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1 (*.f64 c (*.f64 b z))) (+.f64 (*.f64 -1 (*.f64 i (+.f64 (*.f64 y j) (*.f64 -1 (*.f64 a b))))) (+.f64 (*.f64 (-.f64 (*.f64 y z) (*.f64 a t)) x) (*.f64 c (*.f64 t j)))))): 23 points increase in error, 0 points decrease in error
Taylor expanded in y around inf 19.4
\[\leadsto \left(c \cdot \left(t \cdot j - z \cdot b\right) - i \cdot \left(y \cdot j - a \cdot b\right)\right) + \color{blue}{y \cdot \left(z \cdot x\right)}
\]
Initial program 0.9
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
Simplified0.9
\[\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 (Rewrite<= *-commutative_binary64 (*.f64 i a)) (*.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 i a) (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 (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 (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.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)) (neg.f64 (neg.f64 (*.f64 i a))))) (*.f64 j (-.f64 (*.f64 t c) (*.f64 y i))))): 21 points increase in error, 0 points decrease in error
(fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (fma.f64 b (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 c z) (neg.f64 (*.f64 i a))))) (*.f64 j (-.f64 (*.f64 t c) (*.f64 y i))))): 21 points increase in error, 0 points decrease in error
(fma.f64 x (-.f64 (*.f64 y z) (*.f64 t a)) (fma.f64 b (neg.f64 (Rewrite<= sub-neg_binary64 (-.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 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 c t)))) (*.f64 y i))))): 0 points increase in error, 21 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 (neg.f64 (neg.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))) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 j (neg.f64 (neg.f64 (*.f64 c t)))) (*.f64 j (*.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 (*.f64 j (Rewrite=> remove-double-neg_binary64 (*.f64 c t))) (*.f64 j (*.f64 i y))))): 21 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))) (Rewrite=> distribute-lft-out--_binary64 (*.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<= 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, 21 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))))))): 21 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)))))): 0 points increase in error, 21 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
Applied egg-rr0.9
\[\leadsto \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\mathsf{fma}\left(b, i \cdot a - c \cdot z, j \cdot \left(t \cdot c - y \cdot i\right)\right) + \mathsf{fma}\left(-i, y, y \cdot i\right) \cdot j}\right)
\]