let n be Element of NAT ; :: thesis: 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; :: thesis: 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 ; :: thesis: for p being Polynomial of n,L holds PolyRedRel ({p},T) is locally-confluent
let p be Polynomial of n,L; :: thesis: 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) ; :: thesis: PolyRedRel ({p},T) is locally-confluent

now :: thesis: 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 ; :: 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
[a,c] in PolyRedRel ({p},T) ; :: thesis: 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; :: thesis: verum

end;

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

end;

suppose p <> 0_ (n,L) ; :: thesis: PolyRedRel ({p},T) is locally-confluent

then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;

now :: thesis: 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 ; :: thesis: ( [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) ; :: thesis: 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 :: thesis: ( ( 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) ; :: thesis: 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 :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: verum

end;

case mb <> mc ; :: thesis: 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; :: thesis: verum

end;

end;

end;

hence ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ; :: thesis: verum

end;

case A27: pc = 0_ (n,L) ; :: thesis: 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 :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: verum

end;

case mb <> mc ; :: thesis: 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; :: thesis: verum

end;

end;

end;

hence ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ; :: thesis: verum

end;

case ( not pb = 0_ (n,L) & not pc = 0_ (n,L) ) ; :: thesis: 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 :: thesis: ( ( 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 pb = pc ; :: thesis: ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d )

hence ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) by A14, A20, REWRITE1:12; :: thesis: verum

end;

case A32: pb <> pc ; :: thesis: ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d )

now :: thesis: not pb - pc = 0_ (n,L)

assume pb - pc = 0_ (n,L) ; :: thesis: contradiction
then (pb + (- pc)) + pc = (0_ (n,L)) + pc by POLYNOM1:def 7;
then pb + ((- pc) + pc) = (0_ (n,L)) + pc by POLYNOM1:21;
then pb + (0_ (n,L)) = (0_ (n,L)) + pc by POLYRED:3;
then pb + (0_ (n,L)) = pc by POLYRED:2;
hence contradiction by A32, POLYNOM1:23; :: thesis: verum

end;

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;

now :: thesis: not (- mb) + mc = 0_ (n,L)

assume (- mb) + mc = 0_ (n,L) ; :: thesis: contradiction
then mc + ((- mb) + mb) = (0_ (n,L)) + mb by POLYNOM1:21;
then mc + (0_ (n,L)) = (0_ (n,L)) + mb by POLYRED:3;
then mc + (0_ (n,L)) = mb by POLYRED:2;
hence contradiction by A32, A33, A34, POLYNOM1:23; :: thesis: verum

end;

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; :: thesis: verum

end;

end;

end;

hence ex d being set st
( PolyRedRel ({p},T) reduces b,d & PolyRedRel ({p},T) reduces c,d ) ; :: thesis: verum

end;

end;

end;

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

end;

end;