Initial program 64.0
\[\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)
\]
Simplified64.0
\[\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, 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 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, 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 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in z around 0 39.9
\[\leadsto \color{blue}{\left(c \cdot t - y \cdot i\right) \cdot j + \left(-1 \cdot \left(a \cdot \left(t \cdot x\right)\right) + a \cdot \left(i \cdot b\right)\right)}
\]
Taylor expanded in t around 0 27.1
\[\leadsto \color{blue}{\left(c \cdot j + -1 \cdot \left(a \cdot x\right)\right) \cdot t + \left(-1 \cdot \left(y \cdot \left(i \cdot j\right)\right) + a \cdot \left(i \cdot b\right)\right)}
\]
Initial program 58.5
\[\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)
\]
Simplified58.5
\[\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, 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 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, 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 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in z around 0 41.8
\[\leadsto \color{blue}{\left(c \cdot t - y \cdot i\right) \cdot j + \left(-1 \cdot \left(a \cdot \left(t \cdot x\right)\right) + a \cdot \left(i \cdot b\right)\right)}
\]
Taylor expanded in c around 0 31.6
\[\leadsto \color{blue}{c \cdot \left(t \cdot j\right) + \left(-1 \cdot \left(a \cdot \left(t \cdot x\right)\right) + \left(-1 \cdot \left(y \cdot \left(i \cdot j\right)\right) + a \cdot \left(i \cdot b\right)\right)\right)}
\]
Simplified28.7
\[\leadsto \color{blue}{\mathsf{fma}\left(t, \mathsf{fma}\left(j, c, a \cdot \left(-x\right)\right), i \cdot \left(a \cdot b - y \cdot j\right)\right)}
\]
Proof
(fma.f64 t (fma.f64 j c (*.f64 a (neg.f64 x))) (*.f64 i (-.f64 (*.f64 a b) (*.f64 y j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (fma.f64 j c (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a x)))) (*.f64 i (-.f64 (*.f64 a b) (*.f64 y j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (fma.f64 j c (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 a x)))) (*.f64 i (-.f64 (*.f64 a b) (*.f64 y j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (Rewrite<= fma-def_binary64 (+.f64 (*.f64 j c) (*.f64 -1 (*.f64 a x)))) (*.f64 i (-.f64 (*.f64 a b) (*.f64 y j)))): 0 points increase in error, 1 points decrease in error
(fma.f64 t (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 c j)) (*.f64 -1 (*.f64 a x))) (*.f64 i (-.f64 (*.f64 a b) (*.f64 y j)))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 a b) i) (*.f64 (*.f64 y j) i)))): 1 points increase in error, 0 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (-.f64 (Rewrite=> associate-*l*_binary64 (*.f64 a (*.f64 b i))) (*.f64 (*.f64 y j) i))): 5 points increase in error, 24 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (-.f64 (*.f64 a (Rewrite<= *-commutative_binary64 (*.f64 i b))) (*.f64 (*.f64 y j) i))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (-.f64 (*.f64 a (*.f64 i b)) (Rewrite=> associate-*l*_binary64 (*.f64 y (*.f64 j i))))): 13 points increase in error, 15 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (-.f64 (*.f64 a (*.f64 i b)) (*.f64 y (Rewrite<= *-commutative_binary64 (*.f64 i j))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 a (*.f64 i b)) (neg.f64 (*.f64 y (*.f64 i j)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (+.f64 (*.f64 a (*.f64 i b)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 y (*.f64 i j)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (+.f64 (*.f64 c j) (*.f64 -1 (*.f64 a x)))) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b))))): 3 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 (*.f64 c j) t) (*.f64 (*.f64 -1 (*.f64 a x)) t))) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))): 0 points increase in error, 2 points decrease in error
(+.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 j t))) (*.f64 (*.f64 -1 (*.f64 a x)) t)) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))): 15 points increase in error, 21 points decrease in error
(+.f64 (+.f64 (*.f64 c (Rewrite<= *-commutative_binary64 (*.f64 t j))) (*.f64 (*.f64 -1 (*.f64 a x)) t)) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 c (*.f64 t j)) (*.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 -1 a) x)) t)) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 c (*.f64 t j)) (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 -1 a) (*.f64 x t)))) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))): 15 points increase in error, 16 points decrease in error
(+.f64 (+.f64 (*.f64 c (*.f64 t j)) (*.f64 (*.f64 -1 a) (Rewrite<= *-commutative_binary64 (*.f64 t x)))) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 c (*.f64 t j)) (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 a (*.f64 t x))))) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 c (*.f64 t j)) (+.f64 (*.f64 -1 (*.f64 a (*.f64 t x))) (+.f64 (*.f64 -1 (*.f64 y (*.f64 i j))) (*.f64 a (*.f64 i b)))))): 0 points increase in error, 0 points decrease in error