let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT (p,T) <= HT (f,T),T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT (p,T) <= HT (f,T),T
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT (p,T) <= HT (f,T),T
let f, p be non-zero Polynomial of n,L; :: thesis: ( f is_reducible_wrt p,T implies HT (p,T) <= HT (f,T),T )
assume f is_reducible_wrt p,T ; :: thesis: HT (p,T) <= HT (f,T),T
then consider b being bag of n such that
A1: ( b in Support f & HT (p,T) divides b ) by POLYRED:36;
( b <= HT (f,T),T & HT (p,T) <= b,T ) by A1, TERMORD:10, TERMORD:def 6;
hence HT (p,T) <= HT (f,T),T by TERMORD:8; :: thesis: verum