:: Construction of {G}r\"obner bases. S-Polynomials and Standard Representations
:: by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem :: GROEB_2:1
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of L
for n being Element of NAT st ( for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L ) holds
Sum p = Sum (p | n)
proofend;

theorem :: GROEB_2:2
for L being non empty Abelian add-associative right_zeroed addLoopStr
for f being FinSequence of L
for i, j being Element of NAT holds Sum (Swap (f,i,j)) = Sum f
proofend;

definition
let X be set ;
let b1, b2 be bag of X;
assume A1: b2 divides b1 ;
funcb1 / b2 ->  bag of X means :Def1: :: GROEB_2:def 1
b2 + it = b1;
existence
 ex b1 being bag of X st b2 + b1 = b1 by A1, TERMORD:1;
uniqueness
 for b1, b2 being bag of X st b2 + b1 = b1 & b2 + b2 = b1 holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines / GROEB_2:def_1_:_
 for X being set
for b1, b2 being bag of X st b2 divides b1 holds
for b4 being bag of X holds
( b4 = b1 / b2 iff b2 + b4 = b1 );

definition
let X be set ;
let b1, b2 be bag of X;
func lcm (b1,b2) ->  bag of X means :Def2: :: GROEB_2:def 2
 for k being set holds it . k = max ((b1 . k),(b2 . k));
existence
 ex b1 being bag of X st
for k being set holds b1 . k = max ((b1 . k),(b2 . k))
proofend;
uniqueness
 for b1, b2 being bag of X st ( for k being set holds b1 . k = max ((b1 . k),(b2 . k)) ) & ( for k being set holds b2 . k = max ((b1 . k),(b2 . k)) ) holds
b1 = b2
proofend;
commutativity
 for b1, b1, b2 being bag of X st ( for k being set holds b1 . k = max ((b1 . k),(b2 . k)) ) holds
for k being set holds b1 . k = max ((b2 . k),(b1 . k)) ;
idempotence
 for b1 being bag of X
for k being set holds b1 . k = max ((b1 . k),(b1 . k)) ;
end;

:: deftheorem Def2 defines lcm GROEB_2:def_2_:_
 for X being set
for b1, b2, b4 being bag of X holds
( b4 = lcm (b1,b2) iff for k being set holds b4 . k = max ((b1 . k),(b2 . k)) );

notation
let X be set ;
let b1, b2 be bag of X;
synonym b1 lcm b2 for  lcm (b1,b2);
end;

:: exercise 5.45, p. 211
definition
let X be set ;
let b1, b2 be bag of X;
predb1,b2 are_disjoint  means :Def3: :: GROEB_2:def 3
 for i being set holds
( b1 . i = 0 or b2 . i = 0 );
end;

:: deftheorem Def3 defines are_disjoint GROEB_2:def_3_:_
 for X being set
for b1, b2 being bag of X holds
( b1,b2 are_disjoint iff for i being set holds
( b1 . i = 0 or b2 . i = 0 ) );

notation
let X be set ;
let b1, b2 be bag of X;
antonym b1,b2 are_non_disjoint for b1,b2 are_disjoint ;
end;

theorem Th3: :: GROEB_2:3
for X being set
for b1, b2 being bag of X holds
( b1 divides lcm (b1,b2) & b2 divides lcm (b1,b2) )
proofend;

:: exercise 5.45, p. 211
theorem Th4: :: GROEB_2:4
for X being set
for b1, b2, b3 being bag of X st b1 divides b3 & b2 divides b3 holds
lcm (b1,b2) divides b3
proofend;

:: exercise 5.45, p. 211
theorem :: GROEB_2:5
for X being set
for b1, b2 being bag of X holds
( b1,b2 are_disjoint iff lcm (b1,b2) = b1 + b2 )
proofend;

theorem Th6: :: GROEB_2:6
for X being set
for b being bag of X holds b / b = EmptyBag X
proofend;

theorem Th7: :: GROEB_2:7
for X being set
for b1, b2 being bag of X holds
( b2 divides b1 iff lcm (b1,b2) = b1 )
proofend;

theorem :: GROEB_2:8
for X being set
for b1, b2, b3 being bag of X st b1 divides lcm (b2,b3) holds
lcm (b2,b1) divides lcm (b2,b3)
proofend;

:: exercise 5.69 (i) ==> (ii), p. 223
theorem :: GROEB_2:9
for X being set
for b1, b2, b3 being bag of X st lcm (b2,b1) divides lcm (b2,b3) holds
lcm (b1,b3) divides lcm (b2,b3)
proofend;

:: exercise 5.69 (ii) ==> (iii), p. 223
theorem :: GROEB_2:10
for n being set
for b1, b2, b3 being bag of n st lcm (b1,b3) divides lcm (b2,b3) holds
b1 divides lcm (b2,b3)
proofend;

:: exercise 5.69 (iii) ==> (i), p. 223
theorem :: GROEB_2:11
for n being Element of NAT
for T being connected admissible TermOrder of n
for P being non empty Subset of (Bags n) ex b being bag of n st
( b in P & ( for b9 being bag of n st b9 in P holds
b <= b9,T ) )
proofend;

registration
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ;
let a be non zero Element of L;
cluster - a ->  non zero ;
coherence
 not - a is zero
proofend;
end;

registration
let X be set ;
let L be non empty add-cancelable distributive right_zeroed left_zeroed doubleLoopStr ;
let m be Monomial of X,L;
let a be Element of L;
clustera * m ->  monomial-like ;
coherence
 a * m is monomial-like
proofend;
end;

registration
let n be Ordinal;
let L be non trivial add-cancelable distributive right_zeroed domRing-like left_zeroed doubleLoopStr ;
let p be non-zero Polynomial of n,L;
let a be non zero Element of L;
clustera * p ->  non-zero ;
coherence
 a * p is non-zero
proofend;
end;

theorem Th12: :: GROEB_2:12
for n being Ordinal
for L being non empty right-distributive right_zeroed doubleLoopStr
for p, q being Series of n,L
for b being bag of n holds b *' (p + q) = (b *' p) + (b *' q)
proofend;

theorem Th13: :: GROEB_2:13
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for b being bag of n holds b *' (- p) = - (b *' p)
proofend;

theorem Th14: :: GROEB_2:14
for n being Ordinal
for L being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for p being Series of n,L
for b being bag of n
for a being Element of L holds b *' (a * p) = a * (b *' p)
proofend;

theorem Th15: :: GROEB_2:15
for n being Ordinal
for L being non empty right-distributive doubleLoopStr
for p, q being Series of n,L
for a being Element of L holds a * (p + q) = (a * p) + (a * q)
proofend;

theorem Th16: :: GROEB_2:16
for X being set
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of L holds - (a | (X,L)) = (- a) | (X,L)
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;

begin

theorem Th17: :: GROEB_2:17
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 P being Subset of (Polynom-Ring (n,L)) st ( for p1, p2 being Polynomial of n,L st p1 <> p2 &amp; p1 in P &amp; p2 in P holds
for m1, m2 being Monomial of n,L st HM ((m1 *' p1),T) = HM ((m2 *' p2),T) holds
PolyRedRel (P,T) reduces (m1 *' p1) - (m2 *' p2), 0_ (n,L) ) holds
P is_Groebner_basis_wrt T
proofend;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p1, p2 be Polynomial of n,L;
func S-Poly (p1,p2,T) ->  Polynomial of n,L equals :: GROEB_2:def 4
((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));
coherence
 ((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)) is Polynomial of n,L ;
end;

:: deftheorem  defines S-Poly GROEB_2:def_4_:_
 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 p1, p2 being Polynomial of n,L holds S-Poly (p1,p2,T) = ((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));

Lm2:  for L being non empty add-cancelable right_complementable associative well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal
proofend;

Lm3:  for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring (n,L)) st f = p &amp; g = q holds
f - g = p - q
proofend;

theorem Th18: :: GROEB_2:18
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 P being Subset of (Polynom-Ring (n,L))
for p1, p2 being Polynomial of n,L st p1 in P &amp; p2 in P holds
S-Poly (p1,p2,T) in P -Ideal
proofend;

theorem Th19: :: GROEB_2:19
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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)
proofend;

:: exercise 5.47 (i), p. 211
theorem Th20: :: GROEB_2:20
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 Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) &amp; S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
proofend;

theorem :: GROEB_2:21
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 holds
( S-Poly (p1,p2,T) = 0_ (n,L) or HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T )
proofend;

:: exercise 5.47 (ii), p. 211
theorem :: GROEB_2:22
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 p1, p2 being non-zero Polynomial of n,L st HT (p2,T) divides HT (p1,T) holds
(HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T
proofend;

:: exercise 5.47 (iii), p. 211
theorem :: GROEB_2:23
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, h being Polynomial of n,L st g1 in G &amp; g2 in G &amp; h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
proofend;

:: theorem 5.48 (i) ==> (ii), p. 211
theorem :: GROEB_2:24
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 ( for g1, g2, h being Polynomial of n,L st g1 in G &amp; g2 in G &amp; h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ) holds
for g1, g2 being Polynomial of n,L st g1 in G &amp; g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
proofend;

:: theorem 5.48 (ii) ==> (iii), p. 211
theorem Th25: :: GROEB_2:25
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 being Polynomial of n,L st g1 in G &amp; g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds
G is_Groebner_basis_wrt T
proofend;

:: theorem 5.48 (iii) ==> (i), p. 211
definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let P be Subset of (Polynom-Ring (n,L));
func S-Poly (P,T) ->  Subset of (Polynom-Ring (n,L)) equals :: GROEB_2:def 5
 {  (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P &amp; p2 in P )  }  ;
coherence
  {  (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P &amp; p2 in P )  }  is Subset of (Polynom-Ring (n,L))
proofend;
end;

:: deftheorem  defines S-Poly GROEB_2:def_5_:_
 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)) holds S-Poly (P,T) =  {  (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P &amp; p2 in P )  }  ;

registration
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let P be finite Subset of (Polynom-Ring (n,L));
cluster S-Poly (P,T) ->  finite ;
coherence
 S-Poly (P,T) is finite
proofend;
end;

theorem :: GROEB_2:26
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 g being Polynomial of n,L st g in G holds
g is Monomial of n,L ) holds
G is_Groebner_basis_wrt T
proofend;

begin

theorem :: GROEB_2:27
for L being non empty multLoopStr
for P being non empty Subset of L
for A being LeftLinearCombination of P
for i being Element of NAT holds A | i is LeftLinearCombination of P
proofend;

theorem :: GROEB_2:28
for L being non empty multLoopStr
for P being non empty Subset of L
for A being LeftLinearCombination of P
for i being Element of NAT holds A /^ i is LeftLinearCombination of P
proofend;

theorem :: GROEB_2:29
for L being non empty multLoopStr
for P, Q being non empty Subset of L
for A being LeftLinearCombination of P st P c= Q holds
A is LeftLinearCombination of Q
proofend;

definition
let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let P be non empty Subset of (Polynom-Ring (n,L));
let A, B be LeftLinearCombination of P;
:: original:^
redefine funcA ^ B ->  LeftLinearCombination of P;
coherence
 A ^ B is LeftLinearCombination of P
proofend;
end;

definition
let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring (n,L));
let A be LeftLinearCombination of P;
predA is_MonomialRepresentation_of f means :Def6: :: GROEB_2:def 6
( Sum A = f &amp; ( for i being Element of NAT st i in dom A holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P &amp; A /. i = m *' p ) ) );
end;

:: deftheorem Def6 defines is_MonomialRepresentation_of GROEB_2:def_6_:_
 for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P holds
( A is_MonomialRepresentation_of f iff ( Sum A = f &amp; ( for i being Element of NAT st i in dom A holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P &amp; A /. i = m *' p ) ) ) );

theorem :: GROEB_2:30
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
Support f c= union  {  (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A &amp; A /. i = m *' p )  }
proofend;

theorem :: GROEB_2:31
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f &amp; B is_MonomialRepresentation_of g holds
A ^ B is_MonomialRepresentation_of f + g
proofend;

Lm4:  for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
for b being bag of n st ( for i being Element of NAT st i in dom A holds
for m being Monomial of n,L
for p being Polynomial of n,L st A . i = m *' p &amp; p in P holds
(m *' p) . b = 0. L ) holds
f . b = 0. L
proofend;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring (n,L));
let A be LeftLinearCombination of P;
let b be bag of n;
predA is_Standard_Representation_of f,P,b,T means :Def7: :: GROEB_2:def 7
( Sum A = f &amp; ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P &amp; A /. i = m *' p &amp; HT ((m *' p),T) <= b,T ) ) );
end;

:: deftheorem Def7 defines is_Standard_Representation_of GROEB_2:def_7_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P
for b being bag of n holds
( A is_Standard_Representation_of f,P,b,T iff ( Sum A = f &amp; ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P &amp; A /. i = m *' p &amp; HT ((m *' p),T) <= b,T ) ) ) );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring (n,L));
let A be LeftLinearCombination of P;
predA is_Standard_Representation_of f,P,T means :Def8: :: GROEB_2:def 8
A is_Standard_Representation_of f,P, HT (f,T),T;
end;

:: deftheorem Def8 defines is_Standard_Representation_of GROEB_2:def_8_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P holds
( A is_Standard_Representation_of f,P,T iff A is_Standard_Representation_of f,P, HT (f,T),T );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring (n,L));
let b be bag of n;
predf has_a_Standard_Representation_of P,b,T means :: GROEB_2:def 9
 ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T;
end;

:: deftheorem  defines has_a_Standard_Representation_of GROEB_2:def_9_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for b being bag of n holds
( f has_a_Standard_Representation_of P,b,T iff ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring (n,L));
predf has_a_Standard_Representation_of P,T means :Def10: :: GROEB_2:def 10
 ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T;
end;

:: deftheorem Def10 defines has_a_Standard_Representation_of GROEB_2:def_10_:_
 for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) holds
( f has_a_Standard_Representation_of P,T iff ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T );

theorem Th32: :: GROEB_2:32
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
proofend;

Lm5:  for n being Ordinal
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 f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 &amp; g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (Sum A) &amp; ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P &amp; A . i = m *' p &amp; HT ((m *' p),T) <= HT (f,T),T ) ) )
proofend;

theorem :: GROEB_2:33
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T &amp; B is_Standard_Representation_of g,P,b,T holds
A ^ B is_Standard_Representation_of f + g,P,b,T
proofend;

theorem :: GROEB_2:34
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P
for b being bag of n
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T &amp; B = A | i &amp; g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
proofend;

theorem :: GROEB_2:35
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P
for b being bag of n
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T &amp; B = A /^ i &amp; g = Sum (A | i) &amp; i <= len A holds
B is_Standard_Representation_of f - g,P,b,T
proofend;

theorem Th36: :: GROEB_2:36
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( i in dom A &amp; p in P &amp; A . i = m *' p &amp; HT (f,T) <= HT ((m *' p),T),T )
proofend;

theorem Th37: :: GROEB_2:37
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T holds
ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P &amp; i in dom A &amp; A /. i = m *' p &amp; HT (f,T) = HT ((m *' p),T) )
proofend;

theorem Th38: :: GROEB_2:38
for n being Ordinal
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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f has_a_Standard_Representation_of P,T
proofend;

:: lemma 5.60, p. 218
theorem Th39: :: GROEB_2:39
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 f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds
f is_top_reducible_wrt P,T
proofend;

:: lemma 5.61, p. 218
theorem :: GROEB_2:40
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 non empty Subset of (Polynom-Ring (n,L)) holds
( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds
f has_a_Standard_Representation_of G,T )
proofend;