:: Construction of {G}r\"obner Bases: Avoiding S-Polynomials -- Buchberger's First Criterium
:: by Christoph Schwarzweller
::
:: Received December 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: GROEB_3:1
for X being set
for b1, b2 being bag of X holds (b1 + b2) / b2 = b1
proofend;

theorem Th2: :: GROEB_3:2
for n being Ordinal
for T being admissible TermOrder of n
for b1, b2, b3 being bag of n st b1 <= b2,T holds
b1 + b3 <= b2 + b3,T
proofend;

theorem Th3: :: GROEB_3:3
for n being Ordinal
for T being TermOrder of n
for b1, b2, b3 being bag of n st b1 <= b2,T &amp; b2 < b3,T holds
b1 < b3,T
proofend;

theorem Th4: :: GROEB_3:4
for n being Ordinal
for T being admissible TermOrder of n
for b1, b2, b3 being bag of n st b1 < b2,T holds
b1 + b3 < b2 + b3,T
proofend;

theorem Th5: :: GROEB_3:5
for n being Ordinal
for T being admissible TermOrder of n
for b1, b2, b3, b4 being bag of n st b1 < b2,T &amp; b3 <= b4,T holds
b1 + b3 < b2 + b4,T
proofend;

theorem Th6: :: GROEB_3:6
for n being Ordinal
for T being admissible TermOrder of n
for b1, b2, b3, b4 being bag of n st b1 <= b2,T &amp; b3 < b4,T holds
b1 + b3 < b2 + b4,T
proofend;

begin

