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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: not for P being Subset of (Polynom-Ring n,L) holds P is_Groebner_basis_wrt T
set 1bag = (EmptyBag n) +* {} ,1;
reconsider 1bag = (EmptyBag n) +* {} ,1 as Element of Bags n by POLYNOM1:def 14;
A1:
{} in n
by ORDINAL1:24;
dom (EmptyBag n) = n
by PBOOLE:def 3;
then
1bag . {} = 1
by A1, FUNCT_7:33;
then A2:
EmptyBag n <> 1bag
by POLYNOM1:56;
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 ;
A3:
1. L <> 0. L
;
A4:
dom ((1. L) | n,L) = Bags n
by FUNCT_2:def 1;
then A5:
p . 1bag = 1. L
by FUNCT_7:33;
then A6:
p <> 0_ n,L
by A3, POLYNOM1:81;
A7: p . (EmptyBag n) =
((1. L) | n,L) . (EmptyBag n)
by A2, FUNCT_7:34
.=
(1_ n,L) . (EmptyBag n)
by POLYNOM7:20
.=
1. L
by POLYNOM1:84
;
then A14:
Support p = {(EmptyBag n),1bag}
by A10, TARSKI:2;
then reconsider p = p as Polynomial of n,L by POLYNOM1:def 10;
reconsider p = p as non-zero Polynomial of n,L by A6, POLYNOM7:def 2;
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 ;
dom ((0. L) | n,L) = Bags n
by FUNCT_2:def 1;
then A15:
q . 1bag = 1. L
by FUNCT_7:33;
then A16:
q <> 0_ n,L
by POLYNOM1:81;
A17: q . (EmptyBag n) =
((0. L) | n,L) . (EmptyBag n)
by A2, FUNCT_7:34
.=
(0_ n,L) . (EmptyBag n)
by POLYNOM7:19
.=
0. L
by POLYNOM1:81
;
then A22:
Support q = {1bag}
by A19, TARSKI:2;
then reconsider q = q as Polynomial of n,L by POLYNOM1:def 10;
reconsider q = q as non-zero Polynomial of n,L by A16, POLYNOM7:def 2;
Support p <> {}
by A6, POLYNOM7:1;
then A23:
HT p,T in Support p
by TERMORD:def 6;
then A27:
HT p,T = 1bag
by A14, A23, TARSKI:def 2;
Support q <> {}
by A16, POLYNOM7:1;
then A28:
HT q,T in Support q
by TERMORD:def 6;
set P = {p,q};
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: not P is_Groebner_basis_wrt T
set p1 = q - (((q . (HT p,T)) / (HC p,T)) * ((EmptyBag n) *' p));
A29:
HT p,T in Support q
by A22, A27, TARSKI:def 1;
(EmptyBag n) + (HT p,T) = HT p,T
by POLYNOM1:57;
then
q reduces_to q - (((q . (HT p,T)) / (HC p,T)) * ((EmptyBag n) *' p)),p, HT p,T,T
by A6, A16, A29, POLYRED:def 5;
then A30:
q reduces_to q - (((q . (HT p,T)) / (HC p,T)) * ((EmptyBag n) *' p)),p,T
by POLYRED:def 6;
A31: q - (((q . (HT p,T)) / (HC p,T)) * ((EmptyBag n) *' p)) =
q - (((1. L) / (p . 1bag)) * ((EmptyBag n) *' p))
by A15, A27, TERMORD:def 7
.=
q - (((1. L) / (1. L)) * ((EmptyBag n) *' p))
by A4, FUNCT_7:33
.=
q - (((1. L) * ((1. L) " )) * ((EmptyBag n) *' p))
by VECTSP_1:def 23
.=
q - ((1. L) * ((EmptyBag n) *' p))
by VECTSP_1:def 22
.=
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:89
;
p in P
by TARSKI:def 2;
then
q reduces_to q - p,P,T
by A30, A31, POLYRED:def 7;
then A32:
[q,(q - p)] in PolyRedRel P,T
by POLYRED:def 13;
set q1 = q - (((q . (HT q,T)) / (HC q,T)) * ((EmptyBag n) *' q));
(EmptyBag n) + (HT q,T) = HT q,T
by POLYNOM1:57;
then
q reduces_to q - (((q . (HT q,T)) / (HC q,T)) * ((EmptyBag n) *' q)),q, HT q,T,T
by A16, A28, POLYRED:def 5;
then A33:
q reduces_to q - (((q . (HT q,T)) / (HC q,T)) * ((EmptyBag n) *' q)),q,T
by POLYRED:def 6;
A34:
HC q,T <> 0. L
by A16, TERMORD:17;
A35: 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))
by VECTSP_1:def 23
.=
q - ((1. L) * ((EmptyBag n) *' q))
by A34, VECTSP_1:def 22
.=
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:89
.=
0_ n,L
by POLYNOM1:83
;
q in P
by TARSKI:def 2;
then
q reduces_to 0_ n,L,P,T
by A33, A35, POLYRED:def 7;
then A36:
[q,(0_ n,L)] in PolyRedRel P,T
by POLYRED:def 13;
now assume
PolyRedRel P,
T is
locally-confluent
;
:: thesis: contradictionthen
0_ n,
L,
q - p are_convergent_wrt PolyRedRel P,
T
by A32, A36, REWRITE1:def 24;
then consider c being
set such that A39:
(
PolyRedRel P,
T reduces 0_ n,
L,
c &
PolyRedRel P,
T reduces q - p,
c )
by REWRITE1:def 7;
reconsider c =
c as
Polynomial of
n,
L by A39, Lm4;
consider s being
FinSequence such that A40:
(
len s > 0 &
s . 1
= 0_ n,
L &
s . (len s) = c & ( for
i being
Element of
NAT st
i in dom s &
i + 1
in dom s holds
[(s . i),(s . (i + 1))] in PolyRedRel P,
T ) )
by A39, REWRITE1:12;
A41:
now assume A42:
len s <> 1
;
:: thesis: contradictionA43:
0 + 1
<= len s
by A40, NAT_1:13;
then
1
< len s
by A42, XXREAL_0:1;
then A44:
1
+ 1
<= len s
by NAT_1:13;
A45:
dom s = Seg (len s)
by FINSEQ_1:def 3;
then A46:
1
in dom s
by A43, FINSEQ_1:3;
1
+ 1
in dom s
by A44, A45, FINSEQ_1:3;
then A47:
[(s . 1),(s . 2)] in PolyRedRel P,
T
by A40, A46;
then consider f',
h' being
set such that A48:
(
[(0_ n,L),(s . 2)] = [f',h'] &
f' in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
h' in the
carrier of
(Polynom-Ring n,L) )
by A40, RELSET_1:6;
s . 2 =
[f',h'] `2
by A48, MCART_1:def 2
.=
h'
by MCART_1:def 2
;
then reconsider c' =
s . 2 as
Polynomial of
n,
L by A48, POLYNOM1:def 27;
0_ n,
L reduces_to c',
P,
T
by A40, A47, POLYRED:def 13;
then consider g being
Polynomial of
n,
L such that A49:
(
g in P &
0_ n,
L reduces_to c',
g,
T )
by POLYRED:def 7;
0_ n,
L is_reducible_wrt g,
T
by A49, POLYRED:def 8;
hence
contradiction
by POLYRED:37;
:: thesis: verum end; now let u be
set ;
:: thesis: ( u in Support (q - p) implies u in {(EmptyBag n)} )assume A53:
u in Support (q - p)
;
:: thesis: u in {(EmptyBag n)}then A54:
(q - p) . u <> 0. L
by POLYNOM1:def 9;
Support (q - p) = Support (q + (- p))
by POLYNOM1:def 23;
then
Support (q - p) c= (Support q) \/ (Support (- p))
by POLYNOM1:79;
then A55:
Support (q - p) c= {1bag} \/ {(EmptyBag n),1bag}
by A14, A22, Th5;
then
{1bag} c= {(EmptyBag n),1bag}
by TARSKI:def 3;
then A56:
{1bag} \/ {(EmptyBag n),1bag} = {(EmptyBag n),1bag}
by XBOOLE_1:12;
(q - p) . 1bag =
(q + (- p)) . 1bag
by POLYNOM1:def 23
.=
(q . 1bag) + ((- p) . 1bag)
by POLYNOM1:def 21
.=
(q . 1bag) + (- (p . 1bag))
by POLYNOM1:def 22
.=
(1. L) + (- (1. L))
by A4, A15, FUNCT_7:33
.=
0. L
by RLVECT_1:16
;
then
u = EmptyBag n
by A53, A54, A55, A56, TARSKI:def 2;
hence
u in {(EmptyBag n)}
by TARSKI:def 1;
:: thesis: verum end; then A57:
Support (q - p) = {(EmptyBag n)}
by A51, TARSKI:2;
A58:
now assume
q - p is_reducible_wrt P,
T
;
:: thesis: contradictionthen consider g being
Polynomial of
n,
L such that A59:
q - p reduces_to g,
P,
T
by POLYRED:def 9;
consider h being
Polynomial of
n,
L such that A60:
(
h in P &
q - p reduces_to g,
h,
T )
by A59, POLYRED:def 7;
consider b being
bag of
n such that A61:
q - p reduces_to g,
h,
b,
T
by A60, POLYRED:def 6;
(
q - p <> 0_ n,
L &
h <> 0_ n,
L &
b in Support (q - p) & ex
s being
bag of
n st
(
s + (HT h,T) = b &
g = (q - p) - ((((q - p) . b) / (HC h,T)) * (s *' h)) ) )
by A61, POLYRED:def 5;
then reconsider h =
h as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
q - p is_reducible_wrt h,
T
by A60, POLYRED:def 8;
then consider b' being
bag of
n such that A62:
(
b' in Support (q - p) &
HT h,
T divides b' )
by POLYRED:36;
A63:
b' = EmptyBag n
by A57, A62, TARSKI:def 1;
HT h,
T = 1bag
hence
contradiction
by A2, A62, A63, POLYNOM1:62;
:: thesis: verum end; consider s being
FinSequence such that A64:
(
len s > 0 &
s . 1
= q - p &
s . (len s) = 0_ n,
L & ( for
i being
Element of
NAT st
i in dom s &
i + 1
in dom s holds
[(s . i),(s . (i + 1))] in PolyRedRel P,
T ) )
by A39, A40, A41, REWRITE1:12;
now assume A65:
len s <> 1
;
:: thesis: contradictionA66:
0 + 1
<= len s
by A64, NAT_1:13;
then
1
< len s
by A65, XXREAL_0:1;
then A67:
1
+ 1
<= len s
by NAT_1:13;
A68:
dom s = Seg (len s)
by FINSEQ_1:def 3;
then A69:
1
in dom s
by A66, FINSEQ_1:3;
1
+ 1
in dom s
by A67, A68, FINSEQ_1:3;
then A70:
[(q - p),(s . 2)] in PolyRedRel P,
T
by A64, A69;
then consider f',
h' being
set such that A71:
(
[(q - p),(s . 2)] = [f',h'] &
f' in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
h' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
s . 2 =
[f',h'] `2
by A71, MCART_1:def 2
.=
h'
by MCART_1:def 2
;
then reconsider c' =
s . 2 as
Polynomial of
n,
L by A71, POLYNOM1:def 27;
q - p reduces_to c',
P,
T
by A70, POLYRED:def 13;
hence
contradiction
by A58, POLYRED:def 9;
:: thesis: verum end; hence
contradiction
by A38, A64;
:: thesis: verum end;
hence
not P is_Groebner_basis_wrt T
by Def3; :: thesis: verum