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:30;
then A5: b,a are_convertible_wrt PolyRedRel P,T by REWRITE1:32;
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 27;
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 27;
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 27;
reconsider pc9 = pc9, pb9 = pb9 as Element of (Polynom-Ring n,L) ;
a,c are_convertible_wrt PolyRedRel P,T by A4, REWRITE1:30;
then pb9,pc9 are_congruent_mod {p} -Ideal by A2, A8, A11, A5, POLYRED:57, REWRITE1:31;
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:23;
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