let n be Element of NAT ; 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 Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st HT (P -Ideal ),T c= multiples (HT P,T) holds
PolyRedRel P,T is locally-confluent
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 Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st HT (P -Ideal ),T c= multiples (HT P,T) holds
PolyRedRel P,T is locally-confluent
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; for P being Subset of (Polynom-Ring n,L) st HT (P -Ideal ),T c= multiples (HT P,T) holds
PolyRedRel P,T is locally-confluent
let P be Subset of (Polynom-Ring n,L); ( HT (P -Ideal ),T c= multiples (HT P,T) implies PolyRedRel P,T is locally-confluent )
set R = PolyRedRel P,T;
assume A1:
HT (P -Ideal ),T c= multiples (HT P,T)
; PolyRedRel P,T is locally-confluent
A2:
for f being Polynomial of n,L st f in P -Ideal & f <> 0_ n,L holds
f is_reducible_wrt P,T
proof
let f be
Polynomial of
n,
L;
( f in P -Ideal & f <> 0_ n,L implies f is_reducible_wrt P,T )
assume that A3:
f in P -Ideal
and A4:
f <> 0_ n,
L
;
f is_reducible_wrt P,T
HT f,
T in { (HT p,T) where p is Polynomial of n,L : ( p in P -Ideal & p <> 0_ n,L ) }
by A3, A4;
then
HT f,
T in multiples (HT P,T)
by A1;
then
ex
b being
Element of
Bags n st
(
b = HT f,
T & ex
b9 being
bag of
n st
(
b9 in HT P,
T &
b9 divides b ) )
;
then consider b9 being
bag of
n such that A5:
b9 in HT P,
T
and A6:
b9 divides HT f,
T
;
consider p being
Polynomial of
n,
L such that A7:
b9 = HT p,
T
and A8:
p in P
and A9:
p <> 0_ n,
L
by A5;
consider s being
bag of
n such that A10:
b9 + s = HT f,
T
by A6, TERMORD:1;
set g =
f - (((f . (HT f,T)) / (HC p,T)) * (s *' p));
Support f <> {}
by A4, POLYNOM7:1;
then
HT f,
T in Support f
by TERMORD:def 6;
then
f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),
p,
HT f,
T,
T
by A4, A7, A9, A10, POLYRED:def 5;
then
f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),
p,
T
by POLYRED:def 6;
then
f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),
P,
T
by A8, POLYRED:def 7;
hence
f is_reducible_wrt P,
T
by POLYRED:def 9;
verum
end;
A11:
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
proof
let f be
Polynomial of
n,
L;
( f in P -Ideal implies PolyRedRel P,T reduces f, 0_ n,L )
assume A12:
f in P -Ideal
;
PolyRedRel P,T reduces f, 0_ n,L
per cases
( f = 0_ n,L or f <> 0_ n,L )
;
suppose
f <> 0_ n,
L
;
PolyRedRel P,T reduces f, 0_ n,Lthen
f is_reducible_wrt P,
T
by A2, A12;
then consider v being
Polynomial of
n,
L such that A13:
f reduces_to v,
P,
T
by POLYRED:def 9;
[f,v] in PolyRedRel P,
T
by A13, POLYRED:def 13;
then
f in field (PolyRedRel P,T)
by RELAT_1:30;
then
f has_a_normal_form_wrt PolyRedRel P,
T
by REWRITE1:def 14;
then consider g being
set such that A14:
g is_a_normal_form_of f,
PolyRedRel P,
T
by REWRITE1:def 11;
A15:
PolyRedRel P,
T reduces f,
g
by A14, REWRITE1:def 6;
then reconsider g9 =
g as
Polynomial of
n,
L by Lm4;
reconsider ff =
f,
gg =
g9 as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider ff =
ff,
gg =
gg as
Element of
(Polynom-Ring n,L) ;
f - g9 = ff - gg
by Lm2;
then
ff - gg in P -Ideal
by A15, POLYRED:59;
then A16:
(ff - gg) - ff in P -Ideal
by A12, IDEAL_1:16;
(ff - gg) - ff =
(ff + (- gg)) - ff
by RLVECT_1:def 14
.=
(ff + (- gg)) + (- ff)
by RLVECT_1:def 14
.=
(ff + (- ff)) + (- gg)
by RLVECT_1:def 6
.=
(0. (Polynom-Ring n,L)) + (- gg)
by RLVECT_1:16
.=
- gg
by ALGSTR_1:def 5
;
then
- (- gg) in P -Ideal
by A16, IDEAL_1:14;
then A17:
g in P -Ideal
by RLVECT_1:30;
assume
not
PolyRedRel P,
T reduces f,
0_ n,
L
;
contradictionthen
g <> 0_ n,
L
by A14, REWRITE1:def 6;
then
g9 is_reducible_wrt P,
T
by A2, A17;
then consider u being
Polynomial of
n,
L such that A18:
g9 reduces_to u,
P,
T
by POLYRED:def 9;
A19:
[g9,u] in PolyRedRel P,
T
by A18, POLYRED:def 13;
g is_a_normal_form_wrt PolyRedRel P,
T
by A14, REWRITE1:def 6;
hence
contradiction
by A19, REWRITE1:def 5;
verum end;
end;
now let a,
b,
c be
set ;
( [a,b] in PolyRedRel P,T & [a,c] in PolyRedRel P,T implies b,c are_convergent_wrt PolyRedRel P,T )assume that A20:
[a,b] in PolyRedRel P,
T
and A21:
[a,c] in PolyRedRel P,
T
;
b,c are_convergent_wrt PolyRedRel P,Tconsider a9,
b9 being
set such that
a9 in NonZero (Polynom-Ring n,L)
and A22:
b9 in the
carrier of
(Polynom-Ring n,L)
and A23:
[a,b] = [a9,b9]
by A20, ZFMISC_1:def 2;
A24:
b9 =
[a,b] `2
by A23, MCART_1:def 2
.=
b
by MCART_1:def 2
;
a,
b are_convertible_wrt PolyRedRel P,
T
by A20, REWRITE1:30;
then A25:
b,
a are_convertible_wrt PolyRedRel P,
T
by REWRITE1:32;
consider aa,
c9 being
set such that
aa in NonZero (Polynom-Ring n,L)
and A26:
c9 in the
carrier of
(Polynom-Ring n,L)
and A27:
[a,c] = [aa,c9]
by A21, ZFMISC_1:def 2;
A28:
c9 =
[a,c] `2
by A27, MCART_1:def 2
.=
c
by MCART_1:def 2
;
reconsider b9 =
b9,
c9 =
c9 as
Polynomial of
n,
L by A22, A26, POLYNOM1:def 27;
reconsider bb =
b9,
cc =
c9 as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider bb =
bb,
cc =
cc as
Element of
(Polynom-Ring n,L) ;
a,
c are_convertible_wrt PolyRedRel P,
T
by A21, REWRITE1:30;
then
bb,
cc are_congruent_mod P -Ideal
by A24, A28, A25, POLYRED:57, REWRITE1:31;
then A29:
bb - cc in P -Ideal
by POLYRED:def 14;
b9 - c9 = bb - cc
by Lm2;
hence
b,
c are_convergent_wrt PolyRedRel P,
T
by A11, A24, A28, A29, POLYRED:50;
verum end;
hence
PolyRedRel P,T is locally-confluent
by REWRITE1:def 24; verum