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
proof
hence
HT (
h,
T)
= 1bag
;
verum
end;
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