:: GROEB_1 semantic presentation

definition

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

proof end;

end;

theorem Th1: :: GROEB_1:1

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₅, b₆ being Polynomial of b₁,b₃ st b₄ reduces_to b₆,b₅,b₂ holds
ex b₇ being Monomial of b₁,b₃ st b₆ = b₄ - (b₇ *' b₅)

proof end;

theorem Th2: :: GROEB_1:2

proof end;

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

Lemma3: for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative 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
b₆ - b₇ = b₄ - b₅

proof end;

Lemma4: 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 b₄ is_irreducible_wrt 0_ b₁,b₃,b₂

proof end;

theorem Th3: :: GROEB_1:3

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₃
for b₆, b₇ being Subset of (Polynom-Ring b₁,b₃) st b₆ c= b₇ & b₄ reduces_to b₅,b₆,b₂ holds
b₄ reduces_to b₅,b₇,b₂

proof end;

theorem Th4: :: GROEB_1:4

proof end;

theorem Th5: :: GROEB_1:5

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b₃ being Polynomial of b₁,b₂ holds Support (- b₃) = Support b₃

proof end;

theorem Th6: :: GROEB_1:6

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₃ holds HT (- b₄),b₂ = HT b₄,b₂

proof end;

theorem Th7: :: GROEB_1:7

for b₁ being Ordinal
for b₂ being connected admissible 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₃ holds HT (b₄ - b₅),b₂ <= max (HT b₄,b₂),(HT b₅,b₂),b₂,b₂

proof end;

theorem Th8: :: GROEB_1:8

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₃ st Support b₅ c= Support b₄ holds
b₅ <= b₄,b₂

proof end;

theorem Th9: :: GROEB_1:9

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ st b₄ is_reducible_wrt b₅,b₂ holds
HT b₅,b₂ <= HT b₄,b₂,b₂

proof end;

theorem Th10: :: GROEB_1:10

for b₁ being Nat
for b₂ being connected admissible 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 Polynomial of b₁,b₃ holds PolyRedRel {b₄},b₂ is locally-confluent

proof end;

theorem Th11: :: GROEB_1:11

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 Subset of (Polynom-Ring c₁,c₃);
func HT c₄,c₂ -> Subset of (Bags a₁) equals :: GROEB_1:def 1
{ (HT b₁,a₂) where B is Polynomial of a₁,a₃ : ( b₁ in a₄ & b₁ <> 0_ a₁,a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines HT GROEB_1:def 1 :

definition

let c₁ be Ordinal;
let c₂ be Subset of (Bags c₁);
func multiples c₂ -> Subset of (Bags a₁) equals :: GROEB_1:def 2
{ b₁ where B is Element of Bags a₁ : ex b₁ being bag of a₁ st
( b₂ in a₂ & b₂ divides b₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines multiples GROEB_1:def 2 :

theorem Th12: :: GROEB_1:12

proof end;

theorem Th13: :: GROEB_1:13

proof end;

theorem Th14: :: GROEB_1:14

proof end;

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

Lemma17: 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₃
for b₆ being Subset of (Polynom-Ring b₁,b₃) st PolyRedRel b₆,b₂ reduces b₄,b₅ & b₅ <> b₄ holds
ex b₇ being Polynomial of b₁,b₃ st
( b₄ reduces_to b₇,b₆,b₂ & PolyRedRel b₆,b₂ reduces b₇,b₅ )

proof end;

theorem Th15: :: GROEB_1:15

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₃) st PolyRedRel b₄,b₂ is with_Church-Rosser_property holds
for b₅ being Polynomial of b₁,b₃ st b₅ in b₄ -Ideal holds
PolyRedRel b₄,b₂ reduces b₅, 0_ b₁,b₃

proof end;

theorem Th16: :: GROEB_1:16

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 Subset of (Polynom-Ring b₁,b₃) st ( for b₅ being Polynomial of b₁,b₃ st b₅ in b₄ -Ideal holds
PolyRedRel b₄,b₂ reduces b₅, 0_ b₁,b₃ ) holds
for b₅ being non-zero Polynomial of b₁,b₃ st b₅ in b₄ -Ideal holds
b₅ is_reducible_wrt b₄,b₂

proof end;

theorem Th17: :: GROEB_1:17

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₅ being non-zero Polynomial of b₁,b₃ st b₅ in b₄ -Ideal holds
b₅ is_reducible_wrt b₄,b₂ ) holds
for b₅ being non-zero Polynomial of b₁,b₃ st b₅ in b₄ -Ideal holds
b₅ is_top_reducible_wrt b₄,b₂

proof end;

theorem Th18: :: GROEB_1:18

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 Subset of (Polynom-Ring b₁,b₃) st ( for b₅ being non-zero Polynomial of b₁,b₃ st b₅ in b₄ -Ideal holds
b₅ is_top_reducible_wrt b₄,b₂ ) holds
for b₅ being bag of b₁ st b₅ in HT (b₄ -Ideal ),b₂ holds
ex b₆ being bag of b₁ st
( b₆ in HT b₄,b₂ & b₆ divides b₅ )

proof end;

theorem Th19: :: GROEB_1:19

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 Subset of (Polynom-Ring b₁,b₃) st ( for b₅ being bag of b₁ st b₅ in HT (b₄ -Ideal ),b₂ holds
ex b₆ being bag of b₁ st
( b₆ in HT b₄,b₂ & b₆ divides b₅ ) ) holds
HT (b₄ -Ideal ),b₂ c= multiples (HT b₄,b₂)

proof end;

theorem Th20: :: GROEB_1:20

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 HT (b₄ -Ideal ),b₂ c= multiples (HT b₄,b₂) holds
PolyRedRel b₄,b₂ is locally-confluent

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₃);
pred c₄ is_Groebner_basis_wrt c₂ means :Def3: :: GROEB_1:def 3
PolyRedRel a₄,a₂ is locally-confluent;

end;

:: deftheorem Def3 defines is_Groebner_basis_wrt GROEB_1:def 3 :

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 Subset of (Polynom-Ring c₁,c₃);
pred c₄ is_Groebner_basis_of c₅,c₂ means :Def4: :: GROEB_1:def 4
( a₄ -Ideal = a₅ & PolyRedRel a₄,a₂ is locally-confluent );

end;

:: deftheorem Def4 defines is_Groebner_basis_of GROEB_1:def 4 :

Lemma24: 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 Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being set st b₅ <> b₆ & PolyRedRel b₄,b₂ reduces b₅,b₆ holds
( b₅ is Polynomial of b₁,b₃ & b₆ is Polynomial of b₁,b₃ )

proof end;

theorem Th21: :: GROEB_1:21

proof end;

theorem Th22: :: GROEB_1:22

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₄, b₅ being Element of (Polynom-Ring b₁,b₃)
for b₆ being non empty Subset of (Polynom-Ring b₁,b₃) st b₆ is_Groebner_basis_wrt b₂ holds
( b₄,b₅ are_congruent_mod b₆ -Ideal iff nf b₄,(PolyRedRel b₆,b₂) = nf b₅,(PolyRedRel b₆,b₂) )

proof end;

theorem Th23: :: GROEB_1:23

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 Polynomial of b₁,b₃
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃) st b₅ is_Groebner_basis_wrt b₂ holds
( b₄ in b₅ -Ideal iff PolyRedRel b₅,b₂ reduces b₄, 0_ b₁,b₃ )

proof end;

Lemma25: 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 LeftIdeal of (Polynom-Ring b₁,b₃)
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃) st b₅ c= b₄ & ( for b₆ being Polynomial of b₁,b₃ st b₆ in b₄ holds
PolyRedRel b₅,b₂ reduces b₆, 0_ b₁,b₃ ) holds
b₅ -Ideal = b₄

