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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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:28;
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:29; :: thesis: verum