let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 11;
per cases
( p = 0_ (n,L) or p <> 0_ (n,L) )
;
suppose A2:
p = 0_ (
n,
L)
;
PolyRedRel ({p},T) is locally-confluent 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)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
[a,c] in PolyRedRel (
{p},
T)
;
b,c are_convergent_wrt PolyRedRel ({p},T)consider p9,
q being
object 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 11;
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 11, POLYNOM7:def 1;
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 1;
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)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 A9:
[a,b] in PolyRedRel (
{p},
T)
and A10:
[a,c] in PolyRedRel (
{p},
T)
;
b,c are_convergent_wrt PolyRedRel ({p},T)consider pa,
pb being
object 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 11, POLYNOM7:def 1;
reconsider pb =
pb as
Polynomial of
n,
L by A12, POLYNOM1:def 11;
A14:
pb = b
by A13, XTUPLE_0:1;
A15:
pa = a
by A13, XTUPLE_0: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
object 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 11;
A19:
p in {p}
by TARSKI:def 1;
A20:
pc = c
by A18, XTUPLE_0:1;
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 ( ( pb = 0_ (n,L) & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) or ( pc = 0_ (n,L) & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) or ( 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 ) ) )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 7;
then
mb *' p = (pa + (- (mb *' p))) + (mb *' p)
by POLYRED:2;
then
mb *' p = pa + ((- (mb *' p)) + (mb *' p))
by POLYNOM1:21;
then
mb *' p = pa + (0_ (n,L))
by POLYRED:3;
then
mb *' p = pa
by POLYNOM1:23;
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 7;
then
pc = (mb *' p) + ((- mc) *' p)
by POLYRED:6;
then A25:
pc = (mb + (- mc)) *' p
by POLYNOM1:26;
then A26:
pc = (mb - mc) *' p
by POLYNOM1:def 7;
now ( ( mb = mc & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) or ( mb <> mc & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) )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:24;
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:12;
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:12;
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 7;
then
mc *' p = (pa + (- (mc *' p))) + (mc *' p)
by POLYRED:2;
then
mc *' p = pa + ((- (mc *' p)) + (mc *' p))
by POLYNOM1:21;
then
mc *' p = pa + (0_ (n,L))
by POLYRED:3;
then
mc *' p = pa
by POLYNOM1:23;
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 7;
then
pb = (mc *' p) + ((- mb) *' p)
by POLYRED:6;
then A30:
pb = (mc + (- mb)) *' p
by POLYNOM1:26;
then A31:
pb = (mc - mb) *' p
by POLYNOM1:def 7;
now ( ( mb = mc & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) or ( mb <> mc & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) )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:24;
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:12;
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:12;
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 1;
now ( ( pb = pc & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) or ( pb <> pc & ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ) )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 1;
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 1;
A35:
- (- (mc *' p)) = mc *' p
by POLYNOM1:19;
h =
(pa - (mb *' p)) + (- (pa - (mc *' p)))
by A33, A34, POLYNOM1:def 7
.=
(pa - (mb *' p)) + (- (pa + (- (mc *' p))))
by POLYNOM1:def 7
.=
(pa - (mb *' p)) + ((- pa) + (- (- (mc *' p))))
by POLYRED:1
.=
(pa + (- (mb *' p))) + ((- pa) + (- (- (mc *' p))))
by POLYNOM1:def 7
.=
((pa + (- (mb *' p))) + (- pa)) + (mc *' p)
by A35, POLYNOM1:21
.=
((pa + (- pa)) + (- (mb *' p))) + (mc *' p)
by POLYNOM1:21
.=
((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:26
;
then consider f1,
g1 being
Polynomial of
n,
L such that A36:
f1 - g1 = 0_ (
n,
L)
and A37:
(
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 A36, POLYNOM1:def 7;
then
f1 + ((- g1) + g1) = (0_ (n,L)) + g1
by POLYNOM1:21;
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:23;
hence
ex
d being
set st
(
PolyRedRel (
{p},
T)
reduces b,
d &
PolyRedRel (
{p},
T)
reduces c,
d )
by A14, A20, A37;
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;