:: GROEB_2 semantic presentation

theorem Th1: :: GROEB_2:1

canceled;

theorem Th2: :: GROEB_2:2

for b₁ being non empty LoopStr
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st b₄ <= b₃ holds
(b₂ | b₃) | b₄ = b₂ | b₄

proof end;

theorem Th3: :: GROEB_2:3

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of b₁
for b₃ being Nat st ( for b₄ being Nat st b₄ in dom b₂ & b₄ > b₃ holds
b₂ . b₄ = 0. b₁ ) holds
Sum b₂ = Sum (b₂ | b₃)

proof end;

theorem Th4: :: GROEB_2:4

for b₁ being non empty Abelian add-associative right_zeroed LoopStr
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat holds Sum (Swap b₂,b₃,b₄) = Sum b₂

proof end;

definition

let c₁ be set ;
let c₂, c₃ be bag of c₁;
assume E2: c₃ divides c₂ ;
func c₂ / c₃ -> bag of a₁ means :Def1: :: GROEB_2:def 1
a₃ + a₄ = a₂;
existence by E2, TERMORD:1;
uniqueness

proof end;

end;

:: deftheorem Def1 defines / GROEB_2:def 1 :

definition

let c₁ be set ;
let c₂, c₃ be bag of c₁;
func lcm c₂,c₃ -> bag of a₁ means :Def2: :: GROEB_2:def 2
for b₁ being set holds a₄ . b₁ = max (a₂ . b₁),(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;

end;

:: deftheorem Def2 defines lcm GROEB_2:def 2 :

notation

let c₁ be set ;
let c₂, c₃ be bag of c₁;
synonym c₂ lcm c₃ for lcm c₂,c₃;

end;

definition

let c₁ be set ;
let c₂, c₃ be bag of c₁;
pred c₂,c₃ are_disjoint means :Def3: :: GROEB_2:def 3
for b₁ being set holds
( a₂ . b₁ = 0 or a₃ . b₁ = 0 );

end;

:: deftheorem Def3 defines are_disjoint GROEB_2:def 3 :

notation

let c₁ be set ;
let c₂, c₃ be bag of c₁;
antonym c₂,c₃ are_non_disjoint for c₂,c₃ are_disjoint ;

end;

theorem Th5: :: GROEB_2:5

canceled;

theorem Th6: :: GROEB_2:6

canceled;

theorem Th7: :: GROEB_2:7

for b₁ being set
for b₂, b₃ being bag of b₁ holds
( b₂ divides lcm b₂,b₃ & b₃ divides lcm b₂,b₃ )

proof end;

theorem Th8: :: GROEB_2:8

for b₁ being set
for b₂, b₃, b₄ being bag of b₁ st b₂ divides b₄ & b₃ divides b₄ holds
lcm b₂,b₃ divides b₄

proof end;

theorem Th9: :: GROEB_2:9

for b₁ being set
for b₂, b₃ being bag of b₁ holds
( b₂,b₃ are_disjoint iff lcm b₂,b₃ = b₂ + b₃ )

proof end;

theorem Th10: :: GROEB_2:10

for b₁ being set
for b₂ being bag of b₁ holds b₂ / b₂ = EmptyBag b₁

proof end;

theorem Th11: :: GROEB_2:11

for b₁ being set
for b₂, b₃ being bag of b₁ holds
( b₃ divides b₂ iff lcm b₂,b₃ = b₂ )

proof end;

theorem Th12: :: GROEB_2:12

for b₁ being set
for b₂, b₃, b₄ being bag of b₁ st b₂ divides lcm b₃,b₄ holds
lcm b₃,b₂ divides lcm b₃,b₄

proof end;

theorem Th13: :: GROEB_2:13

for b₁ being set
for b₂, b₃, b₄ being bag of b₁ st lcm b₃,b₂ divides lcm b₃,b₄ holds
lcm b₂,b₄ divides lcm b₃,b₄

proof end;

theorem Th14: :: GROEB_2:14

for b₁ being set
for b₂, b₃, b₄ being bag of b₁ st lcm b₂,b₄ divides lcm b₃,b₄ holds
b₂ divides lcm b₃,b₄

proof end;

theorem Th15: :: GROEB_2:15

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty Subset of (Bags b₁) ex b₄ being bag of b₁ st
( b₄ in b₃ & ( for b₅ being bag of b₁ st b₅ in b₃ holds
b₄ <= b₅,b₂ ) )

proof end;

registration

let c₁ be add-associative right_zeroed right_complementable non trivial LoopStr ;
let c₂ be non-zero Element of c₁;
cluster - a₂ -> non-zero ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non empty right_zeroed distributive add-cancelable left_zeroed doubleLoopStr ;
let c₃ be Monomial of c₁,c₂;
let c₄ be Element of c₂;
cluster a₄ * a₃ -> monomial-like ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be right_zeroed distributive add-cancelable left_zeroed non trivial domRing-like doubleLoopStr ;
let c₃ be non-zero Polynomial of c₁,c₂;
let c₄ be non-zero Element of c₂;
cluster a₄ * a₃ -> non-zero ;
coherence

proof end;

end;

theorem Th16: :: GROEB_2:16

for b₁ being Ordinal
for b₂ being non empty right_zeroed right-distributive doubleLoopStr
for b₃, b₄ being Series of b₁,b₂
for b₅ being bag of b₁ holds b₅ *' (b₃ + b₄) = (b₅ *' b₃) + (b₅ *' b₄)

proof end;

theorem Th17: :: GROEB_2:17

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr
for b₃ being Series of b₁,b₂
for b₄ being bag of b₁ holds b₄ *' (- b₃) = - (b₄ *' b₃)

