let n be non empty Ordinal; 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; 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 ; 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 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 ;
( {} in n & dom (EmptyBag n) = n )
by ORDINAL1:24, PARTFUN1:def 4;
then
1bag . {} = 1
by FUNCT_7:33;
then A8:
EmptyBag n <> 1bag
by PRE_POLY:52;
then A9: q . (EmptyBag n) =
((0. L) | n,L) . (EmptyBag n)
by FUNCT_7:34
.=
(0_ n,L) . (EmptyBag n)
by POLYNOM7:19
.=
0. L
by POLYNOM1:81
;
dom ((0. L) | n,L) = Bags n
by FUNCT_2:def 1;
then A14:
q . 1bag = 1. L
by FUNCT_7:33;
then A15:
q <> 0_ n,L
by POLYNOM1:81;
then A16:
Support q = {1bag}
by A11, 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 A15, POLYNOM7:def 2;
set q1 = q - (((q . (HT q,T)) / (HC q,T)) * ((EmptyBag n) *' q));
Support q <> {}
by A15, POLYNOM7:1;
then A18:
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, A18, POLYRED:def 5;
then A19:
q reduces_to q - (((q . (HT q,T)) / (HC q,T)) * ((EmptyBag n) *' q)),q,T
by POLYRED:def 6;
A20: 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 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
;
A21:
dom ((1. L) | n,L) = Bags n
by FUNCT_2:def 1;
then A22:
p . 1bag = 1. L
by FUNCT_7:33;
then A23:
p <> 0_ n,L
by A1, POLYNOM1:81;
A24: p . (EmptyBag n) =
((1. L) | n,L) . (EmptyBag n)
by A8, FUNCT_7:34
.=
(1_ n,L) . (EmptyBag n)
by POLYNOM7:20
.=
1. L
by POLYNOM1:84
;
then A26:
Support p = {(EmptyBag n),1bag}
by A5, 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 A23, POLYNOM7:def 2;
A27:
(EmptyBag n) + (HT p,T) = HT p,T
by PRE_POLY:53;
set p1 = q - (((q . (HT p,T)) / (HC p,T)) * ((EmptyBag n) *' p));
Support p <> {}
by A23, POLYNOM7:1;
then A31:
HT p,T in Support p
by TERMORD:def 6;
then A32:
HT p,T = 1bag
by A26, A28, 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 A23, A15, A27, POLYRED:def 5;
then A33:
q reduces_to q - (((q . (HT p,T)) / (HC p,T)) * ((EmptyBag n) *' p)),p,T
by POLYRED: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
; not P is_Groebner_basis_wrt T
A36:
p in P
by TARSKI:def 2;
q in P
by TARSKI:def 2;
then
q reduces_to 0_ n,L,P,T
by A19, A20, POLYRED:def 7;
then A37:
[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, A32, TERMORD:def 7
.=
q - (((1. L) / (1. L)) * ((EmptyBag n) *' p))
by A21, 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
;
then
q reduces_to q - p,P,T
by A33, A36, POLYRED:def 7;
then A38:
[q,(q - p)] in PolyRedRel P,T
by POLYRED:def 13;
now A39:
now let u be
set ;
( u in Support (q - p) implies u in {(EmptyBag n)} )then
{1bag} c= {(EmptyBag n),1bag}
by TARSKI:def 3;
then A40:
{1bag} \/ {(EmptyBag n),1bag} = {(EmptyBag n),1bag}
by XBOOLE_1:12;
A41:
(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 A21, A14, FUNCT_7:33
.=
0. L
by RLVECT_1:16
;
Support (q - p) = Support (q + (- p))
by POLYNOM1:def 23;
then
Support (q - p) c= (Support q) \/ (Support (- p))
by POLYNOM1:79;
then A42:
Support (q - p) c= {1bag} \/ {(EmptyBag n),1bag}
by A26, A16, Th5;
assume A43:
u in Support (q - p)
;
u in {(EmptyBag n)}then
(q - p) . u <> 0. L
by POLYNOM1:def 9;
then
u = EmptyBag n
by A43, A42, A40, A41, TARSKI:def 2;
hence
u in {(EmptyBag n)}
by TARSKI:def 1;
verum end; assume
PolyRedRel P,
T is
locally-confluent
;
contradictionthen
0_ n,
L,
q - p are_convergent_wrt PolyRedRel P,
T
by A38, A37, REWRITE1:def 24;
then consider c being
set such that A44:
PolyRedRel P,
T reduces 0_ n,
L,
c
and A45:
PolyRedRel P,
T reduces q - p,
c
by REWRITE1:def 7;
reconsider c =
c as
Polynomial of
n,
L by A44, Lm4;
consider s being
FinSequence such that A46:
len s > 0
and A47:
s . 1
= 0_ n,
L
and A48:
s . (len s) = c
and A49:
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 A44, REWRITE1:12;
now A50:
0 + 1
<= len s
by A46, NAT_1:13;
A51:
dom s = Seg (len s)
by FINSEQ_1:def 3;
assume
len s <> 1
;
contradictionthen
1
< len s
by A50, XXREAL_0:1;
then
1
+ 1
<= len s
by NAT_1:13;
then A52:
1
+ 1
in dom s
by A51, FINSEQ_1:3;
A53:
1
in dom s
by A50, A51, FINSEQ_1:3;
then consider f9,
h9 being
set such that A54:
[(0_ n,L),(s . 2)] = [f9,h9]
and
f9 in NonZero (Polynom-Ring n,L)
and A55:
h9 in the
carrier of
(Polynom-Ring n,L)
by A47, A49, A52, RELSET_1:6;
s . 2 =
[f9,h9] `2
by A54, MCART_1:def 2
.=
h9
by MCART_1:def 2
;
then reconsider c9 =
s . 2 as
Polynomial of
n,
L by A55, POLYNOM1:def 27;
[(s . 1),(s . 2)] in PolyRedRel P,
T
by A49, A53, A52;
then
0_ n,
L reduces_to c9,
P,
T
by A47, POLYRED:def 13;
then consider g being
Polynomial of
n,
L such that
g in P
and A56:
0_ n,
L reduces_to c9,
g,
T
by POLYRED:def 7;
0_ n,
L is_reducible_wrt g,
T
by A56, POLYRED:def 8;
hence
contradiction
by POLYRED:37;
verum end; then consider s being
FinSequence such that A57:
len s > 0
and A58:
s . 1
= q - p
and A59:
s . (len s) = 0_ n,
L
and A60:
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 A45, A47, A48, REWRITE1:12;
then A63:
Support (q - p) = {(EmptyBag n)}
by A39, TARSKI:2;
A64:
now assume
q - p is_reducible_wrt P,
T
;
contradictionthen consider g being
Polynomial of
n,
L such that A65:
q - p reduces_to g,
P,
T
by POLYRED:def 9;
consider h being
Polynomial of
n,
L such that A66:
h in P
and A67:
q - p reduces_to g,
h,
T
by A65, POLYRED:def 7;
ex
b being
bag of
n st
q - p reduces_to g,
h,
b,
T
by A67, 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 2;
q - p is_reducible_wrt h,
T
by A67, POLYRED:def 8;
then consider b9 being
bag of
n such that A68:
b9 in Support (q - p)
and A69:
HT h,
T divides b9
by POLYRED:36;
A70:
HT h,
T = 1bag
b9 = EmptyBag n
by A63, A68, TARSKI:def 1;
hence
contradiction
by A8, A69, A70, PRE_POLY:58;
verum end; now A71:
0 + 1
<= len s
by A57, NAT_1:13;
A72:
dom s = Seg (len s)
by FINSEQ_1:def 3;
assume
len s <> 1
;
contradictionthen
1
< len s
by A71, XXREAL_0:1;
then
1
+ 1
<= len s
by NAT_1:13;
then A73:
1
+ 1
in dom s
by A72, FINSEQ_1:3;
A74:
1
in dom s
by A71, A72, FINSEQ_1:3;
then consider f9,
h9 being
set such that A75:
[(q - p),(s . 2)] = [f9,h9]
and
f9 in NonZero (Polynom-Ring n,L)
and A76:
h9 in the
carrier of
(Polynom-Ring n,L)
by A58, A60, A73, RELSET_1:6;
s . 2 =
[f9,h9] `2
by A75, MCART_1:def 2
.=
h9
by MCART_1:def 2
;
then reconsider c9 =
s . 2 as
Polynomial of
n,
L by A76, POLYNOM1:def 27;
[(q - p),(s . 2)] in PolyRedRel P,
T
by A58, A60, A74, A73;
then
q - p reduces_to c9,
P,
T
by POLYRED:def 13;
hence
contradiction
by A64, POLYRED:def 9;
verum end; hence
contradiction
by A35, A58, A59;
verum
hence
not P is_Groebner_basis_wrt T
by Def3; verum