Simplified6.8
\[\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, 1 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)))): 37 points increase in error, 10 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))))): 0 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, 1 points decrease in error
Simplified11.6
\[\leadsto \color{blue}{2 \cdot \mathsf{fma}\left(c \cdot \left(-i\right), \mathsf{fma}\left(c, b, a\right), y \cdot x\right)}
\]
Proof
(*.f64 2 (fma.f64 (*.f64 c (neg.f64 i)) (fma.f64 c b a) (*.f64 y x))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 c i))) (fma.f64 c b a) (*.f64 y x))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 c i))) (fma.f64 c b a) (*.f64 y x))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (fma.f64 (*.f64 -1 (*.f64 c i)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 c b) a)) (*.f64 y x))): 0 points increase in error, 1 points decrease in error
(*.f64 2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 -1 (*.f64 c i)) (+.f64 (*.f64 c b) a)) (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (*.f64 c i) (+.f64 (*.f64 c b) a)))) (*.f64 y x))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (+.f64 (*.f64 -1 (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 i (+.f64 (*.f64 c b) a))))) (*.f64 y x))): 38 points increase in error, 23 points decrease in error
(*.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y x) (*.f64 -1 (*.f64 c (*.f64 i (+.f64 (*.f64 c b) a))))))): 0 points increase in error, 0 points decrease in error