proof end;

theorem Th18: :: GROEB_2:18

for b₁ being Ordinal
for b₂ being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₃ being Series of b₁,b₂
for b₄ being bag of b₁
for b₅ being Element of b₂ holds b₄ *' (b₅ * b₃) = b₅ * (b₄ *' b₃)

proof end;

theorem Th19: :: GROEB_2:19

for b₁ being Ordinal
for b₂ being non empty right-distributive doubleLoopStr
for b₃, b₄ being Series of b₁,b₂
for b₅ being Element of b₂ holds b₅ * (b₃ + b₄) = (b₅ * b₃) + (b₅ * b₄)

proof end;

theorem Th20: :: GROEB_2:20

for b₁ being set
for b₂ being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b₃ being Element of b₂ holds - (b₃ | b₁,b₂) = (- b₃) | b₁,b₂

proof end;

Lemma14: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being set
for b₆ being Subset of (Polynom-Ring b₁,b₃) st PolyRedRel b₆,b₂ reduces b₄,b₅ holds
b₅ is Polynomial of b₁,b₃

proof end;

theorem Th21: :: GROEB_2:21

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st not 0_ b₁,b₃ in b₄ & ( for b₅, b₆ being Polynomial of b₁,b₃ st b₅ <> b₆ & b₅ in b₄ & b₆ in b₄ holds
for b₇, b₈ being Monomial of b₁,b₃ st HM (b₇ *' b₅),b₂ = HM (b₈ *' b₆),b₂ holds
PolyRedRel b₄,b₂ reduces (b₇ *' b₅) - (b₈ *' b₆), 0_ b₁,b₃ ) holds
b₄ is_Groebner_basis_wrt b₂

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄, c₅ be Polynomial of c₁,c₃;
func S-Poly c₄,c₅,c₂ -> Polynomial of a₁,a₃ equals :: GROEB_2:def 4
((HC a₅,a₂) * (((lcm (HT a₄,a₂),(HT a₅,a₂)) / (HT a₄,a₂)) *' a₄)) - ((HC a₄,a₂) * (((lcm (HT a₄,a₂),(HT a₅,a₂)) / (HT a₅,a₂)) *' a₅));
coherence ;

end;

:: deftheorem Def4 defines S-Poly GROEB_2:def 4 :

Lemma16: for b₁ being non empty unital associative add-associative right_zeroed right_complementable distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
b₃ in b₂ -Ideal

proof end;

Lemma17: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃
for b₆, b₇ being Element of (Polynom-Ring b₁,b₃) st b₆ = b₄ & b₇ = b₅ holds
b₆ - b₇ = b₄ - b₅

proof end;

theorem Th22: :: GROEB_2:22

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ holds
S-Poly b₅,b₆,b₂ in b₄ -Ideal

proof end;

theorem Th23: :: GROEB_2:23

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃ st b₄ = b₅ holds
S-Poly b₄,b₅,b₂ = 0_ b₁,b₃ by POLYNOM1:83;

theorem Th24: :: GROEB_2:24

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄, b₅ being Monomial of b₁,b₃ holds S-Poly b₄,b₅,b₂ = 0_ b₁,b₃

proof end;

theorem Th25: :: GROEB_2:25

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Polynomial of b₁,b₃ holds
( S-Poly b₄,(0_ b₁,b₃),b₂ = 0_ b₁,b₃ & S-Poly (0_ b₁,b₃),b₄,b₂ = 0_ b₁,b₃ )

proof end;

theorem Th26: :: GROEB_2:26

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃ holds
( S-Poly b₄,b₅,b₂ = 0_ b₁,b₃ or HT (S-Poly b₄,b₅,b₂),b₂ < lcm (HT b₄,b₂),(HT b₅,b₂),b₂ )

proof end;

theorem Th27: :: GROEB_2:27

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ st HT b₅,b₂ divides HT b₄,b₂ holds
(HC b₅,b₂) * b₄ top_reduces_to S-Poly b₄,b₅,b₂,b₅,b₂

proof end;

theorem Th28: :: GROEB_2:28

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st b₄ is_Groebner_basis_wrt b₂ holds
for b₅, b₆, b₇ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ & b₇ is_a_normal_form_of S-Poly b₅,b₆,b₂, PolyRedRel b₄,b₂ holds
b₇ = 0_ b₁,b₃

proof end;

theorem Th29: :: GROEB_2:29

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st ( for b₅, b₆, b₇ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ & b₇ is_a_normal_form_of S-Poly b₅,b₆,b₂, PolyRedRel b₄,b₂ holds
b₇ = 0_ b₁,b₃ ) holds
for b₅, b₆ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ holds
PolyRedRel b₄,b₂ reduces S-Poly b₅,b₆,b₂, 0_ b₁,b₃

proof end;

theorem Th30: :: GROEB_2:30

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st not 0_ b₁,b₃ in b₄ & ( for b₅, b₆ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ holds
PolyRedRel b₄,b₂ reduces S-Poly b₅,b₆,b₂, 0_ b₁,b₃ ) holds
b₄ is_Groebner_basis_wrt b₂

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be Subset of (Polynom-Ring c₁,c₃);
func S-Poly c₄,c₂ -> Subset of (Polynom-Ring a₁,a₃) equals :: GROEB_2:def 5
{ (S-Poly b₁,b₂,a₂) where B is Polynomial of a₁,a₃, B is Polynomial of a₁,a₃ : ( b₁ in a₄ & b₂ in a₄ ) } ;
coherence

proof end;

end;

:: deftheorem Def5 defines S-Poly GROEB_2:def 5 :

registration

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be finite Subset of (Polynom-Ring c₁,c₃);
cluster S-Poly a₄,a₂ -> finite ;
coherence

proof end;

end;

theorem Th31: :: GROEB_2:31

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st not 0_ b₁,b₃ in b₄ & ( for b₅ being Polynomial of b₁,b₃ st b₅ in b₄ holds
b₅ is Monomial of b₁,b₃ ) holds
b₄ is_Groebner_basis_wrt b₂

proof end;

theorem Th32: :: GROEB_2:32

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LeftLinearCombination of b₂
for b₄ being Nat holds b₃ | b₄ is LeftLinearCombination of b₂

proof end;

theorem Th33: :: GROEB_2:33

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LeftLinearCombination of b₂
for b₄ being Nat holds b₃ /^ b₄ is LeftLinearCombination of b₂

proof end;

theorem Th34: :: GROEB_2:34

for b₁ being non empty multLoopStr
for b₂, b₃ being non empty Subset of b₁
for b₄ being LeftLinearCombination of b₂ st b₂ c= b₃ holds
b₄ is LeftLinearCombination of b₃

proof end;

definition

let c₁ be Ordinal;
let c₂ be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let c₃ be non empty Subset of (Polynom-Ring c₁,c₂);
let c₄, c₅ be LeftLinearCombination of c₃;
redefine func ^ as c₄ ^ c₅ -> LeftLinearCombination of a₃;
coherence

