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 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; :: thesis: 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 ; :: 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;
X: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;
per cases ( p = 0_ n,L or p <> 0_ n,L ) ;
suppose A1: p = 0_ n,L ; :: thesis: PolyRedRel {p},T is locally-confluent
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},T
then consider p', q being set such that
A3: ( p' in NonZero (Polynom-Ring n,L) & q in the carrier of (Polynom-Ring n,L) & [a,b] = [p',q] ) by ZFMISC_1:def 2;
reconsider q = q as Polynomial of n,L by A3, POLYNOM1:def 27;
not p' in {(0_ n,L)} by A3, X, XBOOLE_0:def 5;
then p' <> 0_ n,L by TARSKI:def 1;
then reconsider p' = p' as non-zero Polynomial of n,L by A3, POLYNOM1:def 27, POLYNOM7:def 2;
p' reduces_to q,{p},T by A2, A3, POLYRED:def 13;
then consider g being Polynomial of n,L such that
A4: ( g in {p} & p' reduces_to q,g,T ) by POLYRED:def 7;
g = 0_ n,L by A1, A4, TARSKI:def 1;
then p' is_reducible_wrt 0_ n,L,T by A4, 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 2;
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 A5: ( [a,b] in PolyRedRel {p},T & [a,c] in PolyRedRel {p},T ) ; :: thesis: b,c are_convergent_wrt PolyRedRel {p},T
then consider pa, pb being set such that
A6: ( pa in NonZero (Polynom-Ring 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 A6, POLYNOM1:def 27;
not pa in {(0_ n,L)} by A6, X, 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 A6, POLYNOM1:def 27, POLYNOM7:def 2;
A7: pa = [a,b] `1 by A6, MCART_1:def 1
.= a by MCART_1:def 1 ;
A8: pb = [a,b] `2 by A6, MCART_1:def 2
.= b by MCART_1:def 2 ;
then pa reduces_to pb,{p},T by A5, A7, POLYRED:def 13;
then consider p' being Polynomial of n,L such that
A9: ( p' in {p} & pa reduces_to pb,p',T ) by POLYRED:def 7;
A10: pa reduces_to pb,p,T by A9, TARSKI:def 1;
consider pa', pc being set such that
A11: ( pa' in NonZero (Polynom-Ring n,L) & pc in the carrier of (Polynom-Ring n,L) & [a,c] = [pa',pc] ) by A5, ZFMISC_1:def 2;
reconsider pc = pc as Polynomial of n,L by A11, POLYNOM1:def 27;
A12: pc = [a,c] `2 by A11, MCART_1:def 2
.= c by MCART_1:def 2 ;
then pa reduces_to pc,{p},T by A5, A7, POLYRED:def 13;
then consider p' being Polynomial of n,L such that
A13: ( p' in {p} & pa reduces_to pc,p',T ) by POLYRED:def 7;
A14: pa reduces_to pc,p,T by A13, TARSKI:def 1;
A15: p in {p} 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 A16: 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
A17: 0_ n,L = pa - (mb *' p) by A10, Th1;
(0_ n,L) + (mb *' p) = (pa + (- (mb *' p))) + (mb *' p) by A17, 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
A18: pc = (mb *' p) - (mc *' p) by A14, Th1;
pc = (mb *' p) + (- (mc *' p)) by A18, POLYNOM1:def 23;
then pc = (mb *' p) + ((- mc) *' p) by POLYRED:6;
then pc = (mb + (- mc)) *' p by POLYNOM1:85;
then A19: pc = (mb - mc) *' p by POLYNOM1:def 23;
now
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 )
PolyRedRel {p},T reduces pb, 0_ n,L by A16, REWRITE1:13;
hence ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d ) by A8, A12, A15, A19, 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 A21: 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
A22: 0_ n,L = pa - (mc *' p) by A14, Th1;
(0_ n,L) + (mc *' p) = (pa + (- (mc *' p))) + (mc *' p) by A22, 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
A23: pb = (mc *' p) - (mb *' p) by A10, Th1;
pb = (mc *' p) + (- (mb *' p)) by A23, POLYNOM1:def 23;
then pb = (mc *' p) + ((- mb) *' p) by POLYRED:6;
then pb = (mc + (- mb)) *' p by POLYNOM1:85;
then A24: pb = (mc - mb) *' p by POLYNOM1:def 23;
now
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 )
PolyRedRel {p},T reduces pc, 0_ n,L by A21, REWRITE1:13;
hence ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d ) by A8, A12, A15, A24, 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 2;
now
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 A8, A12, REWRITE1:13; :: thesis: verum
end;
case A26: pb <> pc ; :: thesis: ex d being set st
( PolyRedRel {p},T reduces b,d & PolyRedRel {p},T reduces c,d )
now
assume pb - pc = 0_ n,L ; :: thesis: contradiction
then (pb + (- pc)) + pc = (0_ n,L) + pc by POLYNOM1:def 23;
then pb + ((- pc) + pc) = (0_ n,L) + pc by POLYNOM1:80;
then pb + (0_ n,L) = (0_ n,L) + pc by POLYRED:3;
then pb + (0_ n,L) = pc by POLYRED:2;
hence contradiction by A26, POLYNOM1:82; :: thesis: verum
end;
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
A27: pb = pa - (mb *' p) by A10, Th1;
consider mc being Monomial of n,L such that
A28: pc = pa - (mc *' p) by A14, Th1;
now
assume (- mb) + mc = 0_ n,L ; :: thesis: contradiction
then mc + ((- mb) + mb) = (0_ n,L) + mb by POLYNOM1:80;
then mc + (0_ n,L) = (0_ n,L) + mb by POLYRED:3;
then mc + (0_ n,L) = mb by POLYRED:2;
hence contradiction by A26, A27, A28, POLYNOM1:82; :: thesis: verum
end;
then reconsider hh = (- mb) + mc as non-zero Polynomial of n,L by POLYNOM7:def 2;
h = (pa - (mb *' p)) + (- (pa - (mc *' p))) by A27, A28, 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 PolyRedRel {p},T reduces h, 0_ n,L by A15, POLYRED:45;
then consider f1, g1 being Polynomial of n,L such that
A29: ( f1 - g1 = 0_ n,L & PolyRedRel {p},T reduces pb,f1 & PolyRedRel {p},T reduces pc,g1 ) by POLYRED:49;
(f1 + (- g1)) + g1 = (0_ n,L) + g1 by A29, 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 A8, A12, A29; :: 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;