:: by Christoph Schwarzweller

::

:: Received December 10, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

theorem Th2: :: GROEB_3:2

for n being Ordinal

for T being admissible TermOrder of n

for b1, b2, b3 being bag of n st b1 <= b2,T holds

b1 + b3 <= b2 + b3,T

for T being admissible TermOrder of n

for b1, b2, b3 being bag of n st b1 <= b2,T holds

b1 + b3 <= b2 + b3,T

proof end;

theorem Th3: :: GROEB_3:3

for n being Ordinal

for T being TermOrder of n

for b1, b2, b3 being bag of n st b1 <= b2,T & b2 < b3,T holds

b1 < b3,T

for T being TermOrder of n

for b1, b2, b3 being bag of n st b1 <= b2,T & b2 < b3,T holds

b1 < b3,T

proof end;

theorem Th4: :: GROEB_3:4

for n being Ordinal

for T being admissible TermOrder of n

for b1, b2, b3 being bag of n st b1 < b2,T holds

b1 + b3 < b2 + b3,T

for T being admissible TermOrder of n

for b1, b2, b3 being bag of n st b1 < b2,T holds

b1 + b3 < b2 + b3,T

proof end;

theorem Th5: :: GROEB_3:5

for n being Ordinal

for T being admissible TermOrder of n

for b1, b2, b3, b4 being bag of n st b1 < b2,T & b3 <= b4,T holds

b1 + b3 < b2 + b4,T

for T being admissible TermOrder of n

for b1, b2, b3, b4 being bag of n st b1 < b2,T & b3 <= b4,T holds

b1 + b3 < b2 + b4,T

proof end;

theorem Th6: :: GROEB_3:6

for n being Ordinal

for T being admissible TermOrder of n

for b1, b2, b3, b4 being bag of n st b1 <= b2,T & b3 < b4,T holds

b1 + b3 < b2 + b4,T

for T being admissible TermOrder of n

for b1, b2, b3, b4 being bag of n st b1 <= b2,T & b3 < b4,T holds

b1 + b3 < b2 + b4,T

proof end;

theorem Th7: :: GROEB_3:7

