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 ex p being Polynomial of n,L st
( p in P & P -Ideal = {p} -Ideal ) 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 ex p being Polynomial of n,L st
( p in P & P -Ideal = {p} -Ideal ) 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 ex p being Polynomial of n,L st
( p in P & P -Ideal = {p} -Ideal ) holds
PolyRedRel (P,T) is locally-confluent
let P be Subset of (Polynom-Ring (n,L)); ( ex p being Polynomial of n,L st
( p in P & P -Ideal = {p} -Ideal ) implies PolyRedRel (P,T) is locally-confluent )
set R = PolyRedRel (P,T);
assume
ex p being Polynomial of n,L st
( p in P & P -Ideal = {p} -Ideal )
; PolyRedRel (P,T) is locally-confluent
then consider p being Polynomial of n,L such that
A1:
p in P
and
A2:
P -Ideal = {p} -Ideal
;
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)set Rp =
PolyRedRel (
{p},
T);
reconsider Rp =
PolyRedRel (
{p},
T) as
strongly-normalizing locally-confluent Relation by Th10;
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 A3:
[a,b] in PolyRedRel (
P,
T)
and A4:
[a,c] in PolyRedRel (
P,
T)
;
b,c are_convergent_wrt PolyRedRel (P,T)
a,
b are_convertible_wrt PolyRedRel (
P,
T)
by A3, REWRITE1:29;
then A5:
b,
a are_convertible_wrt PolyRedRel (
P,
T)
by REWRITE1:31;
consider pa,
pb being
object such that
pa in NonZero (Polynom-Ring (n,L))
and A6:
pb in the
carrier of
(Polynom-Ring (n,L))
and A7:
[a,b] = [pa,pb]
by A3, ZFMISC_1:def 2;
reconsider pb =
pb as
Polynomial of
n,
L by A6, POLYNOM1:def 11;
A8:
pb = b
by A7, XTUPLE_0:1;
consider pa9,
pc being
object such that
pa9 in NonZero (Polynom-Ring (n,L))
and A9:
pc in the
carrier of
(Polynom-Ring (n,L))
and A10:
[a,c] = [pa9,pc]
by A4, ZFMISC_1:def 2;
reconsider pc =
pc as
Polynomial of
n,
L by A9, POLYNOM1:def 11;
A11:
pc = c
by A10, XTUPLE_0:1;
reconsider pb9 =
pb,
pc9 =
pc as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider pc9 =
pc9,
pb9 =
pb9 as
Element of
(Polynom-Ring (n,L)) ;
a,
c are_convertible_wrt PolyRedRel (
P,
T)
by A4, REWRITE1:29;
then
pb9,
pc9 are_congruent_mod {p} -Ideal
by A2, A8, A11, A5, POLYRED:57, REWRITE1:30;
then
pb,
pc are_convertible_wrt PolyRedRel (
{p},
T)
by POLYRED:58;
then
b,
c are_convergent_wrt Rp
by A8, A11, REWRITE1:def 23;
then consider d being
object such that A12:
(
Rp reduces b,
d &
Rp reduces c,
d )
by REWRITE1:def 7;
for
u being
object st
u in {p} holds
u in P
by A1, TARSKI:def 1;
then
{p} c= P
;
then
(
PolyRedRel (
P,
T)
reduces b,
d &
PolyRedRel (
P,
T)
reduces c,
d )
by A12, Th4, REWRITE1:22;
hence
b,
c are_convergent_wrt PolyRedRel (
P,
T)
by REWRITE1:def 7;
verum end;
hence
PolyRedRel (P,T) is locally-confluent
by REWRITE1:def 24; verum