:: deftheorem defines top_reduces_to POLYRED:def 10 :
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 holds
( f top_reduces_to g,p,T iff f reduces_to g,p, HT (f,T),T );