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 )
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 & P -Ideal = {p} -Ideal )
;
set R = PolyRedRel P,T;
now 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 A2:
(
[a,b] in PolyRedRel P,
T &
[a,c] in PolyRedRel P,
T )
;
:: thesis: b,c are_convergent_wrt PolyRedRel P,Tthen consider pa,
pb being
set such that A3:
(
pa in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
pb in the
carrier of
(Polynom-Ring n,L) &
[a,b] = [pa,pb] )
by ZFMISC_1:def 2;
reconsider pb =
pb as
Polynomial of
n,
L by A3, POLYNOM1:def 27;
A4:
pb =
[a,b] `2
by A3, MCART_1:def 2
.=
b
by MCART_1:def 2
;
consider pa',
pc being
set such that A5:
(
pa' in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
pc in the
carrier of
(Polynom-Ring n,L) &
[a,c] = [pa',pc] )
by A2, ZFMISC_1:def 2;
reconsider pc =
pc as
Polynomial of
n,
L by A5, POLYNOM1:def 27;
A6:
pc =
[a,c] `2
by A5, MCART_1:def 2
.=
c
by MCART_1:def 2
;
A7:
(
a,
b are_convertible_wrt PolyRedRel P,
T &
a,
c are_convertible_wrt PolyRedRel P,
T )
by A2, REWRITE1:30;
then A8:
b,
a are_convertible_wrt PolyRedRel P,
T
by REWRITE1:32;
reconsider pb' =
pb,
pc' =
pc as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider pc' =
pc',
pb' =
pb' as
Element of
(Polynom-Ring n,L) ;
pb',
pc' are_congruent_mod {p} -Ideal
by A1, A4, A6, A7, A8, POLYRED:57, REWRITE1:31;
then A9:
pb,
pc are_convertible_wrt PolyRedRel {p},
T
by POLYRED:58;
set Rp =
PolyRedRel {p},
T;
reconsider Rp =
PolyRedRel {p},
T as
strongly-normalizing locally-confluent Relation by Th10;
b,
c are_convergent_wrt Rp
by A4, A6, A9, REWRITE1:def 23;
then consider d being
set such that A10:
(
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 A10, 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