let n be non empty Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
set 1bag = (EmptyBag n) +* ({},1);
reconsider 1bag = (EmptyBag n) +* ({},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:

let u be bag of n; :: thesis:
assume that
A3: u <> EmptyBag n and
A4: u <> 1bag ; :: thesis:
p . u = ((1. L) | (n,L)) . u by A4, FUNCT_7:32;
then p . u = (1_ (n,L)) . u by POLYNOM7:20;
hence p . u = 0. L by A3, POLYNOM1:25; :: thesis:

end;

A5: now :: thesis:

let u9 be object ; :: thesis:
assume A6: u9 in Support p ; :: thesis:
then reconsider u = u9 as Element of Bags n ;
A7: p . u <> 0. L by A6, POLYNOM1:def 4;

now :: thesis:

assume not u in {(EmptyBag n),1bag} ; :: thesis:
then ( u <> EmptyBag n & u <> 1bag ) by TARSKI:def 2;
hence contradiction by A2, A7; :: thesis:

end;

hence u9 in {(EmptyBag n),1bag} ; :: thesis:

end;

( {} in n & dom (EmptyBag n) = n ) by ORDINAL1:14, PARTFUN1:def 2;
then 1bag . {} = 1 by FUNCT_7:31;
then A8: EmptyBag n <> 1bag by PBOOLE:5;
then A9: q . (EmptyBag n) = ((0. L) | (n,L)) . (EmptyBag n) by FUNCT_7:32
.= (0_ (n,L)) . (EmptyBag n) by POLYNOM7:19
.= 0. L by POLYNOM1:22 ;

A10: now :: thesis:

let u be bag of n; :: thesis:
assume u <> 1bag ; :: thesis:
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:

end;

A11: now :: thesis:

let u9 be object ; :: thesis:
assume A12: u9 in Support q ; :: thesis:
then reconsider u = u9 as Element of Bags n ;
A13: q . u <> 0. L by A12, POLYNOM1:def 4;

now :: thesis:

assume not u in {1bag} ; :: thesis:
then u <> 1bag by TARSKI:def 1;
hence contradiction by A10, A13; :: thesis:

end;

hence u9 in {1bag} ; :: thesis:

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:

let u be object ; :: thesis:
assume u in {1bag} ; :: thesis:
then u = 1bag by TARSKI:def 1;
hence u in Support q by A14, POLYNOM1:def 4; :: thesis:

end;

then A16: Support q = {1bag} by A11, TARSKI:2;
then reconsider q = q as Polynomial of n,L by POLYNOM1:def 5;
reconsider q = q as non-zero Polynomial of n,L by A15, POLYNOM7:def 1;
set q1 = q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q));
Support q <> {} by A15, POLYNOM7:1;
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))) * ((EmptyBag n) *' q)),q, HT (q,T),T by A15, A17, POLYRED:def 5;
then A18: q reduces_to q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)),q,T by POLYRED:def 6;
A19: q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)) = q - (((HC (q,T)) / (HC (q,T))) * ((EmptyBag n) *' q)) by TERMORD:def 7
.= q - (((HC (q,T)) * ((HC (q,T)) ")) * ((EmptyBag n) *' q))
.= q - ((1. L) * ((EmptyBag n) *' 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 A1, POLYNOM1:22;
A23: p . (EmptyBag n) = ((1. L) | (n,L)) . (EmptyBag n) by A8, FUNCT_7:32
.= (1_ (n,L)) . (EmptyBag n) by POLYNOM7:20
.= 1. L by POLYNOM1:25 ;

now :: thesis:

let u be object ; :: thesis:
assume A24: u in {(EmptyBag n),1bag} ; :: thesis:

now :: thesis:

per cases by A24, TARSKI:def 2;

case u = EmptyBag n ; :: thesis:

hence u in Support p by A1, A23, POLYNOM1:def 4; :: thesis:

end;

case u = 1bag ; :: thesis:

hence u in Support p by A1, A21, POLYNOM1:def 4; :: thesis:

end;

hence u in Support p ; :: thesis:

end;

then A25: Support p = {(EmptyBag n),1bag} by A5, TARSKI:2;
then reconsider p = p as Polynomial of n,L by POLYNOM1:def 5;
reconsider p = p as non-zero Polynomial of n,L by A22, POLYNOM7:def 1;
A26: (EmptyBag n) + (HT (p,T)) = HT (p,T) by PRE_POLY:53;

A27: now :: thesis:

A28: EmptyBag n <= 1bag,T by TERMORD:9;
assume A29: HT (p,T) = EmptyBag n ; :: thesis:
1bag in Support p by A25, TARSKI:def 2;
then 1bag <= EmptyBag n,T by A29, TERMORD:def 6;
hence contradiction by A8, A28, TERMORD:7; :: thesis:

end;

set p1 = q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p));
Support p <> {} by A22, POLYNOM7:1;
then A30: HT (p,T) in Support p by TERMORD:def 6;
then A31: HT (p,T) = 1bag by A25, A27, TARSKI:def 2;
then HT (p,T) in Support q by A16, TARSKI:def 1;
then q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)),p, HT (p,T),T by A22, A15, A26, POLYRED:def 5;
then A32: q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)),p,T by POLYRED:def 6;

A33: now :: thesis:

assume Support q = Support p ; :: thesis:
then EmptyBag n in {1bag} by A25, A16, TARSKI:def 2;
hence contradiction by A8, TARSKI:def 1; :: thesis:

end;

A34: now :: thesis:

assume q - p = 0_ (n,L) ; :: thesis:
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:

end;

set P = {p,q};

now :: thesis:

let u be object ; :: thesis:
assume u in {p,q} ; :: thesis:
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:

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 A18, A19, POLYRED:def 7;
then A36: [q,(0_ (n,L))] in PolyRedRel (P,T) by POLYRED:def 13;
q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)) = q - (((1. L) / (p . 1bag)) * ((EmptyBag n) *' p)) by A14, A31, TERMORD:def 7
.= q - (((1. L) / (1. L)) * ((EmptyBag n) *' p)) by A20, FUNCT_7:31
.= q - (((1. L) * ((1. L) ")) * ((EmptyBag n) *' p))
.= q - ((1. L) * ((EmptyBag n) *' 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 A32, A35, POLYRED:def 7;
then A37: [q,(q - p)] in PolyRedRel (P,T) by POLYRED:def 13;

now :: thesis:

A38: now :: thesis:

let u be object ; :: thesis:

now :: thesis:

let u be object ; :: thesis:
assume u in {1bag} ; :: thesis:
then u = 1bag by TARSKI:def 1;
hence u in {(EmptyBag n),1bag} by TARSKI:def 2; :: thesis:

end;

then {1bag} c= {(EmptyBag n),1bag} ;
then A39: {1bag} \/ {(EmptyBag n),1bag} = {(EmptyBag n),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 A20, A14, FUNCT_7:31
.= 0. L by RLVECT_1:5 ;
Support (q - p) = Support (q + (- p)) by POLYNOM1:def 7;
then Support (q - p) c= (Support q) \/ (Support (- p)) by POLYNOM1:20;
then A41: Support (q - p) c= {1bag} \/ {(EmptyBag n),1bag} by A25, A16, Th5;
assume A42: u in Support (q - p) ; :: thesis:
then (q - p) . u <> 0. L by POLYNOM1:def 4;
then u = EmptyBag n by A42, A41, A39, A40, TARSKI:def 2;
hence u in {(EmptyBag n)} by TARSKI:def 1; :: thesis:

end;

assume PolyRedRel (P,T) is locally-confluent ; :: thesis:
then 0_ (n,L),q - p are_convergent_wrt PolyRedRel (P,T) by A37, A36, REWRITE1:def 24;
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 A43, Lm4;
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 A43, REWRITE1:11;

now :: thesis:

A49: 0 + 1 <= len s by A45, NAT_1:13;
A50: dom s = Seg (len s) by FINSEQ_1:def 3;
assume len s <> 1 ; :: thesis:
then 1 < len s by A49, XXREAL_0:1;
then 1 + 1 <= len s by NAT_1:13;
then A51: 1 + 1 in dom s by A50, FINSEQ_1:1;
A52: 1 in dom s by A49, A50, FINSEQ_1:1;
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 A46, A48, A51, RELSET_1:2;
s . 2 = h9 by A53, XTUPLE_0:1;
then reconsider c9 = s . 2 as Polynomial of n,L by A54, POLYNOM1:def 11;
[(s . 1),(s . 2)] in PolyRedRel (P,T) by A48, A52, A51;
then 0_ (n,L) reduces_to c9,P,T by A46, POLYRED:def 13;
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 A55, POLYRED:def 8;
hence contradiction by POLYRED:37; :: thesis:

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 A44, A46, A47, REWRITE1:11;

A60: now :: thesis:

assume - (1. L) = 0. L ; :: thesis:
then - (- (1. L)) = 0. L by RLVECT_1:12;
hence contradiction by RLVECT_1:17; :: thesis:

end;

now :: thesis:

let u be object ; :: thesis:
assume A61: u in {(EmptyBag n)} ; :: thesis:
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 A9, A61, TARSKI:def 1
.= (0. L) + (- (1. L)) by A23, A61, TARSKI:def 1
.= - (1. L) by ALGSTR_1:def 2 ;
hence u in Support (q - p) by A60, POLYNOM1:def 4; :: thesis:

end;

then A62: Support (q - p) = {(EmptyBag n)} by A38, TARSKI:2;

A63: now :: thesis:

assume q - p is_reducible_wrt P,T ; :: thesis:
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 A64, POLYRED:def 7;
ex b being bag of n st q - p reduces_to g,h,b,T by A66, POLYRED:def 6;
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 A66, POLYRED:def 8;
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:

per cases by A65, TARSKI:def 2;

case h = p ; :: thesis:

hence HT (h,T) = 1bag by A25, A30, A27, TARSKI:def 2; :: thesis:

end;

case h = q ; :: thesis:

hence HT (h,T) = 1bag by A16, A17, TARSKI:def 1; :: thesis:

end;

hence HT (h,T) = 1bag ; :: thesis:

end;

b9 = EmptyBag n by A62, A67, TARSKI:def 1;
hence contradiction by A8, A68, A69, PRE_POLY:58; :: thesis:

end;

now :: thesis:

A70: 0 + 1 <= len s by A56, NAT_1:13;
A71: dom s = Seg (len s) by FINSEQ_1:def 3;
assume len s <> 1 ; :: thesis:
then 1 < len s by A70, XXREAL_0:1;
then 1 + 1 <= len s by NAT_1:13;
then A72: 1 + 1 in dom s by A71, FINSEQ_1:1;
A73: 1 in dom s by A70, A71, FINSEQ_1:1;
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 A57, A59, A72, RELSET_1:2;
s . 2 = h9 by A74, XTUPLE_0:1;
then reconsider c9 = s . 2 as Polynomial of n,L by A75, POLYNOM1:def 11;
[(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:

end;

hence contradiction by A34, A57, A58; :: thesis:

end;

hence not P is_Groebner_basis_wrt T ; :: thesis: