let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds PolyRedRel {p},T is locally-confluent
let T be connected admissible TermOrder of n; for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds PolyRedRel {p},T is locally-confluent
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; for p being Polynomial of n,L holds PolyRedRel {p},T is locally-confluent
let p be Polynomial of n,L; PolyRedRel {p},T is locally-confluent
set R = PolyRedRel {p},T;
A1:
0_ n,L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
per cases
( p = 0_ n,L or p <> 0_ n,L )
;
suppose A2:
p = 0_ n,
L
;
PolyRedRel {p},T is locally-confluent now let a,
b,
c be
set ;
( [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
[a,c] in PolyRedRel {p},
T
;
b,c are_convergent_wrt PolyRedRel {p},Tconsider p9,
q being
set such that A4:
p9 in NonZero (Polynom-Ring n,L)
and A5:
q in the
carrier of
(Polynom-Ring n,L)
and A6:
[a,b] = [p9,q]
by A3, ZFMISC_1:def 2;
reconsider q =
q as
Polynomial of
n,
L by A5, POLYNOM1:def 27;
not
p9 in {(0_ n,L)}
by A1, A4, XBOOLE_0:def 5;
then
p9 <> 0_ n,
L
by TARSKI:def 1;
then reconsider p9 =
p9 as
non-zero Polynomial of
n,
L by A4, POLYNOM1:def 27, POLYNOM7:def 2;
p9 reduces_to q,
{p},
T
by A3, A6, POLYRED:def 13;
then consider g being
Polynomial of
n,
L such that A7:
g in {p}
and A8:
p9 reduces_to q,
g,
T
by POLYRED:def 7;
g = 0_ n,
L
by A2, A7, TARSKI:def 1;
then
p9 is_reducible_wrt 0_ n,
L,
T
by A8, POLYRED:def 8;
hence
b,
c are_convergent_wrt PolyRedRel {p},
T
by Lm3;
verum end; hence
PolyRedRel {p},
T is
locally-confluent
by REWRITE1:def 24;
verum suppose
p <> 0_ n,
L
;
PolyRedRel {p},T is locally-confluent then reconsider p =
p as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
now let a,
b,
c be
set ;
( [a,b] in PolyRedRel {p},T & [a,c] in PolyRedRel {p},T implies b,c are_convergent_wrt PolyRedRel {p},T )assume that A9:
[a,b] in PolyRedRel {p},
T
and A10:
[a,c] in PolyRedRel {p},
T
;
b,c are_convergent_wrt PolyRedRel {p},Tconsider pa,
pb being
set such that A11:
pa in NonZero (Polynom-Ring n,L)
and A12:
pb in the
carrier of
(Polynom-Ring n,L)
and A13:
[a,b] = [pa,pb]
by A9, ZFMISC_1:def 2;
not
pa in {(0_ n,L)}
by A1, A11, XBOOLE_0:def 5;
then
pa <> 0_ n,
L
by TARSKI:def 1;
then reconsider pa =
pa as
non-zero Polynomial of
n,
L by A11, POLYNOM1:def 27, POLYNOM7:def 2;
reconsider pb =
pb as
Polynomial of
n,
L by A12, POLYNOM1:def 27;
A14:
pb =
[a,b] `2
by A13, MCART_1:def 2
.=
b
by MCART_1:def 2
;
A15:
pa =
[a,b] `1
by A13, MCART_1:def 1
.=
a
by MCART_1:def 1
;
then
pa reduces_to pb,
{p},
T
by A9, A14, POLYRED:def 13;
then
ex
p9 being
Polynomial of
n,
L st
(
p9 in {p} &
pa reduces_to pb,
p9,
T )
by POLYRED:def 7;
then A16:
pa reduces_to pb,
p,
T
by TARSKI:def 1;
consider pa9,
pc being
set such that
pa9 in NonZero (Polynom-Ring n,L)
and A17:
pc in the
carrier of
(Polynom-Ring n,L)
and A18:
[a,c] = [pa9,pc]
by A10, ZFMISC_1:def 2;
reconsider pc =
pc as
Polynomial of
n,
L by A17, POLYNOM1:def 27;
A19:
p in {p}
by TARSKI:def 1;
A20:
pc =
[a,c] `2
by A18, MCART_1:def 2
.=
c
by MCART_1:def 2
;
then
pa reduces_to pc,
{p},
T
by A10, A15, POLYRED:def 13;
then
ex
p9 being
Polynomial of
n,
L st
(
p9 in {p} &
pa reduces_to pc,
p9,
T )
by POLYRED:def 7;
then A21:
pa reduces_to pc,
p,
T
by TARSKI:def 1;
now per cases
( pb = 0_ n,L or pc = 0_ n,L or ( not pb = 0_ n,L & not pc = 0_ n,L ) )
;
case A22:
pb = 0_ n,
L
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )then consider mb being
Monomial of
n,
L such that A23:
0_ n,
L = pa - (mb *' p)
by A16, Th1;
(0_ n,L) + (mb *' p) = (pa + (- (mb *' p))) + (mb *' p)
by A23, POLYNOM1:def 23;
then
mb *' p = (pa + (- (mb *' p))) + (mb *' p)
by POLYRED:2;
then
mb *' p = pa + ((- (mb *' p)) + (mb *' p))
by POLYNOM1:80;
then
mb *' p = pa + (0_ n,L)
by POLYRED:3;
then
mb *' p = pa
by POLYNOM1:82;
then consider mc being
Monomial of
n,
L such that A24:
pc = (mb *' p) - (mc *' p)
by A21, Th1;
pc = (mb *' p) + (- (mc *' p))
by A24, POLYNOM1:def 23;
then
pc = (mb *' p) + ((- mc) *' p)
by POLYRED:6;
then A25:
pc = (mb + (- mc)) *' p
by POLYNOM1:85;
then A26:
pc = (mb - mc) *' p
by POLYNOM1:def 23;
now per cases
( mb = mc or mb <> mc )
;
case
mb = mc
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )then
pc = (0_ n,L) *' p
by A26, POLYNOM1:83;
then
pc = 0_ n,
L
by POLYRED:5;
hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
by A14, A20, A22, REWRITE1:13;
verum end; case
mb <> mc
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )
PolyRedRel {p},
T reduces pb,
0_ n,
L
by A22, REWRITE1:13;
hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
by A14, A20, A19, A25, POLYRED:45;
verum end; hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
;
verum end; case A27:
pc = 0_ n,
L
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )then consider mc being
Monomial of
n,
L such that A28:
0_ n,
L = pa - (mc *' p)
by A21, Th1;
(0_ n,L) + (mc *' p) = (pa + (- (mc *' p))) + (mc *' p)
by A28, POLYNOM1:def 23;
then
mc *' p = (pa + (- (mc *' p))) + (mc *' p)
by POLYRED:2;
then
mc *' p = pa + ((- (mc *' p)) + (mc *' p))
by POLYNOM1:80;
then
mc *' p = pa + (0_ n,L)
by POLYRED:3;
then
mc *' p = pa
by POLYNOM1:82;
then consider mb being
Monomial of
n,
L such that A29:
pb = (mc *' p) - (mb *' p)
by A16, Th1;
pb = (mc *' p) + (- (mb *' p))
by A29, POLYNOM1:def 23;
then
pb = (mc *' p) + ((- mb) *' p)
by POLYRED:6;
then A30:
pb = (mc + (- mb)) *' p
by POLYNOM1:85;
then A31:
pb = (mc - mb) *' p
by POLYNOM1:def 23;
now per cases
( mb = mc or mb <> mc )
;
case
mb = mc
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )then
pb = (0_ n,L) *' p
by A31, POLYNOM1:83;
then
pb = 0_ n,
L
by POLYRED:5;
hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
by A14, A20, A27, REWRITE1:13;
verum end; case
mb <> mc
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )
PolyRedRel {p},
T reduces pc,
0_ n,
L
by A27, REWRITE1:13;
hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
by A14, A20, A19, A30, POLYRED:45;
verum end; hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
;
verum end; case
( not
pb = 0_ n,
L & not
pc = 0_ n,
L )
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )then reconsider pb =
pb,
pc =
pc as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
now per cases
( pb = pc or pb <> pc )
;
case A32:
pb <> pc
;
ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )then reconsider h =
pb - pc as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
consider mb being
Monomial of
n,
L such that A33:
pb = pa - (mb *' p)
by A16, Th1;
consider mc being
Monomial of
n,
L such that A34:
pc = pa - (mc *' p)
by A21, Th1;
then reconsider hh =
(- mb) + mc as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
h =
(pa - (mb *' p)) + (- (pa - (mc *' p)))
by A33, A34, POLYNOM1:def 23
.=
(pa - (mb *' p)) + (- (pa + (- (mc *' p))))
by POLYNOM1:def 23
.=
(pa - (mb *' p)) + ((- pa) + (- (- (mc *' p))))
by POLYRED:1
.=
(pa + (- (mb *' p))) + ((- pa) + (- (- (mc *' p))))
by POLYNOM1:def 23
.=
((pa + (- (mb *' p))) + (- pa)) + (mc *' p)
by POLYNOM1:80
.=
((pa + (- pa)) + (- (mb *' p))) + (mc *' p)
by POLYNOM1:80
.=
((0_ n,L) + (- (mb *' p))) + (mc *' p)
by POLYRED:3
.=
(- (mb *' p)) + (mc *' p)
by POLYRED:2
.=
((- mb) *' p) + (mc *' p)
by POLYRED:6
.=
hh *' p
by POLYNOM1:85
;
then consider f1,
g1 being
Polynomial of
n,
L such that A35:
f1 - g1 = 0_ n,
L
and A36:
(
PolyRedRel {p},
T reduces pb,
f1 &
PolyRedRel {p},
T reduces pc,
g1 )
by A19, POLYRED:45, POLYRED:49;
(f1 + (- g1)) + g1 = (0_ n,L) + g1
by A35, POLYNOM1:def 23;
then
f1 + ((- g1) + g1) = (0_ n,L) + g1
by POLYNOM1:80;
then
f1 + (0_ n,L) = (0_ n,L) + g1
by POLYRED:3;
then
f1 + (0_ n,L) = g1
by POLYRED:2;
then
f1 = g1
by POLYNOM1:82;
hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
by A14, A20, A36;
verum end; hence
ex
d being
set st
(
PolyRedRel {p},
T reduces b,
d &
PolyRedRel {p},
T reduces c,
d )
;
verum end; 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 end;