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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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,L)then
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:15;
then
f has_a_normal_form_wrt PolyRedRel (
P,
T)
by REWRITE1:def 14;
then consider g being
object 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 11;
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
.=
(ff + (- gg)) + (- ff)
.=
(ff + (- ff)) + (- gg)
by RLVECT_1:def 3
.=
(0. (Polynom-Ring (n,L))) + (- gg)
by RLVECT_1:5
.=
- gg
by ALGSTR_1:def 2
;
then
- (- gg) in P -Ideal
by A16, IDEAL_1:14;
then A17:
g in P -Ideal
by RLVECT_1:17;
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 for a, b, c being object st [a,b] in PolyRedRel (P,T) & [a,c] in PolyRedRel (P,T) holds
b,c are_convergent_wrt PolyRedRel (P,T)let a,
b,
c be
object ;
( [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,T)consider a9,
b9 being
object 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 = b
by A23, XTUPLE_0:1;
a,
b are_convertible_wrt PolyRedRel (
P,
T)
by A20, REWRITE1:29;
then A25:
b,
a are_convertible_wrt PolyRedRel (
P,
T)
by REWRITE1:31;
consider aa,
c9 being
object 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 = c
by A27, XTUPLE_0:1;
reconsider b9 =
b9,
c9 =
c9 as
Polynomial of
n,
L by A22, A26, POLYNOM1:def 11;
reconsider bb =
b9,
cc =
c9 as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider bb =
bb,
cc =
cc as
Element of
(Polynom-Ring (n,L)) ;
a,
c are_convertible_wrt PolyRedRel (
P,
T)
by A21, REWRITE1:29;
then
bb,
cc are_congruent_mod P -Ideal
by A24, A28, A25, POLYRED:57, REWRITE1:30;
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