let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_wrt T implies for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) )
assume G is_Groebner_basis_wrt T ; :: thesis: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
then for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) by GROEB_2:23;
hence for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by GROEB_2:24; :: thesis: verum