proof end;

end;

definition

let c₁ be Ordinal;
let c₂ be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let c₃ be Polynomial of c₁,c₂;
let c₄ be non empty Subset of (Polynom-Ring c₁,c₂);
let c₅ be LeftLinearCombination of c₄;
pred c₅ is_MonomialRepresentation_of c₃ means :Def6: :: GROEB_2:def 6
( Sum a₅ = a₃ & ( for b₁ being Nat st b₁ in dom a₅ holds
ex b₂ being Monomial of a₁,a₂ex b₃ being Polynomial of a₁,a₂ st
( b₃ in a₄ & a₅ /. b₁ = b₂ *' b₃ ) ) );

end;

:: deftheorem Def6 defines is_MonomialRepresentation_of GROEB_2:def 6 :

theorem Th35: :: GROEB_2:35

for b₁ being Ordinal
for b₂ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being non empty Subset of (Polynom-Ring b₁,b₂)
for b₅ being LeftLinearCombination of b₄ st b₅ is_MonomialRepresentation_of b₃ holds
Support b₃ c= union { (Support (b₆ *' b₇)) where B is Monomial of b₁,b₂, B is Polynomial of b₁,b₂ : ex b₁ being Nat st
( b₈ in dom b₅ & b₅ /. b₈ = b₆ *' b₇ ) }

proof end;

theorem Th36: :: GROEB_2:36

for b₁ being Ordinal
for b₂ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₃, b₄ being Polynomial of b₁,b₂
for b₅ being non empty Subset of (Polynom-Ring b₁,b₂)
for b₆, b₇ being LeftLinearCombination of b₅ st b₆ is_MonomialRepresentation_of b₃ & b₇ is_MonomialRepresentation_of b₄ holds
b₆ ^ b₇ is_MonomialRepresentation_of b₃ + b₄

proof end;

Lemma23: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₆ being LeftLinearCombination of b₅ st b₆ is_MonomialRepresentation_of b₄ holds
for b₇ being bag of b₁ st ( for b₈ being Nat st b₈ in dom b₆ holds
for b₉ being Monomial of b₁,b₃
for b₁₀ being Polynomial of b₁,b₃ st b₆ . b₈ = b₉ *' b₁₀ & b₁₀ in b₅ holds
(b₉ *' b₁₀) . b₇ = 0. b₃ ) holds
b₄ . b₇ = 0. b₃

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be non empty Subset of (Polynom-Ring c₁,c₃);
let c₆ be LeftLinearCombination of c₅;
let c₇ be bag of c₁;
pred c₆ is_Standard_Representation_of c₄,c₅,c₇,c₂ means :Def7: :: GROEB_2:def 7
( Sum a₆ = a₄ & ( for b₁ being Nat st b₁ in dom a₆ holds
ex b₂ being non-zero Monomial of a₁,a₃ex b₃ being non-zero Polynomial of a₁,a₃ st
( b₃ in a₅ & a₆ /. b₁ = b₂ *' b₃ & HT (b₂ *' b₃),a₂ <= a₇,a₂ ) ) );

end;

:: deftheorem Def7 defines is_Standard_Representation_of GROEB_2:def 7 :

definition

end;

:: deftheorem Def8 defines is_Standard_Representation_of GROEB_2:def 8 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be non empty Subset of (Polynom-Ring c₁,c₃);
let c₆ be bag of c₁;
pred c₄ has_a_Standard_Representation_of c₅,c₆,c₂ means :: GROEB_2:def 9
ex b₁ being LeftLinearCombination of a₅ st b₁ is_Standard_Representation_of a₄,a₅,a₆,a₂;

end;

:: deftheorem Def9 defines has_a_Standard_Representation_of GROEB_2:def 9 :

definition

end;

:: deftheorem Def10 defines has_a_Standard_Representation_of GROEB_2:def 10 :

theorem Th37: :: GROEB_2:37

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₆ being LeftLinearCombination of b₅
for b₇ being bag of b₁ st b₆ is_Standard_Representation_of b₄,b₅,b₇,b₂ holds
b₆ is_MonomialRepresentation_of b₄

proof end;

Lemma28: for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃
for b₆, b₇ being Element of (Polynom-Ring b₁,b₃) st b₄ = b₆ & b₅ = b₇ holds
for b₈ being non empty Subset of (Polynom-Ring b₁,b₃) st PolyRedRel b₈,b₂ reduces b₄,b₅ holds
ex b₉ being LeftLinearCombination of b₈ st
( b₆ = b₇ + (Sum b₉) & ( for b₁₀ being Nat st b₁₀ in dom b₉ holds
ex b₁₁ being non-zero Monomial of b₁,b₃ex b₁₂ being non-zero Polynomial of b₁,b₃ st
( b₁₂ in b₈ & b₉ . b₁₀ = b₁₁ *' b₁₂ & HT (b₁₁ *' b₁₂),b₂ <= HT b₄,b₂,b₂ ) ) )

proof end;

theorem Th38: :: GROEB_2:38

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃
for b₆ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₇, b₈ being LeftLinearCombination of b₆
for b₉ being bag of b₁ st b₇ is_Standard_Representation_of b₄,b₆,b₉,b₂ & b₈ is_Standard_Representation_of b₅,b₆,b₉,b₂ holds
b₇ ^ b₈ is_Standard_Representation_of b₄ + b₅,b₆,b₉,b₂

proof end;

theorem Th39: :: GROEB_2:39

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃
for b₆ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₇, b₈ being LeftLinearCombination of b₆
for b₉ being bag of b₁
for b₁₀ being Nat st b₇ is_Standard_Representation_of b₄,b₆,b₉,b₂ & b₈ = b₇ | b₁₀ & b₅ = Sum (b₇ /^ b₁₀) holds
b₈ is_Standard_Representation_of b₄ - b₅,b₆,b₉,b₂

proof end;

theorem Th40: :: GROEB_2:40

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃
for b₆ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₇, b₈ being LeftLinearCombination of b₆
for b₉ being bag of b₁
for b₁₀ being Nat st b₇ is_Standard_Representation_of b₄,b₆,b₉,b₂ & b₈ = b₇ /^ b₁₀ & b₅ = Sum (b₇ | b₁₀) & b₁₀ <= len b₇ holds
b₈ is_Standard_Representation_of b₄ - b₅,b₆,b₉,b₂

proof end;

theorem Th41: :: GROEB_2:41

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄ being non-zero Polynomial of b₁,b₃
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₆ being LeftLinearCombination of b₅ st b₆ is_MonomialRepresentation_of b₄ holds
ex b₇ being Natex b₈ being non-zero Monomial of b₁,b₃ex b₉ being non-zero Polynomial of b₁,b₃ st
( b₇ in dom b₆ & b₉ in b₅ & b₆ . b₇ = b₈ *' b₉ & HT b₄,b₂ <= HT (b₈ *' b₉),b₂,b₂ )

proof end;

theorem Th42: :: GROEB_2:42

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄ being non-zero Polynomial of b₁,b₃
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₆ being LeftLinearCombination of b₅ st b₆ is_Standard_Representation_of b₄,b₅,b₂ holds
ex b₇ being Natex b₈ being non-zero Monomial of b₁,b₃ex b₉ being non-zero Polynomial of b₁,b₃ st
( b₉ in b₅ & b₇ in dom b₆ & b₆ /. b₇ = b₈ *' b₉ & HT b₄,b₂ = HT (b₈ *' b₉),b₂ )

proof end;

theorem Th43: :: GROEB_2:43

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃) st PolyRedRel b₅,b₂ reduces b₄, 0_ b₁,b₃ holds
b₄ has_a_Standard_Representation_of b₅,b₂

proof end;

theorem Th44: :: GROEB_2:44

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being non-zero Polynomial of b₁,b₃
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃) st b₄ has_a_Standard_Representation_of b₅,b₂ holds
b₄ is_top_reducible_wrt b₅,b₂

proof end;

theorem Th45: :: GROEB_2:45

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being non empty Subset of (Polynom-Ring b₁,b₃) holds
( b₄ is_Groebner_basis_wrt b₂ iff for b₅ being non-zero Polynomial of b₁,b₃ st b₅ in b₄ -Ideal holds
b₅ has_a_Standard_Representation_of b₄,b₂ )

proof end;