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 ((P -Ideal),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 ((P -Ideal),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 ((P -Ideal),T) c= multiples (HT (P,T)) holds

PolyRedRel (P,T) is locally-confluent

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( HT ((P -Ideal),T) c= multiples (HT (P,T)) implies PolyRedRel (P,T) is locally-confluent )

set R = PolyRedRel (P,T);

assume A1: HT ((P -Ideal),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

PolyRedRel (P,T) reduces f, 0_ (n,L)

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 ((P -Ideal),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 ((P -Ideal),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 ((P -Ideal),T) c= multiples (HT (P,T)) holds

PolyRedRel (P,T) is locally-confluent

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( HT ((P -Ideal),T) c= multiples (HT (P,T)) implies PolyRedRel (P,T) is locally-confluent )

set R = PolyRedRel (P,T);

assume A1: HT ((P -Ideal),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

A11:
for f being Polynomial of n,L st f in P -Ideal holds
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 A6, TERMORD:1;

set g = f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p));

Support f <> {} by A4, POLYNOM7:1;

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 A4, A7, A9, A10, POLYRED:def 5;

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 A8, POLYRED:def 7;

hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

end;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 A6, TERMORD:1;

set g = f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p));

Support f <> {} by A4, POLYNOM7:1;

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 A4, A7, A9, A10, POLYRED:def 5;

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 A8, POLYRED:def 7;

hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

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)

end;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) )
;

end;

suppose
f <> 0_ (n,L)
; :: thesis: PolyRedRel (P,T) reduces f, 0_ (n,L)

then
f is_reducible_wrt P,T
by A2, A12;

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 A13, POLYRED:def 13;

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 A14, REWRITE1:def 6;

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 A15, POLYRED:59;

then A16: (ff - gg) - ff in P -Ideal by A12, IDEAL_1:16;

(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 A16, IDEAL_1:14;

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 A14, REWRITE1:def 6;

then g9 is_reducible_wrt P,T by A2, A17;

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 A18, POLYRED:def 13;

g is_a_normal_form_wrt PolyRedRel (P,T) by A14, REWRITE1:def 6;

hence contradiction by A19, REWRITE1:def 5; :: thesis: verum

end;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 A13, POLYRED:def 13;

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 A14, REWRITE1:def 6;

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 A15, POLYRED:59;

then A16: (ff - gg) - ff in P -Ideal by A12, IDEAL_1:16;

(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 A16, IDEAL_1:14;

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 A14, REWRITE1:def 6;

then g9 is_reducible_wrt P,T by A2, A17;

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 A18, POLYRED:def 13;

g is_a_normal_form_wrt PolyRedRel (P,T) by A14, REWRITE1:def 6;

hence contradiction by A19, REWRITE1:def 5; :: thesis: verum

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)

hence
PolyRedRel (P,T) is locally-confluent
by REWRITE1:def 24; :: thesis: verumb,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 A20, ZFMISC_1:def 2;

A24: b9 = b by A23, XTUPLE_0:1;

a,b are_convertible_wrt PolyRedRel (P,T) by A20, REWRITE1:29;

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 A21, ZFMISC_1:def 2;

A28: c9 = c by A27, XTUPLE_0:1;

reconsider b9 = b9, c9 = c9 as Polynomial of n,L by A22, A26, POLYNOM1:def 11;

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 A21, REWRITE1:29;

then bb,cc are_congruent_mod P -Ideal by A24, A28, A25, POLYRED:57, REWRITE1:30;

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 A11, A24, A28, A29, POLYRED:50; :: thesis: verum

end;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 A20, ZFMISC_1:def 2;

A24: b9 = b by A23, XTUPLE_0:1;

a,b are_convertible_wrt PolyRedRel (P,T) by A20, REWRITE1:29;

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 A21, ZFMISC_1:def 2;

A28: c9 = c by A27, XTUPLE_0:1;

reconsider b9 = b9, c9 = c9 as Polynomial of n,L by A22, A26, POLYNOM1:def 11;

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 A21, REWRITE1:29;

then bb,cc are_congruent_mod P -Ideal by A24, A28, A25, POLYRED:57, REWRITE1:30;

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 A11, A24, A28, A29, POLYRED:50; :: thesis: verum