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 p, q being Element of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,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 Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Element of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
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 p, q being Element of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
let p, q be Element of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
let G be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_wrt T implies ( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) ) )
set R = PolyRedRel (G,T);
assume G is_Groebner_basis_wrt T ; :: thesis: ( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
then A1: PolyRedRel (G,T) is locally-confluent ;
hence ( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) ) by A1, POLYRED:58, REWRITE1:55; :: thesis: verum