let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis:
let G, P be non empty Subset of (Polynom-Ring (n,L)); :: thesis:
set R = PolyRedRel (P,T);
assume A1: G is_Groebner_basis_of P,T ; :: thesis:
then PolyRedRel (G,T) is locally-confluent by Def4;
then reconsider RG = PolyRedRel (G,T) as complete Relation ;
for a, b being set holds
( a,b are_convertible_wrt PolyRedRel (P,T) iff a,b are_convergent_wrt RG )

proof

let a, b be set ; :: thesis:
A2: G -Ideal = P by A1, Def4;

A3: now

assume A4: a,b are_convertible_wrt PolyRedRel (P,T) ; :: thesis:

now

per cases ;

case a = b ; :: thesis:

hence a,b are_convergent_wrt RG by REWRITE1:38; :: thesis:

end;

case A5: a <> b ; :: thesis:

(PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) reduces a,b by A4, REWRITE1:def 4;
then consider p being RedSequence of (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) such that
A6: p . 1 = a and
A7: p . (len p) = b by REWRITE1:def 3;
reconsider l = (len p) - 1 as Element of NAT by INT_1:5, NAT_1:14;
A8: 1 <= len p by NAT_1:14;
set h = p . l;
set g = p . (1 + 1);
1 <= l + 1 by NAT_1:12;
then l + 1 in Seg (len p) by FINSEQ_1:1;
then A9: l + 1 in dom p by FINSEQ_1:def 3;

now

per cases ;

case len p = 1 ; :: thesis:

hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A5, A6, A7; :: thesis:

end;

case A10: len p <> 1 ; :: thesis:

then 0 + 1 < l + 1 by A8, XXREAL_0:1;
then A11: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg (len p) by A11, FINSEQ_1:1;
then l in dom p by FINSEQ_1:def 3;
then A12: [(p . l),b] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by A7, A9, REWRITE1:def 2;

A13: now

per cases in PolyRedRel (P,T) or [(p . l),b] in (PolyRedRel (P,T)) ~ ) by A12, XBOOLE_0:def 3;

case [(p . l),b] in PolyRedRel (P,T) ; :: thesis:

then consider h9, b9 being set such that
A14: [(p . l),b] = [h9,b9] and
h9 in NonZero (Polynom-Ring (n,L)) and
A15: b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
b = [h9,b9] `2 by A14, MCART_1:def 2
.= b9 by MCART_1:def 2 ;
hence b is Polynomial of n,L by A15, POLYNOM1:def 10; :: thesis:

end;

case [(p . l),b] in (PolyRedRel (P,T)) ~ ; :: thesis:

then [b,(p . l)] in PolyRedRel (P,T) by RELAT_1:def 7;
then consider h9, b9 being set such that
A16: [b,(p . l)] = [h9,b9] and
A17: h9 in NonZero (Polynom-Ring (n,L)) and
b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
b = [h9,b9] `1 by A16, MCART_1:def 1
.= h9 by MCART_1:def 1 ;
hence b is Polynomial of n,L by A17, POLYNOM1:def 10; :: thesis:

end;

end;

end;

1 < len p by A8, A10, XXREAL_0:1;
then 1 + 1 <= len p by NAT_1:13;
then 1 + 1 in Seg (len p) by FINSEQ_1:1;
then A18: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg (len p) by A8, FINSEQ_1:1;
then 1 in dom p by FINSEQ_1:def 3;
then A19: [a,(p . (1 + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by A6, A18, REWRITE1:def 2;

now

per cases in PolyRedRel (P,T) or [a,(p . (1 + 1))] in (PolyRedRel (P,T)) ~ ) by A19, XBOOLE_0:def 3;

case [a,(p . (1 + 1))] in PolyRedRel (P,T) ; :: thesis:

then consider h9, b9 being set such that
A20: [a,(p . (1 + 1))] = [h9,b9] and
A21: h9 in NonZero (Polynom-Ring (n,L)) and
b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
a = [h9,b9] `1 by A20, MCART_1:def 1
.= h9 by MCART_1:def 1 ;
hence a is Polynomial of n,L by A21, POLYNOM1:def 10; :: thesis:

end;

case [a,(p . (1 + 1))] in (PolyRedRel (P,T)) ~ ; :: thesis:

then [(p . (1 + 1)),a] in PolyRedRel (P,T) by RELAT_1:def 7;
then consider h9, b9 being set such that
A22: [(p . (1 + 1)),a] = [h9,b9] and
h9 in NonZero (Polynom-Ring (n,L)) and
A23: b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
a = [h9,b9] `2 by A22, MCART_1:def 2
.= b9 by MCART_1:def 2 ;
hence a is Polynomial of n,L by A23, POLYNOM1:def 10; :: thesis:

end;

end;

end;

hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A13; :: thesis:

end;

end;

end;

then reconsider a9 = a, b9 = b as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 10;
reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;
G -Ideal = P -Ideal by A2, IDEAL_1:44;
then a9,b9 are_congruent_mod G -Ideal by A4, POLYRED:57;
then a9,b9 are_convertible_wrt RG by POLYRED:58;
hence a,b are_convergent_wrt RG by REWRITE1:def 23; :: thesis:

end;

end;

end;

hence a,b are_convergent_wrt RG ; :: thesis:

end;

now

assume A24: a,b are_convergent_wrt RG ; :: thesis:

now

per cases ;

case a = b ; :: thesis:

hence a,b are_convertible_wrt PolyRedRel (P,T) by REWRITE1:26; :: thesis:

end;

case A25: a <> b ; :: thesis:

consider c being set such that
A26: RG reduces a,c and
A27: RG reduces b,c by A24, REWRITE1:def 7;
( a is Polynomial of n,L & b is Polynomial of n,L )

proof

now

per cases ;

case a = c ; :: thesis:

hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A25, A27, Lm6; :: thesis:

end;

case A28: a <> c ; :: thesis:

now

per cases ;

case b = c ; :: thesis:

hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A25, A26, Lm6; :: thesis:

end;

case b <> c ; :: thesis:

hence b is Polynomial of n,L by A27, Lm6; :: thesis:

end;

end;

end;

hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A26, A28, Lm6; :: thesis:

end;

end;

end;

hence ( a is Polynomial of n,L & b is Polynomial of n,L ) ; :: thesis:

end;

then reconsider a9 = a, b9 = b as Element of the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 10;
reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;
( G -Ideal = P -Ideal & a9,b9 are_convertible_wrt RG ) by A2, A24, IDEAL_1:44, REWRITE1:37;
then a9,b9 are_congruent_mod P -Ideal by POLYRED:57;
hence a,b are_convertible_wrt PolyRedRel (P,T) by POLYRED:58; :: thesis:

end;

end;

end;

hence a,b are_convertible_wrt PolyRedRel (P,T) ; :: thesis:

end;

hence ( a,b are_convertible_wrt PolyRedRel (P,T) iff a,b are_convergent_wrt RG ) by A3; :: thesis:

end;

hence PolyRedRel (G,T) is Completion of PolyRedRel (P,T) by REWRITE1:def 28; :: thesis: