let n be non empty Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr holds
not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr holds
not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T
set 1bag = () +* ({},1);
reconsider 1bag = () +* ({},1) as Element of Bags n by PRE_POLY:def 12;
set p = ((1. L) | (n,L)) +* (1bag,(1. L));
reconsider p = ((1. L) | (n,L)) +* (1bag,(1. L)) as Function of (Bags n),L ;
reconsider p = p as Series of n,L ;
A1: 1. L <> 0. L ;
set q = ((0. L) | (n,L)) +* (1bag,(1. L));
reconsider q = ((0. L) | (n,L)) +* (1bag,(1. L)) as Function of (Bags n),L ;
reconsider q = q as Series of n,L ;
A2: now :: thesis: for u being bag of n st u <> EmptyBag n & u <> 1bag holds
p . u = 0. L
let u be bag of n; :: thesis: ( u <> EmptyBag n & u <> 1bag implies p . u = 0. L )
assume that
A3: u <> EmptyBag n and
A4: u <> 1bag ; :: thesis: p . u = 0. L
p . u = ((1. L) | (n,L)) . u by ;
then p . u = (1_ (n,L)) . u by POLYNOM7:20;
hence p . u = 0. L by ; :: thesis: verum
end;
A5: now :: thesis: for u9 being object st u9 in Support p holds
u9 in {(),1bag}
let u9 be object ; :: thesis: ( u9 in Support p implies u9 in {(),1bag} )
assume A6: u9 in Support p ; :: thesis: u9 in {(),1bag}
then reconsider u = u9 as Element of Bags n ;
A7: p . u <> 0. L by ;
now :: thesis: u in {(),1bag}
assume not u in {(),1bag} ; :: thesis: contradiction
then ( u <> EmptyBag n & u <> 1bag ) by TARSKI:def 2;
hence contradiction by A2, A7; :: thesis: verum
end;
hence u9 in {(),1bag} ; :: thesis: verum
end;
( {} in n & dom () = n ) by ;
then 1bag . {} = 1 by FUNCT_7:31;
then A8: EmptyBag n <> 1bag by PBOOLE:5;
then A9: q . () = ((0. L) | (n,L)) . () by FUNCT_7:32
.= (0_ (n,L)) . () by POLYNOM7:19
.= 0. L by POLYNOM1:22 ;
A10: now :: thesis: for u being bag of n st u <> 1bag holds
q . u = 0. L
let u be bag of n; :: thesis: ( u <> 1bag implies q . u = 0. L )
assume u <> 1bag ; :: thesis: q . u = 0. L
then q . u = ((0. L) | (n,L)) . u by FUNCT_7:32;
then q . u = (0_ (n,L)) . u by POLYNOM7:19;
hence q . u = 0. L by POLYNOM1:22; :: thesis: verum
end;
A11: now :: thesis: for u9 being object st u9 in Support q holds
u9 in {1bag}
let u9 be object ; :: thesis: ( u9 in Support q implies u9 in {1bag} )
assume A12: u9 in Support q ; :: thesis: u9 in {1bag}
then reconsider u = u9 as Element of Bags n ;
A13: q . u <> 0. L by ;
now :: thesis: u in {1bag}end;
hence u9 in {1bag} ; :: thesis: verum
end;
dom ((0. L) | (n,L)) = Bags n by FUNCT_2:def 1;
then A14: q . 1bag = 1. L by FUNCT_7:31;
then A15: q <> 0_ (n,L) by POLYNOM1:22;
now :: thesis: for u being object st u in {1bag} holds
u in Support q
let u be object ; :: thesis: ( u in {1bag} implies u in Support q )
assume u in {1bag} ; :: thesis:
then u = 1bag by TARSKI:def 1;
hence u in Support q by ; :: thesis: verum
end;
then A16: Support q = {1bag} by ;
then reconsider q = q as Polynomial of n,L by POLYNOM1:def 5;
reconsider q = q as non-zero Polynomial of n,L by ;
set q1 = q - (((q . (HT (q,T))) / (HC (q,T))) * (() *' q));
Support q <> {} by ;
then A17: HT (q,T) in Support q by TERMORD:def 6;
(EmptyBag n) + (HT (q,T)) = HT (q,T) by PRE_POLY:53;
then q reduces_to q - (((q . (HT (q,T))) / (HC (q,T))) * (() *' q)),q, HT (q,T),T by ;
then A18: q reduces_to q - (((q . (HT (q,T))) / (HC (q,T))) * (() *' q)),q,T by POLYRED:def 6;
A19: q - (((q . (HT (q,T))) / (HC (q,T))) * (() *' q)) = q - (((HC (q,T)) / (HC (q,T))) * (() *' q)) by TERMORD:def 7
.= q - (((HC (q,T)) * ((HC (q,T)) ")) * (() *' q))
.= q - ((1. L) * (() *' q)) by VECTSP_1:def 10
.= q - ((1. L) * q) by POLYRED:17
.= q - (((1. L) | (n,L)) *' q) by POLYNOM7:27
.= q - ((1_ (n,L)) *' q) by POLYNOM7:20
.= q - q by POLYNOM1:30
.= 0_ (n,L) by POLYNOM1:24 ;
A20: dom ((1. L) | (n,L)) = Bags n by FUNCT_2:def 1;
then A21: p . 1bag = 1. L by FUNCT_7:31;
then A22: p <> 0_ (n,L) by ;
A23: p . () = ((1. L) | (n,L)) . () by
.= (1_ (n,L)) . () by POLYNOM7:20
.= 1. L by POLYNOM1:25 ;
now :: thesis: for u being object st u in {(),1bag} holds
u in Support p
let u be object ; :: thesis: ( u in {(),1bag} implies u in Support p )
assume A24: u in {(),1bag} ; :: thesis:
now :: thesis: ( ( u = EmptyBag n & u in Support p ) or ( u = 1bag & u in Support p ) )
per cases ( u = EmptyBag n or u = 1bag ) by ;
end;
end;
hence u in Support p ; :: thesis: verum
end;
then A25: Support p = {(),1bag} by ;
then reconsider p = p as Polynomial of n,L by POLYNOM1:def 5;
reconsider p = p as non-zero Polynomial of n,L by ;
A26: (EmptyBag n) + (HT (p,T)) = HT (p,T) by PRE_POLY:53;
A27: now :: thesis: not HT (p,T) = EmptyBag nend;
set p1 = q - (((q . (HT (p,T))) / (HC (p,T))) * (() *' p));
Support p <> {} by ;
then A30: HT (p,T) in Support p by TERMORD:def 6;
then A31: HT (p,T) = 1bag by ;
then HT (p,T) in Support q by ;
then q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * (() *' p)),p, HT (p,T),T by ;
then A32: q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * (() *' p)),p,T by POLYRED:def 6;
A33: now :: thesis: not Support q = Support pend;
A34: now :: thesis: not q - p = 0_ (n,L)
assume q - p = 0_ (n,L) ; :: thesis: contradiction
then p = (q - p) + p by POLYRED:2
.= (q + (- p)) + p by POLYNOM1:def 7
.= q + ((- p) + p) by POLYNOM1:21
.= q + (0_ (n,L)) by POLYRED:3 ;
hence contradiction by A33, POLYNOM1:23; :: thesis: verum
end;
set P = {p,q};
now :: thesis: for u being object st u in {p,q} holds
u in the carrier of (Polynom-Ring (n,L))
let u be object ; :: thesis: ( u in {p,q} implies u in the carrier of (Polynom-Ring (n,L)) )
assume u in {p,q} ; :: thesis: u in the carrier of (Polynom-Ring (n,L))
then ( u = p or u = q ) by TARSKI:def 2;
hence u in the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11; :: thesis: verum
end;
then reconsider P = {p,q} as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;
reconsider P = P as Subset of (Polynom-Ring (n,L)) ;
set R = PolyRedRel (P,T);
take P ; :: thesis:
A35: p in P by TARSKI:def 2;
q in P by TARSKI:def 2;
then q reduces_to 0_ (n,L),P,T by ;
then A36: [q,(0_ (n,L))] in PolyRedRel (P,T) by POLYRED:def 13;
q - (((q . (HT (p,T))) / (HC (p,T))) * (() *' p)) = q - (((1. L) / (p . 1bag)) * (() *' p)) by
.= q - (((1. L) / (1. L)) * (() *' p)) by
.= q - (((1. L) * ((1. L) ")) * (() *' p))
.= q - ((1. L) * (() *' p)) by VECTSP_1:def 10
.= q - ((1. L) * p) by POLYRED:17
.= q - (((1. L) | (n,L)) *' p) by POLYNOM7:27
.= q - ((1_ (n,L)) *' p) by POLYNOM7:20
.= q - p by POLYNOM1:30 ;
then q reduces_to q - p,P,T by ;
then A37: [q,(q - p)] in PolyRedRel (P,T) by POLYRED:def 13;
now :: thesis: not PolyRedRel (P,T) is locally-confluent
A38: now :: thesis: for u being object st u in Support (q - p) holds
u in {()}
let u be object ; :: thesis: ( u in Support (q - p) implies u in {()} )
now :: thesis: for u being object st u in {1bag} holds
u in {(),1bag}
let u be object ; :: thesis: ( u in {1bag} implies u in {(),1bag} )
assume u in {1bag} ; :: thesis: u in {(),1bag}
then u = 1bag by TARSKI:def 1;
hence u in {(),1bag} by TARSKI:def 2; :: thesis: verum
end;
then {1bag} c= {(),1bag} ;
then A39: {1bag} \/ {(),1bag} = {(),1bag} by XBOOLE_1:12;
A40: (q - p) . 1bag = (q + (- p)) . 1bag by POLYNOM1:def 7
.= (q . 1bag) + ((- p) . 1bag) by POLYNOM1:15
.= (q . 1bag) + (- (p . 1bag)) by POLYNOM1:17
.= (1. L) + (- (1. L)) by
.= 0. L by RLVECT_1:5 ;
Support (q - p) = Support (q + (- p)) by POLYNOM1:def 7;
then Support (q - p) c= () \/ (Support (- p)) by POLYNOM1:20;
then A41: Support (q - p) c= {1bag} \/ {(),1bag} by ;
assume A42: u in Support (q - p) ; :: thesis: u in {()}
then (q - p) . u <> 0. L by POLYNOM1:def 4;
then u = EmptyBag n by ;
hence u in {()} by TARSKI:def 1; :: thesis: verum
end;
assume PolyRedRel (P,T) is locally-confluent ; :: thesis: contradiction
then 0_ (n,L),q - p are_convergent_wrt PolyRedRel (P,T) by ;
then consider c being object such that
A43: PolyRedRel (P,T) reduces 0_ (n,L),c and
A44: PolyRedRel (P,T) reduces q - p,c by REWRITE1:def 7;
reconsider c = c as Polynomial of n,L by ;
consider s being FinSequence such that
A45: len s > 0 and
A46: s . 1 = 0_ (n,L) and
A47: s . (len s) = c and
A48: for i being Nat st i in dom s & i + 1 in dom s holds
[(s . i),(s . (i + 1))] in PolyRedRel (P,T) by ;
now :: thesis: not len s <> 1
A49: 0 + 1 <= len s by ;
A50: dom s = Seg (len s) by FINSEQ_1:def 3;
assume len s <> 1 ; :: thesis: contradiction
then 1 < len s by ;
then 1 + 1 <= len s by NAT_1:13;
then A51: 1 + 1 in dom s by ;
A52: 1 in dom s by ;
then consider f9, h9 being object such that
A53: [(0_ (n,L)),(s . 2)] = [f9,h9] and
f9 in NonZero (Polynom-Ring (n,L)) and
A54: h9 in the carrier of (Polynom-Ring (n,L)) by ;
s . 2 = h9 by ;
then reconsider c9 = s . 2 as Polynomial of n,L by ;
[(s . 1),(s . 2)] in PolyRedRel (P,T) by ;
then 0_ (n,L) reduces_to c9,P,T by ;
then consider g being Polynomial of n,L such that
g in P and
A55: 0_ (n,L) reduces_to c9,g,T by POLYRED:def 7;
0_ (n,L) is_reducible_wrt g,T by ;
hence contradiction by POLYRED:37; :: thesis: verum
end;
then consider s being FinSequence such that
A56: len s > 0 and
A57: s . 1 = q - p and
A58: s . (len s) = 0_ (n,L) and
A59: for i being Nat st i in dom s & i + 1 in dom s holds
[(s . i),(s . (i + 1))] in PolyRedRel (P,T) by ;
A60: now :: thesis: not - (1. L) = 0. L
assume - (1. L) = 0. L ; :: thesis: contradiction
then - (- (1. L)) = 0. L by RLVECT_1:12;
hence contradiction by RLVECT_1:17; :: thesis: verum
end;
now :: thesis: for u being object st u in {()} holds
u in Support (q - p)
let u be object ; :: thesis: ( u in {()} implies u in Support (q - p) )
assume A61: u in {()} ; :: thesis: u in Support (q - p)
then reconsider u9 = u as Element of Bags n by TARSKI:def 1;
(q - p) . u9 = (q + (- p)) . u9 by POLYNOM1:def 7
.= (q . u9) + ((- p) . u9) by POLYNOM1:15
.= (q . u9) + (- (p . u9)) by POLYNOM1:17
.= (0. L) + (- (p . u9)) by
.= (0. L) + (- (1. L)) by
.= - (1. L) by ALGSTR_1:def 2 ;
hence u in Support (q - p) by ; :: thesis: verum
end;
then A62: Support (q - p) = {()} by ;
A63: now :: thesis: not q - p is_reducible_wrt P,T
assume q - p is_reducible_wrt P,T ; :: thesis: contradiction
then consider g being Polynomial of n,L such that
A64: q - p reduces_to g,P,T by POLYRED:def 9;
consider h being Polynomial of n,L such that
A65: h in P and
A66: q - p reduces_to g,h,T by ;
ex b being bag of n st q - p reduces_to g,h,b,T by ;
then h <> 0_ (n,L) by POLYRED:def 5;
then reconsider h = h as non-zero Polynomial of n,L by POLYNOM7:def 1;
q - p is_reducible_wrt h,T by ;
then consider b9 being bag of n such that
A67: b9 in Support (q - p) and
A68: HT (h,T) divides b9 by POLYRED:36;
A69: HT (h,T) = 1bag
proof
now :: thesis: ( ( h = p & HT (h,T) = 1bag ) or ( h = q & HT (h,T) = 1bag ) )
per cases ( h = p or h = q ) by ;
case h = p ; :: thesis: HT (h,T) = 1bag
hence HT (h,T) = 1bag by ; :: thesis: verum
end;
case h = q ; :: thesis: HT (h,T) = 1bag
hence HT (h,T) = 1bag by ; :: thesis: verum
end;
end;
end;
hence HT (h,T) = 1bag ; :: thesis: verum
end;
b9 = EmptyBag n by ;
hence contradiction by A8, A68, A69, PRE_POLY:58; :: thesis: verum
end;
now :: thesis: not len s <> 1
A70: 0 + 1 <= len s by ;
A71: dom s = Seg (len s) by FINSEQ_1:def 3;
assume len s <> 1 ; :: thesis: contradiction
then 1 < len s by ;
then 1 + 1 <= len s by NAT_1:13;
then A72: 1 + 1 in dom s by ;
A73: 1 in dom s by ;
then consider f9, h9 being object such that
A74: [(q - p),(s . 2)] = [f9,h9] and
f9 in NonZero (Polynom-Ring (n,L)) and
A75: h9 in the carrier of (Polynom-Ring (n,L)) by ;
s . 2 = h9 by ;
then reconsider c9 = s . 2 as Polynomial of n,L by ;
[(q - p),(s . 2)] in PolyRedRel (P,T) by A57, A59, A73, A72;
then q - p reduces_to c9,P,T by POLYRED:def 13;
hence contradiction by A63, POLYRED:def 9; :: thesis: verum
end;
hence contradiction by A34, A57, A58; :: thesis: verum
end;
hence not P is_Groebner_basis_wrt T ; :: thesis: verum