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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st HT ((),T) c= multiples (HT (P,T)) 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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st HT ((),T) c= multiples (HT (P,T)) holds
PolyRedRel (P,T) is locally-confluent

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st HT ((),T) c= multiples (HT (P,T)) holds
PolyRedRel (P,T) is locally-confluent

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( HT ((),T) c= multiples (HT (P,T)) implies PolyRedRel (P,T) is locally-confluent )
set R = PolyRedRel (P,T);
assume A1: HT ((),T) c= multiples (HT (P,T)) ; :: thesis: PolyRedRel (P,T) is locally-confluent
A2: for f being Polynomial of n,L st f in P -Ideal & f <> 0_ (n,L) holds
f is_reducible_wrt P,T
proof
let f be Polynomial of n,L; :: thesis: ( f in P -Ideal & f <> 0_ (n,L) implies f is_reducible_wrt P,T )
assume that
A3: f in P -Ideal and
A4: f <> 0_ (n,L) ; :: thesis: f is_reducible_wrt P,T
HT (f,T) in { (HT (p,T)) where p is Polynomial of n,L : ( p in P -Ideal & p <> 0_ (n,L) ) } by A3, A4;
then HT (f,T) in multiples (HT (P,T)) by A1;
then ex b being Element of Bags n st
( b = HT (f,T) & ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b ) ) ;
then consider b9 being bag of n such that
A5: b9 in HT (P,T) and
A6: b9 divides HT (f,T) ;
consider p being Polynomial of n,L such that
A7: b9 = HT (p,T) and
A8: p in P and
A9: p <> 0_ (n,L) by A5;
consider s being bag of n such that
A10: b9 + s = HT (f,T) by ;
set g = f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p));
Support f <> {} by ;
then HT (f,T) in Support f by TERMORD:def 6;
then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),p, HT (f,T),T by ;
then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),p,T by POLYRED:def 6;
then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),P,T by ;
hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum
end;
A11: for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
proof
let f be Polynomial of n,L; :: thesis: ( f in P -Ideal implies PolyRedRel (P,T) reduces f, 0_ (n,L) )
assume A12: f in P -Ideal ; :: thesis: PolyRedRel (P,T) reduces f, 0_ (n,L)
per cases ( f = 0_ (n,L) or f <> 0_ (n,L) ) ;
suppose f = 0_ (n,L) ; :: thesis: PolyRedRel (P,T) reduces f, 0_ (n,L)
hence PolyRedRel (P,T) reduces f, 0_ (n,L) by REWRITE1:12; :: thesis: verum
end;
suppose f <> 0_ (n,L) ; :: thesis: PolyRedRel (P,T) reduces f, 0_ (n,L)
then f is_reducible_wrt P,T by ;
then consider v being Polynomial of n,L such that
A13: f reduces_to v,P,T by POLYRED:def 9;
[f,v] in PolyRedRel (P,T) by ;
then f in field (PolyRedRel (P,T)) by RELAT_1:15;
then f has_a_normal_form_wrt PolyRedRel (P,T) by REWRITE1:def 14;
then consider g being object such that
A14: g is_a_normal_form_of f, PolyRedRel (P,T) by REWRITE1:def 11;
A15: PolyRedRel (P,T) reduces f,g by ;
then reconsider g9 = g as Polynomial of n,L by Lm4;
reconsider ff = f, gg = g9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider ff = ff, gg = gg as Element of (Polynom-Ring (n,L)) ;
f - g9 = ff - gg by Lm2;
then ff - gg in P -Ideal by ;
then A16: (ff - gg) - ff in P -Ideal by ;
(ff - gg) - ff = (ff + (- gg)) - ff
.= (ff + (- gg)) + (- ff)
.= (ff + (- ff)) + (- gg) by RLVECT_1:def 3
.= (0. (Polynom-Ring (n,L))) + (- gg) by RLVECT_1:5
.= - gg by ALGSTR_1:def 2 ;
then - (- gg) in P -Ideal by ;
then A17: g in P -Ideal by RLVECT_1:17;
assume not PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: contradiction
then g <> 0_ (n,L) by ;
then g9 is_reducible_wrt P,T by ;
then consider u being Polynomial of n,L such that
A18: g9 reduces_to u,P,T by POLYRED:def 9;
A19: [g9,u] in PolyRedRel (P,T) by ;
g is_a_normal_form_wrt PolyRedRel (P,T) by ;
hence contradiction by A19, REWRITE1:def 5; :: thesis: verum
end;
end;
end;
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
A20: [a,b] in PolyRedRel (P,T) and
A21: [a,c] in PolyRedRel (P,T) ; :: thesis: b,c are_convergent_wrt PolyRedRel (P,T)
consider a9, b9 being object such that
a9 in NonZero (Polynom-Ring (n,L)) and
A22: b9 in the carrier of (Polynom-Ring (n,L)) and
A23: [a,b] = [a9,b9] by ;
A24: b9 = b by ;
a,b are_convertible_wrt PolyRedRel (P,T) by ;
then A25: b,a are_convertible_wrt PolyRedRel (P,T) by REWRITE1:31;
consider aa, c9 being object such that
aa in NonZero (Polynom-Ring (n,L)) and
A26: c9 in the carrier of (Polynom-Ring (n,L)) and
A27: [a,c] = [aa,c9] by ;
A28: c9 = c by ;
reconsider b9 = b9, c9 = c9 as Polynomial of n,L by ;
reconsider bb = b9, cc = c9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider bb = bb, cc = cc as Element of (Polynom-Ring (n,L)) ;
a,c are_convertible_wrt PolyRedRel (P,T) by ;
then bb,cc are_congruent_mod P -Ideal by ;
then A29: bb - cc in P -Ideal by POLYRED:def 14;
b9 - c9 = bb - cc by Lm2;
hence b,c are_convergent_wrt PolyRedRel (P,T) by ; :: thesis: verum
end;
hence PolyRedRel (P,T) is locally-confluent by REWRITE1:def 24; :: thesis: verum