:: deftheorem defines reduces_to POLYRED:def 5 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n holds
( f reduces_to g,p,b,T iff ( f <> 0_ (n,L) & p <> 0_ (n,L) & b in Support f & ex s being bag of n st
( s + (HT (p,T)) = b & g = f - (((f . b) / (HC (p,T))) * (s *' p)) ) ) );