:: GROEB_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

theorem Th1: :: GROEB_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st g = f - (m *' p)
proof end;

theorem :: GROEB_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st
( g = f - (m *' p) & not HT (m *' p),T in Support g & HT (m *' p),T <= HT f,T,T )
proof end;

Lm1: for L being non empty unital associative add-associative right_zeroed right_complementable distributive add-cancelable 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;

Lm2: for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated 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;

Lm3: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f being Polynomial of n,L holds f is_irreducible_wrt 0_ n,L,T
proof end;

theorem Th3: :: GROEB_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f, g being Polynomial of n,L
for P, Q being Subset of (Polynom-Ring n,L) st P c= Q & f reduces_to g,P,T holds
f reduces_to g,Q,T
proof end;

theorem Th4: :: GROEB_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P, Q being Subset of (Polynom-Ring n,L) st P c= Q holds
PolyRedRel P,T c= PolyRedRel Q,T
proof end;

theorem Th5: :: GROEB_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable doubleLoopStr
for p being Polynomial of n,L holds Support (- p) = Support p
proof end;

theorem Th6: :: GROEB_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for p being Polynomial of n,L holds HT (- p),T = HT p,T
proof end;

theorem Th7: :: GROEB_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for p, q being Polynomial of n,L holds HT (p - q),T <= max (HT p,T),(HT q,T),T,T
proof end;

theorem Th8: :: GROEB_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
proof end;

theorem Th9: :: GROEB_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT p,T <= HT f,T,T
proof end;

theorem Th10: :: GROEB_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p being Polynomial of n,L holds PolyRedRel {p},T is locally-confluent
proof end;

theorem :: GROEB_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ex p being Polynomial of n,L st
( p in P & P -Ideal = {p} -Ideal ) holds
PolyRedRel P,T is locally-confluent
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let P be Subset of (Polynom-Ring n,L);
func HT P,T -> Subset of (Bags n) equals :: GROEB_1:def 1
{ (HT p,T) where p is Polynomial of n,L : ( p in P & p <> 0_ n,L ) } ;
coherence
{ (HT p,T) where p is Polynomial of n,L : ( p in P & p <> 0_ n,L ) } is Subset of (Bags n)
proof end;
end;

:: deftheorem defines HT GROEB_1:def 1 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L) holds HT P,T = { (HT p,T) where p is Polynomial of n,L : ( p in P & p <> 0_ n,L ) } ;

definition
let n be Ordinal;
let S be Subset of (Bags n);
func multiples S -> Subset of (Bags n) equals :: GROEB_1:def 2
{ b where b is Element of Bags n : ex b' being bag of n st
( b' in S & b' divides b )
}
;
coherence
{ b where b is Element of Bags n : ex b' being bag of n st
( b' in S & b' divides b )
}
is Subset of (Bags n)
proof end;
end;

:: deftheorem defines multiples GROEB_1:def 2 :
for n being Ordinal
for S being Subset of (Bags n) holds multiples S = { b where b is Element of Bags n : ex b' being bag of n st
( b' in S & b' divides b )
}
;

theorem Th12: :: GROEB_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T is locally-confluent holds
PolyRedRel P,T is confluent
proof end;

theorem Th13: :: GROEB_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T is confluent holds
PolyRedRel P,T is with_UN_property
proof end;

theorem Th14: :: GROEB_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T is with_UN_property holds
PolyRedRel P,T is with_Church-Rosser_property
proof end;

Lm4: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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
proof end;

Lm5: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel P,T reduces h,g )
proof end;

theorem Th15: :: GROEB_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
proof end;

theorem Th16: :: GROEB_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
proof end;

theorem Th17: :: GROEB_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
proof end;

theorem Th18: :: GROEB_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of n st b in HT (P -Ideal ),T holds
ex b' being bag of n st
( b' in HT P,T & b' divides b )
proof end;

theorem :: GROEB_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for b being bag of n st b in HT (P -Ideal ),T holds
ex b' being bag of n st
( b' in HT P,T & b' divides b ) ) holds
HT (P -Ideal ),T c= multiples (HT P,T)
proof end;

