Simplified8.2
\[\leadsto \color{blue}{2 \cdot \mathsf{fma}\left(z, t, \mathsf{fma}\left(\mathsf{fma}\left(b, c, a\right), i \cdot \left(-c\right), x \cdot y\right)\right)}
\]
Proof
(*.f64 2 (fma.f64 z t (fma.f64 (fma.f64 b c a) (*.f64 i (neg.f64 c)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (fma.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 b c) a)) (*.f64 i (neg.f64 c)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (fma.f64 (Rewrite<= +-commutative_binary64 (+.f64 a (*.f64 b c))) (*.f64 i (neg.f64 c)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (fma.f64 (+.f64 a (*.f64 b c)) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 i c))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (fma.f64 (+.f64 a (*.f64 b c)) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 c i))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 a (*.f64 b c)) (neg.f64 (*.f64 c i))) (*.f64 x y))))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (+.f64 a (*.f64 b c)) (*.f64 c i)))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (+.f64 (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i))) (*.f64 x y)))): 33 points increase in error, 13 points decrease in error
(*.f64 2 (fma.f64 z t (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) (*.f64 x y)))))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 z t (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) (*.f64 x y)))))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 z t) (-.f64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) (*.f64 x y))))): 1 points increase in error, 0 points decrease in error
(*.f64 2 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (*.f64 z t) (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x y) (-.f64 (*.f64 z t) (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i))))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)))): 0 points increase in error, 0 points decrease in error
Simplified14.4
\[\leadsto 2 \cdot \color{blue}{\left(t \cdot z - \mathsf{fma}\left(c, b, a\right) \cdot \left(c \cdot i\right)\right)}
\]
Proof
(-.f64 (*.f64 t z) (*.f64 (fma.f64 c b a) (*.f64 c i))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (*.f64 (fma.f64 c b (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 a)))) (*.f64 c i))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 c b) (neg.f64 a))) (*.f64 c i))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c i) (-.f64 (*.f64 c b) (neg.f64 a))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (*.f64 c i) (*.f64 c b)) (*.f64 (*.f64 c i) (neg.f64 a))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (Rewrite=> associate-*l*_binary64 (*.f64 c (*.f64 i (*.f64 c b)))) (*.f64 (*.f64 c i) (neg.f64 a)))): 12 points increase in error, 4 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (*.f64 c (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 c b) i))) (*.f64 (*.f64 c i) (neg.f64 a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (*.f64 c (Rewrite=> associate-*l*_binary64 (*.f64 c (*.f64 b i)))) (*.f64 (*.f64 c i) (neg.f64 a)))): 18 points increase in error, 11 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (*.f64 c (*.f64 c (Rewrite<= *-commutative_binary64 (*.f64 i b)))) (*.f64 (*.f64 c i) (neg.f64 a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c c) (*.f64 i b))) (*.f64 (*.f64 c i) (neg.f64 a)))): 31 points increase in error, 4 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 i b)) (*.f64 (*.f64 c i) (neg.f64 a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 c i) a))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (-.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 (*.f64 c i)) a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (Rewrite=> cancel-sign-sub_binary64 (+.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (*.f64 (*.f64 c i) a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (+.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 i a))))): 20 points increase in error, 14 points decrease in error
(-.f64 (*.f64 t z) (+.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 c c)) (*.f64 i b)) (*.f64 c (*.f64 i a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (+.f64 (Rewrite=> associate-*l*_binary64 (*.f64 c (*.f64 c (*.f64 i b)))) (*.f64 c (*.f64 i a)))): 4 points increase in error, 31 points decrease in error
(-.f64 (*.f64 t z) (+.f64 (*.f64 c (*.f64 c (Rewrite=> *-commutative_binary64 (*.f64 b i)))) (*.f64 c (*.f64 i a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (+.f64 (*.f64 c (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c b) i))) (*.f64 c (*.f64 i a)))): 11 points increase in error, 17 points decrease in error
(-.f64 (*.f64 t z) (+.f64 (*.f64 c (Rewrite<= *-commutative_binary64 (*.f64 i (*.f64 c b)))) (*.f64 c (*.f64 i a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (Rewrite<= distribute-lft-in_binary64 (*.f64 c (+.f64 (*.f64 i (*.f64 c b)) (*.f64 i a))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 t z) (*.f64 c (Rewrite<= distribute-lft-in_binary64 (*.f64 i (+.f64 (*.f64 c b) a))))): 1 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 t z) (neg.f64 (*.f64 c (*.f64 i (+.f64 (*.f64 c b) a)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 t z) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 c (*.f64 i (+.f64 (*.f64 c b) a)))))): 0 points increase in error, 0 points decrease in error