Simplified11.1
\[\leadsto 2 \cdot \color{blue}{\left(y \cdot x - \mathsf{fma}\left(c, b, a\right) \cdot \left(c \cdot i\right)\right)}
\]
Proof
(-.f64 (*.f64 y x) (*.f64 (fma.f64 c b a) (*.f64 c i))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (*.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 c b) a)) (*.f64 c i))): 1 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c i) (+.f64 (*.f64 c b) a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 i (+.f64 (*.f64 c b) a))))): 31 points increase in error, 19 points decrease in error
(-.f64 (*.f64 y x) (*.f64 c (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 (*.f64 c b) i) (*.f64 a i))))): 2 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 c (*.f64 (*.f64 c b) i)) (*.f64 c (*.f64 a i))))): 1 points increase in error, 2 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (*.f64 c (Rewrite=> associate-*l*_binary64 (*.f64 c (*.f64 b i)))) (*.f64 c (*.f64 a i)))): 18 points increase in error, 13 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (*.f64 c (*.f64 c (Rewrite<= *-commutative_binary64 (*.f64 i b)))) (*.f64 c (*.f64 a i)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c c) (*.f64 i b))) (*.f64 c (*.f64 a i)))): 26 points increase in error, 4 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 i b)) (*.f64 c (*.f64 a i)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (Rewrite<= cancel-sign-sub_binary64 (-.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (*.f64 (neg.f64 c) (*.f64 a i))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (-.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 c (*.f64 a i)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (-.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 c (*.f64 a i)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (-.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 c (*.f64 a i)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (-.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 c) (*.f64 a i))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (Rewrite=> cancel-sign-sub_binary64 (+.f64 (*.f64 (pow.f64 c 2) (*.f64 i b)) (*.f64 c (*.f64 a i))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 c c)) (*.f64 i b)) (*.f64 c (*.f64 a i)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (Rewrite=> associate-*l*_binary64 (*.f64 c (*.f64 c (*.f64 i b)))) (*.f64 c (*.f64 a i)))): 4 points increase in error, 26 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (*.f64 c (*.f64 c (Rewrite=> *-commutative_binary64 (*.f64 b i)))) (*.f64 c (*.f64 a i)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 y x) (+.f64 (*.f64 c (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c b) i))) (*.f64 c (*.f64 a i)))): 13 points increase in error, 18 points decrease in error
(-.f64 (*.f64 y x) (Rewrite<= distribute-lft-in_binary64 (*.f64 c (+.f64 (*.f64 (*.f64 c b) i) (*.f64 a i))))): 2 points increase in error, 1 points decrease in error
(-.f64 (*.f64 y x) (*.f64 c (Rewrite<= distribute-rgt-in_binary64 (*.f64 i (+.f64 (*.f64 c b) a))))): 0 points increase in error, 2 points decrease in error