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 I being Subset of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T holds
for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 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 I being Subset of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T holds
for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 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 I being Subset of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T holds
for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L)
let I be Subset of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T holds
for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L)
let G be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_of I,T implies for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) )
assume G is_Groebner_basis_of I,T ; :: thesis: for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L)
then ( G -Ideal = I & PolyRedRel (G,T) is locally-confluent ) by Def4;
hence for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) by Th15; :: thesis: verum