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

theorem Th1: :: GROEB_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for b1, b2 being bag of X holds (b1 + b2) / b2 = b1
proof end;

theorem Th2: :: GROEB_3: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 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  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 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  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 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  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 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  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 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  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 add-associative right_zeroed right_complementable unital distributive non trivial 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  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 add-associative right_zeroed right_complementable unital distributive non trivial 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  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 add-associative right_zeroed right_complementable unital distributive non trivial 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  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 add-associative right_zeroed right_complementable unital distributive non trivial left_zeroed domRing-like 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 add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital 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;

theorem Th11: :: GROEB_3:11  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 add-associative right_zeroed right_complementable non trivial LoopStr holds Red (0_ n,L),T = 0_ n,L
proof end;

theorem Th12: :: GROEB_3:12  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 Abelian add-associative right_zeroed right_complementable unital commutative distributive non trivial 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty add-associative right_zeroed right_complementable LoopStr holds - (0_ X,L) = 0_ X,L
proof end;

theorem Th14: :: GROEB_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty add-associative right_zeroed right_complementable LoopStr
for f being Series of X,L holds (0_ X,L) - f = - f
proof end;

theorem Th15: :: GROEB_3:15  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 add-associative right_zeroed right_complementable non trivial 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 add-associative right_zeroed right_complementable LoopStr ;
let p be Polynomial of n,L;
cluster Support p -> finite ;
coherence
Support p is finite
by POLYNOM1:def 10;
end;

definition
let n be Ordinal;
let L be add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let p, q be Polynomial of n,L;
:: original: {
redefine func {p,q} -> non empty finite Subset of (Polynom-Ring n,L);
coherence
{p,q} is non empty finite Subset of (Polynom-Ring n,L)
proof end;
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);
func s | Y -> Series of X,L equals :: GROEB_3:def 1
s +* (((Support s) \ Y) --> (0. L));
coherence
s +* (((Support s) \ Y) --> (0. L)) is Series of X,L
proof end;
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));

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);
cluster p | Y -> finite-Support ;
coherence
p | Y is finite-Support
proof end;
end;

theorem Th16: :: GROEB_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: GROEB_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 by Lm2;

theorem :: GROEB_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty add-associative right_zeroed right_complementable LoopStr ;
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, b' being bag of n st b in it & b' in Support p & b <= b',T holds
b' in it ) );
existence
ex b1 being finite Subset of (Bags n) st
( b1 c= Support p & card b1 = i & ( for b, b' being bag of n st b in b1 & b' in Support p & b <= b',T holds
b' in b1 ) )
proof end;
uniqueness
for b1, b2 being finite Subset of (Bags n) st b1 c= Support p & card b1 = i & ( for b, b' being bag of n st b in b1 & b' in Support p & b <= b',T holds
b' in b1 ) & b2 c= Support p & card b2 = i & ( for b, b' being bag of n st b in b2 & b' in Support p & b <= b',T holds
b' in b2 ) holds
b1 = b2
proof end;
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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being Nat st i <= card (Support p) holds
for b6 being finite Subset of (Bags n) holds
( b6 = Upper_Support p,T,i iff ( b6 c= Support p & card b6 = i & ( for b, b' being bag of n st b in b6 & b' in Support p & b <= b',T holds
b' in b6 ) ) );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty add-associative right_zeroed right_complementable LoopStr ;
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) is finite Subset of (Bags n)
proof end;
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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being Nat holds Lower_Support p,T,i = (Support p) \ (Upper_Support p,T,i);

Lm3: for n being Ordinal
for T being connected TermOrder of n
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being Nat st i <= card (Support p) holds
Lower_Support p,T,i c= Support p
by XBOOLE_1:36;

theorem Th19: :: GROEB_3: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 non empty add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being Nat st i <= card (Support p) holds
for b, b' being bag of n st b in Upper_Support p,T,i & b' in Lower_Support p,T,i holds
b' < b,T
proof end;

theorem :: GROEB_3:21  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 add-associative right_zeroed right_complementable LoopStr
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  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 add-associative right_zeroed right_complementable LoopStr
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  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 add-associative right_zeroed right_complementable non trivial LoopStr
for p being non-zero Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' 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 add-associative right_zeroed right_complementable LoopStr ;
let p be Polynomial of n,L;
let i be Nat;
func Up p,T,i -> Polynomial of n,L equals :: GROEB_3:def 4
p | (Upper_Support p,T,i);
coherence
p | (Upper_Support p,T,i) is Polynomial of n,L
;
func Low p,T,i -> Polynomial of n,L equals :: GROEB_3:def 5
p | (Lower_Support p,T,i);
coherence
p | (Lower_Support p,T,i) is Polynomial of n,L
;
end;

:: deftheorem defines Up GROEB_3:def 4 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty add-associative right_zeroed right_complementable LoopStr
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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being Nat holds Low p,T,i = p | (Lower_Support p,T,i);

Lm4: for n being Ordinal
for T being connected TermOrder of n
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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 Th25: :: GROEB_3: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 non empty add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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 Lm4;

theorem Th26: :: GROEB_3:26  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being Nat st i <= card (Support p) holds
for b, b' being bag of n st b in Support (Low p,T,i) & b' in Support (Up p,T,i) holds
b < b',T
proof end;

theorem Th30: :: GROEB_3:30  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being Nat st i <= card (Support p) holds
(Up p,T,i) + (Low p,T,i) = p
proof end;

theorem Th34: :: GROEB_3:34  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 add-associative right_zeroed right_complementable LoopStr
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  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 Abelian add-associative right_zeroed right_complementable 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  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 Abelian add-associative right_zeroed right_complementable non trivial 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 add-associative right_zeroed right_complementable non trivial LoopStr ;
let p be non-zero Polynomial of n,L;
cluster Up p,T,0 -> monomial-like ;
coherence
Up p,T,0 is monomial-like
proof end;
end;

registration
let n be Ordinal;
let T be connected TermOrder of n;
let L be Abelian add-associative right_zeroed right_complementable non trivial doubleLoopStr ;
let p be non-zero Polynomial of n,L;
cluster Up p,T,1 -> non-zero monomial-like ;
coherence
( Up p,T,1 is non-zero & Up p,T,1 is monomial-like )
proof end;
cluster Low p,T,(card (Support p)) -> monomial-like ;
coherence
Low p,T,(card (Support p)) is monomial-like
proof end;
end;

theorem Th37: :: GROEB_3: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 TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L
for j being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L
for i being 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  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 add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Nat st i <= card (Support p) holds
Low (m *' p),T,i = m *' (Low p,T,i)
proof end;

Lm5: for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for R being RedSequence of PolyRedRel P,T
for i being 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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;

Lm6: for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial 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 :: GROEB_3:57  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non degenerated 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 :: GROEB_3:58  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non degenerated non trivial 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 :: GROEB_3:59  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 Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non degenerated 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;