for n being Ordinal

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for m1, m2 being non-zero Monomial of n,L holds term (m1 *' m2) = (term m1) + (term m2)

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for m1, m2 being non-zero Monomial of n,L holds term (m1 *' m2) = (term m1) + (term m2)

proof end;

theorem Th8: :: GROEB_3:8

for n being Ordinal

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for b being bag of n holds

( b in Support p iff (term m) + b in Support (m *' p) )

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for b being bag of n holds

( b in Support p iff (term m) + b in Support (m *' p) )

proof end;

theorem Th9: :: GROEB_3:9

for n being Ordinal

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L holds Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L holds Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }

proof end;

theorem Th10: :: GROEB_3:10

for n being Ordinal

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L holds card (Support p) = card (Support (m *' p))

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L holds card (Support p) = card (Support (m *' p))

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 Th11: :: GROEB_3:11

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr holds Red ((0_ (n,L)),T) = 0_ (n,L)

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr holds Red ((0_ (n,L)),T) = 0_ (n,L)

proof end;

theorem Th12: :: GROEB_3:12

for n being Ordinal

for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr

for p, q being Polynomial of n,L st p - q = 0_ (n,L) holds

p = q

for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr

for p, q being Polynomial of n,L st p - q = 0_ (n,L) holds

p = q

proof end;

theorem Th13: :: GROEB_3:13

for X being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_ (X,L)) = 0_ (X,L)

for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_ (X,L)) = 0_ (X,L)

proof end;

theorem Th14: :: GROEB_3:14

for X being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for f being Series of X,L holds (0_ (X,L)) - f = - f

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for f being Series of X,L holds (0_ (X,L)) - f = - f

proof end;

theorem Th15: :: GROEB_3:15

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds p - (Red (p,T)) = HM (p,T)

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds p - (Red (p,T)) = HM (p,T)

proof end;

registration

let n be Ordinal;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

coherence

Support p is finite by POLYNOM1:def 5;

end;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

coherence

Support p is finite by POLYNOM1:def 5;

definition

let n be Ordinal;

let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;

let p, q be Polynomial of n,L;

:: original: {

redefine func {p,q} -> Subset of (Polynom-Ring (n,L));

coherence

{p,q} is Subset of (Polynom-Ring (n,L))

end;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;

let p, q be Polynomial of n,L;

:: original: {

redefine func {p,q} -> Subset of (Polynom-Ring (n,L));

coherence

{p,q} is Subset of (Polynom-Ring (n,L))

proof end;

definition

let X be set ;

let L be non empty ZeroStr ;

let s be Series of X,L;

let Y be Subset of (Bags X);

coherence

s +* (((Support s) \ Y) --> (0. L)) is Series of X,L

end;
let L be non empty ZeroStr ;

let s be Series of X,L;

let Y be Subset of (Bags X);

coherence

s +* (((Support s) \ Y) --> (0. L)) is Series of X,L

proof end;

:: deftheorem defines | GROEB_3:def 1 :

for X being set

for L being non empty ZeroStr

for s being Series of X,L

for Y being Subset of (Bags X) holds s | Y = s +* (((Support s) \ Y) --> (0. L));

for X being set

for L being non empty ZeroStr

for s being Series of X,L

for Y being Subset of (Bags X) holds s | Y = s +* (((Support s) \ Y) --> (0. L));

Lm2: for X being set

for L being non empty ZeroStr

for s being Series of X,L

for Y being Subset of (Bags X) holds Support (s | Y) c= Support s

proof end;

registration

let n be Ordinal;

let L be non empty ZeroStr ;

let p be Polynomial of n,L;

let Y be Subset of (Bags n);

coherence

p | Y is finite-Support

end;
let L be non empty ZeroStr ;

let p be Polynomial of n,L;

let Y be Subset of (Bags n);

coherence

p | Y is finite-Support

proof end;

theorem Th16: :: GROEB_3:16

for X being set

for L being non empty ZeroStr

for s being Series of X,L

for Y being Subset of (Bags X) holds

( Support (s | Y) = (Support s) /\ Y & ( for b being bag of X st b in Support (s | Y) holds

(s | Y) . b = s . b ) )

for L being non empty ZeroStr

for s being Series of X,L

for Y being Subset of (Bags X) holds

( Support (s | Y) = (Support s) /\ Y & ( for b being bag of X st b in Support (s | Y) holds

(s | Y) . b = s . b ) )

proof end;

theorem :: GROEB_3:17

theorem :: GROEB_3:18

for X being set

for L being non empty ZeroStr

for s being Series of X,L holds

( s | (Support s) = s & s | ({} (Bags X)) = 0_ (X,L) )

for L being non empty ZeroStr

for s being Series of X,L holds

( s | (Support s) = s & s | ({} (Bags X)) = 0_ (X,L) )

proof end;

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

let i be Nat;

assume A1: i <= card (Support p) ;

ex b_{1} being finite Subset of (Bags n) st

( b_{1} c= Support p & card b_{1} = i & ( for b, b9 being bag of n st b in b_{1} & b9 in Support p & b <= b9,T holds

b9 in b_{1} ) )

for b_{1}, b_{2} being finite Subset of (Bags n) st b_{1} c= Support p & card b_{1} = i & ( for b, b9 being bag of n st b in b_{1} & b9 in Support p & b <= b9,T holds

b9 in b_{1} ) & b_{2} c= Support p & card b_{2} = i & ( for b, b9 being bag of n st b in b_{2} & b9 in Support p & b <= b9,T holds

b9 in b_{2} ) holds

b_{1} = b_{2}

end;
let T be connected TermOrder of n;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

let i be Nat;

assume A1: i <= card (Support p) ;

func Upper_Support (p,T,i) -> finite Subset of (Bags n) means :Def2: :: GROEB_3:def 2

( it c= Support p & card it = i & ( for b, b9 being bag of n st b in it & b9 in Support p & b <= b9,T holds

b9 in it ) );

existence ( it c= Support p & card it = i & ( for b, b9 being bag of n st b in it & b9 in Support p & b <= b9,T holds

b9 in it ) );

ex b

( b

b9 in b

proof end;

uniqueness for b

b9 in b

b9 in b

b

proof end;

:: deftheorem Def2 defines Upper_Support GROEB_3:def 2 :

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat st i <= card (Support p) holds

for b_{6} being finite Subset of (Bags n) holds

( b_{6} = Upper_Support (p,T,i) iff ( b_{6} c= Support p & card b_{6} = i & ( for b, b9 being bag of n st b in b_{6} & b9 in Support p & b <= b9,T holds

b9 in b_{6} ) ) );

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat st i <= card (Support p) holds

for b

( b

b9 in b

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

let i be Nat;

(Support p) \ (Upper_Support (p,T,i)) is finite Subset of (Bags n)

end;
let T be connected TermOrder of n;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

let i be Nat;

func Lower_Support (p,T,i) -> finite Subset of (Bags n) equals :: GROEB_3:def 3

(Support p) \ (Upper_Support (p,T,i));

coherence (Support p) \ (Upper_Support (p,T,i));

(Support p) \ (Upper_Support (p,T,i)) is finite Subset of (Bags n)

proof end;

:: deftheorem defines Lower_Support GROEB_3:def 3 :

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat holds Lower_Support (p,T,i) = (Support p) \ (Upper_Support (p,T,i));

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat holds Lower_Support (p,T,i) = (Support p) \ (Upper_Support (p,T,i));

theorem Th19: :: GROEB_3:19

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} )

proof end;

theorem Th20: :: GROEB_3:20

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds

b9 < b,T

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds

b9 < b,T

proof end;

theorem :: GROEB_3:21

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( Upper_Support (p,T,0) = {} & Lower_Support (p,T,0) = Support p )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( Upper_Support (p,T,0) = {} & Lower_Support (p,T,0) = Support p )

proof end;

theorem Th22: :: GROEB_3:22

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( Upper_Support (p,T,(card (Support p))) = Support p & Lower_Support (p,T,(card (Support p))) = {} )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( Upper_Support (p,T,(card (Support p))) = Support p & Lower_Support (p,T,(card (Support p))) = {} )

proof end;

theorem Th23: :: GROEB_3:23

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being non-zero Polynomial of n,L

for i being Element of NAT st 1 <= i & i <= card (Support p) holds

HT (p,T) in Upper_Support (p,T,i)

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being non-zero Polynomial of n,L

for i being Element of NAT st 1 <= i & i <= card (Support p) holds

HT (p,T) in Upper_Support (p,T,i)

proof end;

theorem Th24: :: GROEB_3:24

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( Lower_Support (p,T,i) c= Support p & card (Lower_Support (p,T,i)) = (card (Support p)) - i & ( for b, b9 being bag of n st b in Lower_Support (p,T,i) & b9 in Support p & b9 <= b,T holds

b9 in Lower_Support (p,T,i) ) )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( Lower_Support (p,T,i) c= Support p & card (Lower_Support (p,T,i)) = (card (Support p)) - i & ( for b, b9 being bag of n st b in Lower_Support (p,T,i) & b9 in Support p & b9 <= b,T holds

b9 in Lower_Support (p,T,i) ) )

proof end;

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

let i be Nat;

coherence

p | (Upper_Support (p,T,i)) is Polynomial of n,L ;

coherence

p | (Lower_Support (p,T,i)) is Polynomial of n,L ;

end;
let T be connected TermOrder of n;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

let i be Nat;

coherence

p | (Upper_Support (p,T,i)) is Polynomial of n,L ;

coherence

p | (Lower_Support (p,T,i)) is Polynomial of n,L ;

:: deftheorem defines Up GROEB_3:def 4 :

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat holds Up (p,T,i) = p | (Upper_Support (p,T,i));

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat holds Up (p,T,i) = p | (Upper_Support (p,T,i));

:: deftheorem defines Low GROEB_3:def 5 :

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat holds Low (p,T,i) = p | (Lower_Support (p,T,i));

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Nat holds Low (p,T,i) = p | (Lower_Support (p,T,i));

Lm3: for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( Support (p | (Upper_Support (p,T,i))) = Upper_Support (p,T,i) & Support (p | (Lower_Support (p,T,i))) = Lower_Support (p,T,i) )

proof end;

theorem :: GROEB_3:25

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( Support (Up (p,T,i)) = Upper_Support (p,T,i) & Support (Low (p,T,i)) = Lower_Support (p,T,i) ) by Lm3;

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( Support (Up (p,T,i)) = Upper_Support (p,T,i) & Support (Low (p,T,i)) = Lower_Support (p,T,i) ) by Lm3;

theorem Th26: :: GROEB_3:26

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )

proof end;

theorem Th27: :: GROEB_3:27

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 1 <= i & i <= card (Support p) holds

Support (Low (p,T,i)) c= Support (Red (p,T))

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 1 <= i & i <= card (Support p) holds

Support (Low (p,T,i)) c= Support (Red (p,T))

proof end;

theorem Th28: :: GROEB_3:28

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n st b in Support p holds

( ( b in Support (Up (p,T,i)) or b in Support (Low (p,T,i)) ) & not b in (Support (Up (p,T,i))) /\ (Support (Low (p,T,i))) )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n st b in Support p holds

( ( b in Support (Up (p,T,i)) or b in Support (Low (p,T,i)) ) & not b in (Support (Up (p,T,i))) /\ (Support (Low (p,T,i))) )

proof end;

theorem Th29: :: GROEB_3:29

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds

b < b9,T

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds

b < b9,T

proof end;

theorem Th30: :: GROEB_3:30

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 1 <= i & i <= card (Support p) holds

HT (p,T) in Support (Up (p,T,i))

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 1 <= i & i <= card (Support p) holds

HT (p,T) in Support (Up (p,T,i))

proof end;

theorem Th31: :: GROEB_3:31

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n st b in Support (Low (p,T,i)) holds

( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n st b in Support (Low (p,T,i)) holds

( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )

proof end;

theorem Th32: :: GROEB_3:32

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n st b in Support (Up (p,T,i)) holds

( (Up (p,T,i)) . b = p . b & (Low (p,T,i)) . b = 0. L )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n st b in Support (Up (p,T,i)) holds

( (Up (p,T,i)) . b = p . b & (Low (p,T,i)) . b = 0. L )

proof end;

theorem Th33: :: GROEB_3:33

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

(Up (p,T,i)) + (Low (p,T,i)) = p

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i <= card (Support p) holds

(Up (p,T,i)) + (Low (p,T,i)) = p

proof end;

theorem Th34: :: GROEB_3:34

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( Up (p,T,0) = 0_ (n,L) & Low (p,T,0) = p )

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( Up (p,T,0) = 0_ (n,L) & Low (p,T,0) = p )

proof end;

theorem Th35: :: GROEB_3:35

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds

( Up (p,T,(card (Support p))) = p & Low (p,T,(card (Support p))) = 0_ (n,L) )

for T being connected TermOrder of n

for L being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds

( Up (p,T,(card (Support p))) = p & Low (p,T,(card (Support p))) = 0_ (n,L) )

proof end;

theorem Th36: :: GROEB_3:36

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr

for p being non-zero Polynomial of n,L holds

( Up (p,T,1) = HM (p,T) & Low (p,T,1) = Red (p,T) )

for T being connected TermOrder of n

for L being non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr

for p being non-zero Polynomial of n,L holds

( Up (p,T,1) = HM (p,T) & Low (p,T,1) = Red (p,T) )

proof end;

registration

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ;

let p be non-zero Polynomial of n,L;

coherence

Up (p,T,0) is monomial-like

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ;

let p be non-zero Polynomial of n,L;

coherence

Up (p,T,0) is monomial-like

proof end;

registration

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr ;

let p be non-zero Polynomial of n,L;

coherence

( Up (p,T,1) is non-zero & Up (p,T,1) is monomial-like )

Low (p,T,(card (Support p))) is monomial-like

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr ;

let p be non-zero Polynomial of n,L;

coherence

( Up (p,T,1) is non-zero & Up (p,T,1) is monomial-like )

proof end;

coherence Low (p,T,(card (Support p))) is monomial-like

proof end;

theorem Th37: :: GROEB_3:37

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

proof end;

theorem Th38: :: GROEB_3:38

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T

for T being connected admissible TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T

proof end;

theorem Th39: :: GROEB_3:39

for n being Ordinal

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

proof end;

theorem Th40: :: GROEB_3:40

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n holds

( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )

for T being connected admissible TermOrder of n

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

for b being bag of n holds

( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )

proof end;

theorem Th41: :: GROEB_3:41

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))

for T being connected admissible TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))

proof end;

theorem Th42: :: GROEB_3:42

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

for T being connected admissible TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

proof end;

theorem Th43: :: GROEB_3:43

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

proof end;

theorem Th44: :: GROEB_3:44

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

for T being connected admissible TermOrder of n

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

proof end;

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

for R being RedSequence of PolyRedRel (P,T)

for i being Element of NAT st 1 <= i & i <= len R & len R > 1 holds

R . i is Polynomial of n,L

proof end;

theorem Th45: :: GROEB_3:45

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds

- f reduces_to - g,p,T

for T being connected admissible 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 f, g, p being Polynomial of n,L st f reduces_to g,p,T holds

- f reduces_to - g,p,T

proof end;

Lm5: 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 st HT (p1,T), HT (p2,T) are_disjoint holds

for b1, b2 being bag of n st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT (p1,T) or not b2 = HT (p2,T) ) holds

not (HT (p1,T)) + b2 = (HT (p2,T)) + b1

proof end;

theorem Th46: :: GROEB_3:46

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

f + g reduces_to f1 + g,{p},T

for T being connected admissible 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 f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

f + g reduces_to f1 + g,{p},T

proof end;

theorem Th47: :: GROEB_3:47

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red (f,T)) *' g,{g},T

for T being connected admissible 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 f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red (f,T)) *' g,{g},T

proof end;

theorem :: GROEB_3:48

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, g being non-zero Polynomial of n,L

for p being Polynomial of n,L st p . (HT ((f *' g),T)) = 0. L holds

(f *' g) + p reduces_to ((Red (f,T)) *' g) + p,{g},T

for T being connected admissible 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 f, g being non-zero Polynomial of n,L

for p being Polynomial of n,L st p . (HT ((f *' g),T)) = 0. L holds

(f *' g) + p reduces_to ((Red (f,T)) *' g) + p,{g},T

proof end;

theorem Th49: :: GROEB_3:49

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds

PolyRedRel (P,T) reduces - f, - g

for T being connected admissible 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 f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds

PolyRedRel (P,T) reduces - f, - g

proof end;

theorem :: GROEB_3:50

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

for T being connected admissible 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 f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

proof end;

theorem Th51: :: GROEB_3:51

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, g being non-zero Polynomial of n,L holds PolyRedRel ({g},T) reduces f *' g, 0_ (n,L)

for T being connected admissible 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 f, g being non-zero Polynomial of n,L holds PolyRedRel ({g},T) reduces f *' g, 0_ (n,L)

proof end;

theorem Th52: :: GROEB_3:52

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 st HT (p1,T), HT (p2,T) are_disjoint holds

for b1, b2 being bag of n st b1 in Support (Red (p1,T)) & b2 in Support (Red (p2,T)) holds

not (HT (p1,T)) + b2 = (HT (p2,T)) + b1

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 st HT (p1,T), HT (p2,T) are_disjoint holds

for b1, b2 being bag of n st b1 in Support (Red (p1,T)) & b2 in Support (Red (p2,T)) holds

not (HT (p1,T)) + b2 = (HT (p2,T)) + b1

proof end;

theorem Th53: :: GROEB_3:53

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 p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds

S-Poly (p1,p2,T) = ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))

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 p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds

S-Poly (p1,p2,T) = ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))

proof end;

theorem Th54: :: GROEB_3:54

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 p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds

S-Poly (p1,p2,T) = ((Red (p1,T)) *' p2) - ((Red (p2,T)) *' p1)

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 p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds

S-Poly (p1,p2,T) = ((Red (p1,T)) *' p2) - ((Red (p2,T)) *' p1)

proof end;

theorem Th55: :: GROEB_3:55

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p1, p2 being non-zero Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint & Red (p1,T) is non-zero & Red (p2,T) is non-zero holds

PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T))

for T being connected admissible 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 p1, p2 being non-zero Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint & Red (p1,T) is non-zero & Red (p2,T) is non-zero holds

PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T))

proof end;

theorem Th56: :: GROEB_3:56

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 Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds

PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L)

for T being connected admissible 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 p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds

PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L)

proof end;

:: theorem 5.66, p. 222 (Buchberger's first criterium)

theorem :: GROEB_3:57

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 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

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 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

proof end;

:: theorem 5.68 (i) ==> (ii), p. 223

theorem :: GROEB_3:58

for n being Element of NAT

for T being connected admissible TermOrder of n

for L being non degenerated non trivial 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 & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L)

for T being connected admissible TermOrder of n

for L being non degenerated non trivial 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 & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L)

proof end;

:: theorem 5.68 (ii) ==> (iii), p. 223

theorem :: GROEB_3:59

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, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

G is_Groebner_basis_wrt T

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, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

G is_Groebner_basis_wrt T

proof end;