theorem :: GROEB_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st HT (P -Ideal ),T c= multiples (HT P,T) holds
PolyRedRel P,T is locally-confluent
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let G be Subset of (Polynom-Ring n,L);
pred G is_Groebner_basis_wrt T means :Def3: :: GROEB_1:def 3
PolyRedRel G,T is locally-confluent;
end;

:: deftheorem Def3 defines is_Groebner_basis_wrt GROEB_1:def 3 :
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for G being Subset of (Polynom-Ring n,L) holds
( G is_Groebner_basis_wrt T iff PolyRedRel G,T is locally-confluent );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let G, I be Subset of (Polynom-Ring n,L);
pred G is_Groebner_basis_of I,T means :Def4: :: GROEB_1:def 4
( G -Ideal = I & PolyRedRel G,T is locally-confluent );
end;

:: deftheorem Def4 defines is_Groebner_basis_of GROEB_1:def 4 :
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for G, I being Subset of (Polynom-Ring n,L) holds
( G is_Groebner_basis_of I,T iff ( G -Ideal = I & PolyRedRel G,T is locally-confluent ) );

Lm6: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for a, b being set st a <> b & PolyRedRel P,T reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
proof end;

theorem :: GROEB_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for G, P being non empty Subset of (Polynom-Ring n,L) st G is_Groebner_basis_of P,T holds
PolyRedRel G,T is Completion of PolyRedRel P,T
proof end;

theorem :: GROEB_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for p, q being Element of (Polynom-Ring n,L)
for G being non empty Subset of (Polynom-Ring n,L) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf p,(PolyRedRel G,T) = nf q,(PolyRedRel G,T) )
proof end;

theorem :: GROEB_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L) st P is_Groebner_basis_wrt T holds
( f in P -Ideal iff PolyRedRel P,T reduces f, 0_ n,L )
proof end;

Lm7: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for I being LeftIdeal of (Polynom-Ring n,L)
for G being non empty Subset of (Polynom-Ring n,L) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel G,T reduces f, 0_ n,L ) holds
G -Ideal = I
proof end;

theorem Th24: :: GROEB_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being Subset of (Polynom-Ring n,L)
for G being non empty Subset of (Polynom-Ring n,L) st G is_Groebner_basis_of I,T holds
for f being Polynomial of n,L st f in I holds
PolyRedRel G,T reduces f, 0_ n,L
proof end;

theorem Th25: :: GROEB_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for G, I being Subset of (Polynom-Ring n,L) st ( for f being Polynomial of n,L st f in I holds
PolyRedRel G,T reduces f, 0_ n,L ) holds
for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt G,T
proof end;

theorem Th26: :: GROEB_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring n,L)
for G being Subset of (Polynom-Ring n,L) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt G,T ) holds
for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T
proof end;

theorem Th27: :: GROEB_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for G, I being Subset of (Polynom-Ring n,L) st ( for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T ) holds
for b being bag of n st b in HT I,T holds
ex b' being bag of n st
( b' in HT G,T & b' divides b )
proof end;

theorem Th28: :: GROEB_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for G, I being Subset of (Polynom-Ring n,L) st ( for b being bag of n st b in HT I,T holds
ex b' being bag of n st
( b' in HT G,T & b' divides b ) ) holds
HT I,T c= multiples (HT G,T)
proof end;

theorem Th29: :: GROEB_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L)
for G being non empty Subset of (Polynom-Ring n,L) st G c= I & HT I,T c= multiples (HT G,T) holds
G is_Groebner_basis_of I,T
proof end;

theorem Th30: :: GROEB_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr holds {(0_ n,L)} is_Groebner_basis_of {(0_ n,L)},T
proof end;

theorem :: GROEB_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p being Polynomial of n,L holds {p} is_Groebner_basis_of {p} -Ideal ,T
proof end;

theorem :: GROEB_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being connected admissible TermOrder of {}
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring {} ,L)
for P being non empty Subset of (Polynom-Ring {} ,L) st P c= I & P <> {(0_ {} ,L)} holds
P is_Groebner_basis_of I,T
proof end;

theorem :: GROEB_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr holds
not for P being Subset of (Polynom-Ring n,L) holds P is_Groebner_basis_wrt T
proof end;

Lm8: for n being Ordinal
for b1, b2, b3 being bag of n st b1 divides b2 & b2 divides b3 holds
b1 divides b3
proof end;

definition
let n be Ordinal;
func DivOrder n -> Order of Bags n means :Def5: :: GROEB_1:def 5
for b1, b2 being bag of n holds
( [b1,b2] in it iff b1 divides b2 );
existence
ex b1 being Order of Bags n st
for b1, b2 being bag of n holds
( [b1,b2] in b1 iff b1 divides b2 )
proof end;
uniqueness
for b1, b2 being Order of Bags n st ( for b1, b2 being bag of n holds
( [b1,b2] in b1 iff b1 divides b2 ) ) & ( for b1, b2 being bag of n holds
( [b1,b2] in b2 iff b1 divides b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :
for n being Ordinal
for b2 being Order of Bags n holds
( b2 = DivOrder n iff for b1, b2 being bag of n holds
( [b1,b2] in b2 iff b1 divides b2 ) );

registration
let n be Nat;
cluster RelStr(# (Bags n),(DivOrder n) #) -> Dickson ;
coherence
RelStr(# (Bags n),(DivOrder n) #) is Dickson
proof end;
end;

theorem Th34: :: GROEB_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for N being Subset of RelStr(# (Bags n),(DivOrder n) #) ex B being finite Subset of (Bags n) st B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #)
proof end;

theorem Th35: :: GROEB_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) ex G being finite Subset of (Polynom-Ring n,L) st G is_Groebner_basis_of I,T
proof end;

Lm9: for L being non empty unital associative add-associative right_zeroed right_complementable distributive left_zeroed doubleLoopStr
for A, B being non empty Subset of L st 0. L in A & B = A \ {(0. L)} holds
for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
proof end;

theorem :: GROEB_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st I <> {(0_ n,L)} holds
ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & not 0_ n,L in G )
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty multLoopStr_0 ;
let p be Polynomial of n,L;
pred p is_monic_wrt T means :Def6: :: GROEB_1:def 6
HC p,T = 1. L;
end;

:: deftheorem Def6 defines is_monic_wrt GROEB_1:def 6 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty multLoopStr_0
for p being Polynomial of n,L holds
( p is_monic_wrt T iff HC p,T = 1. L );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let P be Subset of (Polynom-Ring n,L);
pred P is_reduced_wrt T means :Def7: :: GROEB_1:def 7
for p being Polynomial of n,L st p in P holds
( p is_monic_wrt T & p is_irreducible_wrt P \ {p},T );
end;

:: deftheorem Def7 defines is_reduced_wrt GROEB_1:def 7 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L) holds
( P is_reduced_wrt T iff for p being Polynomial of n,L st p in P holds
( p is_monic_wrt T & p is_irreducible_wrt P \ {p},T ) );

notation
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let P be Subset of (Polynom-Ring n,L);
synonym P is_autoreduced_wrt T for P is_reduced_wrt T;
end;

theorem Th37: :: GROEB_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring n,L)
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM f,T = m & HM g,T = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) holds
f = g
proof end;

Lm10: for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for p being Polynomial of n,L
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st p in I & p <> 0_ n,L holds
ex q being Polynomial of n,L st
( q in I & HM q,T = Monom (1. L),(HT p,T) & q <> 0_ n,L )
proof end;

theorem :: GROEB_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L)
for G being Subset of (Polynom-Ring n,L)
for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T
proof end;

theorem :: GROEB_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st I <> {(0_ n,L)} holds
ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
proof end;

theorem :: GROEB_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L)
for G1, G2 being non empty finite Subset of (Polynom-Ring n,L) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds
G1 = G2
proof end;