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:39; :: 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:18, 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:3;
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:3;
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:6;
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 27; :: 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:6;
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 27; :: 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:3;
then A18: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg (len p) by A8, FINSEQ_1:3;
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:6;
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 27; :: 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:6;
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 27; :: 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 27;
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:27; :: 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 27;
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:38;
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: