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

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)

proof end;

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

proof end;

definition

let X be set ;
let b1, b2 be bag of X;
assume A1: b2 divides b1 ;

func b1 / b2 -> bag of X means :Def1: :: GROEB_2:def 1
b2 + it = b1;

existence
ex b₁ being bag of X st b2 + b₁ = b1 by A1, TERMORD:1;
uniqueness
for b₁, b₂ being bag of X st b2 + b₁ = b1 & b2 + b₂ = b1 holds
b₁ = b₂

proof end;

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 b₄ being bag of X holds
( b₄ = b1 / b2 iff b2 + b₄ = 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 object holds it . k = max ((b1 . k),(b2 . k));

existence
ex b₁ being bag of X st
for k being object holds b₁ . k = max ((b1 . k),(b2 . k))

proof end;

uniqueness
for b₁, b₂ being bag of X st ( for k being object holds b₁ . k = max ((b1 . k),(b2 . k)) ) & ( for k being object holds b₂ . k = max ((b1 . k),(b2 . k)) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, b1, b2 being bag of X st ( for k being object holds b₁ . k = max ((b1 . k),(b2 . k)) ) holds
for k being object holds b₁ . k = max ((b2 . k),(b1 . k)) ;
idempotence
for b1 being bag of X
for k being object holds b1 . k = max ((b1 . k),(b1 . k)) ;

end;

:: deftheorem Def2 defines lcm GROEB_2:def 2 :
for X being set
for b1, b2, b₄ being bag of X holds
( b₄ = lcm (b1,b2) iff for k being object holds b₄ . 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;

pred b1,b2 are_disjoint means :: GROEB_2:def 3
for i being object holds
( b1 . i = 0 or b2 . i = 0 );

end;

:: deftheorem 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 object 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) )

proof end;

:: 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

proof end;

:: 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 )

proof end;

theorem Th6: :: GROEB_2:6

for X being set
for b being bag of X holds b / b = EmptyBag X

proof end;

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 )

proof end;

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)

proof end;

:: 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)

proof end;

:: 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)

proof end;

:: 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 ) )

proof end;

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

proof end;

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;

cluster a * m -> monomial-like ;

coherence
a * m is monomial-like

proof end;

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;

cluster a * p -> non-zero ;

coherence
a * p is non-zero

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & 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

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal

proof end;

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 & g = q holds
f - g = p - q

proof end;

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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds
S-Poly (p1,p2,T) in P -Ideal

proof end;

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 well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)

proof end;

:: 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 well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )

proof end;

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 well-unital distributive add-associative right_zeroed associative commutative 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 )

proof end;

:: 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 well-unital distributive add-associative right_zeroed associative commutative 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

proof end;

:: 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)

proof end;

:: 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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & 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 & g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

proof end;

:: 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 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 holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds
G is_Groebner_basis_wrt T

proof end;

:: 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 well-unital distributive add-associative right_zeroed associative commutative 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 & p2 in P ) } ;

coherence
{ (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } is Subset of (Polynom-Ring (n,L))

proof end;

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 well-unital distributive add-associative right_zeroed associative commutative 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 & 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 well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let P be finite Subset of (Polynom-Ring (n,L));

cluster S-Poly (P,T) -> finite ;

coherence
S-Poly (P,T) is finite

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 func A ^ B -> LeftLinearCombination of P;
coherence
A ^ B is LeftLinearCombination of P

proof end;

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;

pred A is_MonomialRepresentation_of f means :: GROEB_2:def 6
( Sum A = f & ( 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 & A /. i = m *' p ) ) );

end;

:: deftheorem 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 & ( 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 & 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 & A /. i = m *' p ) }

proof end;

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 & B is_MonomialRepresentation_of g holds
A ^ B is_MonomialRepresentation_of f + g

proof end;

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 & p in P holds
(m *' p) . b = 0. L ) holds
f . b = 0. L

proof end;

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;

pred A is_Standard_Representation_of f,P,b,T means :: GROEB_2:def 7
( Sum A = f & ( 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 & A /. i = m *' p & HT ((m *' p),T) <= b,T ) ) );

end;

:: deftheorem 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 & ( 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 & A /. i = m *' p & 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;

pred A is_Standard_Representation_of f,P,T means :: GROEB_2:def 8
A is_Standard_Representation_of f,P, HT (f,T),T;

end;

:: deftheorem 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;

pred f 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));

pred f has_a_Standard_Representation_of P,T means :: GROEB_2:def 10
ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T;

end;

:: deftheorem 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

proof end;

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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & 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) & ( 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 & A . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) ) )

proof end;

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 & B is_Standard_Representation_of g,P,b,T holds
A ^ B is_Standard_Representation_of f + g,P,b,T

proof end;

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 & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T

proof end;

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 & B = A /^ i & g = Sum (A | i) & i <= len A holds
B is_Standard_Representation_of f - g,P,b,T

proof end;

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 & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

proof end;

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 & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),T) )

proof end;

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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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

proof end;

:: 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 well-unital distributive add-associative right_zeroed associative commutative 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

proof end;

:: 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 )

proof end;