theorem
for
n being
Element of
NAT for
T being
connected admissible TermOrder of
n for
L being non
degenerated non
trivial 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 not
0_ (
n,
L)
in G & ( 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) ) holds
for
g1,
g2,
h being
Polynomial of
n,
L st
g1 in G &
g2 in G & not
HT (
g1,
T),
HT (
g2,
T)
are_disjoint &
h is_a_normal_form_of S-Poly (
g1,
g2,
T),
PolyRedRel (
G,
T) holds
h = 0_ (
n,
L)