let n be Element of NAT ; :: thesis: 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 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; :: thesis: 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 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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)); :: thesis: ( 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 ) ; :: thesis: 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

set Rp = PolyRedRel ({p},T);
reconsider Rp = PolyRedRel ({p},T) as strongly-normalizing locally-confluent Relation by Th10;
let a, b, c be set ; :: thesis: ( [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) ; :: thesis: 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 set 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 10;
A8: pb = [a,b] `2 by A7, MCART_1:def 2
.= b by MCART_1:def 2 ;
consider pa9, pc being set 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 10;
A11: pc = [a,c] `2 by A10, MCART_1:def 2
.= c by MCART_1:def 2 ;
reconsider pb9 = pb, pc9 = pc as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 10;
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 set such that
A12: ( Rp reduces b,d & Rp reduces c,d ) by REWRITE1:def 7;
for u being set st u in {p} holds
u in P by A1, TARSKI:def 1;
then {p} c= P by TARSKI:def 3;
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; :: thesis: verum

end;

hence PolyRedRel (P,T) is locally-confluent by REWRITE1:def 24; :: thesis: verum