theorem Th7: :: GROEB_3:7
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for m1, m2 being non-zero Monomial of n,L holds term (m1 *' m2) = (term m1) + (term m2)
proofend;

theorem Th8: :: GROEB_3:8
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for b being bag of n holds
( b in Support p iff (term m) + b in Support (m *' p) )
proofend;

theorem Th9: :: GROEB_3:9
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for 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  }
proofend;

theorem Th10: :: GROEB_3:10
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L holds card (Support p) = card (Support (m *' p))
proofend;

Lm1:  for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for g being set
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
g is Polynomial of n,L
proofend;

theorem Th11: :: GROEB_3:11
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr holds Red ((0_ (n,L)),T) = 0_ (n,L)
proofend;

theorem Th12: :: GROEB_3:12
for n being Ordinal
for L being non trivial right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L st p - q = 0_ (n,L) holds
p = q
proofend;

theorem Th13: :: GROEB_3:13
for X being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_ (X,L)) = 0_ (X,L)
proofend;

theorem Th14: :: GROEB_3:14
for X being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for f being Series of X,L holds (0_ (X,L)) - f = - f
proofend;

theorem Th15: :: GROEB_3:15
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds p - (Red (p,T)) = HM (p,T)
proofend;

registration
let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
cluster Support p ->  finite ;
coherence
 Support p is finite by POLYNOM1:def_4;
end;

definition
let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p, q be Polynomial of n,L;
:: original:{
redefine func{p,q} ->  Subset of (Polynom-Ring (n,L));
coherence
 {p,q} is Subset of (Polynom-Ring (n,L))
proofend;
end;

begin

definition
let X be set ;
let L be non empty ZeroStr ;
let s be Series of X,L;
let Y be Subset of (Bags X);
funcs | Y ->  Series of X,L equals :: GROEB_3:def 1
s +* (((Support s) \ Y) --> (0. L));
coherence
 s +* (((Support s) \ Y) --> (0. L)) is Series of X,L
proofend;
end;

:: deftheorem  defines | GROEB_3:def_1_:_
 for X being set
for L being non empty ZeroStr
for s being Series of X,L
for Y being Subset of (Bags X) holds s | Y = s +* (((Support s) \ Y) --> (0. L));

Lm2:  for X being set
for L being non empty ZeroStr
for s being Series of X,L
for Y being Subset of (Bags X) holds Support (s | Y) c= Support s
proofend;

registration
let n be Ordinal;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
let Y be Subset of (Bags n);
clusterp | Y ->  finite-Support ;
coherence
 p | Y is finite-Support
proofend;
end;

theorem Th16: :: GROEB_3:16
for X being set
for L being non empty ZeroStr
for s being Series of X,L
for Y being Subset of (Bags X) holds
( Support (s | Y) = (Support s) /\ Y &amp; ( for b being bag of X st b in Support (s | Y) holds
(s | Y) . b = s . b ) )
proofend;

theorem :: GROEB_3:17
for X being set
for L being non empty ZeroStr
for s being Series of X,L
for Y being Subset of (Bags X) holds Support (s | Y) c= Support s by Lm2;

theorem :: GROEB_3:18
for X being set
for L being non empty ZeroStr
for s being Series of X,L holds
( s | (Support s) = s &amp; s | ({} (Bags X)) = 0_ (X,L) )
proofend;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
let i be Element of NAT ;
assume A1: i <= card (Support p) ;
func Upper_Support (p,T,i) ->  finite Subset of (Bags n) means :Def2: :: GROEB_3:def 2
( it c= Support p &amp; card it = i &amp; ( for b, b9 being bag of n st b in it &amp; b9 in Support p &amp; b <= b9,T holds
b9 in it ) );
existence
 ex b1 being finite Subset of (Bags n) st
( b1 c= Support p &amp; card b1 = i &amp; ( for b, b9 being bag of n st b in b1 &amp; b9 in Support p &amp; b <= b9,T holds
b9 in b1 ) )
proofend;
uniqueness
 for b1, b2 being finite Subset of (Bags n) st b1 c= Support p &amp; card b1 = i &amp; ( for b, b9 being bag of n st b in b1 &amp; b9 in Support p &amp; b <= b9,T holds
b9 in b1 ) &amp; b2 c= Support p &amp; card b2 = i &amp; ( for b, b9 being bag of n st b in b2 &amp; b9 in Support p &amp; b <= b9,T holds
b9 in b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Upper_Support GROEB_3:def_2_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b6 being finite Subset of (Bags n) holds
( b6 = Upper_Support (p,T,i) iff ( b6 c= Support p &amp; card b6 = i &amp; ( for b, b9 being bag of n st b in b6 &amp; b9 in Support p &amp; b <= b9,T holds
b9 in b6 ) ) );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
let i be Element of NAT ;
func Lower_Support (p,T,i) ->  finite Subset of (Bags n) equals :: GROEB_3:def 3
(Support p) \ (Upper_Support (p,T,i));
coherence
 (Support p) \ (Upper_Support (p,T,i)) is finite Subset of (Bags n)
proofend;
end;

:: deftheorem  defines Lower_Support GROEB_3:def_3_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT holds Lower_Support (p,T,i) = (Support p) \ (Upper_Support (p,T,i));

theorem Th19: :: GROEB_3:19
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p &amp; (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} )
proofend;

theorem Th20: :: GROEB_3:20
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b, b9 being bag of n st b in Upper_Support (p,T,i) &amp; b9 in Lower_Support (p,T,i) holds
b9 < b,T
proofend;

theorem :: GROEB_3:21
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( Upper_Support (p,T,0) = {} &amp; Lower_Support (p,T,0) = Support p )
proofend;

theorem Th22: :: GROEB_3:22
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( Upper_Support (p,T,(card (Support p))) = Support p &amp; Lower_Support (p,T,(card (Support p))) = {} )
proofend;

theorem Th23: :: GROEB_3:23
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i &amp; i <= card (Support p) holds
HT (p,T) in Upper_Support (p,T,i)
proofend;

theorem Th24: :: GROEB_3:24
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Lower_Support (p,T,i) c= Support p &amp; card (Lower_Support (p,T,i)) = (card (Support p)) - i &amp; ( for b, b9 being bag of n st b in Lower_Support (p,T,i) &amp; b9 in Support p &amp; b9 <= b,T holds
b9 in Lower_Support (p,T,i) ) )
proofend;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
let i be Element of NAT ;
func Up (p,T,i) ->  Polynomial of n,L equals :: GROEB_3:def 4
p | (Upper_Support (p,T,i));
coherence
 p | (Upper_Support (p,T,i)) is Polynomial of n,L ;
func Low (p,T,i) ->  Polynomial of n,L equals :: GROEB_3:def 5
p | (Lower_Support (p,T,i));
coherence
 p | (Lower_Support (p,T,i)) is Polynomial of n,L ;
end;

:: deftheorem  defines Up GROEB_3:def_4_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT holds Up (p,T,i) = p | (Upper_Support (p,T,i));

:: deftheorem  defines Low GROEB_3:def_5_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT holds Low (p,T,i) = p | (Lower_Support (p,T,i));

Lm3:  for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Support (p | (Upper_Support (p,T,i))) = Upper_Support (p,T,i) &amp; Support (p | (Lower_Support (p,T,i))) = Lower_Support (p,T,i) )
proofend;

theorem :: GROEB_3:25
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Support (Up (p,T,i)) = Upper_Support (p,T,i) &amp; Support (Low (p,T,i)) = Lower_Support (p,T,i) ) by Lm3;

theorem Th26: :: GROEB_3:26
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Support (Up (p,T,i)) c= Support p &amp; Support (Low (p,T,i)) c= Support p )
proofend;

theorem Th27: :: GROEB_3:27
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st 1 <= i &amp; i <= card (Support p) holds
Support (Low (p,T,i)) c= Support (Red (p,T))
proofend;

theorem Th28: :: GROEB_3:28
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
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)) ) &amp; not b in (Support (Up (p,T,i))) /\ (Support (Low (p,T,i))) )
proofend;

theorem Th29: :: GROEB_3:29
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b, b9 being bag of n st b in Support (Low (p,T,i)) &amp; b9 in Support (Up (p,T,i)) holds
b < b9,T
proofend;

theorem Th30: :: GROEB_3:30
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st 1 <= i &amp; i <= card (Support p) holds
HT (p,T) in Support (Up (p,T,i))
proofend;

theorem Th31: :: GROEB_3:31
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n st b in Support (Low (p,T,i)) holds
( (Low (p,T,i)) . b = p . b &amp; (Up (p,T,i)) . b = 0. L )
proofend;

theorem Th32: :: GROEB_3:32
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n st b in Support (Up (p,T,i)) holds
( (Up (p,T,i)) . b = p . b &amp; (Low (p,T,i)) . b = 0. L )
proofend;

theorem Th33: :: GROEB_3:33
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
(Up (p,T,i)) + (Low (p,T,i)) = p
proofend;

theorem Th34: :: GROEB_3:34
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( Up (p,T,0) = 0_ (n,L) &amp; Low (p,T,0) = p )
proofend;

theorem Th35: :: GROEB_3:35
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds
( Up (p,T,(card (Support p))) = p &amp; Low (p,T,(card (Support p))) = 0_ (n,L) )
proofend;

theorem Th36: :: GROEB_3:36
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being non-zero Polynomial of n,L holds
( Up (p,T,1) = HM (p,T) &amp; Low (p,T,1) = Red (p,T) )
proofend;

registration
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ;
let p be non-zero Polynomial of n,L;
cluster Up (p,T,0) ->  monomial-like ;
coherence
 Up (p,T,0) is monomial-like
proofend;
end;

registration
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr ;
let p be non-zero Polynomial of n,L;
cluster Up (p,T,1) ->  non-zero monomial-like ;
coherence
 ( Up (p,T,1) is non-zero &amp; Up (p,T,1) is monomial-like )
proofend;
cluster Low (p,T,(card (Support p))) ->  monomial-like ;
coherence
 Low (p,T,(card (Support p))) is monomial-like
proofend;
end;

theorem Th37: :: GROEB_3:37
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for j being Element of NAT st j = (card (Support p)) - 1 holds
Low (p,T,j) is non-zero Monomial of n,L
proofend;

theorem Th38: :: GROEB_3:38
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for 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
proofend;

theorem Th39: :: GROEB_3:39
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st 0 < i &amp; i < card (Support p) holds
HT ((Low (p,T,i)),T) < HT (p,T),T
proofend;

theorem Th40: :: GROEB_3:40
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
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)) )
proofend;

theorem Th41: :: GROEB_3:41
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i < card (Support p) holds
Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))
proofend;

theorem Th42: :: GROEB_3:42
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for 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))}
proofend;

theorem Th43: :: GROEB_3:43
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i < card (Support p) holds
Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)
proofend;

theorem Th44: :: GROEB_3:44
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
Low ((m *' p),T,i) = m *' (Low (p,T,i))
proofend;

begin

Lm4:  for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for R being RedSequence of PolyRedRel (P,T)
for i being Element of NAT st 1 <= i &amp; i <= len R &amp; len R > 1 holds
R . i is Polynomial of n,L
proofend;

theorem Th45: :: GROEB_3:45
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds
- f reduces_to - g,p,T
proofend;

Lm5:  for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds
for b1, b2 being bag of n st b1 in Support p1 &amp; b2 in Support p2 &amp; ( not b1 = HT (p1,T) or not b2 = HT (p2,T) ) holds
not (HT (p1,T)) + b2 = (HT (p2,T)) + b1
proofend;

theorem Th46: :: GROEB_3:46
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T &amp; ( 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
proofend;

theorem Th47: :: GROEB_3:47
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red (f,T)) *' g,{g},T
proofend;

theorem :: GROEB_3:48
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L
for 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
proofend;

theorem Th49: :: GROEB_3:49
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces - f, - g
proofend;

theorem :: GROEB_3:50
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 &amp; ( 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
proofend;

theorem Th51: :: GROEB_3:51
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L holds PolyRedRel ({g},T) reduces f *' g, 0_ (n,L)
proofend;

begin

theorem Th52: :: GROEB_3:52
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds
for b1, b2 being bag of n st b1 in Support (Red (p1,T)) &amp; b2 in Support (Red (p2,T)) holds
not (HT (p1,T)) + b2 = (HT (p2,T)) + b1
proofend;

theorem Th53: :: GROEB_3:53
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for 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)))
proofend;

theorem Th54: :: GROEB_3:54
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for 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)
proofend;

theorem Th55: :: GROEB_3:55
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being non-zero Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint &amp; Red (p1,T) is non-zero &amp; 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))
proofend;

theorem Th56: :: GROEB_3:56
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for 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)
proofend;

:: theorem 5.66, p. 222 (Buchberger's first criterium)
theorem :: GROEB_3:57
for n being Element of NAT
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 &amp; g2 in G &amp; not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
proofend;

:: theorem 5.68 (i) ==> (ii), p. 223
theorem :: GROEB_3:58
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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G &amp; ( for g1, g2 being Polynomial of n,L st g1 in G &amp; g2 in G &amp; 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 &amp; g2 in G &amp; not HT (g1,T), HT (g2,T) are_disjoint &amp; h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
proofend;

:: theorem 5.68 (ii) ==> (iii), p. 223
theorem :: GROEB_3:59
for n being Element of NAT
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 not 0_ (n,L) in G &amp; ( for g1, g2, h being Polynomial of n,L st g1 in G &amp; g2 in G &amp; not HT (g1,T), HT (g2,T) are_disjoint &amp; h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ) holds
G is_Groebner_basis_wrt T
proofend;