proof end;

theorem Th24: :: GROEB_1:24

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₃)
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃) st b₅ is_Groebner_basis_of b₄,b₂ holds
for b₆ being Polynomial of b₁,b₃ st b₆ in b₄ holds
PolyRedRel b₅,b₂ reduces b₆, 0_ b₁,b₃

proof end;

theorem Th25: :: GROEB_1: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₄, b₅ being Subset of (Polynom-Ring b₁,b₃) st ( for b₆ being Polynomial of b₁,b₃ st b₆ in b₅ holds
PolyRedRel b₄,b₂ reduces b₆, 0_ b₁,b₃ ) holds
for b₆ being non-zero Polynomial of b₁,b₃ st b₆ in b₅ holds
b₆ is_reducible_wrt b₄,b₂

proof end;

theorem Th26: :: GROEB_1:26

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 add-closed left-ideal Subset of (Polynom-Ring b₁,b₃)
for b₅ being Subset of (Polynom-Ring b₁,b₃) st b₅ c= b₄ & ( for b₆ being non-zero Polynomial of b₁,b₃ st b₆ in b₄ holds
b₆ is_reducible_wrt b₅,b₂ ) holds
for b₆ being non-zero Polynomial of b₁,b₃ st b₆ in b₄ holds
b₆ is_top_reducible_wrt b₅,b₂

proof end;

theorem Th27: :: GROEB_1: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 Subset of (Polynom-Ring b₁,b₃) st ( for b₆ being non-zero Polynomial of b₁,b₃ st b₆ in b₅ holds
b₆ is_top_reducible_wrt b₄,b₂ ) holds
for b₆ being bag of b₁ st b₆ in HT b₅,b₂ holds
ex b₇ being bag of b₁ st
( b₇ in HT b₄,b₂ & b₇ divides b₆ )

proof end;

theorem Th28: :: GROEB_1:28

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 Subset of (Polynom-Ring b₁,b₃) st ( for b₆ being bag of b₁ st b₆ in HT b₅,b₂ holds
ex b₇ being bag of b₁ st
( b₇ in HT b₄,b₂ & b₇ divides b₆ ) ) holds
HT b₅,b₂ c= multiples (HT b₄,b₂)

proof end;

theorem Th29: :: GROEB_1: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 non empty add-closed left-ideal Subset of (Polynom-Ring b₁,b₃)
for b₅ being non empty Subset of (Polynom-Ring b₁,b₃) st b₅ c= b₄ & HT b₄,b₂ c= multiples (HT b₅,b₂) holds
b₅ is_Groebner_basis_of b₄,b₂

proof end;

theorem Th30: :: GROEB_1:30

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr holds {(0_ b₁,b₃)} is_Groebner_basis_of {(0_ b₁,b₃)},b₂

proof end;

theorem Th31: :: GROEB_1:31

proof end;

theorem Th32: :: GROEB_1:32

for b₁ being connected admissible TermOrder of {}
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 add-closed left-ideal Subset of (Polynom-Ring {} ,b₂)
for b₄ being non empty Subset of (Polynom-Ring {} ,b₂) st b₄ c= b₃ & b₄ <> {(0_ {} ,b₂)} holds
b₄ is_Groebner_basis_of b₃,b₁

proof end;

theorem Th33: :: GROEB_1:33

for b₁ being non empty Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr holds
not for b₄ being Subset of (Polynom-Ring b₁,b₃) holds b₄ is_Groebner_basis_wrt b₂

proof end;

Lemma33: for b₁ being Ordinal
for b₂, b₃, b₄ being bag of b₁ st b₂ divides b₃ & b₃ divides b₄ holds
b₂ divides b₄

proof end;

definition

let c₁ be Ordinal;
func DivOrder c₁ -> Order of Bags a₁ means :Def5: :: GROEB_1:def 5
for b₁, b₂ being bag of a₁ holds
( [b₁,b₂] in a₂ iff b₁ divides b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :

registration

let c₁ be Nat;
cluster RelStr(# (Bags a₁),(DivOrder a₁) #) -> Dickson ;
coherence

proof end;

end;

theorem Th34: :: GROEB_1:34

for b₁ being Nat
for b₂ being Subset of RelStr(# (Bags b₁),(DivOrder b₁) #) ex b₃ being finite Subset of (Bags b₁) st b₃ is_Dickson-basis_of b₂, RelStr(# (Bags b₁),(DivOrder b₁) #)

proof end;

theorem Th35: :: GROEB_1:35

proof end;

Lemma37: for b₁ being non empty unital associative add-associative right_zeroed right_complementable distributive left_zeroed doubleLoopStr
for b₂, b₃ being non empty Subset of b₁ st 0. b₁ in b₂ & b₃ = b₂ \ {(0. b₁)} holds
for b₄ being LinearCombination of b₂
for b₅ being set st b₅ = Sum b₄ holds
ex b₆ being LinearCombination of b₃ st b₅ = Sum b₆

proof end;

theorem Th36: :: GROEB_1:36

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 add-closed left-ideal Subset of (Polynom-Ring b₁,b₃) st b₄ <> {(0_ b₁,b₃)} holds
ex b₅ being finite Subset of (Polynom-Ring b₁,b₃) st
( b₅ is_Groebner_basis_of b₄,b₂ & not 0_ b₁,b₃ in b₅ )

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty multLoopStr_0 ;
let c₄ be Polynomial of c₁,c₃;
pred c₄ is_monic_wrt c₂ means :Def6: :: GROEB_1:def 6
HC a₄,a₂ = 1. a₃;

end;

:: deftheorem Def6 defines is_monic_wrt GROEB_1:def 6 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be Subset of (Polynom-Ring c₁,c₃);
pred c₄ is_reduced_wrt c₂ means :Def7: :: GROEB_1:def 7
for b₁ being Polynomial of a₁,a₃ st b₁ in a₄ holds
( b₁ is_monic_wrt a₂ & b₁ is_irreducible_wrt a₄ \ {b₁},a₂ );

end;

:: deftheorem Def7 defines is_reduced_wrt GROEB_1:def 7 :

notation

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be Subset of (Polynom-Ring c₁,c₃);
synonym c₄ is_autoreduced_wrt c₂ for c₄ is_reduced_wrt c₂;

end;

theorem Th37: :: GROEB_1:37

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 add-closed left-ideal Subset of (Polynom-Ring b₁,b₃)
for b₅ being Monomial of b₁,b₃
for b₆, b₇ being Polynomial of b₁,b₃ st b₆ in b₄ & b₇ in b₄ & HM b₆,b₂ = b₅ & HM b₇,b₂ = b₅ & ( for b₈ being Polynomial of b₁,b₃ holds
( not b₈ in b₄ or not b₈ < b₆,b₂ or not HM b₈,b₂ = b₅ ) ) & ( for b₈ being Polynomial of b₁,b₃ holds
( not b₈ in b₄ or not b₈ < b₇,b₂ or not HM b₈,b₂ = b₅ ) ) holds
b₆ = b₇

proof end;

Lemma41: 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 Polynomial of b₁,b₃
for b₅ being non empty add-closed left-ideal Subset of (Polynom-Ring b₁,b₃) st b₄ in b₅ & b₄ <> 0_ b₁,b₃ holds
ex b₆ being Polynomial of b₁,b₃ st
( b₆ in b₅ & HM b₆,b₂ = Monom (1. b₃),(HT b₄,b₂) & b₆ <> 0_ b₁,b₃ )

proof end;

theorem Th38: :: GROEB_1:38

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 add-closed left-ideal Subset of (Polynom-Ring b₁,b₃)
for b₅ being Subset of (Polynom-Ring b₁,b₃)
for b₆ being Polynomial of b₁,b₃
for b₇ being non-zero Polynomial of b₁,b₃ st b₆ in b₅ & b₇ in b₅ & b₆ <> b₇ & HT b₇,b₂ divides HT b₆,b₂ & b₅ is_Groebner_basis_of b₄,b₂ holds
b₅ \ {b₆} is_Groebner_basis_of b₄,b₂

proof end;

theorem Th39: :: GROEB_1:39

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 add-closed left-ideal Subset of (Polynom-Ring b₁,b₃) st b₄ <> {(0_ b₁,b₃)} holds
ex b₅ being finite Subset of (Polynom-Ring b₁,b₃) st
( b₅ is_Groebner_basis_of b₄,b₂ & b₅ is_reduced_wrt b₂ )

proof end;

theorem Th40: :: GROEB_1:40

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 add-closed left-ideal Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being non empty finite Subset of (Polynom-Ring b₁,b₃) st b₅ is_Groebner_basis_of b₄,b₂ & b₅ is_reduced_wrt b₂ & b₆ is_Groebner_basis_of b₄,b₂ & b₆ is_reduced_wrt b₂ holds
b₅ = b₆

proof end;