:: Construction of {G}r\"obner Bases: Avoiding S-Polynomials -- Buchberger's
:: First Criterium
:: by Christoph Schwarzweller
::
:: Received December 10, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_POLY, ARYTM_3, ARYTM_1, ORDINAL1, BAGORDER,
XXREAL_0, RLVECT_1, ALGSTR_0, VECTSP_1, LATTICES, VECTSP_2, ZFMISC_1,
VALUED_0, POLYNOM7, CAT_3, RELAT_2, POLYNOM1, BROUWER, SUPINF_2,
XCMPLX_0, SUBSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, ALGSTR_1, CARD_1,
FUNCT_7, TERMORD, BINOP_1, POLYRED, REWRITE1, FINSEQ_1, STRUCT_0,
FINSET_1, FUNCT_4, FUNCOP_1, ALGSEQ_1, ORDERS_2, WAYBEL_4, RUSUB_4,
GROEB_2, MESFUNC1, GROEB_1, GROEB_3, NAT_1;
notations TARSKI, SUBSET_1, RELAT_1, XBOOLE_0, RELAT_2, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_4,
FUNCOP_1, PRE_POLY, STRUCT_0, ALGSTR_0, GROUP_1, ALGSTR_1, RLVECT_1,
VFUNCT_1, FINSET_1, XTUPLE_0, MCART_1, FINSEQ_1, VECTSP_2, VECTSP_1,
POLYNOM7, ORDERS_2, FUNCT_7, REWRITE1, BAGORDER, TERMORD, GROEB_1,
POLYRED, GROEB_2, WAYBEL_4, POLYNOM1;
constructors XXREAL_0, REWRITE1, VECTSP_2, WAYBEL_4, POLYNOM2, BAGORDER,
TERMORD, POLYRED, GROEB_1, GROEB_2, RELSET_1, PBOOLE, FUNCT_7, VFUNCT_1,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, NAT_1,
INT_1, CARD_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1,
POLYNOM1, POLYNOM2, POLYNOM4, POLYNOM7, TERMORD, POLYRED, ORDINAL1,
VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, RELSET_1, FUNCT_4;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
theorem :: GROEB_3:1
for X being set, b1,b2 being bag of X holds (b1 + b2) / b2 = b1;
theorem :: GROEB_3:2
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3
being bag of n holds b1 <= b2,T implies b1 + b3 <= b2 + b3,T;
theorem :: GROEB_3:3
for n being Ordinal, T being TermOrder of n, b1,b2,b3 being bag
of n holds b1 <= b2,T & b2 < b3,T implies b1 < b3,T;
theorem :: GROEB_3:4
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3
being bag of n holds b1 < b2,T implies b1 + b3 < b2 + b3,T;
theorem :: GROEB_3:5
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3,
b4 being bag of n holds b1 < b2,T & b3 <= b4,T implies b1 + b3 < b2 + b4,T;
theorem :: GROEB_3:6
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3,
b4 being bag of n holds b1 <= b2,T & b3 < b4,T implies b1 + b3 < b2 + b4,T;
begin :: More on Polynomials
theorem :: GROEB_3:7
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
m1,m2 being non-zero Monomial of n,L holds term(m1*'m2) = term(m1) + term(m2)
;
theorem :: GROEB_3:8
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, m being non-zero Monomial of n,L, b being bag of n
holds b in Support(p) iff term(m) + b in Support(m*'p);
theorem :: GROEB_3:9
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, m being non-zero Monomial of n,L holds Support(m*'p)
= { term(m) + b where b is Element of Bags n : b in Support p };
theorem :: GROEB_3:10
for n being Ordinal, L being add-associative
right_complementable left_zeroed right_zeroed well-unital distributive
domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, m being
non-zero Monomial of n,L holds card Support(p) = card Support(m*'p);
theorem :: GROEB_3:11
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr
holds Red(0_(n,L),T) = 0_(n,L);
theorem :: GROEB_3:12
for n being Ordinal, L being Abelian add-associative
right_zeroed right_complementable commutative well-unital distributive non
trivial doubleLoopStr, p,q being Polynomial of n,L holds p - q = 0_(n,L)
implies p = q;
theorem :: GROEB_3:13
for X being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr holds -(0_(X,L)) = 0_(X,L);
theorem :: GROEB_3:14
for X being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, f being Series of X,L holds 0_(X,L
) - f = -f;
theorem :: GROEB_3:15
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial doubleLoopStr,
p being Polynomial of n,L holds p - Red(p,T) = HM(p,T);
registration
let n be Ordinal, L be add-associative right_complementable right_zeroed
non empty addLoopStr, p be Polynomial of n,L;
cluster Support p -> finite;
end;
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n,L;
redefine func {p,q} -> Subset of Polynom-Ring(n,L);
end;
begin :: Restriction and Splitting of Polynomials
definition
let X be set, L be non empty ZeroStr, s be Series of X,L, Y be Subset of
Bags X;
func s|Y -> Series of X,L equals
:: GROEB_3:def 1
s +* ((Support s \ Y) --> 0.L);
end;
registration
let n be Ordinal, L be non empty ZeroStr, p be Polynomial of n,L, Y be
Subset of Bags n;
cluster p|Y -> finite-Support;
end;
theorem :: GROEB_3:16
for X being set, L being non empty ZeroStr, s being Series of X,
L, Y being Subset of Bags X holds Support s|Y = (Support s) /\ Y & for b being
bag of X st b in Support s|Y holds (s|Y).b = s.b;
theorem :: GROEB_3:17
for X being set, L being non empty ZeroStr, s being Series of X,L, Y
being Subset of Bags X holds Support(s|Y) c= Support s;
theorem :: GROEB_3:18
for X being set, L being non empty ZeroStr, s being Series of X,L
holds s|(Support s) = s & s|({} Bags X) = 0_(X,L);
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Nat such that
i <= card(Support p);
func Upper_Support(p,T,i) -> finite Subset of Bags n means
:: GROEB_3:def 2
it c=
Support p & card it = i & for b,b9 being bag of n st b in it & b9 in Support p
& b <= b9,T holds b9 in it;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Nat;
func Lower_Support(p,T,i) -> finite Subset of Bags n equals
:: GROEB_3:def 3
Support(p) \ Upper_Support(p,T,i);
end;
theorem :: GROEB_3:19
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Upper_Support(p,T,i) \/ Lower_Support(p,T,i) = Support p & Upper_Support(p,T,i)
/\ Lower_Support(p,T,i) = {};
theorem :: GROEB_3:20
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b,
b9 being bag of n st b in Upper_Support(p,T,i) & b9 in Lower_Support(p,T,i)
holds b9 < b,T;
theorem :: GROEB_3:21
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Upper_Support(p,T,0) = {} & Lower_Support(p,T,0)
= Support p;
theorem :: GROEB_3:22
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Upper_Support(p,T,card(Support p)) = Support p &
Lower_Support(p,T,card(Support p)) = {};
theorem :: GROEB_3:23
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non trivial addLoopStr, p
being non-zero Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(
Support p) holds HT(p,T) in Upper_Support(p,T,i);
theorem :: GROEB_3:24
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Lower_Support(p,T,i) c= Support p & card Lower_Support(p,T,i) = card(Support p)
- i & for b,b9 being bag of n st b in Lower_Support(p,T,i) & b9 in Support p &
b9 <= b,T holds b9 in Lower_Support(p,T,i);
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Nat;
func Up(p,T,i) -> Polynomial of n,L equals
:: GROEB_3:def 4
p|(Upper_Support(p,T,i));
func Low(p,T,i) -> Polynomial of n,L equals
:: GROEB_3:def 5
p|(Lower_Support(p,T,i));
end;
theorem :: GROEB_3:25
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Support Up(p,T,i) = Upper_Support(p,T,i) & Support Low(p,T,i) = Lower_Support(p
,T,i);
theorem :: GROEB_3:26
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Support(Up(p,T,i)) c= Support(p) & Support(Low(p,T,i)) c= Support(p);
theorem :: GROEB_3:27
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(Support p
) holds Support(Low(p,T,i)) c= Support(Red(p,T));
theorem :: GROEB_3:28
for n be Ordinal, T be connected TermOrder of n, L be
add-associative right_zeroed right_complementable non empty addLoopStr, p be
Polynomial of n,L, i be Element of NAT st i <= card(Support p) for b being bag
of n st b in Support p holds (b in Support Up(p,T,i) or b in Support Low(p,T,i)
) & not(b in Support Up(p,T,i) /\ Support Low(p,T,i));
theorem :: GROEB_3:29
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b,
b9 being bag of n st b in Support Low(p,T,i) & b9 in Support Up(p,T,i) holds b
< b9,T;
theorem :: GROEB_3:30
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(Support p
) holds HT(p,T) in Support Up(p,T,i);
theorem :: GROEB_3:31
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b
being bag of n st b in Support Low(p,T,i) holds Low(p,T,i).b = p.b & Up(p,T,i).
b = 0.L;
theorem :: GROEB_3:32
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b
being bag of n st b in Support Up(p,T,i) holds Up(p,T,i).b = p.b & Low(p,T,i).b
= 0.L;
theorem :: GROEB_3:33
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Up(p,T,i) + Low(p,T,i) = p;
theorem :: GROEB_3:34
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Up(p,T,0) = 0_(n,L) & Low(p,T,0) = p;
theorem :: GROEB_3:35
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable Abelian non empty
doubleLoopStr, p being Polynomial of n,L holds Up(p,T,card(Support p)) = p &
Low(p,T,card(Support p)) = 0_(n,L);
theorem :: GROEB_3:36
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable Abelian non trivial
doubleLoopStr, p being non-zero Polynomial of n,L holds Up(p,T,1) = HM(p,T) &
Low(p,T,1) = Red(p,T);
registration
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non trivial addLoopStr, p be non-zero
Polynomial of n,L;
cluster Up(p,T,0) -> monomial-like;
end;
registration
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable Abelian non trivial doubleLoopStr, p be
non-zero Polynomial of n,L;
cluster Up(p,T,1) -> non-zero monomial-like;
cluster Low(p,T,card(Support p)) -> monomial-like;
end;
theorem :: GROEB_3:37
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non trivial addLoopStr, p
being Polynomial of n,L, j being Element of NAT st j = card(Support p) - 1
holds Low(p,T,j) is non-zero Monomial of n,L;
theorem :: GROEB_3:38
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non empty
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds HT(Low(p,T,i+1),T) <= HT(Low(p,T,i),T), T;
theorem :: GROEB_3:39
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 0 < i & i < card(Support p)
holds HT(Low(p,T,i),T) < HT(p,T),T;
theorem :: GROEB_3:40
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed well-unital
distributive domRing-like non trivial doubleLoopStr, p being Polynomial of n,
L, m being non-zero Monomial of n,L, i being Element of NAT st i <= card(
Support p) for b being bag of n holds term(m) + b in Support Low(m*'p,T,i) iff
b in Support Low(p,T,i);
theorem :: GROEB_3:41
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non empty
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds Support Low(p,T,i+1) c= Support Low(p,T,i);
theorem :: GROEB_3:42
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non empty
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds Support Low(p,T,i) \ Support Low(p,T,i+1) = {HT(Low(p,T,i),T)}
;
theorem :: GROEB_3:43
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non trivial
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds Low(p,T,i+1) = Red(Low(p,T,i),T);
theorem :: GROEB_3:44
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed well-unital
distributive domRing-like non trivial doubleLoopStr, p being Polynomial of n,
L, m being non-zero Monomial of n,L, i being Element of NAT st i <= card(
Support p) holds Low(m*'p,T,i) = m *' Low(p,T,i);
begin
theorem :: GROEB_3:45
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, f,g,p being Polynomial of n,L st f reduces_to g,p,T
holds -f reduces_to -g,p,T;
theorem :: GROEB_3:46
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, f,f1,g,p being Polynomial of n,L st f reduces_to f1,{p}
,T & for b1 being bag of n st b1 in Support g holds not(HT(p,T) divides b1)
holds f + g reduces_to f1 + g,{p},T;
theorem :: GROEB_3:47
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, f,g being non-zero Polynomial of n,L holds f*'g
reduces_to Red(f,T)*'g,{g},T;
theorem :: GROEB_3:48
for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,g being non-zero Polynomial of n,L, p being Polynomial of n,L
st p.(HT(f*'g,T)) = 0.L holds f*'g+p reduces_to Red(f,T)*'g+p,{g},T;
theorem :: GROEB_3:49
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g being Polynomial
of n,L st PolyRedRel(P,T) reduces f,g holds PolyRedRel(P,T) reduces -f,-g;
theorem :: GROEB_3:50
for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,f1,g,p being Polynomial of n,L st PolyRedRel({p},T) reduces f
,f1 & for b1 being bag of n st b1 in Support g holds not(HT(p,T) divides b1)
holds PolyRedRel({p},T) reduces f+g,f1+g;
theorem :: GROEB_3:51
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, f,g being non-zero Polynomial of n,L holds PolyRedRel({
g},T) reduces f*'g,0_(n,L);
begin :: The Criterium
theorem :: GROEB_3:52
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
for b1,b2 being bag of n st b1 in Support Red(p1,T) & b2 in Support Red(p2,T)
holds not(HT(p1,T) + b2 = HT(p2,T) + b1);
theorem :: GROEB_3:53
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
holds S-Poly(p1,p2,T) = HM(p2,T) *' Red(p1,T) - HM(p1,T) *' Red(p2,T);
theorem :: GROEB_3:54
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
holds S-Poly(p1,p2,T) = Red(p1,T) *' p2 - Red(p2,T) *' p1;
theorem :: GROEB_3:55
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, p1,p2 being non-zero Polynomial of n,L st HT(p1,T),HT(
p2,T) are_disjoint & Red(p1,T) is non-zero & Red(p2,T) is non-zero holds
PolyRedRel({p1},T) reduces HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(p2,T), p2 *' Red
(p1,T);
theorem :: GROEB_3:56
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T)
are_disjoint holds PolyRedRel({p1,p2},T) reduces S-Poly(p1,p2,T),0_(n,L);
:: theorem 5.66, p. 222 (Buchberger's first criterium)
theorem :: GROEB_3:57
for n being Element of NAT, T being connected admissible TermOrder of
n, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
degenerated non empty doubleLoopStr, G being Subset of Polynom-Ring(n,L)
holds 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));
:: theorem 5.68 (i) ==> (ii), p. 223
theorem :: GROEB_3:58
for n being Element of NAT, T being connected admissible TermOrder of
n, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
degenerated non trivial doubleLoopStr, G being Subset of Polynom-Ring(n,L) st
not(0_(n,L) in G) 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)) implies (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));
:: theorem 5.68 (ii) ==> (iii), p. 223
theorem :: GROEB_3:59
for n being Element of NAT, T being connected admissible TermOrder of
n, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
degenerated non empty doubleLoopStr, G being Subset of Polynom-Ring(n,L) st
not(0_(n,L) in G) 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)) implies G is_Groebner_basis_wrt T;
:: theorem 5.68 (iii) ==> (i), p. 223